极客工场

Appearance

共 1,551 字预计阅读约 5 分钟

逻辑等价检查 LEC/Formality：综合、DFT、ECO 后如何证明没改坏功能 ​

更新时间：2026-09-14。本文是数字验证系列第 10 篇。Formal 入门讲的是“性质是否成立”，这一篇讲更标准的签核形式验证：两个设计是否逐周期功能等价。代表工具为 Cadence Conformal LEC、Synopsys Formality。

一、为什么仿真不能替代 LEC ​

综合会做常量传播、retiming、状态机重编码、DFT 会插入 scan mux、时钟门控，后端还可能手工 ECO。门级仿真慢且向量有限；LEC 不依赖向量，直接证明：

对所有合法输入，golden 与 revised 的状态单元在下一状态和输出上等价。

典型比较点：

GoldenRevised时机
RTL综合网表synthesis 后
综合网表DFT 插入网表scan/压缩/测试控制器插入后
DFT 网表布局布线网表P&R 后
旧网表ECO 网表metal/functional ECO 后

二、基本模型：key point ​

工具把设计切成状态点和比较点：

  • DFF / latch：状态元件，是主要 compare point。
  • primary output：顶层输出。
  • black box output：无法展开时按边界处理。
  • cut point：人为切断后分别证明的内部点。

工具先做映射（mapping），再做组合锥（combinational cone）等价证明。状态点数量不要求完全同名，但必须能一一对应；对不上就会出现 unmatched points。

三、标准流程 ​

bash
1. read design：读 golden RTL 和 revised netlist
2. set top / read libraries：标准单元、黑盒模型
3. read constraints：define、mode、DFT/test mode、常量 tie-off
4. mapping：映射 key points
5. compare：证明组合锥等价
6. analyze：处理 unmatched/non-equivalent/aborted
7. 保存 session 与 signoff report

DFT 模式必须显式告诉工具：scan_en=0 为功能模式，scan_en=1 为移位模式；时钟控制器里的 mux、测试复位、压缩逻辑如果 mode 不一致，会产生大面积假不等价。

四、报告怎么读 ​

报告项含义处理
Equivalent已证明等价保留
Non-equivalent找到反例必修，查 RTL/网表/ECO
Unmappedkey point 对不上查层级、优化、黑盒、retiming
Aborted/Unproven空间或复杂度不足加 cut point、case analysis、分层验证
Extra/Deleted DFF状态点增减综合重编码/DFF 优化或真实 bug

非等价反例会给出输入赋值、状态初值和两个输出波形。先看是否 常量/模式错误，再看最近是否有 ECO、综合属性、DFT 替换。

五、最常见根因 ​

  1. 少读 define：golden 用 define A=1，revised 用了另一配置。
  2. 黑盒不一致：RAM/IO/PLL 端口或行为模型版本不一致。
  3. scan/function mode 错误：test pin tie-off 与网表不符。
  4. case 分析缺失：多模式中未固定时钟选择或隔离使能。
  5. retiming 后映射失败：寄存器跨组合逻辑移动，需要工具识别 retime 或提供 guidance。
  6. 手工 ECO 漏改：只改网表没改 RTL，golden 选错版本。
  7. 异步路径/锁存器：需要正确建模，而不是强行比较。

六、ECO 后的最小闭环 ​

bash
golden RTL（期望） ─┐
                   ├─ LEC：功能期望 vs ECO 网表
ECO gate netlist ──┘
旧网表 vs ECO 网表：确认改动范围只在预期 cone
STA/DFT/Lint：确认 ECO 没有破坏时序和测试

ECO 不要只证明“旧网表与新网表差异”，还应回到最终期望 RTL 或形式化设计意图，否则两个错误版本之间比较没有意义。

七、黑盒、宏与不需要比较的边界 ​

存储器、模拟宏、PHY、PLL、IO cell 通常不能按普通逻辑锥比较。处理方式不是一律黑盒后忽略，而是明确边界协议：哪些输入在功能模式固定、哪些输出由模拟行为驱动、哪些测试模式需要单独比较。硬宏的库模型、端口位宽、电源域、时序弧版本必须与综合和物理设计一致。若 LEC 把宏内部当未知，而 STA 又使用了另一版本的 timing model，就可能出现“等价通过但时序签核对象不同”的问题。

需要 cut 的点也要谨慎。cut point 可以降低复杂度，但它相当于人为切断证明链，必须补充边界驱动假设，并证明下游锥和上游锥分别正确。常见做法是对庞大配置寄存器、测试控制、内存接口分层验证，而不是对关键数据通路随意切断。每个 cut point 都要在报告中列出原因和对应子证明，不能只作为工具跑不过去时的消音手段。

八、签核归档最小集合 ​

一次可审计的 LEC 签核至少应保存：golden/revised 设计文件列表，宏和库的版本，define/mode/setup 脚本，映射报告，compare 报告，未证明点分析，waiver/guidance，工具版本与平台信息。最好保留可恢复的 session，使评审者能打开反例波形。对于最终 ECO，还要记录是谁提交了哪个网表、LEC 结果何时产生、之后是否又有版图修改。LEC 绿灯之后任何重新布线或网表替换，都意味着相关证明必须重新生效。

Checklist ​

  • [ ] RTL→综合网表、DFT 前后、P&R 后、ECO 后都有 LEC 记录。
  • [ ] 所有 key points mapped，无未批准 unmatched。
  • [ ] Non-equivalent = 0，Aborted 有分层证明方案。
  • [ ] 黑盒、宏、DFT mode、tie-off 使用同一版本配置。
  • [ ] ECO 后同时做增量 LEC 与全量 LEC。
  • [ ] signoff 报告、脚本、库版本、日志归档可复现。

相关与延伸 ​

形式验证基础见 Formal 验证入门；ECO 流程见 物理 ECO 与时序收敛；DFT 背景见 可测性设计 DFT；门级/X 态验证见 门级仿真、SDF 与 X-prop。

总结 ​

LEC/Formality 用形式化证明替代“向量碰运气”：每经过综合、DFT 插入、P&R 和 ECO，都要把状态点映射清楚并证明组合锥等价；non-equivalent 是硬伤，unmapped/aborted 也不能靠一句“应该没问题”签出去。