形式验证（二）：用 LEC/Formality 给每一步网表变换兜底（B4）
数据流见 S2 综合交接 与 X3 ECO 传播；本篇握工具：Synopsys Formality（
fm_shell）、Cadence Conformal 怎么把两份设计证明为功能等价。属性证明（不靠激励证断言）归 B3，本篇专讲组合/时序等价这一类流片刚需。设计侧概念见 验证域 LEC。
一、为什么仿真替代不了 LEC
综合会做大量人类难以逐门核对的变换：多级逻辑优化、retiming 跨寄存器搬逻辑、scan 触发器替换、clock gating 插入、缓冲器/反相器重组、物理 ECO。门级仿真只能覆盖你写得出的激励，几十亿种状态空间里漏一个 corner 就放过了；而 LEC 不看激励，它用 SAT/BDD/布尔匹配在数学上回答一个问题：
在所有可能输入、所有可达状态下，golden（参考）与 revised（被改后）两份设计的输出与下一状态是否完全一致？
因为它独立于综合的优化路径、只做布尔层面的证明，所以能抓住工具 bug、脚本误配、手工改网表改错这类「仿真碰巧没触发」的致命错误，是流片流程里成本极低、必须 100% 通过的一道闸门。
二、key point：工具怎么对齐两份设计
LEC 不做门对门比较（门数都不一样），而是先在两份设计里找出一组逻辑上必须等价的「比较点」，再逐点证明其锥（input cone）等价。
| 比较点类型 | 说明 | 易错处 |
|---|---|---|
| 主输入/主输出 | 端口边界 | 端口增删（加 test_mode）需显式说明 |
| 触发器/锁存器 | D 端数据锥逐点比 | retiming 改变寄存器数量时要靠引导 |
| 黑盒端口 | SRAM/IP/模拟宏当黑盒，只比边界 | 漏设黑盒会钻进硬核内部报一堆假错 |
| 切割点 cut point | 多驱动/特殊结构手动切开 | tie 常量、反馈环需单独处理 |
流程固定为 setup（读 golden/revised + 引导）→ match（建立比较点映射）→ verify（逐锥证明） 三段。match 阶段的 unmatched / unmapped 点必须先清零，否则没被比较的逻辑等于免检放行。
三、让工具对得上：SVF 与设置要点
综合会输出一份 SVF（setup guidance / guidance 文件），记录它做过的寄存器重命名、复制、retiming、常量传播等「我知道我改了什么」的提示。LEC 读入它才能把改名/搬位后的寄存器正确映射回去——SVF 与网表必须同一次综合产出，错配版本是 LEC 假不等价的头号原因。
| 设置项 | 作用 |
|---|---|
| SVF/guidance | 传递重命名、retiming、scan 替换映射 |
| black box | SRAM/硬核/PLL 设为黑盒，只比边界一致 |
| 常量/tie | 识别 test_mode、scan_en 等模式引脚在功能模式的固定值 |
| 时钟/锁存器 | 让工具正确识别 DFF 与 DLAT，避免把锁存器当组合点 |
| 多电源/隔离 | UPF 域的隔离/保持单元要按模式设置（见 UPF） |
多模式设计（功能/测试/扫描）要分模式分别证明：功能模式下 scan_en=0 证一次，扫描模式再证一次，不能一个约束包打天下。
四、各阶段分别跑什么
| 阶段 | golden | revised | 重点 |
|---|---|---|---|
| 综合后 | RTL | 综合网表 | 最基础一关，零例外必须过 |
| DFT/scan 插入后 | 综合网表（或 RTL） | 插链网表 | 功能模式下 scan 逻辑应透明 |
| 时钟树综合后 | 插链网表 | CTS 网表 | CTS 只插时钟缓冲，数据锥应等价 |
| 布局布线后 | CTS 网表 | routed 网表 | 布线不应改逻辑，防手工/工具改坏 |
| ECO 后 | ECO 前网表 | ECO 后网表 | 最高频，定位最精准（只看改动锥） |
五、不等价（NON-EQUIV）怎么查
按「从便宜到昂贵」的顺序排除：
- 先看 unmatched/unmapped：八成「不等价」其实是比较点没对上——名字没匹配、黑盒漏设、SVF 没读或版本错。
- 核对模式常量：test_mode/scan_en/电源模式是否两边一致，一个常量差会扇出成上千点假错。
- 看反例向量（counterexample）：工具给出能区分两锥的输入组合与寄存器值，沿数据锥回溯，通常能直接定位到某级逻辑。
- 隔离变更：若总回 RTL 状态爆炸，改成「相邻两版互比」，把问题缩小到具体那一步（呼应 X3 的作废链）。
- 真确认是有意改动却没回灌 RTL（典型是手工 ECO），必须同步改 RTL 或走正规 ECO 流程，绝不靠 waiver 掩盖真实不等价。
相关与延伸
总结
LEC 是不靠激励、用布尔证明为每次网表变换兜底的安全网：setup→match→verify 三段，先把 unmatched/unmapped 与黑盒、模式常量、同版 SVF 这些「对不齐」问题清零，再在综合/DFT/CTS/P&E/每个 ECO 之后逐版相邻互比；出现 NON-EQUIV 先怀疑映射与模式、再沿反例锥回溯，而任何真实功能差异都要回灌 RTL、绝不能拿 waiver 盖住。