1. 从零到一理解形式验证与Formality的核心价值在数字芯片设计的漫长流程里验证环节往往占据了超过70%的时间和精力。我们习惯了搭建测试平台Testbench编写大量的测试向量然后让仿真器Simulator跑上几天几夜盯着波形图Waveform去揪出那些深藏不露的bug。这种方法我们称之为动态仿真Dynamic Simulation它直观、灵活但效率瓶颈也极其明显你永远无法穷尽所有可能的输入组合尤其是当设计规模达到千万门甚至上亿门级别时仿真的时间成本会变得难以承受。更让人头疼的是当你仅仅为了修复一个时序违例Timing Violation而在网表Netlist里手动插入一个缓冲器Buffer或者为了功耗优化替换了一个标准单元Standard Cell后你如何确保这个微小的改动没有引入新的功能错误难道要把之前那套耗时数周的仿真用例全部重跑一遍吗这时候形式验证Formal Verification的价值就凸显出来了。它不依赖测试向量而是通过严密的数学逻辑推理来证明两个设计在功能上是否完全等价。你可以把它想象成一位极其严谨的数学老师他不看你做题的过程仿真波形而是直接对比你修改前和修改后的两道题的最终答案逻辑功能并用数学定理证明它们是否一致。Synopsys的Formality就是这位“数学老师”在芯片设计领域最著名、应用最广泛的工具之一。它主要用于两种场景RTL代码与综合后网表的等价性检查RTL vs. Netlist以及不同版本网表之间的等价性检查Netlist vs. Netlist。对于从事前端设计、逻辑综合、物理实现乃至后期ECOEngineering Change Order的工程师来说掌握Formality是提升验证效率、保证设计质量不可或缺的一环。2. Formality实战环境准备与关键变量设置工欲善其事必先利其器。运行Formality的第一步是启动它。通常我们会在Linux/Unix终端下操作。如果你习惯命令行交互可以直接运行fm_shell进入命令行模式。对于初学者或者需要进行复杂交互调试的场景我更推荐使用图形界面模式启动命令是fm_shell -gui。图形界面能更直观地展示匹配Match和验证Verify的结果特别是查看不匹配Unmatched或失败Failing的点时定位问题会方便很多。启动之后我们并不是直接读入设计就开始验证。Formality的行为由一系列内部变量Variables控制这些变量的设置是否正确直接决定了验证能否顺利进行甚至决定了验证结果的正确性。根据我多年的项目经验以下这些变量的设置是成功运行Formality的基石很多初次使用者踩坑问题往往就出在这里。2.1 基础路径与设计环境设置在开始任何操作前定义好工作环境是必要的。这包括设置一些Shell环境变量和Tcl脚本中的变量以确保工具能找到正确的库文件和设计文件。# 设置工作目录和设计相关变量 set HOME /homes/your_username set RTLHOME $env(RTLHOME) ;# 通常从环境变量中获取RTL根目录 set TARGET_TECH $env(TARGET_TECH) ;# 指定工艺库如tsmc28nm set DESIGN “MY_CHIP_TOP” ;# 设置当前要验证的设计顶层模块名如果你的设计中实例化了Synopsys DesignWare IP那么必须正确设置hdlin_dwroot变量指向你的DesignWare安装路径。否则工具在读取RTL时无法解析这些IP会导致链接Link失败。set hdlin_dwroot /tools/synopsys/2022.03/dw2.2 控制警告与错误行为的变量Formality在读取和分析设计时会产生大量信息INFO、警告WARNING和错误ERROR。有些警告是良性的可以忽略但默认情况下某些特定警告会导致工具停止执行。为了避免这种情况我们需要“白名单”一些警告信息。set hdlin_warn_on_mismatch_message “FMR_VHDL-1002 FMR_VHDL-1027 FMR_VHDL-1014 FMR_ELAB-146 FMR_ELAB-149 FMR_ELAB-130 FMR_ELAB-117 FMR_ELAB-034 FMR_ELAB-261”这条命令告诉Formality当遇到列表中这些特定的警告信息时不要将其视为致命错误而停止继续执行即可。这个列表是经验性的不同版本的工具或不同的设计可能需要调整。一个实用的技巧是第一次运行如果因为某个警告中断可以把这个警告号加到这个列表中再试。另一个重要的变量是verification_failing_point_limit。想象一下如果你的设计中有成千上万个比较点Compare Point而前10个比较点就失败了这通常意味着设计存在根本性的不匹配比如时钟或复位信号没对上继续验证后面成千上万个点毫无意义只会浪费计算资源。设置这个变量可以让工具在遇到指定数量的失败点后自动停止。set verification_failing_point_limit 10 ;# 遇到10个失败点后停止验证2.3 指导匹配过程的策略变量Formality的核心任务是将参考设计Reference中的逻辑单元如寄存器、端口与实现设计Implementation中的对应单元匹配起来。这个过程主要依靠名称匹配Name Matching和拓扑结构匹配Topology Matching。以下变量可以精细地控制匹配策略verification_clock_gate_hold_mode: 这个变量用于处理时钟门控Clock Gating单元。在综合过程中工具可能会插入时钟门控单元来降低动态功耗。这个变量告诉Formality如何识别和处理这些单元。通常设置为any或low。any表示工具会自动识别各种类型的时钟门控low则更具体。在RTL vs. Netlist验证中根据综合工具的报告来设置这个变量往往更准确。verification_inversion_push: 这是一个非常关键且容易出错的设置。在网表中寄存器DFF的输出可能是正端Q也可能是反端QN。如果参考设计RTL中用的是q reg而综合后网表中对应的寄存器输出连的是QN因为优化导致反相器被推到了寄存器内部Formality默认可能无法匹配它们。将此变量设为true会启用“反相器推入”功能工具会尝试将逻辑反相关系考虑在内从而成功匹配。在验证包含大量逻辑优化的设计时这个开关常常需要打开。名称匹配过滤规则: 网表中的名字往往包含许多综合工具添加的特殊字符如[,],_,$等。为了提升名称匹配的准确率我们可以设置过滤规则。set name_match_filter_chars “‘~!#$%^*()_-|\[]{}’:;?,./” set name_match_use_filter true set name_match_allow_subset_match falsename_match_filter_chars定义了在比较名字时要忽略的特殊字符集合。name_match_allow_subset_match设为false要求进行严格的全名匹配避免误匹配。signature_analysis_match_compare_points: 签名分析Signature Analysis是Formality的一种高级匹配算法它通过分析逻辑锥Logic Cone的输入输出关系来匹配比较点即使名称完全不同。对于经过大规模重定时Retiming或重构Re-engineering的设计开启此功能设为true可能有意想不到的奇效。2.4 处理不完整设计黑盒设置在实际项目中我们验证的模块可能调用了其他尚未完成或无需验证的IP例如第三方硬核、模拟模块等。在读取设计时Formality如果找不到这些子模块的定义就会报错。此时我们可以将这些模块声明为黑盒Black Box。set hdlin_unresolved_modules black_box这条命令是全局设置告诉Formality遇到任何无法解析的模块都自动将其视为黑盒。更常见的做法是在读入设计后使用set_black_box命令针对特定的模块进行设置这样更精确。黑盒内部的逻辑将被忽略只将其输入输出端口作为边界参与验证。注意将模块设为黑盒意味着放弃对其内部逻辑正确性的验证。务必确保黑盒模块的接口端口名、位宽、方向在参考设计和实现设计中完全一致否则会导致端口匹配失败进而影响整个验证流程。3. 核心流程拆解从读入设计到生成报告理解了关键变量后我们就可以按部就班地执行Formality的标准流程了。这个过程就像执行一个精心编排的剧本每一步都有其明确的目的和常见的“坑点”。3.1 灵魂向导SVF文件的作用与设置在RTL vs. Netlist的验证中有一个文件至关重要那就是SVFSetup Verification Format文件。它由逻辑综合工具如Design Compiler在综合过程中自动生成。你可以把SVF文件看作是综合工具写给Formality的一封“解释信”。信里详细记录了综合工具对原始RTL做了哪些优化和转换比如哪些寄存器被合并或复制了。哪些层次结构被展平Flatten了。哪些常数传播Constant Propagation和冗余逻辑消除发生了。插入了哪些扫描链Scan Chain或测试逻辑DFT Logic。如果没有这封“解释信”Formality就像一个看不懂魔术揭秘的观众它看到网表魔术结果和RTL魔术描述完全不同会报告大量不匹配和失败。而SVF文件里的guide命令就是一步步向Formality揭示魔术手法帮助它理解“这个网表中的奇怪结构其实对应的是RTL里的那个简单描述”。设置SVF文件的命令如下set svf_path ${RTLHOME}/${DESIGN}/synopsys_output set_svf -append ${svf_path}/my_design.svf-append选项用于当你有多个SVF文件时例如顶层和子模块分开综合将它们依次加载。从Design Compiler 2005.09版本开始工具在生成二进制SVF的同时也会默认生成一个文本格式的.svf.txt文件方便用户阅读。你也可以用report_guidance -to svf.txt命令手动生成文本报告这对于调试复杂的匹配问题非常有帮助。实操心得务必确保加载的SVF文件与当前要验证的网表版本严格对应。如果综合后你对网表做了任何手动修改ECO但SVF文件没有更新Formality的匹配结果很可能是错误的。一个常见的做法是在每次综合或重大网表修改后都重新生成并加载最新的SVF文件。3.2 读入与链接参考设计与实现设计Formality使用“容器”Container的概念来管理不同的设计视图。通常我们用r容器存放参考设计RTL或黄金网表用i容器存放实现设计待验证的网表。步骤一读入参考设计对于VHDL设计read_vhdl -container r -libname WORK [list file1.vhd file2.vhd]对于Verilog设计read_verilog -container r -libname WORK [list file1.v file2.v]-libname指定库名通常为WORK。-container r指明读入到参考容器。步骤二链接参考设计读入文件只是将代码加载到内存链接Link则是解析所有模块实例化建立完整的层次化设计。set_top r:/WORK/${DESIGN}这里r:/WORK/${DESIGN}指定了参考设计的顶层模块路径。如果链接失败通常会报出找不到某个子模块的定义这时就需要检查文件列表是否完整或者是否需要将某些模块设为黑盒。步骤三读入实现设计实现设计通常是综合后或布局布线后的门级网表Gate-level Netlist。read_verilog -container i -netlist ${NETLIST_PATH}/${DESIGN}_final.v关键选项-netlist告诉Formality这是网表文件工具会调用相应的库来解析标准单元和宏单元。步骤四链接实现设计set_top i:/WORK/${DESIGN}3.3 预处理处理测试与时钟门控逻辑在芯片设计中为了可测试性DFT网表中通常会插入扫描链Scan Chain这会在功能端口之外增加ScanEnable,ScanIn,ScanOut等测试信号。在功能等价性验证时我们需要屏蔽这些测试逻辑通常将ScanEnable信号设置为0功能模式并告诉Formality不要验证扫描输出端口。# 将参考和实现设计中的ScanEnable端口固定为0 set_constant -type port r:/WORK/${DESIGN}/ScanEnable 0 set_constant -type port i:/WORK/${DESIGN}/ScanEnable 0 # 设置不验证扫描输出端口 set_dont_verify_point r:/*/${DESIGN}/*ScanOut set_dont_verify_point i:/*/${DESIGN}/*ScanOutset_dont_verify_point命令告诉Formality忽略这些点不将它们纳入等价性比较的范围。这对于通过验证至关重要。3.4 匹配与验证见证结果的时刻在正式验证之前先进行匹配Match是一个好习惯。匹配阶段会尝试将两个设计中的比较点寄存器、端口等关联起来。match执行match命令后Formality会输出匹配报告。你应该重点关注“Unmatched points”的数量。如果存在大量未匹配的点直接进行verify很可能失败并且问题难以定位。此时应该先分析并解决这些不匹配。一个有用的命令是report_unmatched_points它可以列出所有未匹配的点。对于数据路径如乘法器、加法器可以使用-datapath选项来专门报告因为数据路径的优化往往比较激进是未匹配问题的重灾区。report_unmatched_points -datapath unmatched_datapath.rpt当匹配结果令人满意未匹配点数量很少且可以解释如新增的时钟门控单元后就可以进行最终的验证了。verifyverify命令会启动形式验证引擎进行严格的数学证明。验证完成后工具会返回一个成功或失败的状态。我们可以根据这个状态来决定后续操作。3.5 报告生成结果分析与归档无论验证通过与否生成详细的报告都是必须的。这些报告是调试和交付的重要依据。if { [verify] 1 } { echo “Formal Verification PASSED!” quit } else { echo “Formal Verification FAILED!” report_failing -verbose failing_points.rpt report_unmatched unmatched_points.rpt report_error_candidates error_candidates.rpt # 即使失败也生成匹配点报告用于对比分析 report_matched matched_points.rpt }report_failing: 列出所有验证失败的点这是调试的起点。-verbose选项会提供更详细的信息包括失败点的逻辑锥和可能的原因分析。report_unmatched: 再次确认未匹配的点。report_error_candidates: 工具会分析失败点给出一些可能出错的“候选”位置对于复杂问题的定位有提示作用。report_matched: 列出所有成功匹配的点在对比分析时有用。4. 高级调试技巧与常见问题实战Formality验证失败是家常便饭尤其是面对大型、复杂且经过深度优化的设计。能够快速定位并解决失败点是衡量一个工程师形式验证功力的关键。下面我结合几个典型案例分享一些实战调试技巧。4.1 典型失败场景与排查思路验证失败的报告通常会给出失败点的层次路径和类型。我们可以根据失败的特征采取不同的排查策略。场景一大量寄存器DFF不匹配或失败可能原因1时钟/复位信号未对齐。这是最常见的原因。检查参考设计和实现设计中时钟CLK和复位RST_n端口是否被正确识别和约束。确保你没有遗漏设置set_constant或set_case_analysis来固定某些控制信号的状态。排查命令:report_clock r: report_clock i: report_reset r: report_reset i:对比两个报告中时钟和复位的属性周期、边沿、是否门控是否一致。可能原因2verification_inversion_push设置不当。如前所述如果网表中寄存器使用了反相输出而此变量未设置为true会导致大量寄存器匹配失败。尝试打开此开关。可能原因3SVF文件不匹配或未加载。确认加载的SVF文件是否由生成当前网表的综合过程产生。可以尝试不使用SVF文件set_svf -disable运行一次匹配如果匹配点数量剧增说明SVF文件起到了关键作用但也可能包含了错误引导。需要检查SVF文件内容或综合脚本。场景二组合逻辑输出点失败可能原因1常数传播不一致。检查失败点相关的逻辑锥中是否有在参考设计中是常数但在实现设计中由于优化变成了非常数或者反之。使用report_constant命令查看两个设计中哪些信号被工具识别为常数。可能原因2黑盒接口不匹配。如果失败点位于黑盒模块的边界很可能是黑盒的端口位宽、方向或名字在两边不一致。仔细对比report_black_box的输出。可能原因3时序逻辑被优化为组合逻辑。某些情况下综合工具可能将一些简单的时序逻辑如电平敏感的锁存器优化掉了。这需要在参考设计端也做出相应处理或者使用set_dont_verify_point排除这些点。场景三签名分析Signature Analysis相关的失败当启用签名分析匹配了大量比较点后如果这些点验证失败调试会变得复杂因为传统的基于名称的追踪方法可能失效。策略暂时关闭签名分析 (set signature_analysis_match_compare_points false)重新运行匹配和验证。虽然未匹配点会变多但失败点可能会集中在少数几个有名称的逻辑单元上更容易定位根本原因。找到根本原因并修复后再重新开启签名分析。4.2 实用调试命令与信息获取除了生成报告Formality还提供了许多交互式命令用于深入探查设计内部。show_objects: 查看特定对象如寄存器、端口、线网的属性。show_objects -type port r:/WORK/TOP/input_areport_logic: 报告驱动某个信号的所有逻辑或者某个信号驱动的所有负载。这对于追踪信号路径、理解逻辑锥极其有用。report_logic -from r:/WORK/TOP/reg1/D -to r:/WORK/TOP/reg1/Q report_logic -fanin 3 i:/WORK/TOP/some_net ;# 报告某个网线的前3级逻辑锥write_do_lec: 这是一个“杀手锏”命令。当Formality遇到极其棘手、难以定位的失败点时可以使用此命令将失败点的逻辑锥导出为另一个等价性检查工具如Cadence Conformal LEC可读的格式。有时换一个工具视角问题可能豁然开朗。write_do_lec -failure -depth 5 -file difficult_case.lec4.3 ECO验证的特殊处理ECOEngineering Change Order验证是Formality的强项。通常流程是将修改前的网表作为参考设计r。将应用了ECO补丁的网表作为实现设计i。通常不需要SVF文件因为ECO改动很小且是直接对网表的手动修改。重点使用set_constant和set_case_analysis来固定ECO不影响的其他部分如扫描模式、功能模式选择信号将验证范围缩小到ECO影响的局部电路。匹配和验证。由于改动小匹配率应该接近100%验证速度也很快。一个ECO验证的典型命令片段可能是# 假设ECO只修改了模块SUB_MODULE_A中的逻辑 set_black_box r:/WORK/TOP/SUB_MODULE_B set_black_box i:/WORK/TOP/SUB_MODULE_B # 将设计置于功能模式 set_constant -type port r:/WORK/TOP/TestMode 0 set_constant -type port i:/WORK/TOP/TestMode 0 match verify通过将未修改的模块设为黑盒可以极大提升验证效率并聚焦于真正的改动点。5. 解读Formality日志与报告从信息到洞见运行Formality后控制台和日志文件会输出大量信息。学会快速解读这些信息是高效工作的关键。我们以一段典型的日志为例进行拆解*********************************** Matching Results *********************************** 4328 Compare points matched by name 0 Compare points matched by signature analysis 0 Compare points matched by topology 876 Matched primary inputs, black-box outputs 0(345) Unmatched reference(implementation) compare points 0(0) Unmatched reference(implementation) primary inputs, black-box outputs 7562(0) Unmatched reference(implementation) unread points ***********************************************************************************匹配结果摘要4328 Compare points matched by name: 通过名称匹配了4328个比较点主要是寄存器和端口。这是最理想、最主要的匹配方式。0 ... matched by signature analysis: 通过签名分析匹配了0个点。说明要么没开启该功能要么设计优化程度不高名称匹配已足够。876 Matched primary inputs, black-box outputs: 匹配了876个主要输入和黑盒输出。这是设计的边界。0(345) Unmatched reference(implementation) compare points:这是需要重点关注的数据括号外是参考设计中未匹配的点数0括号内是实现设计中未匹配的点数345。这意味着网表中有345个比较点很可能是寄存器在参考设计中找不到对应物。常见原因包括综合工具插入了参考设计中没有的寄存器如用于修复保持时间违例的缓冲寄存器、时钟门控寄存器、扫描链寄存器未被正确排除、或者SVF文件未能正确引导工具识别这些新增的寄存器。7562(0) Unmatched reference(implementation) unread points: 参考设计中有7562个“未读点”未匹配。这通常不是问题。“未读点”可能包括RTL中存在的中间变量wire、常量、或某些层次的实例它们在综合后被优化掉了没有体现在门级网表中。只要实现设计这边是0就说明网表中没有“多余”的逻辑这是好现象。接下来的验证结果报告更为关键--------------------------------------------------------------------------------------- Matched Compare Points BBPin Loop BBNet Cut Port DFF LAT TOTAL --------------------------------------------------------------------------------------- Passing (equivalent) 0 0 0 0 853 34 0 887 Failing (not equivalent) 0 0 0 0 2 198 0 200 Unverified 0 0 0 0 79 4932 0 5011 Not Compared Don‘t verify 0 0 0 0 64 0 0 64 ****************************************************************************************这个表格按类型统计了匹配点的验证状态Passing: 通过验证功能等价。这是我们追求的结果。这里有887个点。Failing: 验证失败功能不等价。必须全部解决这里有200个失败点其中198个是锁存器LAT2个是D触发器DFF。锁存器失败很常见因为锁存器在RTL中容易因编码风格问题隐含产生而综合工具对其处理方式多变容易导致不匹配。Unverified: 未验证的点。数量巨大5011个其中绝大部分4932个是锁存器。这些点之所以未验证很可能是因为它们没有被成功匹配参考前面的未匹配点统计。Formality只会对已匹配的点进行验证。Not Compared Don‘t verify: 被设置为不验证的点比如我们之前用set_dont_verify_point排除的扫描输出端口。这里的64个点符合预期。结论与行动从这个报告看主要问题是大量锁存器LAT未匹配且未验证并且有200个点主要是锁存器失败。调试重点应立即转向这些锁存器使用report_unmatched -type latch查看是哪些锁存器未匹配。检查RTL代码确认这些锁存器是否是设计意图。很多时候RTL中的不完全条件判断incomplete if-else 或 case 语句会综合出非预期的锁存器。如果锁存器是非预期的需要修改RTL代码消除锁存器。如果锁存器是设计意图如用于功耗门控则需要检查SVF文件是否有对应的guide_latch命令来引导匹配或者检查verification_clock_gate_hold_mode等变量设置是否正确。对于那2个失败的DFF需要用report_failing -verbose命令深入查看其逻辑锥定位具体是哪段逻辑不等价。通过这样层层递进地分析日志和报告就能将看似庞大的“失败”问题分解为一个个具体、可解决的子任务最终引导设计通过形式验证为芯片功能的正确性提供坚实的数学保障。这个过程虽然有时繁琐但比起动辄数周的仿真回归其效率优势是决定性的。
芯片设计形式验证实战：Formality环境配置与调试指南
发布时间：2026/6/7 17:34:24
1. 从零到一理解形式验证与Formality的核心价值在数字芯片设计的漫长流程里验证环节往往占据了超过70%的时间和精力。我们习惯了搭建测试平台Testbench编写大量的测试向量然后让仿真器Simulator跑上几天几夜盯着波形图Waveform去揪出那些深藏不露的bug。这种方法我们称之为动态仿真Dynamic Simulation它直观、灵活但效率瓶颈也极其明显你永远无法穷尽所有可能的输入组合尤其是当设计规模达到千万门甚至上亿门级别时仿真的时间成本会变得难以承受。更让人头疼的是当你仅仅为了修复一个时序违例Timing Violation而在网表Netlist里手动插入一个缓冲器Buffer或者为了功耗优化替换了一个标准单元Standard Cell后你如何确保这个微小的改动没有引入新的功能错误难道要把之前那套耗时数周的仿真用例全部重跑一遍吗这时候形式验证Formal Verification的价值就凸显出来了。它不依赖测试向量而是通过严密的数学逻辑推理来证明两个设计在功能上是否完全等价。你可以把它想象成一位极其严谨的数学老师他不看你做题的过程仿真波形而是直接对比你修改前和修改后的两道题的最终答案逻辑功能并用数学定理证明它们是否一致。Synopsys的Formality就是这位“数学老师”在芯片设计领域最著名、应用最广泛的工具之一。它主要用于两种场景RTL代码与综合后网表的等价性检查RTL vs. Netlist以及不同版本网表之间的等价性检查Netlist vs. Netlist。对于从事前端设计、逻辑综合、物理实现乃至后期ECOEngineering Change Order的工程师来说掌握Formality是提升验证效率、保证设计质量不可或缺的一环。2. Formality实战环境准备与关键变量设置工欲善其事必先利其器。运行Formality的第一步是启动它。通常我们会在Linux/Unix终端下操作。如果你习惯命令行交互可以直接运行fm_shell进入命令行模式。对于初学者或者需要进行复杂交互调试的场景我更推荐使用图形界面模式启动命令是fm_shell -gui。图形界面能更直观地展示匹配Match和验证Verify的结果特别是查看不匹配Unmatched或失败Failing的点时定位问题会方便很多。启动之后我们并不是直接读入设计就开始验证。Formality的行为由一系列内部变量Variables控制这些变量的设置是否正确直接决定了验证能否顺利进行甚至决定了验证结果的正确性。根据我多年的项目经验以下这些变量的设置是成功运行Formality的基石很多初次使用者踩坑问题往往就出在这里。2.1 基础路径与设计环境设置在开始任何操作前定义好工作环境是必要的。这包括设置一些Shell环境变量和Tcl脚本中的变量以确保工具能找到正确的库文件和设计文件。# 设置工作目录和设计相关变量 set HOME /homes/your_username set RTLHOME $env(RTLHOME) ;# 通常从环境变量中获取RTL根目录 set TARGET_TECH $env(TARGET_TECH) ;# 指定工艺库如tsmc28nm set DESIGN “MY_CHIP_TOP” ;# 设置当前要验证的设计顶层模块名如果你的设计中实例化了Synopsys DesignWare IP那么必须正确设置hdlin_dwroot变量指向你的DesignWare安装路径。否则工具在读取RTL时无法解析这些IP会导致链接Link失败。set hdlin_dwroot /tools/synopsys/2022.03/dw2.2 控制警告与错误行为的变量Formality在读取和分析设计时会产生大量信息INFO、警告WARNING和错误ERROR。有些警告是良性的可以忽略但默认情况下某些特定警告会导致工具停止执行。为了避免这种情况我们需要“白名单”一些警告信息。set hdlin_warn_on_mismatch_message “FMR_VHDL-1002 FMR_VHDL-1027 FMR_VHDL-1014 FMR_ELAB-146 FMR_ELAB-149 FMR_ELAB-130 FMR_ELAB-117 FMR_ELAB-034 FMR_ELAB-261”这条命令告诉Formality当遇到列表中这些特定的警告信息时不要将其视为致命错误而停止继续执行即可。这个列表是经验性的不同版本的工具或不同的设计可能需要调整。一个实用的技巧是第一次运行如果因为某个警告中断可以把这个警告号加到这个列表中再试。另一个重要的变量是verification_failing_point_limit。想象一下如果你的设计中有成千上万个比较点Compare Point而前10个比较点就失败了这通常意味着设计存在根本性的不匹配比如时钟或复位信号没对上继续验证后面成千上万个点毫无意义只会浪费计算资源。设置这个变量可以让工具在遇到指定数量的失败点后自动停止。set verification_failing_point_limit 10 ;# 遇到10个失败点后停止验证2.3 指导匹配过程的策略变量Formality的核心任务是将参考设计Reference中的逻辑单元如寄存器、端口与实现设计Implementation中的对应单元匹配起来。这个过程主要依靠名称匹配Name Matching和拓扑结构匹配Topology Matching。以下变量可以精细地控制匹配策略verification_clock_gate_hold_mode: 这个变量用于处理时钟门控Clock Gating单元。在综合过程中工具可能会插入时钟门控单元来降低动态功耗。这个变量告诉Formality如何识别和处理这些单元。通常设置为any或low。any表示工具会自动识别各种类型的时钟门控low则更具体。在RTL vs. Netlist验证中根据综合工具的报告来设置这个变量往往更准确。verification_inversion_push: 这是一个非常关键且容易出错的设置。在网表中寄存器DFF的输出可能是正端Q也可能是反端QN。如果参考设计RTL中用的是q reg而综合后网表中对应的寄存器输出连的是QN因为优化导致反相器被推到了寄存器内部Formality默认可能无法匹配它们。将此变量设为true会启用“反相器推入”功能工具会尝试将逻辑反相关系考虑在内从而成功匹配。在验证包含大量逻辑优化的设计时这个开关常常需要打开。名称匹配过滤规则: 网表中的名字往往包含许多综合工具添加的特殊字符如[,],_,$等。为了提升名称匹配的准确率我们可以设置过滤规则。set name_match_filter_chars “‘~!#$%^*()_-|\[]{}’:;?,./” set name_match_use_filter true set name_match_allow_subset_match falsename_match_filter_chars定义了在比较名字时要忽略的特殊字符集合。name_match_allow_subset_match设为false要求进行严格的全名匹配避免误匹配。signature_analysis_match_compare_points: 签名分析Signature Analysis是Formality的一种高级匹配算法它通过分析逻辑锥Logic Cone的输入输出关系来匹配比较点即使名称完全不同。对于经过大规模重定时Retiming或重构Re-engineering的设计开启此功能设为true可能有意想不到的奇效。2.4 处理不完整设计黑盒设置在实际项目中我们验证的模块可能调用了其他尚未完成或无需验证的IP例如第三方硬核、模拟模块等。在读取设计时Formality如果找不到这些子模块的定义就会报错。此时我们可以将这些模块声明为黑盒Black Box。set hdlin_unresolved_modules black_box这条命令是全局设置告诉Formality遇到任何无法解析的模块都自动将其视为黑盒。更常见的做法是在读入设计后使用set_black_box命令针对特定的模块进行设置这样更精确。黑盒内部的逻辑将被忽略只将其输入输出端口作为边界参与验证。注意将模块设为黑盒意味着放弃对其内部逻辑正确性的验证。务必确保黑盒模块的接口端口名、位宽、方向在参考设计和实现设计中完全一致否则会导致端口匹配失败进而影响整个验证流程。3. 核心流程拆解从读入设计到生成报告理解了关键变量后我们就可以按部就班地执行Formality的标准流程了。这个过程就像执行一个精心编排的剧本每一步都有其明确的目的和常见的“坑点”。3.1 灵魂向导SVF文件的作用与设置在RTL vs. Netlist的验证中有一个文件至关重要那就是SVFSetup Verification Format文件。它由逻辑综合工具如Design Compiler在综合过程中自动生成。你可以把SVF文件看作是综合工具写给Formality的一封“解释信”。信里详细记录了综合工具对原始RTL做了哪些优化和转换比如哪些寄存器被合并或复制了。哪些层次结构被展平Flatten了。哪些常数传播Constant Propagation和冗余逻辑消除发生了。插入了哪些扫描链Scan Chain或测试逻辑DFT Logic。如果没有这封“解释信”Formality就像一个看不懂魔术揭秘的观众它看到网表魔术结果和RTL魔术描述完全不同会报告大量不匹配和失败。而SVF文件里的guide命令就是一步步向Formality揭示魔术手法帮助它理解“这个网表中的奇怪结构其实对应的是RTL里的那个简单描述”。设置SVF文件的命令如下set svf_path ${RTLHOME}/${DESIGN}/synopsys_output set_svf -append ${svf_path}/my_design.svf-append选项用于当你有多个SVF文件时例如顶层和子模块分开综合将它们依次加载。从Design Compiler 2005.09版本开始工具在生成二进制SVF的同时也会默认生成一个文本格式的.svf.txt文件方便用户阅读。你也可以用report_guidance -to svf.txt命令手动生成文本报告这对于调试复杂的匹配问题非常有帮助。实操心得务必确保加载的SVF文件与当前要验证的网表版本严格对应。如果综合后你对网表做了任何手动修改ECO但SVF文件没有更新Formality的匹配结果很可能是错误的。一个常见的做法是在每次综合或重大网表修改后都重新生成并加载最新的SVF文件。3.2 读入与链接参考设计与实现设计Formality使用“容器”Container的概念来管理不同的设计视图。通常我们用r容器存放参考设计RTL或黄金网表用i容器存放实现设计待验证的网表。步骤一读入参考设计对于VHDL设计read_vhdl -container r -libname WORK [list file1.vhd file2.vhd]对于Verilog设计read_verilog -container r -libname WORK [list file1.v file2.v]-libname指定库名通常为WORK。-container r指明读入到参考容器。步骤二链接参考设计读入文件只是将代码加载到内存链接Link则是解析所有模块实例化建立完整的层次化设计。set_top r:/WORK/${DESIGN}这里r:/WORK/${DESIGN}指定了参考设计的顶层模块路径。如果链接失败通常会报出找不到某个子模块的定义这时就需要检查文件列表是否完整或者是否需要将某些模块设为黑盒。步骤三读入实现设计实现设计通常是综合后或布局布线后的门级网表Gate-level Netlist。read_verilog -container i -netlist ${NETLIST_PATH}/${DESIGN}_final.v关键选项-netlist告诉Formality这是网表文件工具会调用相应的库来解析标准单元和宏单元。步骤四链接实现设计set_top i:/WORK/${DESIGN}3.3 预处理处理测试与时钟门控逻辑在芯片设计中为了可测试性DFT网表中通常会插入扫描链Scan Chain这会在功能端口之外增加ScanEnable,ScanIn,ScanOut等测试信号。在功能等价性验证时我们需要屏蔽这些测试逻辑通常将ScanEnable信号设置为0功能模式并告诉Formality不要验证扫描输出端口。# 将参考和实现设计中的ScanEnable端口固定为0 set_constant -type port r:/WORK/${DESIGN}/ScanEnable 0 set_constant -type port i:/WORK/${DESIGN}/ScanEnable 0 # 设置不验证扫描输出端口 set_dont_verify_point r:/*/${DESIGN}/*ScanOut set_dont_verify_point i:/*/${DESIGN}/*ScanOutset_dont_verify_point命令告诉Formality忽略这些点不将它们纳入等价性比较的范围。这对于通过验证至关重要。3.4 匹配与验证见证结果的时刻在正式验证之前先进行匹配Match是一个好习惯。匹配阶段会尝试将两个设计中的比较点寄存器、端口等关联起来。match执行match命令后Formality会输出匹配报告。你应该重点关注“Unmatched points”的数量。如果存在大量未匹配的点直接进行verify很可能失败并且问题难以定位。此时应该先分析并解决这些不匹配。一个有用的命令是report_unmatched_points它可以列出所有未匹配的点。对于数据路径如乘法器、加法器可以使用-datapath选项来专门报告因为数据路径的优化往往比较激进是未匹配问题的重灾区。report_unmatched_points -datapath unmatched_datapath.rpt当匹配结果令人满意未匹配点数量很少且可以解释如新增的时钟门控单元后就可以进行最终的验证了。verifyverify命令会启动形式验证引擎进行严格的数学证明。验证完成后工具会返回一个成功或失败的状态。我们可以根据这个状态来决定后续操作。3.5 报告生成结果分析与归档无论验证通过与否生成详细的报告都是必须的。这些报告是调试和交付的重要依据。if { [verify] 1 } { echo “Formal Verification PASSED!” quit } else { echo “Formal Verification FAILED!” report_failing -verbose failing_points.rpt report_unmatched unmatched_points.rpt report_error_candidates error_candidates.rpt # 即使失败也生成匹配点报告用于对比分析 report_matched matched_points.rpt }report_failing: 列出所有验证失败的点这是调试的起点。-verbose选项会提供更详细的信息包括失败点的逻辑锥和可能的原因分析。report_unmatched: 再次确认未匹配的点。report_error_candidates: 工具会分析失败点给出一些可能出错的“候选”位置对于复杂问题的定位有提示作用。report_matched: 列出所有成功匹配的点在对比分析时有用。4. 高级调试技巧与常见问题实战Formality验证失败是家常便饭尤其是面对大型、复杂且经过深度优化的设计。能够快速定位并解决失败点是衡量一个工程师形式验证功力的关键。下面我结合几个典型案例分享一些实战调试技巧。4.1 典型失败场景与排查思路验证失败的报告通常会给出失败点的层次路径和类型。我们可以根据失败的特征采取不同的排查策略。场景一大量寄存器DFF不匹配或失败可能原因1时钟/复位信号未对齐。这是最常见的原因。检查参考设计和实现设计中时钟CLK和复位RST_n端口是否被正确识别和约束。确保你没有遗漏设置set_constant或set_case_analysis来固定某些控制信号的状态。排查命令:report_clock r: report_clock i: report_reset r: report_reset i:对比两个报告中时钟和复位的属性周期、边沿、是否门控是否一致。可能原因2verification_inversion_push设置不当。如前所述如果网表中寄存器使用了反相输出而此变量未设置为true会导致大量寄存器匹配失败。尝试打开此开关。可能原因3SVF文件不匹配或未加载。确认加载的SVF文件是否由生成当前网表的综合过程产生。可以尝试不使用SVF文件set_svf -disable运行一次匹配如果匹配点数量剧增说明SVF文件起到了关键作用但也可能包含了错误引导。需要检查SVF文件内容或综合脚本。场景二组合逻辑输出点失败可能原因1常数传播不一致。检查失败点相关的逻辑锥中是否有在参考设计中是常数但在实现设计中由于优化变成了非常数或者反之。使用report_constant命令查看两个设计中哪些信号被工具识别为常数。可能原因2黑盒接口不匹配。如果失败点位于黑盒模块的边界很可能是黑盒的端口位宽、方向或名字在两边不一致。仔细对比report_black_box的输出。可能原因3时序逻辑被优化为组合逻辑。某些情况下综合工具可能将一些简单的时序逻辑如电平敏感的锁存器优化掉了。这需要在参考设计端也做出相应处理或者使用set_dont_verify_point排除这些点。场景三签名分析Signature Analysis相关的失败当启用签名分析匹配了大量比较点后如果这些点验证失败调试会变得复杂因为传统的基于名称的追踪方法可能失效。策略暂时关闭签名分析 (set signature_analysis_match_compare_points false)重新运行匹配和验证。虽然未匹配点会变多但失败点可能会集中在少数几个有名称的逻辑单元上更容易定位根本原因。找到根本原因并修复后再重新开启签名分析。4.2 实用调试命令与信息获取除了生成报告Formality还提供了许多交互式命令用于深入探查设计内部。show_objects: 查看特定对象如寄存器、端口、线网的属性。show_objects -type port r:/WORK/TOP/input_areport_logic: 报告驱动某个信号的所有逻辑或者某个信号驱动的所有负载。这对于追踪信号路径、理解逻辑锥极其有用。report_logic -from r:/WORK/TOP/reg1/D -to r:/WORK/TOP/reg1/Q report_logic -fanin 3 i:/WORK/TOP/some_net ;# 报告某个网线的前3级逻辑锥write_do_lec: 这是一个“杀手锏”命令。当Formality遇到极其棘手、难以定位的失败点时可以使用此命令将失败点的逻辑锥导出为另一个等价性检查工具如Cadence Conformal LEC可读的格式。有时换一个工具视角问题可能豁然开朗。write_do_lec -failure -depth 5 -file difficult_case.lec4.3 ECO验证的特殊处理ECOEngineering Change Order验证是Formality的强项。通常流程是将修改前的网表作为参考设计r。将应用了ECO补丁的网表作为实现设计i。通常不需要SVF文件因为ECO改动很小且是直接对网表的手动修改。重点使用set_constant和set_case_analysis来固定ECO不影响的其他部分如扫描模式、功能模式选择信号将验证范围缩小到ECO影响的局部电路。匹配和验证。由于改动小匹配率应该接近100%验证速度也很快。一个ECO验证的典型命令片段可能是# 假设ECO只修改了模块SUB_MODULE_A中的逻辑 set_black_box r:/WORK/TOP/SUB_MODULE_B set_black_box i:/WORK/TOP/SUB_MODULE_B # 将设计置于功能模式 set_constant -type port r:/WORK/TOP/TestMode 0 set_constant -type port i:/WORK/TOP/TestMode 0 match verify通过将未修改的模块设为黑盒可以极大提升验证效率并聚焦于真正的改动点。5. 解读Formality日志与报告从信息到洞见运行Formality后控制台和日志文件会输出大量信息。学会快速解读这些信息是高效工作的关键。我们以一段典型的日志为例进行拆解*********************************** Matching Results *********************************** 4328 Compare points matched by name 0 Compare points matched by signature analysis 0 Compare points matched by topology 876 Matched primary inputs, black-box outputs 0(345) Unmatched reference(implementation) compare points 0(0) Unmatched reference(implementation) primary inputs, black-box outputs 7562(0) Unmatched reference(implementation) unread points ***********************************************************************************匹配结果摘要4328 Compare points matched by name: 通过名称匹配了4328个比较点主要是寄存器和端口。这是最理想、最主要的匹配方式。0 ... matched by signature analysis: 通过签名分析匹配了0个点。说明要么没开启该功能要么设计优化程度不高名称匹配已足够。876 Matched primary inputs, black-box outputs: 匹配了876个主要输入和黑盒输出。这是设计的边界。0(345) Unmatched reference(implementation) compare points:这是需要重点关注的数据括号外是参考设计中未匹配的点数0括号内是实现设计中未匹配的点数345。这意味着网表中有345个比较点很可能是寄存器在参考设计中找不到对应物。常见原因包括综合工具插入了参考设计中没有的寄存器如用于修复保持时间违例的缓冲寄存器、时钟门控寄存器、扫描链寄存器未被正确排除、或者SVF文件未能正确引导工具识别这些新增的寄存器。7562(0) Unmatched reference(implementation) unread points: 参考设计中有7562个“未读点”未匹配。这通常不是问题。“未读点”可能包括RTL中存在的中间变量wire、常量、或某些层次的实例它们在综合后被优化掉了没有体现在门级网表中。只要实现设计这边是0就说明网表中没有“多余”的逻辑这是好现象。接下来的验证结果报告更为关键--------------------------------------------------------------------------------------- Matched Compare Points BBPin Loop BBNet Cut Port DFF LAT TOTAL --------------------------------------------------------------------------------------- Passing (equivalent) 0 0 0 0 853 34 0 887 Failing (not equivalent) 0 0 0 0 2 198 0 200 Unverified 0 0 0 0 79 4932 0 5011 Not Compared Don‘t verify 0 0 0 0 64 0 0 64 ****************************************************************************************这个表格按类型统计了匹配点的验证状态Passing: 通过验证功能等价。这是我们追求的结果。这里有887个点。Failing: 验证失败功能不等价。必须全部解决这里有200个失败点其中198个是锁存器LAT2个是D触发器DFF。锁存器失败很常见因为锁存器在RTL中容易因编码风格问题隐含产生而综合工具对其处理方式多变容易导致不匹配。Unverified: 未验证的点。数量巨大5011个其中绝大部分4932个是锁存器。这些点之所以未验证很可能是因为它们没有被成功匹配参考前面的未匹配点统计。Formality只会对已匹配的点进行验证。Not Compared Don‘t verify: 被设置为不验证的点比如我们之前用set_dont_verify_point排除的扫描输出端口。这里的64个点符合预期。结论与行动从这个报告看主要问题是大量锁存器LAT未匹配且未验证并且有200个点主要是锁存器失败。调试重点应立即转向这些锁存器使用report_unmatched -type latch查看是哪些锁存器未匹配。检查RTL代码确认这些锁存器是否是设计意图。很多时候RTL中的不完全条件判断incomplete if-else 或 case 语句会综合出非预期的锁存器。如果锁存器是非预期的需要修改RTL代码消除锁存器。如果锁存器是设计意图如用于功耗门控则需要检查SVF文件是否有对应的guide_latch命令来引导匹配或者检查verification_clock_gate_hold_mode等变量设置是否正确。对于那2个失败的DFF需要用report_failing -verbose命令深入查看其逻辑锥定位具体是哪段逻辑不等价。通过这样层层递进地分析日志和报告就能将看似庞大的“失败”问题分解为一个个具体、可解决的子任务最终引导设计通过形式验证为芯片功能的正确性提供坚实的数学保障。这个过程虽然有时繁琐但比起动辄数周的仿真回归其效率优势是决定性的。
