Formality常值mismatch排查指南：从综合优化到setup引导

1. 当formality卡在"几个常值"上：先搞清楚它在报什么

做形式验证的同行大概都遇到过这种场景：RTL改完，跑formality做等价性检查，结果一上来就报出一堆不匹配的点，而且这些点往往集中在几个看起来"人畜无害"的常值信号上——比如某个配置寄存器、某个模式选择位、某个复位后固定为0或1的控制信号。你盯着波形看了半天，觉得两边逻辑明明一样，工具就是不认。这种时候最容易犯的错就是直接去改脚本、加setup、甚至怀疑工具版本，结果越调越乱。

这篇内容就是围绕"几个常值问题导致formality失败"这个具体场景展开的。它属于数字前端验证里非常典型的一类debug工作：参考设计（reference）和实现设计（implementation）在综合、优化、或者手工改动之后，某些信号被常量传播、被tie到固定电平、或者被优化掉，导致formality在比对点上找不到对应关系，从而报fail。适合正在做逻辑等价性检查（LEC）的验证工程师、综合后做netlist比对的后端同学，以及需要接手别人综合脚本、面对一堆mismatch点无从下手的读者。我会把常值问题的几种典型成因、定位链路、以及我实际踩过的坑拆开讲，尽量让你下次遇到同类报错时能少绕两小时。

先说清楚一个前提：formality的比对逻辑是建立在"比对点（compare point）"上的，工具会把参考设计和实现设计里的寄存器、输出端口等关键节点配对，然后证明两边在相同输入激励下输出一致。一旦某个信号在实现侧被常量替换，工具要么找不到配对点，要么在证明时发现两边对该常量的依赖关系不同，于是报出unmatched或者failing。常值问题之所以烦人，是因为它不像功能性bug那样有明显的逻辑错误，它更像是"结构被改了但语义没变"，工具却因为结构差异而拒绝通过。理解这一点，后面的排查才有方向。

2. 常值问题的四种典型来源：从综合优化到手工改动

在动手debug之前，得先知道常值是从哪儿冒出来的。我梳理下来，实际项目里导致formality因常值失败的情况基本集中在四类，每一类的处理思路都不一样，混在一起查只会越查越乱。

2.1 综合工具的常量传播与死逻辑消除

这是最常见的一类。综合工具在做优化时，会把那些被常量驱动的逻辑直接折叠掉。举个典型例子：某个模块有一个cfg_mode输入，在顶层被tie成2'b00，综合工具看到这个连接关系后，会把模块内部所有依赖cfg_mode的分支全部按2'b00展开，其他分支的逻辑直接被删掉。结果就是实现设计里这个模块的很多寄存器消失了，或者被替换成常量输出。formality拿参考设计去比对时，发现参考侧还有一堆寄存器，实现侧已经没了，于是报unmatched。

这类问题的关键在于：语义上确实等价，但结构上不对应。工具不是不理解常量传播，而是它需要你明确告诉它"这些点允许被常量替换"。很多人第一反应是去查是不是综合脚本写错了，其实脚本没错，错的是没有在formality的setup里做相应的常量引导。

2.2 手写RTL里的参数化分支被展开

第二类来自RTL本身的参数化写法。比如一个模块用parameter WIDTH = 8，在例化时传了WIDTH = 1，那么模块内部所有按8位宽写的逻辑在综合后都会按1位宽重新展开，很多高位逻辑直接变成常量0。这种情况在参考设计和实现设计用的是同一份RTL时通常不会出问题，但如果是拿综合后的netlist去和RTL比，或者两边例化参数不一致，就会冒出大量常值mismatch。

我遇到过一回，参考侧用的是参数化RTL，实现侧是别人手工改过的netlist，改的人把某个DEPTH参数从16改成了8，理由是"上层只用得到8"。功能上确实只用8，但formality不知道这个约定，它看到参考侧还有16深度的地址译码逻辑，实现侧只剩8，直接报一片fail。这种问题的根子不在工具，在于两边的设计意图没有对齐。

2.3 复位逻辑与tie-off处理的差异

复位相关的常值问题特别隐蔽。典型场景是：参考设计里某个寄存器有异步复位，复位值是1'b0；实现设计里综合工具判断这个寄存器在复位后永远保持0（因为它的D端被常量驱动），于是把它优化成了一个常量0的wire。formality在比对时，参考侧是个带复位的寄存器，实现侧是个常量，工具会认为两者在复位释放后的行为可能不同，从而报fail。

还有一种情况是tie-off的处理。有些设计会把不用的输入端口tie到固定电平，参考侧可能保留了这个端口并接了常量，实现侧综合时直接把整个端口相关的逻辑删了。这时候formality会报端口unmatched，或者报依赖该端口的内部节点failing。这类问题的排查难点在于，你从波形上根本看不出差异，因为两边在功能上确实一样，差异纯粹在结构层面。

2.4 黑盒与don't-care处理引入的常量假设

最后一类来自黑盒（black box）和don't-care的处理。当某个子模块在formality里被设为black box时，工具会对它的输出做自由变量处理，但如果这个黑盒的输出在实现侧被常量驱动，就会产生矛盾。另外，don't-care条件如果在两边设置不一致，工具可能会在某些输入组合下把输出当成常量来优化，导致比对时出现本不该有的mismatch。

这四类来源有个共同点：它们都不是"逻辑写错了"，而是"结构信息丢失或不对齐"。所以debug的核心不是去改逻辑，而是去补全工具需要的结构引导信息。下面我就按实际排查的顺序，把这套链路拆开讲。

3. 从报错信息反推：定位常值mismatch的完整排查链路

很多人拿到formality的报错日志，第一反应是看failing points列表，然后逐个点进去看。这个做法在功能bug场景下没问题，但在常值问题场景下效率很低，因为常值导致的fail往往是成片出现的，逐个看会淹没在噪声里。我习惯的排查顺序是：先看unmatched的类型分布，再看failing点的驱动来源，最后才落到具体信号。

3.1 第一步：区分unmatched和failing，别混为一谈

formality的报错大致分两类：unmatched points和failing points。unmatched是指工具在两边找不到配对的比对点，failing是指配对了但证明不通过。常值问题在这两类里都会出现，但含义完全不同。

如果大量unmatched集中在寄存器上，大概率是实现侧这些寄存器被常量传播删掉了，属于2.1和2.2类问题。如果unmatched集中在输出端口上，可能是tie-off导致的端口消失，属于2.3类。如果failing点集中在某些依赖常量的组合逻辑输出上，那更可能是don't-care或black box处理不一致，属于2.4类。

我一般会先在日志里搜Unmatched points这个段落，看它的统计摘要。formality通常会按类型分组，比如Unmatched input ports、Unmatched output ports、Unmatched registers。这个分组信息比逐个点进去看有用得多，它能直接告诉你问题的大方向。比如你看到Unmatched registers有几十个，而Unmatched output ports是0，那基本可以排除tie-off问题，重点查常量传播。

3.2 第二步：用report_unmatched_points看驱动来源

确定了大致方向后，下一步是看这些unmatched点的驱动来源。formality提供了report_unmatched_points命令，可以列出每个unmatched点的详细信息，包括它在参考侧和实现侧的驱动逻辑。我通常会把输出重定向到文件，然后重点看两类信息：一是参考侧该点的fan-in里有没有常量，二是实现侧该点是不是被直接tie到了0或1。

这里有个实操细节：report_unmatched_points的输出默认可能比较简略，建议加上-verbose选项，这样能看到每个点的完整驱动树。如果某个unmatched寄存器在参考侧的D端是一个多路选择器，而实现侧该寄存器根本不存在，那基本可以确认是被常量传播折叠了。这时候要做的不是去恢复寄存器，而是去formality的setup里加常量引导，告诉工具"这个寄存器的值在实现侧是已知常量，允许它被优化"。

3.3 第三步：交叉比对综合日志里的常量传播记录

formality的报错只是结果，真正的线索在综合工具的日志里。大多数综合工具在做常量传播和死逻辑消除时，会在日志里记录被优化的对象。我习惯在跑formality之前，先把综合日志里跟constant propagation、dead logic、tie-off相关的段落grep出来，存成一个参考文件。

当formality报某个寄存器unmatched时，我去这个参考文件里搜该寄存器的名字，如果能找到"被常量传播消除"的记录，那就直接确认了成因，不用再猜。这个做法能省掉大量在formality里反复试探的时间。需要注意的是，综合日志里的信号名可能是优化后的名字，跟RTL名不一定完全一致，所以搜索时要用模糊匹配，或者先查name mapping文件。

3.4 第四步：用波形或网表确认常量的实际取值

最后一步是确认常量的实际取值。有时候formality报mismatch，不是因为常量传播本身有问题，而是因为两边的常量取值不一致。比如参考侧某个配置位默认是0，实现侧被tie成了1，这种差异在功能上可能是bug，也可能是设计意图变更，但formality不管这些，它只认等价性。

确认取值的方法有两个：一是看综合后的网表，直接搜该信号的assign语句；二是如果有仿真环境，跑一个短仿真看该信号的实际值。我一般优先看网表，因为快。如果网表里该信号是assign sig = 1'b0;，而参考侧RTL里它复位后是1，那问题就清楚了——要么是tie错了，要么是设计变更没同步到参考侧。

这条排查链路走下来，大部分常值问题都能定位到具体成因。但定位只是第一步，真正花时间的是怎么让formality接受这个差异。下面讲具体的处理手段。

4. 让formality接受常值差异：setup引导与验证策略

定位到常值成因之后，处理思路分两个方向：如果常量差异是设计意图内的（比如综合优化导致的合法折叠），那就通过formality的setup引导让工具接受；如果常量差异是意外的（比如tie错了、参数传错了），那就得回去改设计或改脚本。这一节重点讲前者的处理手段，因为后者属于常规bug修复，不在常值debug的范畴内。

4.1 用set_constant引导常量传播的比对

formality提供了set_constant命令，用来告诉工具某个信号在比对时应该被当作常量处理。这个命令的典型用法是：当实现侧某个信号被tie成常量，而参考侧还是变量时，用set_constant在参考侧也把这个信号约束成相同常量，这样两边的比对基准就对齐了。

具体操作上，我通常会在formality的setup脚本里加这样一段：

# 将参考侧的配置信号约束为与实现侧一致的常量 set_constant -type port /ref_top/cfg_mode 2'b00 set_constant -type port /ref_top/test_en 1'b0

这里的关键是-type参数要选对。如果是端口，用port；如果是内部信号，用net或pin，具体看工具版本的支持情况。约束完之后重新跑match和verify，如果之前那些unmatched点是因为常量传播导致的，这时候应该会大幅减少。

但这里有个坑我得提醒：set_constant不是万能的。如果参考侧该信号还驱动着其他未被常量化逻辑，强行设常量可能会导致那些逻辑的比对也出问题。所以设常量之前，一定要确认该信号在参考侧的所有fan-out是否都允许被常量化。我吃过一次亏，把一个时钟使能信号设成了常量0，结果依赖它的整个计数器逻辑全报fail，因为参考侧那个计数器还在正常工作，只是使能条件在实现侧被优化了。后来改成只对特定层次设常量，问题才解决。

4.2 用set_dont_verify排除无关比对点

有些常值mismatch点其实跟功能无关，比如测试逻辑、DFT扫描链相关的寄存器、或者一些只在特定模式下才用的配置位。这些点如果因为常量传播报unmatched，逐个去引导很浪费时间，更高效的做法是用set_dont_verify把它们排除在比对范围之外。

# 排除测试逻辑相关的比对点 set_dont_verify -type register /impl_top/dft_chain_reg* set_dont_verify -type register /impl_top/test_mode_cfg*

用这个命令的前提是：你得确认这些点确实不影响功能等价性。我的经验是，DFT相关逻辑、电源管理相关的配置位、以及一些纯调试用的寄存器，通常可以安全排除。但功能路径上的配置寄存器绝对不能随便排除，否则可能掩盖真正的功能bug。排除之后，formality的比对点数量会减少，剩下的点如果还有fail，就更容易聚焦。

4.3 处理black box输出的常量驱动

如果常值问题来自black box，处理方式又不一样。当某个子模块被设为black box时，它的输出在formality里是自由变量。但如果实现侧这个输出被常量驱动了，工具会认为参考侧的自由变量和实现侧的常量不等价，从而报fail。这时候的正确做法不是设常量，而是检查这个black box是否应该被设为black box。

我的处理原则是：如果一个模块在实现侧被完全常量化了，那它在参考侧也不应该作为black box参与比对，而应该用set_black_box的反向操作——也就是把它从black box列表里移除，或者用set_dont_verify把它的输出排除。反过来，如果这个模块确实应该保留为black box（比如它是第三方IP，没有可比对的RTL），那就要在参考侧也把它的输出约束成与实现侧一致的常量，用set_constant处理。

这里有个判断依据：看这个black box的输出在参考侧是否还有别的fan-out。如果它的输出只驱动了被常量化的那部分逻辑，那排除掉没问题；如果它还驱动着其他功能逻辑，那就不能简单排除，得仔细分析常量驱动是否合理。

4.4 验证引导是否生效：看matched points的变化

加完setup引导之后，不能只看fail数量有没有减少，还要看matched points的变化。formality在每次verify之后会输出matched、unmatched、failing的统计。如果加了set_constant之后，unmatched减少了但failing增加了，说明常量引导把一些本来能配对的点搞成了不配对，得回退调整。

我习惯在每次改setup之后，把统计摘要存下来做对比。一个健康的引导应该表现为：unmatched显著减少，failing不增加或只增加少量可解释的点。如果failing大幅增加，那说明引导范围过宽，把不该常量化的信号也常量化了。这时候要缩小set_constant的作用范围，比如从端口级改到特定层次内的net级。

5. 几个我踩过的坑：常值debug里的反直觉经验

理论讲完了，这一节说点实际踩坑的经验。这些东西在工具手册里基本找不到，但每一个都让我多花过半天以上的时间。

5.1 常量传播的"连锁反应"：改一个点带出一片

最坑的一次是：我为了修一个unmatched寄存器，给它加了set_constant，结果那个寄存器是匹配了，但它下游的十几个组合逻辑输出全报fail。原因是这个寄存器在参考侧还驱动着一个状态机的次态逻辑，设成常量后，状态机的行为在两边就不一致了。

这个坑的教训是：常值引导要看fan-out，不能只看单点。在设常量之前，先用report_fanin和report_fanout把该信号的上下游都看一遍。如果它的fan-out里有状态机、计数器、或者任何有时序行为的逻辑，就要格外小心。安全的做法是只对叶子节点设常量，也就是那些不驱动其他时序逻辑的纯配置信号。

5.2 名字匹配的陷阱：优化后的信号名对不上

formality报unmatched时给的是实现侧的名字，而综合日志里记录的是优化前的名字，两者经常对不上。我遇到过一回，formality报/impl/u_core/reg_cfg_0_unmatched，我去综合日志里搜这个名字，什么都搜不到。后来才发现综合工具把这个寄存器重命名成了/impl/u_core/CONST_0_net_123，因为它的值被常量传播成了0。

解决办法是看formality生成的name mapping文件，或者用report_name_mapping命令查对应关系。如果实在对不上，就在综合日志里搜该寄存器原来的RTL名，通常能找到"被优化为常量"的记录。这个环节很考验耐心，但跳过它直接猜成因，往往会猜错。

5.3 复位值与常量值的混淆

有一类fail特别迷惑：参考侧寄存器复位值是0，实现侧该寄存器被优化成常量0，看起来完全一致，但formality就是报fail。查了半天才发现，问题出在复位释放后的第一个时钟沿——参考侧寄存器在复位释放后可能被D端驱动成1，而实现侧常量永远是0。工具在证明时考虑了复位释放后的行为，所以认为不等价。

这种问题的根源是：常量传播只看到了复位值，没考虑复位释放后的动态行为。处理办法是确认该寄存器在复位释放后是否真的恒为0。如果它确实恒为0（比如D端也被常量驱动），那用set_constant引导没问题；如果它复位后可能变1，那说明综合工具的常量传播做错了，得回去查综合约束。

5.4 don't-care设置不一致导致的假常量

最后一坑来自don't-care。formality允许对某些输入组合设don't-care，工具在这些组合下不检查输出。但如果参考侧和实现侧的don't-care设置不一致，工具可能会在某些组合下把输出当成常量来优化，导致比对时出现本不该有的mismatch。

我遇到过一次，参考侧对某个使能信号设了don't-care，实现侧没设，结果formality在使能无效时把实现侧的输出当成了常量，报了一堆fail。后来把两边的don't-care设置对齐，问题消失。这个坑的教训是：don't-care设置必须两边一致，不能只在一侧设。而且设完之后要检查它是否意外影响了常量传播的判断。

6. 把常值debug做成可复用的检查清单

每次遇到常值问题都从头查一遍太累，我后来把这套流程固化成了一个检查清单，跑formality之前先过一遍，能提前规避掉大部分常值相关的fail。

这个清单不是让你每次都全查一遍，而是当formality报出成片unmatched或failing时，按这个顺序快速过一遍，通常能在十分钟内定位到大方向。我实际用下来，大部分常值问题都能在前三项里找到线索。

另外补充一个实操建议：formality的setup脚本最好做成参数化的，把常量引导、dont_verify、black box设置都写成可配置的变量，而不是硬编码。这样不同项目、不同综合配置之间切换时，只需要改参数，不用重写脚本。我现在的做法是把这些引导项按模块分组，每组对应一个配置文件，跑之前根据综合配置选对应的文件加载。这个习惯让我在接手别人项目时省了很多重新理解脚本的时间。

最后说一个我个人的判断标准：如果formality报的常值mismatch点超过比对点总数的5%，那基本可以确定是setup引导没做全，而不是设计本身有问题。这时候不要急着去改RTL，先把引导补全，让工具在正确的基准上比对，剩下的fail才是真正需要关注的。这个比例是我踩了多次坑之后总结出来的经验值，不一定适用于所有项目，但作为一个快速判断的参考，还挺好用的。