相关阅读
本文是对Synopsys Formality User Guide Tutorial中第二个实验的翻译（有删改），Lab文件可以从以下链接获取。
实验二、Verifying fifo_with_scan.v Against fifo_mod.vg
在实验二中，将实验一中已成功验证的网表fifo_mod.vg作为参考设计，包括了扫描逻辑的fifo_with_scan.v作为实现设计，使用GUI界面验证这两者之间的等价性（虽然这不是典型的做法，但采用这种方式可以直观展示操作步骤）。
在任何时候都可以通过执行以下命令退出并保存当前的Formality会话：
| fm_shell | GUI |
| 使用save_session session_file_name命令 | 1、选择File > Save Session |
要重新启动该会话：
| fm_shell | GUI |
| 使用restore_session session_file_name命令 | 1、选择File > Restore Session |
1、首先指定参考设计，在基于流程的工具栏上，点击1. Rel.，默认情况下，1. Read Design Files和Verilog...是激活的，如图1所示。
图1 点击1. Rel.
2、点击Verilog，会弹出Add Verilog Files对话框，如图2所示。
图2 点击Verilog
3、导航到GATE目录并选择fifo_mod.vg文件，如图3所示。
图3 添加设计文件
4、点击Open，然后点击加载文件按钮
，如图4所示。
图4 加载设计文件
5、点击Read DB Libraries，并选择Read as a shared library（默认），如图5所示。 因为这是一个门级到门级的验证，所以fifo_mod.vg和fifo_with_scan.v设计的逻辑库必须同时指定。如果使用的是Verilog或VHDL逻辑库，必须在Formality提示符下指定read_verilog -technology_library或read_vhdl -technology_library命令。
图5 点击Read DB Libraries
6、点击DB，会弹出Add DB Files对话框，如图6所示。
图6 点击DB
7、导航到LIB目录并选择lsi_10k.db逻辑库文件，如图7所示。
图7 添加库文件
8、点击Open，然后点击加载文件按钮，如图8所示。
图8 加载库文件
9、点击Set Top Design，选择WORK库中的fifo设计，点击Set Top将其设置为顶层设计，如图9所示。
图9 设置顶层设计
10、接下来指定实现设计，过程类似于在指定参考设计的步骤。在基于流程的工具栏上，点击2. Impl.，默认情况下，1. Read Design Files和Verilog...是激活的，如图10所示。
图10 点击2. Impl.
11、点击Verilog，会弹出Add Verilog Files对话框，如图11所示。
图11 点击Verilog
12、导航到GATE_WITH_SCAN目录并选择fifo_with_scan.v设计文件，如图12所示。
图12 添加设计文件
13、点击Open，然后点击加载文件按钮，如图13所示。
图13 加载设计文件
14、点击Set Top Design，选择WORK库中的fifo设计，点击Set Top将其设置为顶层设计，如图14所示（跳过Read DB Libraries，因为之前已经将lsi_10k.db指定为共享逻辑库）。
图14 设置顶层设计
15、点击3. Setup，与在fifo.vg和fifo.v之间执行的验证时跳过了设置阶段不同，这次指定的实现设计在验证前必须禁用其插入的扫描功能（如果使用了SVF文件并设置了Automated Setup Mode模式，则不需要人为设置）。
图15 准备进行设置
16、点击Constants，然后点击Set...，会弹出Set Constant对话框，如图16所示。
图16 准备进行常量设置
17、点击Implementation，选择fifo，在显示区域顶部附近的下拉框中会出现列表，如图17所示。
图17 选择实现设计
18、在Show Objects > Ports下选择Inputs，滚动或搜索名为test_se的端口并选择它，也可以使用搜索文本框来定位要更改的信号，如图18所示。
图18 选择输入端口test_se
19、在对话框底部的Constant Value区域，选择0（取消扫描使能）并点击OK，如图19所示。
图19 设置常量0
20、点击4. Match，点击Run Matching，匹配结果显示有三个不匹配的点。
图20 进行匹配
21、点击OK以关闭信息对话框，然后点击Unmatched Points，将看到关于不匹配点的报告，包含test_se、test_si1和test_si2，如图21所示。这些是实现设计中的额外匹配点，与之前禁用的插入扫描逻辑相关，在这种情况下额外的匹配点在实现设计中是预期的，因此可以忽略它们并继续进行验证过程（需要注意的是，这里的三个不匹配点都出现在实现设计中，参考设计中不应该出现不匹配的比较点只能出现不匹配的普通匹配点）。
图21 不匹配点报告
有关比较点匹配的详细介绍，可见下文。
Formality：匹配(match)是如何进行的？https://chenzhang.blog.csdn.net/article/details/144404964
https://chenzhang.blog.csdn.net/article/details/144404964
22、点击5. Verify，点击Verify，验证成功，如图22所示。这说明扫描插入未改变实现设计的功能特性（如果在步骤19中没有禁用测试信号test_se，验证将会失败）。
图22 验证成功
实验三
原文链接
标签：Formality,weixin,fifo,点击,官方,所示,设计,如图,Tutorial From： https://blog.csdn.net/weixin_45791458/article/details/144936604