前阵子我一朋友负责的芯片回片后功能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 abortabort点表示工具由于逻辑锥太大或匹配点太复杂没能完成证明这部分不能直接签核。3.4 黑盒、constant和dont 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 pin0或可解释检查网表是否完整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的中间过程没有被完整留存。你现在把这一步做扎实后面省下的可不止是排查时间。