形式验证深入：LEC 网表一致性、ECO 比对与复杂 set/reset 处理

更新时间：2026-09-25。本篇是验证方法系列在专家层级的第 17 篇。上一篇 ECO 自动化 讲了布线后如何用脚本批量修时序，这一篇回答一个更基础却更致命的问题：你改完的网表，凭什么相信它和 RTL 想做的事一模一样？仿真跑不完所有输入组合，而 形式属性验证 FPV 又只覆盖被写成断言的属性。在每一次综合、每一轮 ECO 之后兜住"功能没被改坏"这条底线的，是 LEC（Logical Equivalence Check，逻辑等价性检查），代表工具是 Cadence Conformal 与 Synopsys Formality。

本文要回答的问题

• LEC 凭什么不靠仿真向量，就能"证明"两份设计功能等价？它到底在比什么？
• Conformal/Formality 的 setup、mapping、verify 三个阶段各做什么，key point 是什么？
• 明明 RTL 没大改，为什么综合后会报 non-equivalent 或 unmapped？哪些是真错、哪些是设置问题？
• retiming、扫描 DFT、时钟门控、异步 set/reset 这些结构为什么是 LEC 的难点，怎么处理？
• ECO 之后为什么必须重新做 LEC，增量验证怎么做？大设计为什么要分层自底向上比？

一、为什么 ECO 后必须做 LEC：仿真给不了穷尽保证

先把一个常见误解挑破：很多人以为"我回归测试全过了，网表就是对的"。问题在于，门级仿真和 RTL 仿真都只能跑有限的测试向量。一个 32 位加法器的输入组合就有 2^64 种，再豪华的回归也覆盖不到九牛一毛。综合器做的优化——跨模块端口重组、retiming 把寄存器搬过组合逻辑、状态机重新编码、常数传播把整段逻辑删掉——任何一步工具出 bug、或者约束给错（比如错误地把某信号当常数），都可能让网表在某个没被测到的角落偏离 RTL 意图。等到流片后在硅上暴露，代价是重新掩模的几百万美元和几个月延期。

LEC 换了一条思路：它不问"对某些输入输出对不对"，而是用数学方法构造一个乘积状态机（product machine），把 golden（参考设计，通常是 RTL 或上一版已签核网表）和 revised（被验证设计，通常是新网表）的对应输出与寄存器接在一起，证明"从复位状态出发，对任意输入序列，两边的输出永远相同"。这是一个基于 BDD（Binary Decision Diagram，二元决策图）和 SAT（布尔可满足性）的形式证明，结论只有三种：等价、不等价、无法判定。它不需要测试平台，覆盖的是全部输入空间。

正因为它比的是"数学上的功能恒等"，所以它对设计的"形状"极其敏感：两边逻辑哪怕结构差得面目全非（综合器把一行 assign 展开成几十个门），只要布尔功能相同就能证明等价；反过来，两边只有一个寄存器复位值不一致，也会被精确地抓出来。这种"对功能宽松、对差异严格"的特性，决定了 LEC 的成败几乎全在 setup——你得先告诉工具哪些点该和哪些点对应。

对比项	仿真	LEC 逻辑等价
输入空间	有限测试向量	全部输入组合（数学证明）
依赖	测试平台、期望结果	golden 与 revised 两份设计
能发现	被测到的功能错	任意导致功能偏离的差异
不能发现	没写到的场景	属性级正确性（那是 FPV 的事）
结论	通过/失败（统计意义）	等价/不等价/不可判定（确定）

这张表也划清了边界：LEC 只证明"revised 和 golden 等价"，它默认 golden 本身是对的。如果 RTL 写的逻辑本来就错，LEC 会忠实地证明网表"正确地错着"。功能意图的正确性仍要靠仿真和 FPV 保证。

二、golden 与 revised：LEC 在比哪两份设计

LEC 永远是一个两两比对：一份 golden（金标准，被信任的参考），一份 revised（待检验的新设计）。在一条典型流程里，这个比对会发生很多次：

读图时注意箭头方向的含义：每一阶段都把"上一阶段已被接受的版本"当 golden，把新阶段的产物当 revised。第一次是 RTL 对综合网表，确认综合没改功能；插入扫描链和测试逻辑后，再以综合网表为 golden 比 DFT 网表；布局布线一般不改变逻辑（只做物理连接和缓冲插入），但仍要比一次；之后每做一轮 ECO，就以 ECO 前的签核网表为 golden 做增量比对。这样任何一步偷偷改坏功能，都会在当步被拦下，而不是累积到最后无从定位。

这里有个工程选择：golden 该始终用 RTL，还是沿用上一版网表？主流做法是两者都保留、以网表为直接 golden。因为越到后期，网表里插入了 isolation、retention、level shifter、扫描复用器、门控时钟单元等大量 RTL 里没有显式存在的结构，直接拿 RTL 去比对最终网表会产生海量需要手工解释的差异；而逐阶段相邻比对，每一步新增的结构是可控、可解释的。当然，RTL 这个"源头 golden"要一直保留，用于争议时回溯。

三、key point 与三阶段：setup、mapping、verify

LEC 把整个流程切成三个阶段，理解这三个阶段就理解了工具的工作方式。

setup（设置）阶段：读入 golden 和 revised 两份设计，告诉工具哪些是黑盒、哪些是常量、扫描/功能模式怎么切、时钟和复位是什么。工具内部把设计展平成一张由 key point 分隔的组合逻辑网络。key point（关键点）是工具比对的"锚点"，包括：主输入、主输出、寄存器（D 到 Q 的边界）、D 锁存器、黑盒的输出引脚、以及被设置为 cut point 的内部点。两个 key point 之间的纯组合逻辑，就是工具要单独证明等价的一个"比对单元"。

mapping（映射）阶段：工具自动给 golden 和 revised 的 key point 配对——这个输入对那个输入、这个寄存器对哪个寄存器、这个输出对哪个输出。能按名字、按功能自动配上的叫 mapped；配不上的 golden 点叫 unmapped（多余/消失），revised 侧配不上的也会列出。mapping 是绝大多数"伪失败"的来源：综合后寄存器被重命名、层次被打平、一组寄存器被拆分合并，都可能让工具配错或配不上。

verify（证明）阶段：对每一对 mapped key point 之前的组合锥（combinational cone），证明它们布尔等价。全部通过才是 equivalent；某一对证不出就是 non-equivalent，并给出反例（counterexample，一组让两边输出不同的输入和内部状态）。

调试顺序因此很清晰：先解决所有 unmapped（它们要么是真丢了逻辑，要么是映射没设对），再看 non-equivalent。一上来就盯着 non-equivalent 的反例，而 map 表里还一堆没配上的点，往往是白费功夫——因为连"在比谁和谁"都没定下来。

四、unmapped 与 non-equivalent：怎么判断是真错还是设置错

这是 LEC 实操中最考验经验的部分。报红分两大类，处理思路完全不同。

unmapped 点先要问：这个点该不该存在？几种典型情况：一是黑盒 IP，RTL 里有个模块实例，网表里对应 IP 被当成黑盒，其内部点本来就不该比——设为黑盒即可；二是综合做了常数传播或死逻辑消除，把某个永远不被用到的输出优化掉了，若确认是预期行为，属于合理 unmapped；三是 ECO 真的删/加了端点，那要回到改动单核对是不是有意为之；四是层次被打平后名字对不上，可通过命名规则、引导映射（guide）让工具重配。判断准则是：能在设计意图里解释的 unmapped 才放行，解释不清的一律当缺陷查。

non-equivalent 则是工具已经配上对、却证明两个组合锥功能不同，必须当真。工具会给反例：某组输入与状态下，golden 输出 0、revised 输出 1。拿着这组反例沿锥回溯，通常能定位到具体门。常见真因有：综合约束错误（错误 set_case_analysis、错误的时钟/复位定义，让工具按错误模式优化）、ECO 改错（连错线、接错选择端）、网表与 RTL 版本不匹配（比错了对象，属于流程管理错误）、多驱动/三态总线在某侧处理不一致。

需要特别强调一类伪 non-equivalent：两边功能其实相同，但 setup 没把特殊结构告诉工具，导致它按普通组合逻辑去比而误判。比如时钟门控、带 scan_enable 的复用器、异步复位释放逻辑、三态使能，如果没有在 setup 里正确声明，工具可能把它们的控制端当普通数据，证不出等价。这类"失败"的特征是反例涉及的恰是那些控制信号。处理方式不是改设计，而是补正确的 setup 约束后重跑。区分真错与设置错，靠的就是看反例落在数据功能上，还是落在时钟/复位/测试/三态这些特殊控制上。

五、难点结构：retiming、DFT、时钟门控、异步 set/reset

下面这几种结构是 LEC setup 公认的硬骨头，逐一说明难在哪、怎么配。

**retiming（寄存器重定时）**是综合为优化时序，把寄存器在组合逻辑前后移动（forward/backward），寄存器总数、名字、对应位置全变了，但整体功能等价。普通按点配对会失败，因为 golden 的一个寄存器在 revised 里可能没有直接对应。Conformal/Formality 都有专门的 retiming 识别/重定时映射算法，需要开启相应选项，让工具在更宽范围内寻找寄存器间的等价关系，而不是一对一。

**扫描 DFT（scan/DFT）**插入扫描链后，寄存器被换成带扫描复用器的扫描触发器，多了 scan_in、scan_en、scan_out。功能模式下 scan_en=0，电路应与原网表等价；测试模式下 scan_en=1 走移位。做法是用 case analysis 把 scan_en 固定为 0、把 test_mode 固定到功能值，先证明功能等价；扫描链本身的移位正确性另由 DFT 流程保证。如果忘了做 case analysis，工具会把 scan_en 当自由输入，自然证不出。相关背景见 DFT 高级扫描压缩。

时钟门控 ICG（Integrated Clock Gating）：RTL 里往往写成 if(en) 条件驱动寄存器，综合换成 ICG 单元，由门控使能控制时钟。工具需要识别这是时钟门控结构，把 RTL 的"使能条件"和网表里 ICG 的使能端对应起来，否则会把被门控寄存器的时钟行为当差异。

**异步 set/reset（复位/置位）**最容易出真问题。要核对的不只是"有没有复位"，还有：异步还是同步、复位电平（高/低有效）、复位值（寄存器复位后是 0 还是 1）、置位与复位的优先级。两侧只要有一个寄存器的复位值不一致，就是确定的 non-equivalent——这往往暴露 RTL 与网表在复位意图上的真实分歧。复杂的多 bit 编码寄存器（如复位到非零值的状态寄存器）尤其要逐位核对。

低功耗单元：综合/插入电源意图时加的 isolation（隔离）、retention（保持）、level shifter（电平转换），若 golden 侧（RTL 或不带电源意图网表）没有对应建模，会产生大量差异。常见做法是用统一的 UPF/CPF 电源意图同时驱动比对两侧，或在 golden 侧补建模，使这些结构可被识别。

难点结构	RTL 表现	网表表现	LEC 处理
retiming	固定寄存器位置	寄存器被搬移	开 retiming 识别
DFT 扫描	普通寄存器	带 scan 复用器	scan_en=0 case analysis
时钟门控	if(en) 条件	ICG 单元	识别门控结构与使能
异步复位	always 块敏感表	set/reset 端	核对电平/值/优先级
低功耗	无显式结构	isolation/retention	两侧统一电源意图

六、ECO 后增量 LEC 与分层验证

最后讲两个工程化实践。

增量 LEC（incremental LEC）：一次 ECO 往往只动几十个点，如果每次都把整颗芯片从头比一遍，几亿门的设计要跑很久。增量流程先做 ECO 比对，识别出受影响的锥（fanout cone of changed points），只重新证明这些锥，未受影响部分沿用上轮结论。这要求维护好 baseline 设计和改动映射。即便用增量，也建议在最终签核前跑一次全量比对兜底，防止增量识别遗漏。ECO 网表与 ECO 前 golden 的差异，必须和实际改动单完全吻合——多出来的任何差异，要么是工具误改，要么是改动单没写全，都要查。

分层 / 自底向上验证：超大设计一次性展平比对，可能因 BDD 膨胀而耗尽内存或陷入"不可判定"。分层方法利用模块边界自底向上：先证明每个子模块 revised 与 golden 等价，把子模块在父层当成已验证的黑盒/约束块，再验证父层装配（端口连接、顶层胶合逻辑）是否一致。这样每一层的比对规模都可控。代价是要保证模块边界、端口在两侧稳定可配，且不能漏掉顶层互连与跨模块优化（综合若跨模块重组端口，分层点会被打破，需要回到展平比对或调整划分）。

完成 signoff LEC 的判据可以收成一张硬清单：所有该映射的 key point 全部 mapped，无未解释的 unmapped；所有比对锥 verify 通过、non-equivalent 为 0；黑盒清单与 IP 版本一致；功能模式经 case analysis 后等价；扫描链移位由 DFT 单独确认；ECO 差异与改动单逐条吻合；最终做一次全量比对留档。这些条目不依赖某个具体项目，是通用的放行口径。

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

本篇用数学等价证明守住"每一步实现都没偏离 RTL 意图"这条底线，和三种相邻能力构成互补：ECO 自动化 负责产生改动，本篇负责证明改动无害；形式属性验证 FPV 证明的是设计"满足某条性质"，本篇证明的是"两个版本功能相同"，两者都属形式方法但命题不同；DFT 高级扫描压缩 插入的扫描逻辑，正是本篇里要靠 case analysis 排除的特殊结构。

总结

LEC 用 BDD/SAT 构造乘积状态机，在 RTL→综合→DFT→布局布线→ECO 每一阶段把上一版当 golden、新版当 revised，不靠仿真向量就能证明所有输入下功能恒等；工具按 setup（读设计、定黑盒与模式、划出 key point）、mapping（配对输入/输出/寄存器/锁存器锚点）、verify（逐组合锥证明）三步推进，unmapped 要判断逻辑是真丢还是命名/黑盒问题，non-equivalent 要拿反例区分真实缺陷与时钟门控、扫描、三态、异步复位设置不当造成的伪失败；retiming 靠专门识别、DFT 靠 scan_en=0、低功耗单元靠两侧统一电源意图，ECO 后必须做增量 LEC 且差异与改动单逐条吻合，大设计用分层自底向上控制规模，最终全量比对签核——LEC 只保证"网表忠实于 RTL"，功能意图本身的正确性仍要靠仿真和 FPV。