做形式验证的朋友十有八九都被unmatched points折磨过。RTL和网表一比对满屏的unmatched第一反应是查约束、查综合脚本但很多时候问题出在一个不起眼的环节——SVF文件没有用好。SVFSetup Verification File是综合工具在优化过程中记录设计变换信息的文件Formality里有没有正确加载SVF直接决定了match阶段的匹配率也决定了verify阶段是干净利落还是陷入一堆假失败的泥潭。这篇东西主要想聊聊set_svf命令的实用玩法不光是命令语法还包括SVF文件本身是什么、为什么它能让Formality“开挂”、实际项目中怎么把这条命令用出效果。适合正在做逻辑综合、形式验证的工程师也适合刚接触Formality、被各种unmatched和fail搞到头疼的新手。我会尽量把底层逻辑和实操经验都讲到毕竟这玩意儿踩坑的人太多了。1. SVF文件到底是什么为什么它对Formality这么关键1.1 从综合优化说起没有SVF的Formality有多难先说一个最直观的场景。你用Design Compiler做综合RTL经过编译、优化、映射之后变成了门级网表。综合工具在这个过程中做了大量改变寄存器被合并、常量传播把某些逻辑直接优化掉、多级组合逻辑被重定时、命名规则被重新映射。这些变换在小设计里不明显到了几十万门、上百万门的设计网表和RTL之间的“距离”会非常大。Formality做的是形式验证本质上是数学意义上的等价性检查。它要把RTL和网表分别转换成布尔逻辑表示然后证明两个表示在功能上等价。这里有个关键问题如果Formality只能靠纯逻辑推理去匹配RTL里的信号和网表里的信号很多经过优化后被改了名字、被合并、甚至被消除的信号匹配起来就会非常困难甚至根本匹配不上。SVF就是为了解决这个问题出现的。它像是一份综合工具留下的“施工日志”详细记录了工具在综合过程中对设计做了哪些变换、原有信号映射到了哪里、哪些寄存器被优化合并了、哪些常量被传播了。Formality读入SVF之后就能沿着这份日志快速建立起RTL和网表之间的对应关系而不是在黑暗中摸索。1.2 SVF文件里到底记了些什么SVF文件不是简单的文本说明它是综合工具主要是Synopsys Design Compiler其他工具也有类似产物在运行过程中自动生成的二进制或文本格式文件。核心内容大致包括几个部分设计名称和版本信息、RTL信号到门级网表信号的映射关系、综合过程中被优化掉的寄存器信息、常量连接的传播信息、边界优化信息等。举个例子RTL里有一个信号a_reg综合时因为逻辑等价合并它在网表里可能被替换成了b_reg的部分逻辑甚至完全消失。如果没有SVFFormality在match阶段根本不知道a_reg和b_reg之间的对应关系只能去猜猜不到就成了unmatched point。有了SVFFormality直接读到“a_reg已经被合并到b_reg”匹配率瞬间提升。所以理解SVF的价值核心就一句话它把综合工具的“内部视角”分享给了Formality让验证工具不用从零开始猜测设计意图。1.3 没有SVF能验证吗能但你不会想这么做理论上不用SVF也能跑Formality。Formality有自己的一套匹配引擎可以基于信号名、结构相似性等方式做匹配。设计比较小、综合优化不激进的情况下即使没有SVF匹配率也能做得不错。但到了真实项目里综合优化通常非常激进各种retiming、datapath优化、寄存器合并下来纯靠Formality自己去匹配会非常痛苦。我见过最典型的情况是一个模块网表综合时没写出SVF文件Formality跑下来unmatched registers有几百个verify阶段报出一堆fail。排查到最后发现大部分fail是因为常数传播和寄存器合并导致的“假失败”——信号本身是等价的但Formality没有SVF的指导在两个设计之间建立了错误的关联。最后只能靠手工设置match策略、写一个个dofile去排除活活折腾了一整天。从那以后我在所有综合脚本里都把SVF输出列为必选项谁都不许省。2. set_svf命令核心用法语法、参数与适用场景2.1 命令标准语法和关键选项解析set_svf这条命令在Formality里是用来控制SVF文件读取和使用的核心命令。标准语法是这样的set_svf [-on|-off] [file_name] [-quiet] [-design design_list] [-replace]我实际用得最多的几个选项是-on启用SVF读取模式后面跟SVF文件路径-off关闭SVF模式通常在一个design的验证完成后清理环境用-quiet读取SVF时不打印详细加载信息批处理脚本里非常实用-design design_list指定只对某个或某几个design启用SVF适合multi-design的验证环境-replace替换当前已加载的SVF文件避免重复加载冲突比较常规的加载方式是这样set_svf -on -quiet ../syn/out/top.svf这条命令让Formality读取指定路径的SVF文件并在后续的match和verify流程中使用其中的映射信息。注意这里的路径建议写绝对路径因为Formality脚本经常会被各种source嵌套相对路径太容易出错了。2.2 SVF加载的时机和顺序到底有多重要很多人在Formality工程里习惯把set_svf和read_design、link等操作混在一起或者在整个流程的最后随便补一条这些都是不推荐的做法。SVF应该在read完参考设计和实现设计之后、正式执行match之前加载。原因在于Formality读取SVF时会把其中的映射信息绑定到当前已读入的设计对象上。如果设计还没读进来SVF加载会发生错误或者绑定时找不到对应对象如果match已经跑完了再加载SVF就来不及了因为匹配过程已经结束SVF的指导作用就发挥不出来了。我在标准化脚本里的顺序一直是这样的read_db 参考设计文件 read_verilog 网表文件 set_top design_name link set_svf -on -quiet /path/to/file.svf match verify这里set_svf夹在link和match之间是整个流程里唯一合理的位置。有些人会问set_svf能不能在link之前放能放但不建议因为link过程可能会改变design的内部结构一些SVF中的引用关系可能因此失效。稳妥起见link之后再加载SVF是最省心的。2.3 多个SVF文件并存时的处理策略真实项目里很少只有一个SVF文件。一个典型的大型SoC设计不同模块可能由不同的综合任务产生每个模块都有自己的SVF文件或者前端做了多次综合迭代生成了多个版本的SVF。set_svf命令的设计是“一次只加载一个SVF”多次调用会覆盖之前的设置。如果需要同时使用多个SVF就得用-design选项分别指定或者用-replace选项逐个加载。我在处理多层次设计时常用这样的写法set_svf -on -quiet ./mod_a.svf -design mod_a set_svf -on -quiet ./mod_b.svf -design mod_b set_svf -on -quiet ./top.svf -design top三条命令并行不冲突因为每个SVF被限定在了对应的design范围内。如果不加-design后面的命令会把前面的覆盖掉等到match的时候可能只加载到了最后一个SVF其他模块的映射信息全部丢失匹配率直接崩掉。3. 实战中的隐藏技巧set_svf怎么用效果最好3.1 综合脚本里就要把SVF写好别等验证时才救命set_svf命令虽然写在Formality脚本里但SVF文件本身的质量是综合阶段决定的。很多项目在综合脚本里没有显式写出SVF文件或者用了默认设置导致SVF内容不完整到了验证阶段再着急已经晚了。Design Compiler里控制SVF输出的命令同样叫set_svf只不过语义是“综合时写出一个SVF文件”。建议这样用set_svf -on -quiet ./results/${DESIGN_NAME}.svf # 后续综合流程... # 综合完成后关闭 set_svf -off这里有个容易被忽略的细节综合过程中如果做了多次compile、或者对设计做了增量修改SVF文件会被追加还是覆盖不同版本工具行为可能不同但稳妥的做法是在综合开始时先删除旧的SVF文件或者用固定命名保证每次综合从头生成。否则一个混入了旧版本信息的SVF文件比没有SVF还可怕它会给出错误的映射关系导致Formality在错误的路线上越走越远。3.2 小心“-quiet”参数批处理脚本里的双刃剑-quiet看起来只是一个减少日志输出的选项但在批处理环境里它有一个非常实际的作用避免日志文件爆炸。一个大型设计的SVF文件可能有几十MB甚至更大如果不加-quietFormality加载SVF时的详细日志会刷出几十万行日志文件暴涨不说还严重影响运行速度。但问题来了如果不打详细日志你根本看不到SVF加载是否成功。SVF文件版本不匹配、文件损坏、路径错误这些问题在-quiet模式下都可能被静默忽略Formality可能只是在日志里简单打一行warning然后继续以没有SVF的状态往下跑最后验证失败了你都不知道原因在哪里。所以我的做法是批处理脚本里保留-quiet但在set_svf之后单独打印一条确认信息并把关键检查命令加进去set_svf -on -quiet ./top.svf if { [file exists ./top.svf] } { puts SVF loaded successfully: ./top.svf } else { puts ERROR: SVF file not found! exit 1 }这样既避免日志爆炸又能在SVF缺失的第一时间发现不用等到match结束才回头排查。3.3 SVF和匹配模式的搭配选择set_svf加载成功之后Formality的match阶段会自动使用SVF中记录的映射关系做引导。但match策略远不止“有SVF就万事大吉”这么简单。Formality里有几个和SVF关联紧密的变量实际项目中我经常需要调整。最典型的两个是set_app_var svf_enable_high_speed_verification true set_app_var svf_enable_guidance truesvf_enable_high_speed_verification开启后Formality会利用SVF中的高位等价信息做快速验证跳过一些不必要的逻辑比对对运行时间和内存都有明显改善。svf_enable_guidance则让Formality在match阶段更积极地使用SVF提供的信息来建立名称匹配之外的逻辑对应。但这两个变量不是在任何情况下都值得开。如果设计本身存在较大的时序或结构差异过激的SVF引导反而可能让Formality忽略了一些必要的比对导致漏报。我的经验是先开默认设置跑一遍如果match率和verify结果都正常再尝试开启高速模式优化runtime如果结果有问题关掉高速选项用保守模式跑对比两者结果。3.4 层次化设计中的SVF管理思路大型设计的验证通常不是一次跑完整个顶层而是先对子模块做验证再逐级向上做层次化验证。这种流程里SVF的管理逻辑是每个层次验证时只需要加载当前层次对应综合任务产生的SVF而不是把整个设计的所有SVF全部堆在一起。举个例子验证子模块mod_a时只需要加载mod_a综合时生成的SVF到了顶层验证时顶层的SVF往往已经涵盖了整个设计的优化信息不需要再逐个子模块去加载。如果硬把所有SVF都加载进来反而可能在match阶段造成映射冲突因为顶层SVF和子模块SVF对某些信号的记录方式可能不一致。层次化验证中还有一个常见问题顶层Formality工程里read进去的网表可能是子模块综合后的netlist拼接而成而不是顶层综合的产物。这种情况下顶层SVF根本不存在或者不匹配。实际处理时应该针对每个子模块分别验证不要试图在顶层阶段用一个SVF覆盖所有逻辑。3.5 网表经过额外处理后SVF失效的应对方案综合完之后网表往往还要经过一系列处理插入扫描链scan insertion、DFT逻辑插入、甚至手工ECO。这些操作会改动网表结构而SVF文件记录的还是综合完成那一刻的映射信息两者之间就会出现偏差。这种情况下最稳妥的做法是关掉SVF让Formality走普通匹配模式。不要死脑筋非要加载一个已经过期的SVF那只会引入错误引导。我在实际项目中遇到过几次后端在网表里插了scan muxFormality带着旧SVF跑match结果把scan相关的信号错误地匹配到了功能信号上verify报出一堆莫名其妙的fail。关掉SVF之后match率确实降了一点但跑出来的结果反而是干净可信的。所以set_svf命令不只是“打开SVF”这么简单什么时候该开、什么时候该关本身就是一种经验判断。4. 常见问题与排查技巧实录4.1 SVF相关故障速查表下面把我在项目中遇到的SVF相关典型问题整理成了一张速查表方便大家遇到问题的时候快速定位问题现象根本原因解决方案set_svf时报file not found路径错误或SVF未生成检查综合脚本中set_svf输出是否成功确认文件实际路径match率正常但verify报大量failSVF版本和当前网表不匹配对比SVF生成时间和网表生成时间确认是否经过额外网表处理set_svf加载后unmatched反而更多SVF内容与设计不一致错误引导关闭SVF用普通匹配模式重跑对比结果SVF文件存在但加载失败综合工具版本和Formality版本不兼容检查工具版本兼容性表必要时用较低版本重新生成SVF日志文件异常巨大set_svf时未加-quiet选项确认加载模式批处理脚本中建议加-quiet并手动打印确认信息4.2 排查思路SVF相关fail的标准定位流程我自己排查SVF相关问题一般遵循一套固定的思路效率比较高。第一步永远是确认SVF文件本身的质量文件是否存在、生成时间是否合理、内容是否完整。这些信息不需要打开SVF文件二进制格式你也看不明白只需要用file命令确认文件类型用ls -l看文件大小和修改时间就行。第二步是跑一个最小复现单独建一个Formality工程只read相关的设计文件set_svf加载目标SVF然后直接match。这样可以把问题隔离在最小范围内避免其他脚本逻辑干扰。第三步是分析match报告。如果match报告显示有大量信号在“SVF guided”类别里匹配成功说明SVF确实在起作用如果这个类别的匹配数很低甚至为零说明SVF可能根本没被正确加载或没有包含有用的映射信息。第四步是看verify阶段的fail模式。如果fail全部集中在常数传播、寄存器合并相关的类型上那大概率还是SVF的指导不够完整如果fail散落在各种不同类型的逻辑上就要怀疑是SVF的信息本身就是错的或者是设计本身存在问题。4.3 我踩过的一个真实坑SVF路径检查的疏漏有次跑一个回归任务综合脚本正常运行SVF文件也生成了但在Formality里一直在报unmatched point超多。我排查了很久最后发现是综合脚本里输出SVF的路径和Formality脚本里读取的路径不一致——综合脚本用的是相对于综合目录的相对路径Formality脚本从另一个目录启动两个路径对不上set_svf实际加载的空气。这个问题的隐蔽之处在于Formality并没有报“file not found”错误因为我加了-quiet选项整个加载过程静默失败后续match继续跑只是匹配率奇差无比。那次之后我给自己定了个规矩所有跨脚本引用的文件路径一律用绝对路径或者从同一个环境变量拼出来不允许在脚本里再写相对路径。同时set_svf后面强烈建议加文件存在性检查哪怕只是简单的file exists判断。4.4 不同综合工具产物和Formality的兼容性处理不是所有综合工具都叫Design Compiler。有些项目中用了其他综合工具比如开源流程里的综合工具生成的验证信息文件格式和SVF格式有差异。这种情况下set_svf命令就行不通了Formality读取不了其他格式的映射文件。我遇到过几个开源综合流程的项目用户希望通过某种方式把综合工具的映射关系导入Formality。方案是有的但比较绕通常是把综合工具的映射信息转换成Formality支持的格式或者干脆放弃SVF指导依赖Formality自己的match引擎。后者在大多数设计上其实也能跑通只是效率差一些。如果你所在的项目组铁了心要用非Synopsys综合工具建议提前在测试模块上跑一遍Formality验证流程确认匹配率和验证时间在可接受范围内不要在项目后期才发现SVF的帮助没了整个验证效率崩盘。5. 规范化脚本示例与综合阶段的配套动作5.1 一个可复用的综合后Formality脚本模板这里给出一套我个人项目中常用的Formality脚本模板结构清晰适合直接套用# 设置设计信息 set DESIGN_NAME top set SVF_FILE /proj/${DESIGN_NAME}/syn/out/${DESIGN_NAME}.svf set RTL_FILE /proj/${DESIGN_NAME}/rtl/${DESIGN_NAME}.v set NETLIST_FILE /proj/${DESIGN_NAME}/syn/out/${DESIGN_NAME}.vg # 读入设计 read_db ${RTL_FILE} read_verilog ${NETLIST_FILE} set_top ${DESIGN_NAME} link # 加载SVF文件 if { [file exists ${SVF_FILE}] } { set_svf -on -quiet ${SVF_FILE} puts SVF loaded: ${SVF_FILE} } else { puts WARNING: SVF file not found, running without SVF! } # 匹配与验证 match report_unmatched_points ./reports/unmatched_points.txt verify report_failing_points ./reports/failing_points.txt这个脚本的优点在于SVF加载前做了文件存在性检查缺失时不会静默失败而是在日志中明确打印警告。实际项目里可以根据需要扩展report的粒度但核心流程逻辑就是这样。5.2 综合脚本端配合set_svf输出的最佳实践Formality侧的set_svf命令再好用也架不住综合侧压根没生成SVF文件。所以在综合脚本里同样要配套做SVF输出的管理。Design Compiler里的set_svf命令用法如下set_svf -off file delete -force ./out/${DESIGN_NAME}.svf set_svf -on -quiet ./out/${DESIGN_NAME}.svf # 这里执行compile等综合流程 set_svf -off第一行先关掉SVF模式是为了清掉之前可能残留的设置第二行删除旧文件是为了防止追加内容的隐患第三行重新开启SVF输出指定文件路径。综合完成后再执行set_svf -off确保文件被正常关闭、写入完整。有一个细节值得注意SVF文件在综合过程中是实时写入还是结束时统一写入不同工具处理方式不完全一样。为了保证文件完整性建议在综合脚本的最后显式执行set_svf -off而不要依赖进程退出时自动关闭。否则万一综合过程被异常中断SVF文件可能停留在未完成状态后续加载时会报文件格式错误或者加载不完整。6. 一些实际操作中的个人体会与细节补充最后再聊点碎碎念。SVF文件和set_svf命令在整个Formality验证流程里看起来很不起眼但它的影响面其实非常广。它直接决定了match阶段的匹配质量而match质量又直接决定了verify阶段有多少fail需要人肉排查。一个设计如果SVF正确加载match率可能轻松做到99%以上verify阶段干干净净如果SVF出了问题哪怕只是版本过旧或路径错误整个验证过程就变成了在一堆假失败里找真问题的噩梦。我个人的建议是把“SVF是否完整、是否匹配、是否正确加载”纳入每次Formality验证开始前的常规检查项和检查约束文件、检查设计文件一样重要。尤其是跑批处理回归和自动化流程的朋友SVF检查的自动化一定要做进去别省那几行代码。还要强调一点set_svf不是万能的。它只是一个工具提供的是综合工具的优化信息它不能替代良好的match策略和验证方法学。有些设计即使SVF加载正确match阶段仍然会有unmatched points这时候需要结合具体情况分析原因——可能是设计本身的问题也可能是综合约束设置不当导致的。不要遇到匹配问题就一味地去折腾SVF花点时间理解设计、理解综合过程反而能更快地找到问题根源。如果某个设计在SVF正确加载后还是反复出问题我建议你把Formality的report文件和综合工具的log文件对照着看用工具日志里的警告信息做线索很多问题都能顺藤摸瓜查明白。毕竟SVF只是桥梁桥梁两端的工程质量和理解深度才是决定验证效率的根本。
Formality中set_svf命令实战：SVF文件加载技巧与常见问题排查
做形式验证的朋友十有八九都被unmatched points折磨过。RTL和网表一比对满屏的unmatched第一反应是查约束、查综合脚本但很多时候问题出在一个不起眼的环节——SVF文件没有用好。SVFSetup Verification File是综合工具在优化过程中记录设计变换信息的文件Formality里有没有正确加载SVF直接决定了match阶段的匹配率也决定了verify阶段是干净利落还是陷入一堆假失败的泥潭。这篇东西主要想聊聊set_svf命令的实用玩法不光是命令语法还包括SVF文件本身是什么、为什么它能让Formality“开挂”、实际项目中怎么把这条命令用出效果。适合正在做逻辑综合、形式验证的工程师也适合刚接触Formality、被各种unmatched和fail搞到头疼的新手。我会尽量把底层逻辑和实操经验都讲到毕竟这玩意儿踩坑的人太多了。1. SVF文件到底是什么为什么它对Formality这么关键1.1 从综合优化说起没有SVF的Formality有多难先说一个最直观的场景。你用Design Compiler做综合RTL经过编译、优化、映射之后变成了门级网表。综合工具在这个过程中做了大量改变寄存器被合并、常量传播把某些逻辑直接优化掉、多级组合逻辑被重定时、命名规则被重新映射。这些变换在小设计里不明显到了几十万门、上百万门的设计网表和RTL之间的“距离”会非常大。Formality做的是形式验证本质上是数学意义上的等价性检查。它要把RTL和网表分别转换成布尔逻辑表示然后证明两个表示在功能上等价。这里有个关键问题如果Formality只能靠纯逻辑推理去匹配RTL里的信号和网表里的信号很多经过优化后被改了名字、被合并、甚至被消除的信号匹配起来就会非常困难甚至根本匹配不上。SVF就是为了解决这个问题出现的。它像是一份综合工具留下的“施工日志”详细记录了工具在综合过程中对设计做了哪些变换、原有信号映射到了哪里、哪些寄存器被优化合并了、哪些常量被传播了。Formality读入SVF之后就能沿着这份日志快速建立起RTL和网表之间的对应关系而不是在黑暗中摸索。1.2 SVF文件里到底记了些什么SVF文件不是简单的文本说明它是综合工具主要是Synopsys Design Compiler其他工具也有类似产物在运行过程中自动生成的二进制或文本格式文件。核心内容大致包括几个部分设计名称和版本信息、RTL信号到门级网表信号的映射关系、综合过程中被优化掉的寄存器信息、常量连接的传播信息、边界优化信息等。举个例子RTL里有一个信号a_reg综合时因为逻辑等价合并它在网表里可能被替换成了b_reg的部分逻辑甚至完全消失。如果没有SVFFormality在match阶段根本不知道a_reg和b_reg之间的对应关系只能去猜猜不到就成了unmatched point。有了SVFFormality直接读到“a_reg已经被合并到b_reg”匹配率瞬间提升。所以理解SVF的价值核心就一句话它把综合工具的“内部视角”分享给了Formality让验证工具不用从零开始猜测设计意图。1.3 没有SVF能验证吗能但你不会想这么做理论上不用SVF也能跑Formality。Formality有自己的一套匹配引擎可以基于信号名、结构相似性等方式做匹配。设计比较小、综合优化不激进的情况下即使没有SVF匹配率也能做得不错。但到了真实项目里综合优化通常非常激进各种retiming、datapath优化、寄存器合并下来纯靠Formality自己去匹配会非常痛苦。我见过最典型的情况是一个模块网表综合时没写出SVF文件Formality跑下来unmatched registers有几百个verify阶段报出一堆fail。排查到最后发现大部分fail是因为常数传播和寄存器合并导致的“假失败”——信号本身是等价的但Formality没有SVF的指导在两个设计之间建立了错误的关联。最后只能靠手工设置match策略、写一个个dofile去排除活活折腾了一整天。从那以后我在所有综合脚本里都把SVF输出列为必选项谁都不许省。2. set_svf命令核心用法语法、参数与适用场景2.1 命令标准语法和关键选项解析set_svf这条命令在Formality里是用来控制SVF文件读取和使用的核心命令。标准语法是这样的set_svf [-on|-off] [file_name] [-quiet] [-design design_list] [-replace]我实际用得最多的几个选项是-on启用SVF读取模式后面跟SVF文件路径-off关闭SVF模式通常在一个design的验证完成后清理环境用-quiet读取SVF时不打印详细加载信息批处理脚本里非常实用-design design_list指定只对某个或某几个design启用SVF适合multi-design的验证环境-replace替换当前已加载的SVF文件避免重复加载冲突比较常规的加载方式是这样set_svf -on -quiet ../syn/out/top.svf这条命令让Formality读取指定路径的SVF文件并在后续的match和verify流程中使用其中的映射信息。注意这里的路径建议写绝对路径因为Formality脚本经常会被各种source嵌套相对路径太容易出错了。2.2 SVF加载的时机和顺序到底有多重要很多人在Formality工程里习惯把set_svf和read_design、link等操作混在一起或者在整个流程的最后随便补一条这些都是不推荐的做法。SVF应该在read完参考设计和实现设计之后、正式执行match之前加载。原因在于Formality读取SVF时会把其中的映射信息绑定到当前已读入的设计对象上。如果设计还没读进来SVF加载会发生错误或者绑定时找不到对应对象如果match已经跑完了再加载SVF就来不及了因为匹配过程已经结束SVF的指导作用就发挥不出来了。我在标准化脚本里的顺序一直是这样的read_db 参考设计文件 read_verilog 网表文件 set_top design_name link set_svf -on -quiet /path/to/file.svf match verify这里set_svf夹在link和match之间是整个流程里唯一合理的位置。有些人会问set_svf能不能在link之前放能放但不建议因为link过程可能会改变design的内部结构一些SVF中的引用关系可能因此失效。稳妥起见link之后再加载SVF是最省心的。2.3 多个SVF文件并存时的处理策略真实项目里很少只有一个SVF文件。一个典型的大型SoC设计不同模块可能由不同的综合任务产生每个模块都有自己的SVF文件或者前端做了多次综合迭代生成了多个版本的SVF。set_svf命令的设计是“一次只加载一个SVF”多次调用会覆盖之前的设置。如果需要同时使用多个SVF就得用-design选项分别指定或者用-replace选项逐个加载。我在处理多层次设计时常用这样的写法set_svf -on -quiet ./mod_a.svf -design mod_a set_svf -on -quiet ./mod_b.svf -design mod_b set_svf -on -quiet ./top.svf -design top三条命令并行不冲突因为每个SVF被限定在了对应的design范围内。如果不加-design后面的命令会把前面的覆盖掉等到match的时候可能只加载到了最后一个SVF其他模块的映射信息全部丢失匹配率直接崩掉。3. 实战中的隐藏技巧set_svf怎么用效果最好3.1 综合脚本里就要把SVF写好别等验证时才救命set_svf命令虽然写在Formality脚本里但SVF文件本身的质量是综合阶段决定的。很多项目在综合脚本里没有显式写出SVF文件或者用了默认设置导致SVF内容不完整到了验证阶段再着急已经晚了。Design Compiler里控制SVF输出的命令同样叫set_svf只不过语义是“综合时写出一个SVF文件”。建议这样用set_svf -on -quiet ./results/${DESIGN_NAME}.svf # 后续综合流程... # 综合完成后关闭 set_svf -off这里有个容易被忽略的细节综合过程中如果做了多次compile、或者对设计做了增量修改SVF文件会被追加还是覆盖不同版本工具行为可能不同但稳妥的做法是在综合开始时先删除旧的SVF文件或者用固定命名保证每次综合从头生成。否则一个混入了旧版本信息的SVF文件比没有SVF还可怕它会给出错误的映射关系导致Formality在错误的路线上越走越远。3.2 小心“-quiet”参数批处理脚本里的双刃剑-quiet看起来只是一个减少日志输出的选项但在批处理环境里它有一个非常实际的作用避免日志文件爆炸。一个大型设计的SVF文件可能有几十MB甚至更大如果不加-quietFormality加载SVF时的详细日志会刷出几十万行日志文件暴涨不说还严重影响运行速度。但问题来了如果不打详细日志你根本看不到SVF加载是否成功。SVF文件版本不匹配、文件损坏、路径错误这些问题在-quiet模式下都可能被静默忽略Formality可能只是在日志里简单打一行warning然后继续以没有SVF的状态往下跑最后验证失败了你都不知道原因在哪里。所以我的做法是批处理脚本里保留-quiet但在set_svf之后单独打印一条确认信息并把关键检查命令加进去set_svf -on -quiet ./top.svf if { [file exists ./top.svf] } { puts SVF loaded successfully: ./top.svf } else { puts ERROR: SVF file not found! exit 1 }这样既避免日志爆炸又能在SVF缺失的第一时间发现不用等到match结束才回头排查。3.3 SVF和匹配模式的搭配选择set_svf加载成功之后Formality的match阶段会自动使用SVF中记录的映射关系做引导。但match策略远不止“有SVF就万事大吉”这么简单。Formality里有几个和SVF关联紧密的变量实际项目中我经常需要调整。最典型的两个是set_app_var svf_enable_high_speed_verification true set_app_var svf_enable_guidance truesvf_enable_high_speed_verification开启后Formality会利用SVF中的高位等价信息做快速验证跳过一些不必要的逻辑比对对运行时间和内存都有明显改善。svf_enable_guidance则让Formality在match阶段更积极地使用SVF提供的信息来建立名称匹配之外的逻辑对应。但这两个变量不是在任何情况下都值得开。如果设计本身存在较大的时序或结构差异过激的SVF引导反而可能让Formality忽略了一些必要的比对导致漏报。我的经验是先开默认设置跑一遍如果match率和verify结果都正常再尝试开启高速模式优化runtime如果结果有问题关掉高速选项用保守模式跑对比两者结果。3.4 层次化设计中的SVF管理思路大型设计的验证通常不是一次跑完整个顶层而是先对子模块做验证再逐级向上做层次化验证。这种流程里SVF的管理逻辑是每个层次验证时只需要加载当前层次对应综合任务产生的SVF而不是把整个设计的所有SVF全部堆在一起。举个例子验证子模块mod_a时只需要加载mod_a综合时生成的SVF到了顶层验证时顶层的SVF往往已经涵盖了整个设计的优化信息不需要再逐个子模块去加载。如果硬把所有SVF都加载进来反而可能在match阶段造成映射冲突因为顶层SVF和子模块SVF对某些信号的记录方式可能不一致。层次化验证中还有一个常见问题顶层Formality工程里read进去的网表可能是子模块综合后的netlist拼接而成而不是顶层综合的产物。这种情况下顶层SVF根本不存在或者不匹配。实际处理时应该针对每个子模块分别验证不要试图在顶层阶段用一个SVF覆盖所有逻辑。3.5 网表经过额外处理后SVF失效的应对方案综合完之后网表往往还要经过一系列处理插入扫描链scan insertion、DFT逻辑插入、甚至手工ECO。这些操作会改动网表结构而SVF文件记录的还是综合完成那一刻的映射信息两者之间就会出现偏差。这种情况下最稳妥的做法是关掉SVF让Formality走普通匹配模式。不要死脑筋非要加载一个已经过期的SVF那只会引入错误引导。我在实际项目中遇到过几次后端在网表里插了scan muxFormality带着旧SVF跑match结果把scan相关的信号错误地匹配到了功能信号上verify报出一堆莫名其妙的fail。关掉SVF之后match率确实降了一点但跑出来的结果反而是干净可信的。所以set_svf命令不只是“打开SVF”这么简单什么时候该开、什么时候该关本身就是一种经验判断。4. 常见问题与排查技巧实录4.1 SVF相关故障速查表下面把我在项目中遇到的SVF相关典型问题整理成了一张速查表方便大家遇到问题的时候快速定位问题现象根本原因解决方案set_svf时报file not found路径错误或SVF未生成检查综合脚本中set_svf输出是否成功确认文件实际路径match率正常但verify报大量failSVF版本和当前网表不匹配对比SVF生成时间和网表生成时间确认是否经过额外网表处理set_svf加载后unmatched反而更多SVF内容与设计不一致错误引导关闭SVF用普通匹配模式重跑对比结果SVF文件存在但加载失败综合工具版本和Formality版本不兼容检查工具版本兼容性表必要时用较低版本重新生成SVF日志文件异常巨大set_svf时未加-quiet选项确认加载模式批处理脚本中建议加-quiet并手动打印确认信息4.2 排查思路SVF相关fail的标准定位流程我自己排查SVF相关问题一般遵循一套固定的思路效率比较高。第一步永远是确认SVF文件本身的质量文件是否存在、生成时间是否合理、内容是否完整。这些信息不需要打开SVF文件二进制格式你也看不明白只需要用file命令确认文件类型用ls -l看文件大小和修改时间就行。第二步是跑一个最小复现单独建一个Formality工程只read相关的设计文件set_svf加载目标SVF然后直接match。这样可以把问题隔离在最小范围内避免其他脚本逻辑干扰。第三步是分析match报告。如果match报告显示有大量信号在“SVF guided”类别里匹配成功说明SVF确实在起作用如果这个类别的匹配数很低甚至为零说明SVF可能根本没被正确加载或没有包含有用的映射信息。第四步是看verify阶段的fail模式。如果fail全部集中在常数传播、寄存器合并相关的类型上那大概率还是SVF的指导不够完整如果fail散落在各种不同类型的逻辑上就要怀疑是SVF的信息本身就是错的或者是设计本身存在问题。4.3 我踩过的一个真实坑SVF路径检查的疏漏有次跑一个回归任务综合脚本正常运行SVF文件也生成了但在Formality里一直在报unmatched point超多。我排查了很久最后发现是综合脚本里输出SVF的路径和Formality脚本里读取的路径不一致——综合脚本用的是相对于综合目录的相对路径Formality脚本从另一个目录启动两个路径对不上set_svf实际加载的空气。这个问题的隐蔽之处在于Formality并没有报“file not found”错误因为我加了-quiet选项整个加载过程静默失败后续match继续跑只是匹配率奇差无比。那次之后我给自己定了个规矩所有跨脚本引用的文件路径一律用绝对路径或者从同一个环境变量拼出来不允许在脚本里再写相对路径。同时set_svf后面强烈建议加文件存在性检查哪怕只是简单的file exists判断。4.4 不同综合工具产物和Formality的兼容性处理不是所有综合工具都叫Design Compiler。有些项目中用了其他综合工具比如开源流程里的综合工具生成的验证信息文件格式和SVF格式有差异。这种情况下set_svf命令就行不通了Formality读取不了其他格式的映射文件。我遇到过几个开源综合流程的项目用户希望通过某种方式把综合工具的映射关系导入Formality。方案是有的但比较绕通常是把综合工具的映射信息转换成Formality支持的格式或者干脆放弃SVF指导依赖Formality自己的match引擎。后者在大多数设计上其实也能跑通只是效率差一些。如果你所在的项目组铁了心要用非Synopsys综合工具建议提前在测试模块上跑一遍Formality验证流程确认匹配率和验证时间在可接受范围内不要在项目后期才发现SVF的帮助没了整个验证效率崩盘。5. 规范化脚本示例与综合阶段的配套动作5.1 一个可复用的综合后Formality脚本模板这里给出一套我个人项目中常用的Formality脚本模板结构清晰适合直接套用# 设置设计信息 set DESIGN_NAME top set SVF_FILE /proj/${DESIGN_NAME}/syn/out/${DESIGN_NAME}.svf set RTL_FILE /proj/${DESIGN_NAME}/rtl/${DESIGN_NAME}.v set NETLIST_FILE /proj/${DESIGN_NAME}/syn/out/${DESIGN_NAME}.vg # 读入设计 read_db ${RTL_FILE} read_verilog ${NETLIST_FILE} set_top ${DESIGN_NAME} link # 加载SVF文件 if { [file exists ${SVF_FILE}] } { set_svf -on -quiet ${SVF_FILE} puts SVF loaded: ${SVF_FILE} } else { puts WARNING: SVF file not found, running without SVF! } # 匹配与验证 match report_unmatched_points ./reports/unmatched_points.txt verify report_failing_points ./reports/failing_points.txt这个脚本的优点在于SVF加载前做了文件存在性检查缺失时不会静默失败而是在日志中明确打印警告。实际项目里可以根据需要扩展report的粒度但核心流程逻辑就是这样。5.2 综合脚本端配合set_svf输出的最佳实践Formality侧的set_svf命令再好用也架不住综合侧压根没生成SVF文件。所以在综合脚本里同样要配套做SVF输出的管理。Design Compiler里的set_svf命令用法如下set_svf -off file delete -force ./out/${DESIGN_NAME}.svf set_svf -on -quiet ./out/${DESIGN_NAME}.svf # 这里执行compile等综合流程 set_svf -off第一行先关掉SVF模式是为了清掉之前可能残留的设置第二行删除旧文件是为了防止追加内容的隐患第三行重新开启SVF输出指定文件路径。综合完成后再执行set_svf -off确保文件被正常关闭、写入完整。有一个细节值得注意SVF文件在综合过程中是实时写入还是结束时统一写入不同工具处理方式不完全一样。为了保证文件完整性建议在综合脚本的最后显式执行set_svf -off而不要依赖进程退出时自动关闭。否则万一综合过程被异常中断SVF文件可能停留在未完成状态后续加载时会报文件格式错误或者加载不完整。6. 一些实际操作中的个人体会与细节补充最后再聊点碎碎念。SVF文件和set_svf命令在整个Formality验证流程里看起来很不起眼但它的影响面其实非常广。它直接决定了match阶段的匹配质量而match质量又直接决定了verify阶段有多少fail需要人肉排查。一个设计如果SVF正确加载match率可能轻松做到99%以上verify阶段干干净净如果SVF出了问题哪怕只是版本过旧或路径错误整个验证过程就变成了在一堆假失败里找真问题的噩梦。我个人的建议是把“SVF是否完整、是否匹配、是否正确加载”纳入每次Formality验证开始前的常规检查项和检查约束文件、检查设计文件一样重要。尤其是跑批处理回归和自动化流程的朋友SVF检查的自动化一定要做进去别省那几行代码。还要强调一点set_svf不是万能的。它只是一个工具提供的是综合工具的优化信息它不能替代良好的match策略和验证方法学。有些设计即使SVF加载正确match阶段仍然会有unmatched points这时候需要结合具体情况分析原因——可能是设计本身的问题也可能是综合约束设置不当导致的。不要遇到匹配问题就一味地去折腾SVF花点时间理解设计、理解综合过程反而能更快地找到问题根源。如果某个设计在SVF正确加载后还是反复出问题我建议你把Formality的report文件和综合工具的log文件对照着看用工具日志里的警告信息做线索很多问题都能顺藤摸瓜查明白。毕竟SVF只是桥梁桥梁两端的工程质量和理解深度才是决定验证效率的根本。
