相关阅读Formalityhttps://blog.csdn.net/weixin_45791458/category_12841971.html?spm1001.2014.3001.5482等价性检查的流程图1概述了使用Formality进行等效性检查的具体步骤。图1 等价性检查流程启动Formality(Start Formality)要启动Formality请在Linux命令行使用fm_shell命令如下所示。% fm_shell ... fm_shell (setup)其中(setup)表示你当前所在的模式所有的模式包括guide、setup、preverify、match和verify启动Formality时默认进入setup模式。如果希望启动GUI有下面三种方法在Linux命令行使用formality命令启动Formality。使用fm_shell命令启动时添加-gui选项。在fm_shell中使用start_gui命令。注意在启动Formality前需要首先设置环境变量、路径和许可证。加载指导文件(Load Guidance)Formality流程中的加载指导文件是一个关键点在这里可以选择提供关于设计更改的设置信息这些更改是由设计流程中使用的其他工具比如Design Compiler引起的。下面的命令加载指导文件。% fm_shell ... fm_shell (setup) set_svf default.svf也可以使用GUI界面加载指导文件如图2所示。图2 加载指导包含指导信息的文件被称为SVF文件通常具有.svf扩展名。其实SVF文件就是由Formality命令构成的文件第一条命令是guide进入guide模式随后执行guide类命令比如guide_environment命令。在SVF文件的最后使用setup命令重新回到了setup模式。手动执行guide类命令也是可以的首先需要使用guide命令进入guide模式随后执行guide类命令最后使用setup命令回到setup阶模式。在Synopsys设计实现流程中推荐提供指导文件而在验证由第三方工具修改的设计时提供指导则是可选的。加载设计(Load Designs)为了执行验证首先需要将两个设计提供给Formality第一个设计是黄金设计(golden design)已知在功能上是正确的设计又称参考设计(reference design)第二个设计是参考设计的修改版本称为实现设计(implementation design)这是希望与参考设计进行验证的设计。下面的命令读取top.v文件并放入参考设计容器中。% fm_shell ... fm_shell (setup) read_verilog -r top.v也可以使用GUI界面加载设计如图3所示。图3 加载设计文件Formality可用于验证两个RTL设计之间的等效性两个门级设计之间的等效性或者一个RTL设计与一个门级设计之间的等效性。加载到Formality中的设计文件只能是可综合的SystemVerilog、Verilog或VHDL代码或者可以是Synopsys内部数据库格式.db、.ddc或Milkyway数据库。注意在加载设计文件后通常要设置顶层设计。执行设置(Perform Setup)设置步骤涉及向Formality提供信息以解决在指导步骤中未自动处理的特定问题以下是一些需要设置的情况内部扫描(internal scan)边界扫描(boundary scan)时钟门控(clock-gating)有限状态机(FSM)重新编码(re-encoding)黑盒(black boxes)流水线重定时(pipeline retiming)下面的命令设置了参考设计扫描端口为常量0。% fm_shell ... fm_shell (setup) set_constant -type port r:/WORK/top/scanmode 0也可以使用GUI界面执行设置如图3所示。​图3 执行设置可以在加载指导文件前设置Automated Setup Mode模式这样可以减少设置模式的任务甚至跳过设置模式详细见下面的博客。Formality设置Automated Setup Mode模式文章浏览阅读628次点赞10次收藏10次。Formality要使用自动设置模式在加载/执行svf文件之前需要将synopsys_auto_setup变量布尔值设置为true或者在GUI界面中选择Use Auto Setup如图1所示。当自动设置模式设置后一组Formality变量会被设置一些设置命令会执行以与Synopsys综合工具例如Design Compiler兼容从而通过使用svf指导文件提高整体工具的设置性能。https://blog.csdn.net/weixin_45791458/article/details/144113957?spm1001.2014.3001.5501匹配比较点(Match Compare Points)在这个步骤中Formality工具会尝试将参考设计中的每个比较点与实现设计中的相应比较点进行匹配其实不止比较点所有应该匹配的点都在这个步骤进行匹配比如输入端口、黑盒输出等。准确的匹配是确保验证准确性的关键匹配确保没有不匹配的逻辑锥并验证实现设计的功能性。比较点包括黑盒输入引脚、循环断开点、多驱动线网、Cut-Point、输出端口、D触发器和锁存器。下面的命令进行匹配。% fm_shell ... fm_shell (setup) match也可以使用GUI界面执行设置如图4所示。图4 进行匹配验证与解释结果(Verify and Interpret Results)验证在加载、设置和比较点匹配步骤之后进行。% fm_shell ... fm_shell (match) verify在验证的结束或在过程中断验证结果将报告为PASS所有比较点是等效的FAIL一些比较点不等效INCONCLUSIVE一些比较点要么未验证要么已终止调试(Debug)如果设计验证不成功则需要进行调试。在调试过程中将使用验证结果来定位失败或未得出结论的结果此步骤有助于确定结果不成功的位置以及可能的原因。设计失败可能是由于设置问题或设计之间的逻辑差异导致的不同的失败原因需要不同的调试解决方案因此Formality提供了多种调试策略。这些策略包括从手动匹配未匹配的比较点到通过基于GUI的分析进行调试对于未得出结论的验证也是如此。工作模式之前已经说到Formality的模式包括guide、setup、preverify、match和verify这些模式分别支持不同的命令。guide模式guide模式用于执行guide类命令例如guide_mark、guide_uniquify等只能在guide模式下使用否则会提示*** restricted to guide mode only不支持执行read类命令出现FM-373错误。在setup模式前提是在读取除工艺库外的设计文件之前使用guide命令会进入guide模式。在setup模式使用set_svf命令前提是在读取除工艺库外的设计文件之前读取指导文件时也会进入guide模式因为SVF文件中的第一条命令就是guide。在等价性检查的流程中加载指导文件(Load Guidance)就是在guide模式进行的。setup模式setup模式用于执行read类命令和setup类命令例如read_verilog、set_top、set_constant、set_black_box等需要注意的是setup类命令不会影响preverify模式下guide类命令的处理。在guide模式或preverify模式使用setup命令会进入setup模式。在match模式或verify模式使用setup命令会抛弃所有的匹配和验证结果并进入setup模式。在等价性检查的流程中加载设计(Load Designs)和执行设置(Perform Setup)就是在setup模式进行的。preverify模式在preverify模式下可以访问最终的参考设计该设计是应用了UPF、SVF和ECO等修改的设计实例该模式下只能执行不修改设计数据库的setup类命令这也是该模式分离出来的原因可对处理后的设计对象进行设置否则工具将发出错误消息如下所示。fm_shell (preverify) remove_design r Error: remove_design can only be executed in SETUP mode. First execute setup. (FM-336)在setup模式使用preverify命令会进入preverify模式并处理注意处理和加载的区别guide类命令SVF文件使用match命令或verify命令使用verify命令时会先自动执行match命令会自动执行preverify命令。在preverify、match或verify模式使用preverify命令会重新处理SVF文件并抛弃所有的匹配和验证结果并进入preverify模式实测会提示Info: Skipping SVF processing - Reference has already been processed。match模式在setup模式或preverify模式使用match命令进入match模式会根据比较点将实现设计与参考设计进行匹配匹配完成后会报告匹配结果。在verify模式使用match命令不会切换模式但仍然会进行匹配。可以增量地执行比较点匹配这在自动匹配失败时非常有用通常是因为参考设计和实现设计之间的名称或结构差异。如果匹配过程被中断工具将保留部分匹配结果重新运行match命令可以继续进行匹配。执行verify命令之前不必先执行match命令因为会先自动执行match命令对于交互式工作建议使用显式的match命令以便获取反馈在脚本中可以省略match命令以减少运行时间。report_unmatched_points和report_matched_points等命令只能在match模式和verify模式下使用否则会提示No unmatched/matched points avaliable before matching。在等价性检查的流程中匹配比较点(Match Compare Points)就是在match模式进行的。verify模式在setup模式、preverify模式或match模式下使用verify命令会进入verify模式并在判断设计是否可比并尝试证明它们的功能等效性如果验证两个设计时所有比较点都证明相等则会报告这些设计为功能等效验证通过如果任何比较点在验证中失败或在验证过程中中止会报告这两个设计为功能不等效验证失败。在等价性检查的流程中验证与解释结果(Verify and Interpret Results)就是在verify模式进行的。