前阵子我一朋友负责的芯片回片后功能fail，定位到最后，是ECO时一个时钟门控被手动挪了位置，原本的使能逻辑悄悄变成了常开。项目组复盘时问得最多的一句话是：为什么没有在ECO之后跑一遍Conformal LEC逻辑等价性检查。这不是个例，很多项目在综合、DFT、PR和ECO各个阶段都容易忽略这个环节，或者只是"跑了但没跑透"，结果把问题一路带到了硅片。这篇内容就围绕Conformal LEC展开，讲清楚它的原理边界、怎么组织参考脚本、常见坑怎么排，以及如何判断结果真的可以签核。适合刚接触逻辑等价性检查的验证工程师，也能给后端和DFT的同事一份可以直接抄作业的脚本框架。
1. 一个ECO把功能改没了：LEC该在什么阶段出手
1.1 我遇到的那个功能FAIL案例
那个case说起来挺憋屈。RTL本来只有两行改动，为了修一个跨时钟域的同步器遗漏问题，ECO工程师直接在门级网表里手工挪了两根线，回归仿真也跑了，覆盖率数字也还行，但芯片回来后某个模块在低功耗唤醒场景下出现了偶发死机。最后逐级追查，发现那个时钟门控的CLK输入端被接到了错误的buffer树上，唤醒时时钟毛刺直接打穿了同步器。
如果当时有人跑一次Conformal LEC，让ECO后的网表和RTL做一次严格的功能等价比对，这个问题在签核前就能暴露。LEC本身不测时序，不跑向量，它做的是形式化的功能比较：给定相同的输入序列，两个设计是否在每一个观察点产生相同的输出。仿真需要激励覆盖，LEC不需要，它是穷举证明，这对ECO后的安全确认极其重要。
这个案例说明一个现实：逻辑等价性检查不是"走过场"，它是RTL到GDSII流程里唯一能在不依赖测试向量的前提下，把功能一致性锁死的环节。仿真能做回归，但不能证明"没有漏测的向量"；LEC能证明。
1.2 LEC与仿真、Formal的关系边界
很多刚开始接触数字流程的同学会把LEC和仿真混在一起，甚至有人觉得SVF、SAIF都是干同一件事的。实际上它们分工完全不同：
| 手段 | 验证目标 | 依赖 | 证明强度 |
|---|---|---|---|
| 动态仿真 | 功能行为是否符合预期 | 激励质量、覆盖率 | 不完整，未测向量可能漏 |
| Formal Property Checking | 断言是否成立 | 属性完备性 | 限定在断言覆盖范围内 |
| LEC等价性检查 | 两个设计功能是否严格一致 | 匹配点、约束、黑盒设置 | 在可比对空间内是完整证明 |
LEC里有两个设计：一个是参考设计reference，通常指RTL，或者被认为是"正确"的网表；另一个是待验证设计implementation，通常是综合、PR或ECO后的网表。Conformal LEC会把两者的内部逻辑重写为规范化的逻辑锥，然后从输入到输出逐级映射、比对。
它和仿真最本质的区别是：仿真看到的是"某几条路径上的行为"，LEC看到的是"所有可能输入下的布尔行为"。这正是它在ECO场景下不可替代的原因。ECO改动哪怕只影响一个与非门，只要逻辑锥有任何差异，LEC都能报出来，而仿真可能要特定向量才能触发。
2. Conformal LEC的底层逻辑：逻辑锥、匹配点与等价性证明
2.1 工具是怎么"看懂"两个网表的
Conformal LEC跑比较前，内部要经过三个核心步骤：编译、映射、验证。
编译阶段，工具读入参考设计和实现设计，把门级网表、RTL都转换成统一的内部布尔表达。RTL会经过逻辑综合变成布尔方程，门级网表会展开成标准单元级别的逻辑锥。这一步如果库或者单元定义读错，后面全白搭，所以读库命令必须谨慎。
映射阶段是重点。工具要回答一个问题：参考设计里的这个寄存器/输出端口，对应实现设计里的哪一个寄存器/输出端口？找到对应关系后，它们就成为一组"匹配点"（mapped point）。匹配点之间的组合逻辑就是逻辑锥。验证阶段就是逐组比较这些逻辑锥的布尔功能是否等价。
如果把逻辑锥看成一个黑盒子，那么锥的输入是匹配点（寄存器输出、输入端口、黑盒输出），锥的输出是另一个匹配点（寄存器输入、输出端口、黑盒输入）。LEC验证的对象就是黑盒子内部的布尔表达式是否与参考设计完全一致。这也是为什么匹配点越多、越完整，验证的覆盖率就越高。
2.2 顺序电路比较：CLKN等特殊引脚背后的匹配机制
时序逻辑的比较和纯组合逻辑不太一样。工具不仅要比较寄存器输入端的数据逻辑，还要比较触发沿、异步复位/置位、时钟使能等控制逻辑。
Conformal LEC在自动识别时序引脚时，会依赖单元库中对引脚功能的描述。比如一个标准DFF，工具会识别CLK、D、Q、RN等引脚角色。很多库单元里时钟引脚名字带CLK或CLKN，复位带RN、RSTN，置位带SN、SETN。工具通过这些关键字的启发式匹配去做时序锥的区分。实际项目中，我们经常用add_clk和add_reset命令显式指定这些信号，避免工具识别错时钟沿。
有一个非常容易翻车的细节：如果一个时钟门控单元ICG在实现网表里被综合成了"数据端接了时钟"的普通逻辑，而不是被识别为时钟结构，LEC会自动走set_clock_gating_style或set_dont_verify_subgraph一类的处理路径。如果脚本里没做好这层声明，工具会默认两边都是普通时序单元，结果出现大面积的不等价报错，但实际功能没有差异。这种情况在低功耗项目中尤其常见。
2.3 等价性证明的关键：key point的映射质量
映射质量直接决定LEC结果的可信度。如果一组寄存器因为命名差异没有被mapping上，那么LEC就认为这个点是unmapped。Unmapped点不会参与自动等价性比较，即使功能错了也可能查不出来。
映射失败的典型原因有三类：
- 命名不匹配：综合或PR过程中插入了缓冲器、改名、加了后缀，导致参考设计和实现设计的寄存器名对不上。
- 结构变化过大：比如DFT插入扫描链、时钟树综合重排buffer，导致寄存器之间的距离和层级发生变化，工具基于结构相似度的匹配算法找不到对应点。
- 黑盒和常量设置不一致：两边对某个IP或某个端口处理方式不同，导致断点位置不同。
处理映射问题的手段在Conformal LEC里有几条：add_name_mapping做简单命名映射，set_mapping_style切换基于名称/基于功能/混合策略，必要时用add_compared_points手动指定。我的经验是先跑一遍自动映射，然后用report unmapped points看哪些点没匹配上，再决定是否手动干预。千万别一上来就手动加一堆点，很容易把错误映射"焊死"。
3. 一套能直接上项目的参考脚本
3.1 环境初始化与库设置细节
下面这套脚本是我个人项目沉淀下来的框架，跑RTL vs Gate和Gate vs Gate都适用，重点是把"设置可追溯、结果可回归"摆在第一位。脚本开头先把系统模式、日志和报告文件准备好：
set_system_mode lec set log file ./result/lec.log -replace set report file ./result/lec.rpt -replace # 库文件建议使用liberty或带timing的db，避免只用Verilog model read_library -liberty ./lib/ss_0p99v_125c.lib -timing read_library -liberty ./lib/ff_1p21v_m40c.lib -timing这里有个容易踩的细节：read_library只读标准单元的lib/db，不要在这个命令里加-verilog参数去读功能仿真模型。如果工具把功能模型当成库读进来，后面识别单元功能时可能出现奇怪的cell not found或者black box异常。读库的目的是让工具拿到每个单元的逻辑功能描述，综合后的网表里引用的是单元名，LEC靠库定义去还原布尔方程。
如果设计里用了自己定制的memory compiler，建议把memory模型以单独的Verilog netlist形式读入，然后对这个模块做black box处理。不要在liberty里强行包含memory内部的bit cell，否则工具会把memory内部复杂的时钟逻辑拿来比较，速度慢且结果乱。
3.2 网表读取、约束加载与时钟处理
接下来是读参考设计和实现设计。读RTL时注意读入文件顺序和include路径，读门级网表时注意-format verilog和-root module参数：
# 参考设计：golden RTL read_design -reference \ -netlist -root tb_top/duv_top \ -filelist ./rtl.f # 实现设计：综合后或ECO后网表 read_design -implementation \ -netlist -root duv_top \ /prj/out/revised_eco.v读完之后，立刻处理时钟和复位。对于门级网表，时钟树上的buffer和ICG会被工具自动处理，但为了减少不必要的逻辑锥扩展，建议显式声明时钟和复位端口：
add_clk 0 clk add_clk 0 clk_div2 add_clk 0 gclk_leaf add_reset 0 rst_n add_reset 0 arst_nadd_clk后面的0表示时钟相位或未约束的沿信息，这里配合set_clock_style使用。如果设计里有门控时钟，工具会自动展开ICG逻辑，不需要过度担心。真正需要注意的是：如果两个设计对时钟的定义不同，比如reference是RTL风格、只有一个clk，而implementation是CTS后的网表、时钟树有几十个leaf clock pin，这时必须在实现设计里把缓冲后的时钟网络都加到clock点列表中，否则工具可能把同一个时钟域内的寄存器当异步点处理，导致大量unmatched。
3.3 等价性验证与结果report
核心验证命令本身不复杂，但执行前必须想清楚需要对比哪些点。建议默认全点比对，再看报告分步处理：
set_constant -type port -value 0 test_mode set_constant -type port -value 0 scan_en set_flatten_model -design implementation -ground gnd -power vdd verifyverify命令执行完后，关注返回状态。如果状态是success或equivalent，说明所有可比较的点全部等价，这是最理想的。如果有non-equivalent或aborted，就需要看报告。
常用的报告命令我一般这样组织：
report compare data report non-equivalent points report not compared points report abort points report unmapped points report black box report floating pins report clock details report constant signals其中report non-equivalent points是最先看的，它告诉我们哪个寄存器输入逻辑和参考设计不一致。其次是report unmapped points，如果这里点很多，说明映射阶段出问题了，后面报的non-equivalent可能都是假错。最后看report abort，abort点表示工具由于逻辑锥太大或匹配点太复杂没能完成证明，这部分不能直接签核。
3.4 黑盒、constant和don't verify的声明
实际项目中几乎不可能让工具对全芯片所有逻辑都做完整证明，总会有一部分需要声明为黑盒、常量或不验证。声明的原因和方式要尽量保守，宁可多验证，不图省事。
# 模拟IO、SENSOR等模拟IP声明为黑盒 add_black_box -module analog_io_top add_black_box -module pll_clkgen # 低功耗隔离逻辑中的某些常开端口 set_constant -type port -value 1 iso_en set_constant -type pin -value 0 u_duv/scan_shift # 某些已知功能等同的寄存器，不参与验证 add_ignored_points -pin u_duv/reg_scratch/Q add_ignored_outputs u_duv/rf_probe_out特别提醒：add_black_box是把某个模块内部逻辑完全屏蔽，只当做一个不透明单元比对它的接口。如果实现设计和参考设计里黑盒模块不一致，或者一个黑盒一个不黑，工具会认为两侧的黑盒外部逻辑等价，从而掩盖内部差异。所以黑盒名单必须是两个设计都确认过是"无需检查"的模块，不能为了跑通脚本随手添加。
set_constant是把某些端口或pin强制固定在0/1，这通常用于测试模式信号、DFT shift等不影响功能路径的信号。用之前一定要确认该信号在功能模式下确实是被固定值的，否则等于人为制造等价假象。
4. 参考脚本跑不通？这些坑我基本都踩过
4.1 library多了一行“-verilog”的后果
有次我接手一个别人的脚本，里面写的是：
read_library -verilog -liberty ./lib/tt.lib初看好像没什么问题，工具也读进去了，没有报错。但跑完verify之后，回报结果非常怪异：参考设计里所有DFF的输出都被识别成常量，导致整个验证结果无效。排查了很久，最后发现工具把tt.lib当成了Verilog网表，读取方式不对，单元逻辑被解析成了空壳。
从那以后我对库读取命令都会坚持分开写：liberty用-liberty读，功能仿真模型如果需要，可以用read_verilog单独读，并且在set_system_mode lec之后立刻确认report library里的单元数量。正常一个三五百个标准单元的库，读进来应该有三五百条cell定义。如果数量明显偏少，基本就是读库姿势不对。
4.2 时钟树未综合导致CEQ大量不匹配
做RTL vs Gate比较时，综合网表里没有时钟树，只有理想时钟，一般问题不大。但做Gate vs Gate、特别是ECO网表和参考网表来自不同PR版本时，时钟树结构可能差异很大，工具在比较寄存器输入的逻辑锥时会把时钟树上buffer的逻辑也纳进去。
这种情况下，即使功能逻辑完全一致，也会报出一堆non-equivalent。处理方式不是去改网表，而是在脚本里显式告诉工具哪些时钟网络不需要验证：
set_dont_verify_subgraph -module clock_root_buf set_dont_verify_subgraph -pin u_duv/clk_gate_inst/CLK更稳妥的办法是用add_clock_as_point把时钟树的leaf都作为时钟点，让工具把时钟网络单独处理，不要混进数据逻辑锥。另一个我常用的做法是：先检查两个设计的时钟结构是否一致，用report clock details输出每一个寄存器的时钟pin对应的时钟源。如果两侧时钟源一一对应，再考虑是否需要排除时钟树buffer。
4.3 黑盒设错引发的“等价”假象
黑盒是把双刃剑。设置正确可以大幅减少逻辑锥，跑得快；设置错误就是给bug开了后门。
我见过最典型的一次：两个网表里都有同一个第三方DDR PHY IP，参考设计里这个IP内部有bug修复逻辑，实现网表里由于ECO把这部分逻辑删掉了。按理说两边功能已经不等价，但脚本里直接把这个IP整体add_black_box，工具只比较接口，当然显示等价。结果这个项目就带着功能差异走完了后续流程。
正确做法是：第三方IP尽量保留在一个明确的验证层级下，先做模块级LEC，再在芯片级决定是否黑盒。如果芯片级不跑该IP，至少在模块级必须证明过。对于客户IP，我还习惯把IP版本号通过read_design -root后的命名路径放进脚本注释里，保证每次跑LEC时能追溯两侧IP版本是否一致。
4.4 内存阵列与DFT逻辑的特别处理
Memory在LEC里是个特殊存在。很多数字项目用compiler生成SRAM，内部有无数的bitcell和冗余修复逻辑。把这些逻辑全部做等价性比较不太现实，通常会把memory模块整体声明为黑盒，只比较地址、数据、控制信号接口处的外围逻辑。
但这里有个细节容易忽略：memory在实现网表里可能被打散成多个叶节点，比如BIST逻辑、redundancy register、ECC校验位都挂在memory周围。如果仅仅对memory cell阵列黑盒，外围BIST逻辑没有被声明，工具会把整个memory wrapper内部的时序逻辑拿来做比较，速度慢不说，还常常因为命名差异大报一堆假错。
我的做法是分两步：第一，module级把memory_bist_wrap整体黑盒；第二，如果ECO改动只涉及memory周边的某个小逻辑，那么手动指定该小逻辑的输入输出点作为compared points，让工具只检查这一段。这样既避免了黑盒范围太大把真实差异盖掉，又不会让工具挑战整个memory内部结构。
DFT逻辑的常见处理包括：
scan_en、scan_mode、test_mode等测试信号，在功能模式下固定为0或1，用set_constant固定。scan_in、scan_out、shift_enable等pin可以加入add_ignored_points或add_ignored_outputs。- 部分DFT压缩逻辑（如XOR tree）可能改变了寄存器到输出的拓扑结构，但功能模式下它们处于透明模式，需要用
set_dft_configuration或手工排除。
这里一定注意：DFT信号是否固定以及固定到哪个值，必须和function mode的约束一致。不要凭印象写死，否则会把真实的时序约束错误掩盖掉。最好在脚本里写上注释，说明每个constant信号的来源（来自SDC约束或DFT spec）。
5. 让LEC从“能跑”到“跑得稳”的实用经验
5.1 命名规范与模块拆分
LEC跑得稳不稳，很多问题不是出在工具使用上，而是出在设计命名规范上。综合时如果设置了change_name规则，把RTL里的寄存器名加了一堆前缀后缀，后端PR又加了一堆buffer，两个网表的映射难度会成倍增加。
如果项目早期就能让前后端对命名规范达成一致，LEC会轻松很多。具体建议：
- RTL中的寄存器、输出端口命名尽量在整个项目周期内保持稳定，不要因为模块重构随意改。
- 综合脚本中禁止不必要的改名，确需改名时保留映射文件，作为LEC脚本的一部分提交。
- 后端工具在place时改名要有规则可预测，比如统一用
_reg作为寄存器实例后缀，用_dup表示复制寄存器。 - LEC脚本中使用
set_name_mapping -type register -mapfile维护一份历史映射，方便ECO后快速匹配。
这些规范看似与验证无关，实际影响巨大。我见过一个团队在综合时开了比较激进的寄存器合并和重新命名，结果LEC unmapped point有上千个，手动修映射修了一周，最后发现其中一个手动映射点是错的，导致整个签核结果失去意义。
5.2 报告核心字段怎么读
很多初级工程师跑完LEC只关心屏幕上有没有出现Verify SUCESSFUL，这个习惯很危险。Conformal LEC的报告要系统性看，不能只看最终状态。我通常按下面的顺序扫：
| 检查项 | 期望结果 | 出现问题时的动作 |
|---|---|---|
| library cell count | 与std cell库数量一致 | 重新读库，检查库格式 |
| mapped point比例 | >99% | 检查unmapped点并逐个确认 |
| compare point数 | 在预期范围 | 对比两侧逻辑锥数量 |
| non-equivalent点 | 0 | 分析逻辑锥差异，确认是否真错 |
| abort点 | 0或可解释 | 若abort多，需要拆分逻辑锥 |
| black box数量 | 与声明一致 | 确认黑盒范围没有缺漏 |
| floating pin | 0或可解释 | 检查网表是否完整 |
report compare data里的Verified列是工具已经证明等价的点，Not Verified包含unmapped和abort两步，这两个状态都不能作为绿色Pass。一份可签核的报告应该是：所有通路上可比较的点都是equivalent，不可比拟的点要么有明确理由（比如黑盒），要么已经由其他手段验证过。
另外，report non-equivalent points输出后，建议把错误路径定位到reference里的逻辑锥，用report cone之类的命令展开前后级，再针对性地看网表。快速判断是真实功能diff还是工具识别问题：真实diff通常表现为某个寄存器D端逻辑的布尔表达式两侧无法化简一致；工具识别问题通常伴随unmapped或时钟结构差异。
5.3 回归与签核时机的把握
LEC不是只跑一次就完事。我的习惯是在这几个节点各跑一轮，并且把脚本和结果都纳入版本管理：
- 综合后RTL vs Gate，确认逻辑综合没有引入功能变化。
- DFT插入后Gate vs Gate，确认扫描链和测试逻辑没有破坏功能路径。
- 时钟树综合后Gate vs Gate，确认CTS的铁树逻辑没有影响功能时序路径。
- ECO改动后，用EVO脚本或手工网表对比确认ECO正确，同时保留SVF文件供下次参考。
- 最终signoff前，再完整跑一次全芯片LEC作为存档。
每个节点侧重点不同。综合后的LEC更多是抓综合工具配置错误，比如set_ungroup导致模块边界变化、接口常数被优化掉；DFT节点的LEC重点在于测试信号处理；CTS后的LEC要关注时钟树结构；ECO后的LEC则要加倍关注手动改动的部分。
签核时不要把LEC单独当唯一依据。我的原则是：LEC必须跑，且必须跑到每个节点全部通过，但LEC之外的formal property、仿真回归、时序收敛一样都不能少。它们各管一段：LEC证明功能一致性，property验证功能正确性，仿真验证场景行为，PR保证时序。少了任何一块，流片风险都会往上走。
最后再分享一个小习惯：每次跑完LEC，我会把report compare data、report unmapped points和report abort points三个文件连同脚本commit到代码库，并且在comment里写明“结果状态是否允许下一步”。这个做法让我们在事后追溯“当时为什么能签这个网表”时，几秒钟就能找到完整证据链。很多项目出问题后找不到是哪个ECO引入的，就是因为LEC的中间过程没有被完整留存。你现在把这一步做扎实，后面省下的可不止是排查时间。
