企业官网建设流程全解析

相关阅读

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_with_scan.v Against fifo_mod.vg

在实验二中，将实验一中已成功验证的网表fifo_mod.vg作为参考设计，包括了扫描逻辑的fifo_with_scan.v作为实现设计，使用GUI界面验证这两者之间的等价性（虽然这不是典型的做法，但采用这种方式可以直观展示操作步骤）。

在任何时候都可以通过执行以下命令退出并保存当前的Formality会话：

要重新启动该会话：

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

22、点击5. Verify，点击Verify，验证成功，如图22所示。这说明扫描插入未改变实现设计的功能特性（如果在步骤19中没有禁用测试信号test_se，验证将会失败）。

图22 验证成功

实验三

Formality：官方Tutorial（三）https://blog.csdn.net/weixin_45791458/article/details/144948032?sharetype=blogdetail&sharerId=144948032&sharerefer=PC&sharesource=weixin_45791458&spm=1011.2480.3001.8118

原文链接

Formality各版本User Guidehttps://download.csdn.net/download/weixin_45791458/90184000?spm=1001.2014.3001.5503