极客工场

Appearance

共 2,533 字预计阅读约 8 分钟

Formality 信号被优化掉：compare point 消失速查 ​

更新时间：2026-10-22。FAQ 速查页，属于 EDA 工具报错速查系列。在 Formality（Synopsys 的逻辑等价检查工具，LEC 流程的一种）里 match 之后，RTL 里明明有的寄存器或端口在 implementation 一侧找不到对应物，报告里一片 Unmatched compare points，信号像被综合「优化掉」了。先别急着认定是工具 bug：等价检查比的是逻辑锥功能，不是信号名一一对应；信号消失既可能是完全正常的等价优化，也可能是 guidance 没喂对导致的配对失败。LEC 总体流程见 形式验证：用 LEC/Formality 给每一步网表变换兜底，retiming 配对深坑见 LEC retiming 比对失败排查。

本文要回答的问题 ​

  • Formality 报 Unmatched compare points，是不是说明信号被综合优化没了？
  • 哪些「优化掉」是正常等价、可以豁免，哪些是真问题必须修？
  • DC 写的 SVF guidance 怎么读进来，漏读会造成什么现象？
  • DFT/scan 插入后 test_mode 没设常量，为什么会让大片 compare point 黑盒化？
  • 用什么命令把消失的信号分类查清楚？

一、报错原文与现象 ​

text
Warning: Unmatched compare points exist. Run 'report_unmatched_objects' for details.
Warning: Reference point u_core/u_fifo/rd_ptr_reg[3] is unmatched.
Warning: Net 'scan_en' is treated as a free variable because it has no constant setting.
Information: Some compare points are constant in the implementation.

第一种是配对阶段的典型形态：match 跑完后 reference（RTL 侧）有 compare point，implementation（综合网表侧）找不到功能等价的配对点，verify 直接带着未配对点进入，结果既不算 PASS 也不能放心签核。第二种是常量化提示：某信号在网表侧被常量传播折成固定值，锥退化了。第三种是 DFT 信号悬空：scan_en、test_mode 这类测试控制信号在功能模式下没有常量约束，工具只能当自由变量，DFT mux 的选择端悬空会让锥的对应关系整片塌掉。

还要注意静默形态：部分流程脚本只看 Verification PASSED 字样，未配对点若恰好被配置成不阻断，verify 可能以带豁免的方式结束。必须以报告里 unmatched 计数为零（或每条都有书面豁免理由）为准。

二、报错 → 原因 → 处置速查表 ​

现象可能原因处置方向
单点 unmatched，网表侧同功能锥存在综合改名/合并，guidance 未跟上读 SVF 后重新 match
一批寄存器全部 unmatched，集中在重定时模块retiming 把寄存器搬过组合逻辑按 retimed 配对流程处理
信号被标记 constant常量传播，功能模式下确为常量确认语义后接受该等价
DFT mux 后整扇出锥 unmatchedtest_mode/scan_en 未设常量补 set_constant 后重跑
某模块边界后整片消失模块被当黑盒、库/网表未 link 全先解黑盒再配对
顶层接口对不上set_top 选错或读入多版本设计核对顶层与读入文件清单
每次综合后随机散点 unmatchedSVF 与网表版本不配对重新导出同版 SVF

三、逐条排查展开 ​

第一步：用报告分类，不要凭信号名下结论。 Formality 看到的是 compare point（比较点：寄存器、端口、黑盒输出等切分逻辑锥的位置），不是 RTL 的每一根线。配对后第一件事是让工具把未配对对象摊开：

tcl
report_unmatched_objects -type all
report_unmatched_objects -type rff
report_unmatched_objects -type compare

按类型看：寄存器（rff）未配对与端口未配对的根因通道不同。再让工具说明为什么没配上，重点看它给出的 constant、merged、black box 等标注。先分类、后归因，是这一步的纪律。

第二步：分清「正常等价优化」与「真丢失」。 综合器对 RTL 做的很多变换会让信号名消失但功能不变：常量传播把使能恒有效的寄存器使能端折掉、死逻辑消除删掉不可达分支、等价寄存器合并、组合逻辑吸收进相邻单元。判断标准只有一个——以该信号为切点的逻辑锥，在两侧是否功能等价。锥等价、只是切点没了，这是正常优化，记录豁免理由即可；若整组功能点连带消失、且网表侧找不到等价锥，才是真问题。对确认无需比对的点，可用 set_dont_verify 一类豁免设置显式排除，但每条豁免要有评审记录，禁止用豁免把报告「清零」了事。

第三步：查 guidance——SVF 漏读是头号原因。 Design Compiler 综合时会把重定时、寄存器复制/合并、状态机重编码等变换写进 SVF（Setup Verification File，指引文件），Formality 靠它知道「RTL 的 A 寄存器对应网表的 B/C 寄存器」。没读 SVF 或读错版本时，工具只能按结构猜测配对，遇到 retiming 必然成片 unmatched。标准动作：用 set_svf 指定与当前网表同一次综合导出的 SVF，重新执行 link 与 match；若流程使用 verification_choice 一类补充指引开关，按模块的变换类型逐项打开。SVF 必须与网表严格同版——综合重跑后旧 SVF 立刻作废。

eda/ts-formality-signal-optimized-away.md D2 示意图

这张分诊图按 C47 语义着色：红是入口现象与坐实的根因，蓝是排查动作，绿是「正常等价」通道，橙是修复动作，紫是收口。读图抓住中间一次四叉分流——报告把缺失点分成「正常优化、guidance、常量、retimed/黑盒」四条通道，只有绿色那条可以直接接受，其余三条修复后统一汇到「重新 match 并核对豁免清单」收口。

第四步：补常量设置，治 DFT 插入后的整片 unmatched。 做过 scan/DFT 插入的网表，功能路径上挂着测试 mux：test_mode=1 走扫描链、scan_en 控制移位。等价检查验证的是功能模式，必须用 set_constant 一类设置把这些控制端钉成功能值（如 test_mode 为 0），工具才能穿过 mux 看到功能锥。漏设时 mux 选择端成为自由变量，其扇出范围内的 compare point 会成片配对失败或黑盒化。同理，综合时通过 case analysis 钉死的模式端（多模选择、静态配置寄存器），Formality 侧也要给同样的常量，两侧世界必须一致。

第五步：retimed 寄存器按专门通道配对。 综合重定时把寄存器从组合路径一端搬到另一端以平衡时序，RTL 与网表的寄存器不再一一对应，名字也失去对应关系。这不是「优化丢了」，而是变换需要专门的映射指引：确认 SVF 中包含 retiming 记录、开启对应的 verification 指引后重新 match；仍对不上的，按 retiming 后寄存器映射失败 的配对流程处理（先配对、再证明，必要时走 SEC 兜底）。不要在这种点上手工 set_dont_verify 跳过——那正是等价检查最该发力的区域。

第六步：黑盒与顶层错误造成的「被动消失」。 implementation 一侧某子模块没 link 上、被当黑盒，它输出之后的锥失去结构依据，工具只能剪枝，表现也是 compare point 成片消失；set_top 选错、或 reference/implementation 读入了不同版本的 RTL，则连顶层端口都对不齐。这类问题先按 Formality 引用无法解析与黑盒速查 把引用和黑盒解干净，再回到配对问题，顺序不能反。

四、预防与纪律 ​

  • SVF 与网表同版同生：综合脚本中 SVF 与网表一次导出、成对归档，Formality 脚本按版本指纹取用，禁止用上次综合的旧 SVF。
  • 常量设置清单化：test_mode、scan_en、静态模式端的功能值写成项目级约束文件，每个等价检查阶段复用，不靠人口袋记忆。
  • unmatched 零容忍 + 豁免留痕：verify 前 unmatched 必须清零或逐条书面豁免，豁免禁止用在 retiming 区域。
  • match 与 verify 分阶段看报告：配对问题（本篇）与真正不等价（NON-EQUIV，见 LEC 不等价调试方法论）是两类病，不要混着治。
  • 脚本不只 grep PASSED：签收条件包含 unmatched 计数、豁免计数、黑盒计数三项，任一非预期即失败。

这一篇在知识体系里的位置 ​

本篇是 EDA 排错速查簇中「形式验证配对」节点的 Formality FAQ 页。流程与原理见 形式验证：LEC/Formality 与 逻辑等价检查（LEC/Formality）；配对失败的两个专项深水区是 retiming 寄存器映射失败 与 引用无法解析/黑盒；配对通过但 verify 不等价时转 LEC 不等价调试方法论。

一句话总结 ​

Formality 里信号「被优化掉」先跑 report_unmatched_objects 按类型分诊：锥功能等价仅切点消失是正常优化（留痕接受），成片 unmatched 优先查 SVF guidance 是否漏读或版本不配对（set_svf 重读重 match），DFT 后整片塌掉补 set_constant 钉死 test_mode/scan_en，retimed 寄存器走专门映射指引、黑盒剪枝先解引用；根治靠「SVF 与网表同版、常量清单复用、unmatched 零容忍且豁免留痕」。