相关阅读
Formalityhttps://blog.csdn.net/weixin_45791458/category_12841971.html?spm=1001.2014.3001.5482
本文是对Synopsys Formality User Guide Tutorial中第三个实验的翻译（有删改），Lab文件可以从以下链接获取。
Formality官方Tutorialhttps://download.csdn.net/download/weixin_45791458/90220600?spm=1001.2014.3001.5501
实验三、Verifying fifo_jtag.v Against fifo_with_scan.v
在实验三中，将包括了扫描逻辑的网表fifo_with_scan.v作为参考设计，包括了扫描逻辑和JTAG逻辑的fifo_jtag.v作为实现设计，验证这两者之间的等价性。
在任何时候都可以通过执行以下命令退出并保存当前的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_WITH_SCAN目录并选择fifo_with_scan.v文件，如图3所示。
图3 添加设计文件
4、点击Open，然后点击加载文件按钮，如图4所示。
图4 加载设计文件
5、点击Read DB Libraries，并选择Read as a shared library（默认），如图5所示。 因为这是一个门级到门级的验证，所以fifo_with_scan.v和fifo_jtag.v设计的逻辑库必须同时指定。
图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_JTAG目录并选择fifo_jtag.v设计文件，如图12所示。
图12 添加设计文件
13、点击Open，然后点击加载文件按钮，如图13所示。
图13 加载设计文件
14、点击Set Top Design，选择WORK库中的fifo设计，点击Set Top将其设置为顶层设计，如图14所示（跳过Read DB Libraries，因为之前已经将lsi_10k.db指定为共享逻辑库）。
注意：你可能需要向下滚动才能找到fifo设计，因为插入的JTAG设计会显示在选择设计窗格的顶部。如果你不小心将错误的设计设置为顶层设计，首先删除容器，然后重新开始添加设计文件。
图14 设置顶层设计
15、点击3. Setup，本次验证中，参考设计在验证前必须禁用其插入的扫描功能，实现设计在验证前必须禁用其插入的扫描和JTAG功能（如果使用了SVF文件并设置了Automated Setup Mode模式，则不需要人为设置）。
图15 准备进行设置
16、点击Constants，然后点击Set...，会弹出Set Constant对话框，如图16所示。
图16 准备进行常量设置
17、点击Reference，选择fifo，在显示区域顶部附近的下拉框中会出现列表，如图17所示。
图17 选择参考设计
18、在Show Objects>Ports下选择Inputs，滚动或搜索名为test_se的端口并选择它，也可以使用搜索文本框来定位要更改的信号，如图18所示。
图18 选择输入端口test_se
19、在对话框底部的Constant Value区域，选择0（取消扫描使能）并点击OK，如图19所示。
图19 设置常量0
20、点击Implementation，选择fifo，在显示区域顶部附近的下拉框中会出现列表，如图20所示。
图20 选择实现设计
21、重复步骤18和19，将实现设计中的test_se、jtag_trst和jtag_tms测试信号设置为常量0并点击Apply，如图21所示。
图21 设置常量0
22、关闭Set Constant对话框，Constants报告列出了四个已禁用的信号，其中一个属于参考设计，三个属于实现设计，如图22所示。
图22 常量报告
23、点击4. Match，点击Run Matching，匹配结果显示有十六个不匹配的点。
图23 进行匹配
24、点击OK以关闭信息对话框，然后点击Unmatched Points，将看到关于不匹配点的报告，如图24所示。这些是实现设计中的额外匹配点，与之前禁用的插入扫描逻辑和JTAG逻辑，在这种情况下额外的匹配点在实现设计中是预期的，因此可以忽略它们并继续进行验证过程。具体来说，JTAG插入会导致一个大型逻辑块（称为TAP控制器）的添加（需要注意的是，一般情况下，参考设计中不能出现未匹配的非常量比较点，否则会验证失败）。
图24 不匹配点报告
有关比较点匹配的详细介绍，可见下文。
Formality：匹配(match)是如何进行的？https://chenzhang.blog.csdn.net/article/details/144404964
25、点击5. Verify，点击Verify，验证成功，如图25所示。这说明JTAG插入未改变实现设计的功能特性（如果在步骤16到21中没有禁用测试信号，验证将会失败）。
图25 验证成功
原文链接
Formality各版本User Guidehttps://download.csdn.net/download/weixin_45791458/90184000?spm=1001.2014.3001.5503
