相关阅读Formalityhttps://blog.csdn.net/weixin_45791458/category_12841971.html?spm1001.2014.3001.5482本文是对Synopsys Formality User Guide Tutorial中第一个实验的翻译有删改Lab文件可以从以下链接获取。Formality官方Tutorialhttps://download.csdn.net/download/weixin_45791458/90220600?spm1001.2014.3001.5501本教程首先解释如何为运行Formality做好准备然后通过三个使用该工具的实验进行讲解。在开始之前在开始本教程之前请确保系统上已正确安装Formality。Shell配置文件如果使用Bash指的是.bashr文件如果使用Zsh指的是~/.zshrc如果使用Csh指的是~/.cshrc应正确设置路径已包含Formality安装的bin目录。例如如果安装目录是/opt/Synopsys/Formality2018/fm/O-2018.06-SP1请在配置文件中添加如下的设置路径语句假设使用Bashexport 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 $HOME2、使用以下命令复制教程数据其中fm_install_path是Formality的安装目录% cp -r fm_install_path/doc/fm/tutorial $HOME3、切换到新的教程目录% cd tutorial教程目录的内容教程目录包含以下子目录GATEVerilog门级网表。GATE_WITH_JTAG带有扫描和联合测试行动组(JTAG)插入的Verilog门级网表。GATE_WITH_SCAN带有扫描插入的Verilog门级网表。LIB门级网表所需的逻辑库。RTLRTL源代码。启动Formality Shell% fm_shell ... fm_shell (setup)fm_shell命令启动了Formality的Shell环境和命令行界面在命令行界面可以通过以下命令启动GUIfm_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_shellGUI使用save_session session_file_name命令1、选择FileSave Session要重新启动该会话fm_shellGUI使用restore_session session_file_name命令1、选择FileRestore Session加载SVF文件在指定参考设计和实现设计之前可以选择性地将自动设置文件(.svf)加载到Formality中。SVF文件帮助Formality处理由设计流程中的其他工具引起的设计变更。Formality使用该文件来协助比较点匹配和验证过程这些信息有助于对正在验证的设计中的比较点进行对齐。对于每个加载的SVF文件Formality会在恰当时机处理其内容以便在基于名称的比较点匹配期间使用。有关SVF文件的详细介绍可见下文。Formalityset_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文件因此本节信息仅供参考。指定参考设计指定参考设计包括读取设计文件、可选地读取逻辑库除了使用逻辑库Verilog仿真库也是一个可选项并设置顶层设计。参考设计是与转换后的实现设计进行比较的设计。在本实验中参考设计是名为fifo.v的RTL源文件。需要显式指定DesignWare根目录因为fifo.v包含一个DesignWare中的RAM实例可按如下所示设置hdlin_dwroot变量fm_shellGUI使用set_app_var hdlin_dwroot path_to_DesignCompiler_install命令1、选择EditFormality Tcl Variables将会显示Formality Tcl Variables对话框。2、在Reading Designs部分选择hdlin_dwroot变量。3、输入或选择路径path_to_DesignCompiler_install并回车确定。现在加载所有参考Verilog文件fm_shellGUI使用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、点击1. Ref.。2、点击Verilog导航到GATE子目录选择文件并点击Open。3、点击加载文件按钮跳过Read DB Libraries因为RTL形式的参考设计不需要映射到任何特定的工艺文件。最后定义参考设计的顶层设计设置顶层设计将启动所有文件的链接和展开过程并报告是否缺少任何文件Formality会自动搜索DesignWare库以寻找RAM的实现fm_shellGUI使用set_top fifo命令1、点击Set Top Design。2、选择WORK库和fifo设计并点击Set Top。指定实现设计指定实现设计的过程与指定参考设计的过程类似首先加载所有实现Verilog文件fm_shellGUI使用read_verilog -i ./GATE/fifo.vg命令1、点击2. Impl.。2、点击Verilog导航到GATE子目录选择文件并点击Open。3、点击加载文件按钮。但于参考设计不同的是此时需要加载逻辑库fm_shellGUI使用read_verilog -i ./LIB/lsi_10k.db命令1、点击Read DB Libraries。2、点击DB导航到LIB子目录选择lsi_10k.db文件并点击Open。3、 点击加载文件按钮。最后定义实现设计的顶层设计fm_shellGUI使用set_top fifo命令1、点击Set Top Design。2、选择WORK库和fifo设计并点击Set Top。执行设置通常需要指定额外的设置信息以考虑设计网表中未包含的信息或为了实现最佳性能。这一步骤涉及向Formality提供信息。例如如果设计经过了如扫描或JTAG插入等转换可能需要设置常量。在这种情况下只有fifo.vg被综合因此可以继续进行到下一个步骤Match。进行匹配匹配是Formality将参考设计和实现设计分割成逻辑单元的过程这些逻辑单元称为逻辑锥(logic cones)。每个逻辑锥都有一个比较点作为顶点且实现设计中的每个比较点必须与参考设计中的每个比较点匹配否则验证将失败。匹配阶段需要确保没有不匹配的逻辑锥并验证实现设计的功能性。要进行匹配请执行以下操作fm_shellGUI使用match命令1、点击4. Match。2、点击Run Matching。匹配结果显示619个点全部匹配成功。验证设计要验证设计请执行以下操作fm_shellGUI使用verify命令1、点击5. Verify。2、点击Verify。在此案例中验证将失败并显示有17个比较点验证失败因为fifo.vg中故意包含了一个设计错误以展示Formality的调试功能。调试对于大多数用户来说调试失败的验证是一个挑战也就是说必须找到设计中功能差异的确切位置然后进行修复。使用GUI进行调试更加直观如果你之前使用的是fm_shell以下命令可以启动GUIfm_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、在基于流程的工具栏上点击6. 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/RestoreIsolate Error Candidates选择EditPrune/RestoreIsolate Error Candidates这样会将不相关的子逻辑锥子逻辑锥并不是真正意义上的逻辑锥因为没有比较点它只是逻辑锥的一部分修建仅显示错误反相器如图6所示。图6 修剪不相关的子逻辑锥可以在Pattern窗口中查看已修剪后的逻辑锥输入需要勾选Filter如图7所示。图7 修剪后的逻辑锥输入Pattern4、选择Pattern1并观察触发器的CLK引脚的标注参考设计显示逻辑0而实现设计显示逻辑1。 注意到驱动实现设计中触发器的CLK引脚的逻辑中包括一个反相器。在综合过程中可能会插入一个反相器以修复保持时间问题你可以通过点击工具栏上的Zoom In图标或者点击示意图进行放大查看。复制/粘贴逻辑锥示意图中的选定对象点击EditCopy并选择以下之一Instance Name、Library Name或Design Name接着通过CtrlV或右键并选择Paste将这些名称粘贴到Formality提示符或任何其他可编辑文本框中。5、通过编辑网表或重新综合设计生成一个新的、无时钟树操作错误的网表。为了节约时间在GATE目录包含了修正后的网表fifo_mod.vg。可以在shell中执行以下命令查看两个网表差异% diff ./GATE/fifo.v ./GATE/fifo.mod.vg将看到修改后的网表去除了反相器。6、最后重新按照本实验的步骤验证fifo.mod.vg和fifo.v之间的等价性略。实验二Formality官方Tutorial二文章浏览阅读450次。本文是对Synopsys Formality User Guide Tutorial中第二个实验的翻译有删改Lab文件可以从以下链接获取。https://blog.csdn.net/weixin_45791458/article/details/144936604?spm1001.2014.3001.5501原文链接Formality各版本User Guidehttps://download.csdn.net/download/weixin_45791458/90184000?spm1001.2014.3001.5503