Formality：官方Tutorial（一）

相关阅读

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

---

         本教程首先解释如何为运行Formality做好准备，然后通过三个使用该工具的实验进行讲解。

在开始之前

        在开始本教程之前，请确保系统上已正确安装Formality。Shell配置文件（如果使用Bash，指的是.bashr文件；如果使用Zsh，指的是~/.zshrc；如果使用Csh，指的是~/.cshrc）应正确设置路径，已包含Formality安装的bin目录。例如，如果安装目录是/opt/Synopsys/Formality2018/fm/O-2018.06-SP1，请在配置文件中添加如下的设置路径语句（假设使用Bash）：

export PATH=$PATH:/opt/Synopsys/Formality2018/fm/O-2018.06-SP1/bin

        不需要为每个平台(64-bit/32-bit)单独设置可执行路径，Formality启动脚本会自动确定使用的平台并调用正确的二进制文件。但是，为了使工具能够执行此操作，必须确保所有需要的平台都已安装在同一个Formality树中。请将Formality安装在其独立的目录树中，与其他Synopsys工具（如Design Compiler）分开。

创建教程目录

        安装Formality后，设计示例所需的文件位于fm_install_path/doc/fm/tutorial目录中。要在用户家目录创建一个包含所有子目录的教程目录，请执行以下操作：

1、切换到主目录

% cd $HOME

2、使用以下命令复制教程数据，其中fm_install_path是Formality的安装目录

% cp -r fm_install_path/doc/fm/tutorial $HOME

3、切换到新的教程目录

% cd tutorial

教程目录的内容

        教程目录包含以下子目录：

• GATE：Verilog门级网表。
• GATE_WITH_JTAG：带有扫描和联合测试行动组(JTAG)插入的Verilog门级网表。
• GATE_WITH_SCAN：带有扫描插入的Verilog门级网表。
• LIB：门级网表所需的逻辑库。
• RTL：RTL源代码。

启动Formality Shell

% fm_shell
...
fm_shell (setup)>

        fm_shell命令启动了Formality的Shell环境和命令行界面，在命令行界面可以通过以下命令启动GUI：

fm_shell (setup)> start_gui

        提示符中的(setup)表示当前使用命令时所在的模式。可用的模式有：guide、setup、preverify、match和verify，有关于模式的更详细讨论，可见下文，当启动Formality时，默认进入setup模式。Formality：等价性检查的流程与模式(Guide、Setup、Preverify、Match与Verify)文章浏览阅读1.3k次，点赞41次，收藏20次。Formality：等价性检查的流程与模式(Guide、Setup、Preverify、Match与Verify)_formality检查https://chenzhang.blog.csdn.net/article/details/144174638

实验一、Verifying fifo.vg Against fifo.v

        在本教程的这一部分，将验证一个综合后的名为fifo.vg的纯Verilog门级网表与名为fifo.v的RTL参考设计之间的等价性。

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

fm_shell> save_session session_file_name

        要重新调用该会话，请执行：

fm_shell> restore_session session_file_name

加载SVF文件

        在指定参考设计和实现设计之前，可以选择性地将自动设置文件(.svf)加载到Formality中。SVF文件帮助Formality处理由设计流程中的其他工具引起的设计变更。Formality使用该文件来协助比较点匹配和验证过程，这些信息有助于对正在验证的设计中的比较点进行对齐。对于每个加载的SVF文件，Formality会在恰当时机处理其内容，以便在基于名称的比较点匹配期间使用。

        有关SVF文件的详细介绍，可见下文。

Formality：set_svf命令文章浏览阅读1.3k次，点赞40次，收藏31次。Formalitysvf文件的全称是Setup Verification for Formality，即Design Compiler提供给Formality的设置验证文件，它的作用是为Formality的指导模式(Guidance)和设置模式(Setup)提供信息，以帮助其更好地理解和处理设计流程中因使用Design Compiler而引起的设计变更的一种机制。svf文件的详细介绍和生成命令在下面的博客中已经讨论，本文主要讨论Formality中的set_svf命令。_formality把svf转成txt命令https://chenzhang.blog.csdn.net/article/details/144404635        有关比较点匹配的详细介绍，可见下文。

Formality：匹配(match)是如何进行的？文章浏览阅读906次，点赞33次，收藏18次。匹配指的是Formality工具尝试将参考设计中的每个匹配点与实现设计中的相应匹配点进行配对，这里的匹配点包括对比点(Compare Points)以及普通的匹配点(Points)。 在介绍匹配点前首先需要了解逻辑锥(Logic Cones)的概念，逻辑锥是指从特定的设计对象出发，并向后延伸至某些设计对象的组合逻辑结构，之所以被称为锥，是因为其就像椎体一样（一般）拥有一个顶点和多个底点，如图1所示。https://chenzhang.blog.csdn.net/article/details/144404964        要加载SVF文件，请执行以下操作：

fm_shell> set_svf svf_file_name.svf

        注意：如果希望将Design Compiler中的附加约束和非约束信息传递给Formality，请在读取SVF文件之前设置自动化设置模式，有关自动化设置模式可见下文。Formality：设置Automated Setup Mode模式文章浏览阅读1.1k次，点赞28次，收藏36次。Formality要使用自动设置模式，在加载/执行svf文件之前，需要将synopsys_auto_setup变量（布尔值）设置为true或者在GUI界面中选择Use Auto Setup，如图1所示。当自动设置模式设置后，一组Formality变量会被设置，一些设置命令会执行，以与Synopsys综合工具例如Design Compiler兼容，从而通过使用svf指导文件提高整体工具的设置性能。_automa ic modehttps://chenzhang.blog.csdn.net/article/details/144113957        注意：本教程不使用SVF文件，因此本节信息仅供参考。

指定参考设计

        指定参考设计包括读取设计文件、可选地读取工艺库，并设置顶层设计。参考设计是与转换后的实现设计进行比较的设计。在本实验中，参考设计是名为fifo.v的RTL源文件。

        需要显式指定DesignWare根目录，因为fifo.v包含一个DesignWare中的RAM实例，可按如下所示设置hdlin_dwroot变量：

fm_shell	GUI
使用set_app_var hdlin_dwroot path_to_DesignCompiler_install命令	1、选择Edit > Formality Tcl Variables，将会显示Formality Tcl Variables对话框。 2、在Reading Designs部分，选择hdlin_dwroot变量。 3、输入或选择路径path_to_DesignCompiler_install并回车确定。

        现在加载所有参考Verilog文件：

fm_shell	GUI
使用read_verilog -r {./RTL/fifo.v ./RTL/gray2bin.v ./RTL/gray_counter.v ./RTL/pop_ctrl.v ./RTL/push_ctrl.v ./RTL/rs_flop.v}命令	1、点击Ref.。 2、点击Verilog，导航到GATE子目录选择文件并点击Open。 3、点击加载文件按钮，跳过Read DB Libraries，因为RTL形式的参考设计不需要映射到任何特定的工艺文件。

        最后定义参考设计的顶层设计，设置顶层设计将启动所有文件的链接和展开过程，并报告是否缺少任何文件，Formality会自动搜索DesignWare库以寻找RAM的实现：

fm_shell	GUI
使用set_top fifo命令	1、点击Set Top Design。 2、选择WORK库和fifo设计，并点击Set Top。

指定实现设计

        指定实现设计的过程与指定参考设计的过程类似，首先加载所有实现Verilog文件：

fm_shell	GUI
使用read_verilog -i ./GATE/fifo.vg命令	1、点击Impl.。 2、点击Verilog，导航到GATE子目录选择文件并点击Open。 3、点击加载文件按钮。

        但于参考设计不同的是，此时需要加载工艺库：

fm_shell	GUI
使用read_verilog -i LIB/lsi_10k.db命令	1、点击Read DB Libraries。 2、点击DB，导航到LIB子目录选择lsi_10k.db文件并点击Open。 3、 点击加载文件按钮 。

        最后定义实现设计的顶层设计：

fm_shell	GUI
使用set_top fifo命令	1、点击Set Top Design。 2、选择WORK库和fifo设计，并点击Set Top。

执行设置

        通常需要指定额外的设置信息，以考虑设计网表中未包含的信息或为了实现最佳性能。这一步骤涉及向Formality提供信息。例如，如果设计经过了如扫描或JTAG插入等转换，可能需要设置常量。在这种情况下，只有fifo.vg被综合，因此可以继续进行到下一个步骤：Match。

进行匹配

        匹配是Formality将参考设计和实现设计分割成逻辑单元的过程，这些逻辑单元称为逻辑锥(logic cones)。每个逻辑锥都有一个比较点作为顶点，且实现设计中的每个比较点必须与参考设计中的每个比较点匹配，否则验证将失败。匹配阶段需要确保没有不匹配的逻辑锥，并验证实现设计的功能性。

        要进行匹配，请执行以下操作：

fm_shell	GUI
使用match命令	1、点击Match。 2、点击Run Matching。

        匹配结果显示619个点全部匹配成功。

验证设计

        要验证设计，请执行以下操作：

fm_shell	GUI
使用verify命令	1、点击Verify。 2、点击Verify。

        在此案例中，验证将失败并显示有17个比较点验证失败，因为fifo.vg中故意包含了一个设计错误，以展示Formality的调试功能。

调试

        对于大多数用户来说，调试失败的验证是一个挑战，也就是说必须找到设计中功能差异的确切位置，然后进行修复。使用GUI进行调试更加直观，如果你之前使用的是fm_shell，以下命令可以启动GUI：

fm_shell> start_gui

        在本实验继续调试之前，下一部分将简要介绍GUI的一些基础知识。

GUI的简单介绍

        主GUI会话窗口如图1所示，包含了表1所示的区域。

图1 主GUI会话窗口

表1 窗口区域

窗口区域	描述
设计栏 (Design bar)	显示参考设计和实现设计的WORK库路径。
菜单栏 (Menu bar)	GUI命令，其中一些在工具栏和右键菜单中也有重复。
工具栏 (Toolbar)	GUI命令。工具栏根据显示在上下文窗格中的视图发生变化。可以重新排列工具栏上的图标，并将工具栏移动到窗口的任意边缘。右键单击工具栏并选择或取消选择以查看所需的工具栏菜单。
基于流程的工具栏 (Flow-based toolbar)	显示执行正式验证所需采用的正确流程的选项。选项会高亮显示，指示当前所在的流程步骤。每个选项都会在上下文窗格中显示一个新视图。默认情况下，GUI从第一个步骤（指导）开始打开，并显示指导工作区。使用fm_shell执行步骤并调用GUI时，GUI将高亮显示当前所在的流程步骤。当继续一个之前保存的Formality会话时，也会发生这种情况。
上下文窗格 (Context pane)	主要的工作区域。在这里执行执行验证所需的操作，也可以在此查看报告。可以调整大小并分离上下文或报告窗格，以查看更大的报告。
命令控制台 (Command console)	显示根据Formality提示符下使用的命令记录和其他信息。可以调整大小并分离命令控制台，以查看较大的命令记录。
Formality提示符 (Formality prompt)	一个文本框，可以在其中输入通过GUI界面无法访问的Formality命令和变量。
状态栏 (Status bar)	显示工具的当前状态。

使用GUI调试

1、在基于流程的工具栏上，点击Debug，如果它尚未被选中。上下文窗格会显示失败点报告，其中可能会出现多个名称相似的失败点，如图2所示。例如，可能会看到*_reg[0]、*_reg[1]、*_reg[2]和*_reg[3]，通常一组失败点是由一个单一的错误引起的。

图2 失败点报告

2、要对失败点进行诊断，请在失败点报告中右键并点击Diagnosis或者在菜单栏Run的下拉栏点击Diagnosis，如图3所示。 在诊断过程中，Formality会分析比较点并找到错误候选项。错误候选项窗口Analyses会出现，显示在实现设计中发现的错误候选项。

图3 执行诊断

        注意：在调试过程中，如果出现错误提示，指出诊断失败是因为错误过多（且知道错误不是由设置问题引起的），请选择某个有相似名称的失败点，右键并点击Diagnose Selected Points或在菜单栏Run的下拉栏点击Diagnose Selected Points。这可能有助于将诊断定向到设计的特定部分。

3、在错误候选项窗口中，右键点击U81并选择Show Logic Cones。窗口会显示该错误相关的失败点列表，可以从中选择一个点（例如使用push_logic/pop_count_svd_reg[0]），双击或点击OK以查看逻辑锥，如图4所示。

图4 选择一个失败比较点以查看逻辑锥

        Failing ConeSchematics窗口会出现，显示参考设计（上屏）和实现设计（下屏）的逻辑锥示意图。实现设计的示意图会突出显示并放大实现设计的逻辑锥中的错误候选项U81反相器，而参考设计的示意图会高亮显示与实现设计中的错误候选项对应的匹配区域，如图5所示。

图5 参考设计和实现设计的逻辑锥

        实现设计中的错误候选项用橙色高亮显示，而参考设计中对应的匹配区域用黄色高亮显示。要单独查看错误区域，可以用一以下任意方式实现：

• 右键并选择Prune/Restore > Isolate Error Candidates
• 选择Edit > Prune/Restore > Isolate Error Candidates

        这样会将不相关的子逻辑锥（子逻辑锥并不是真正意义上的逻辑锥，因为没有比较点，它只是逻辑锥的一部分）修建，仅显示错误反相器，如图6所示。

图6 修剪不相关的子逻辑锥

        可以在Pattern窗口中查看已修剪后的逻辑锥输入（需要勾选Filter），如图7所示。

图7 修剪后的逻辑锥输入Pattern

4、选择Pattern1并观察触发器的CLK引脚的标注：参考设计显示逻辑0，而实现设计显示逻辑1。 注意到驱动实现设计中触发器的CLK引脚的逻辑中包括一个反相器。在综合过程中，可能会插入一个反相器以修复保持时间问题，你可以：

• 通过点击工具栏上的Zoom In图标，或者点击示意图，进行放大查看。
• 复制/粘贴逻辑锥示意图中的选定对象，点击Edit > Copy，并选择以下之一：Instance Name、Library Name或Design Name，接着通过Ctrl+V或右键并选择Paste，将这些名称粘贴到Formality提示符或任何其他可编辑文本框中。

5、通过编辑网表或重新综合设计，生成一个新的、无时钟树操作错误的网表。为了节约时间，在GATE目录包含了修正后的网表fifo_mod.vg。可以在shell中执行以下命令，查看两个网表差异：

% diff ./GATE/fifo.v ./GATE/fifo.mod.vg

        将看到修改后的网表去除了反相器。

6、最后重新按照本实验的步骤验证fifo.mod.vg和fifo.v之间的等价性（略）。

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