两年前我遇到过一件挺打脸的事。后端团队交回来的网表前仿后仿全过时序也签了结果芯片回来一跑功能测试某条关键链路直接罢工。倒查了两周问题出在一个不起眼的ECO——手动替换buffer的时候改错了一个本该保持原逻辑的连接时序修好了功能却悄悄变了。从那以后我给自己立了条铁规矩任何网表级改动签核之前必须补一次Cadence Conformal LEC。LEC这东西表面看就两步Setup Mode里把两个设计装进去然后点Compare但真正把它跑明白、跑出可信结论里面门道不少。这篇就按我日常项目的实际流程从Setup Mode一路讲到Compare说说Formal Check到底该怎么个搞法。1. 为什么最终还得回来跑一遍Formal Check——LEC在流程中的位置1.1 一次ECO事故引出的教训那次ECO本身不复杂版图出来之后发现一条路径的hold违例后端同事在网表里给某个buffer前面又串了一个delay cell。按说这种操作不会碰逻辑功能可问题恰恰出在我以为的地方——那个buffer在一个多路选择器的选通路径上同事修复的时候顺手把网线的连接关系改掉了功能变成了另一条通路。为什么前仿后仿没发现因为激励向量没覆盖到那条配置组合功能测试又只跑了几个典型用例。等芯片回来某个寄存器在特定配置下被写进了错误的值故障才浮出来。这事的教训很直接**动态仿真只能证明“你测过的情况没问题”证明不了“所有情况没问题”。**而LEC这种形式验证工具恰恰是拿数学方法去穷举所有输入组合的可能性从根上补上动态仿真的盲区。尤其是后端ECO、扫描链插入、时钟树综合前后的网表改动逻辑上任何一个微小的偏差都可能变成芯片量产后的灾难。1.2 LEC到底在验证什么它和仿真、文本对比不是一回事Cadence Conformal LEC全称Logic Equivalence Checking逻辑等价性检查。它的工作模式是给你两个设计一个叫Golden参考设计通常是RTL或者修改前的网表一个叫Revised实施设计通常是综合后网表、布局布线后网表或者ECO后的网表工具通过比对逻辑锥的方式证明两个设计在所有可能的输入组合下输出行为完全一致。这里的“所有可能输入组合”不是仿真器跑几百个pattern而是用形式化引擎比如BDD、SAT这类算法对布尔逻辑做严格推导所以它叫Formal Check。这里我要专门提一句LEC的Compare跟大家在Windows下用的Beyond Compare那种文件对比工具完全是两个概念。Beyond Compare是逐行diff文本看的是文件内容差异LEC比较的是电路功能看的是布尔函数是否等价。网表和RTL本来就不是同一个文本层次用文本diff来看两个设计除了能看到“不一样”之外什么结论都得不到。真正能拍板的是逻辑等价性检查。1.3 哪些环节必须安排LEC就我经手的项目来说下面这几个节点LEC是雷打不动的RTL综合后网表综合器做了大量的组合逻辑优化、寄存器合并、门级映射RTL和网表之间的对应关系已经面目全非必须用LEC确认功能等价。布局布线后网表PR工具会插入buffer、修复hold、做时钟树这些操作理论上不改变功能但工具毕竟是工具偶尔也会有意外回到LEC查一遍心里才踏实。DFT插入前后扫描链的插入会改寄存器的连接方式需要确认功能模式下不退化。ECO前后网表不管是前端改RTL重新综合还是后端手工改连线ECO前后必须证明“我只改了想改的地方”。时钟门控插入和优化前后这类结构性改动最容易在形式上出幺蛾子。2. Setup Mode 其实决定了大半个结果——库、设计与映射规则怎么配2.1 库环境先理干净少读一个库后面全是莫名其妙的abort很多人第一次跑LEC上来就把两个设计load进去然后直接点Compare结果看到一堆abort和failed瞬间心态崩了。实际上**LEC的大多数诡异结果根源都在Setup阶段埋下了。**第一个最容易埋雷的地方就是库。LEC要理解Revised网表里的门级cell必须知道每个cell的逻辑功能。这些功能一般来自三种格式Liberty的.lib文件、Synopsys的.db二进制库或者最常见的Verilog model。项目中规范的库环境会同时提供.lib和.v模型LEC读库时优先用带功能描述的模型如果库里只有物理版图信息没有逻辑功能定义工具就只能把这个cell当成黑盒处理——黑盒一多它后面的逻辑全部没法验证表现为大片abort或者“unrecognized cell”的警告。我的习惯是在Setup Mode下先单独把库读一遍用report_library或者GUI里Check Library的功能确认所有cell都被工具识别了。重点检查Memory Compiler生成的SRAM/ROM库、模拟IP库这两类最容易被漏掉或者版本不匹配。版本不匹配也容易出问题比如综合用的库和LEC用的库不是同一套cell功能描述对不上那么等价性结论根本没有意义。在读库上偷的懒后面十倍的debug时间都补不回来。2.2 装载设计的顺序和方式golden、revised与顶层识别库准备好之后再装载设计。GUI操作上你先要在主界面切到Setup Mode不同版本叫法略有差别新版一般在工具栏上有模式切换按钮然后通过Import Design或者Read Design菜单分别指定Golden和Revised。Golden选RTL文件还是旧网表取决于你这次LEC验证的目标Revised选新网表。装载时的顶层识别非常关键。如果工程是多层次设计LEC默认会用design hierarchy里的某个特定焦点比如整个模块的顶层也可以手动指定。我通常会在命令窗口或者GUI里明确设置set_root_module指到要验证的顶层模块避免工具默认选错。比如你只想验证某个IP核的ECO那就应该在这个模块级别做LEC而不是拉上整个SoC否则后面的compare point会多到爆炸编译时间和内存都扛不住。这里还有个容易忽略的点网表里如果还有尚未实现的黑盒子比如某个子系统还没有综合只有空的module声明LEC会把它们当成undefined design默认当作黑盒。这时候你要明确告诉工具哪些是预期的黑盒。如果没设有些场景工具会报error直接停下来有些场景会静默把它当黑盒——但你在最终报告里看不清这个处理就容易产生误判。2.3 别忘了SVF把综合过程信息喂给LECSVF是Cadence Conformal LEC里一个怎么强调都不为过的文件。全称Setup Verification File也常叫guide file一般由综合工具在综合时输出。综合工具在优化过程中做了大量结构性变换比如把mux优化成AOI门电路、把寄存器重命名、把某些组合逻辑擦掉重画这些变换如果LEC完全不知道它就得靠纯逻辑推导去重新匹配耗时长不说匹配率也不好看。SVF的作用就像一张“变形地图”综合工具告诉你“我把这块结构改成那样了中间经历了这些步骤”LEC拿到这些提示后能大幅提升寄存器匹配率和运行速度。在Cadence Genus里综合脚本里一般有一条write_lec或者类似命令生成SVF文件Synopsys综合工具也有对应机制要提前在综合流程里打开这个开关。实际操作中我在Setup Mode里读完设计之后马上做的一件事就是add_svf指定SVF路径。跑之前再确认一次版本SVF必须和本轮综合和本轮网表对应网表和SVF不一致比没有SVF还坑。2.4 常量与初始值设置让工具知道功能模式长什么样第三个关键配置是常量与初始值。LEC一般是在功能模式下做等价性验证所以那些只在测试模式、扫描模式下会翻转的信号在功能模式里应该被固定下来。比如scan_enable、scan_shift、某些debug复位信号在功能仿真里总是0或者1那么在LEC里你也应该告诉工具这些恒定值否则工具会认为它们可以取任意值逻辑锥变复杂匹配率下降甚至出现假fail。在Cadence LEC里这种约束通常用set_constant命令设置比如把scan enable固定为0、把异步复位固定为释放状态。设置完还要看约束是否真的生效有的设计里这些信号在门级被接在了某些cell的使能端上如果常量没生效后面Falcon引擎会比较出奇怪的不等价。还有一个点是寄存器的初始值如果RTL里寄存器有上电复位值而门级网表里对应的复位端接到了实际的reset树那么建LEC环境时要确认两者语义一致避免因为“初始状态不一致”而报错。2.5 Setup完成后的自检先看警告再谈Compare以上配置都做完我一般不急着进Compare而是先看一眼Setup阶段的日志和报告。重点筛查几类警告某个模块被黑盒化、某些端口没有驱动、某些寄存器unmatched、某些常量约束被忽略。这些信号会直接告诉你你在Compare阶段将会看到什么样的结果。在Conformal LEC里Setup之后一般会生成一个关于设计信息和未定义单元的报告GUI里在报告窗口也能看。只要看到“unmatched register超过预期”“黑盒数量异常”这类现象就别往下走了先回头把Setup的问题解决掉。**记住一个原则Setup Mode阶段做的越干净Compare阶段就越安静。**干净的环境Compare跑完应该是少量明确异常点而不是一片红色。3. 把两个“状态”拉到同一起跑线——Compile阶段在做什么3.1 compile不是优化后端而是化简逻辑锥在Setup完成到Compare开始之间还有一个Compile步骤。有些人不理解这个步骤的意义觉得就是个形式上的过渡。实际上Compile阶段LEC会把Golden和Revised两个设计分别做内部的化简和重构把比较的对象由整个网表拆成一个个逻辑锥logic cone。每个逻辑锥的起点是对齐的比较点比如寄存器的D端、顶层输出端口终点是驱动它的组合逻辑工具随后对每一个锥做布尔等价比较。你可以把它理解成要把两篇文章比出是否讲同一个事先把每句话的主谓宾拆出来再去逐句比对。Compile就是那个“拆句子”的过程。所以Compile质量高不高直接决定后面Compare每句话比对得顺不顺。3.2 名称映射与匹配模式的设置Compile阶段最先需要注意的是名称映射策略。Cadence LEC有很强的名称匹配机制它不要求两个设计里寄存器名字一模一样而是可以通过一系列映射规则把它们认识成同一个点。比如综合工具对RTL里的寄存器起了新的名字SVF会告诉LEC怎么对应又比如网表里有reg_A_reg[0]这种带位宽后缀的名字LEC可以通过bus名字简化来匹配。我碰到过一种情况两个设计之间其实逻辑等价但因为Golden里某个寄存器叫data_qRevised里被综合成了data_q_reg没开模糊匹配或者没加SVF工具报unmatched。这时候不必慌可以在Compile之前检查一下映射设置或者直接回顾是不是SVF没加对。绝大多数名称匹配问题根子在SetupCompile只是在执行。反过来如果SVF正确名称映射还是大面积失败那我建议你检查综合工具版本和LEC版本是否兼容——这种问题以前困扰了我很久升级统一版本后豁然开朗。3.3 层次压缩与黑盒化的取舍Compile阶段的另一个选择是层次化压缩。Conformal LEC支持层次化比较和扁平化比较工程上常用的是先把公共子模块压缩掉compression只比较受影响的部分。对于大型SoC这个功能几乎是必须的不然整个设计展开成扁平逻辑锥内存占用会非常夸张。黑盒化的取舍也在这里体现。我前面提到memory和某些模拟IP如果它们的功能模型或者库没有完整读进来LEC在Compile时只能把它们当成黑盒。对于SRAM这类单元只要两端用的库一致黑盒化通常不影响等价性验证的结论因为逻辑等价要求的是焦点逻辑的等价黑盒两边一致就够了。但对于随机逻辑模块如果被黑盒掉它输出后面的整个逻辑锥都无法验证那就不是一个合格的结果。3.4 编译后的报告怎么读寄存器匹配率是关键指标Compile跑完之后工具会生成关于匹配情况的报告我最关心的是寄存器匹配率。正常情况Golden和Revised的时序单元匹配率应该达到接近100%剩下几个没匹配到的要么是有意重命名或合并要么是黑盒边界。如果匹配率只有90%甚至更低别急着Compare这就是明显问题。匹配率不理想时先查这样几件事SVF有没有漏加载或者版本对不对是不是用了set_mapping手动指定映射却没写对或者是否存在memory integrated方式不一致的情况。还有一种常见的两个网表之间做了retiming寄存器重定时比如一个组合逻辑在两段寄存器之间挪了位置这种改动如果不通过SVF或者设定告诉LEC它会认为大量寄存器接不上。寄存器重定时场景下LEC其实可以处理但前提是编译选项里开了对应的模式比如允许sequential compare。所以编译报告里的“匹配率”其实是你整个LEC环境健康度的体温计。4. Compare不是一键点完就完事——结果解读与常见失败模式4.1 compare后先看summary启动Compare之后工具会调用Falcon引擎跑逻辑锥的比较这一步可能需要几分钟到几十分钟。完成后第一件事看整体汇总。正常的理想结果是全部match、零fail、零abort。如果带格式地的工程出现少量fail或者abort而你又不了解原因那就逐项去翻报告把它们当成需要解释的对象。另外LEC的Compare结果目前是按“compare point”分类的包括端口Primary Output、寄存器D端、黑盒输出。在报告里找到对应的点后可以用GUI里的Cross Reference或者逻辑锥图把失败的比较点对应回两边的原理图和RTL代码。这一步一定要会因为它比你在Verilog里grep半天高效得多。4.2 定位到具体逻辑锥用原理图连回代码当某个比较点fail了LEC的GUI会给你提供对应逻辑锥的原理图/示意图同时可以交叉映射回RTL或者网表的具体位置。我的排错路径一般是先看这个失败的点是哪个信号、哪个寄存器然后看它所在逻辑锥里Golden和Revised的布尔表达式是否真的不一致。有时候报告里会直接给出两边表达式化简后的差异这时候一眼就能看出多了一个反相器、少了一个与门之类。如果差异比较抽象可以用Debug Mode反向追踪每个输入变量的取值对结果的影响一点点缩小差异范围。这个过程有点像侦探破案但很吃经验做得多了扫一眼流程图就能判断是约束问题还是真功能错误。4.3 fail要先分环境问题和真实问题我在前面反复强调Setup的重要性就是因为**Compare阶段的fail有相当大比例其实不是真实的功能差异而是环境设置不一致导致的假失败。**遇到fail不要慌先做一个Z-Type分类是X态传播、常量设置不同、跨时钟域CDC逻辑还是真正的Boolean不等价。一个实用的办法是把fail了的比较点随机挑几个回到Setup环节看有没有共性。如果一批fail都集中在某个模块、某个时钟域、某个扫描相关信号附近那基本可以判断是约束或者环境问题。如果fail点分散在各处且彼此没有相关性那就要认真怀疑是否真的有逻辑不一致了。下面是我常用的一个失败原因初始分类表帮你在看到结果时快速定位方向失败类型常见根因优先排查方向大量fail集中某个时钟域时钟约束/时钟门控设置不一致检查时钟定义与常量约束fail集中在扫描相关信号scan使能/扫描链复位设置缺失检查set_constant、扫描约束fail导致逻辑锥很短黑盒或未识别cell检查库完整性、黑盒定义fail对应RTL里x赋值X态处理策略不同检查X态选项或set_constant单个孤立fail真实逻辑差异进入Debug模式做逻辑锥对比大量abort结构复杂度高或引擎无法处理检查SVF、编译选项、引擎选择4.4 几个典型失败案例与标准解法案例一时钟门控。RTL里用if(clock_enable) begin ... end综合后综合器把它映射成一个ICGIntegrated Clock Gating单元。LEC处理这种结构时Golden这边是寄存器配一个使能MUXRevised这边是ICG cell的TE端。两边表现形式完全不同工具如果没识别ICG特性就会报fail。遇到这个先确认库的功能模型是不是标准ICG建模再查一下工具有没有对应的处理选项让引擎明白它们其实是等价的。案例二常量传播差异。我在某个项目里遇到一批fail最后发现是RTL里的一个输入端口本来直接接到了0但综合后的网表里这个pin仍然由顶层pad驱动并没有实际接0。两边逻辑锥一个带常量0一个是自由变量当然不等价。这种问题本质上是在RTL仿真和门级仿真里都不会错但LEC会较真——因为形式验证就是穷举所有情况它不接受“这个pin永远不会变”这种假设。解法也简单就是加一个恰当的常量约束把该信号在功能模式下固定住。案例三DFT插入错误。扫描链插入改变了寄存器的连接方式如果DFT工具在插入扫描链时不小心把某个D端逻辑改掉那么功能模式下LEC会立刻抓出来。这是比较“真”的fail处理起来就是回到DFT的ECO环境去修不要试图用约束把它绕过去——绕过去等于放弃验证。案例四多驱动和tri-state。有些pad或者双向IO在RTL里是三态描述到了门级变成多个输出驱动同一个net。如果LEC没有正确读懂三态语义会把多驱动看成X冲突然后就报出一堆fail。这种情况通常要在LEC环境里对IO或者bus设定合理的驱动模型或者把非活跃驱动设成高阻。否则就算真实电路没问题工具也会认为两个设计不等价。4.5 abort比fail更值得警惕最后特别说下abort。Fail表示工具明确判断不等价abort则表示工具搞了半天无法在当前资源限制下得出结论。abort在LEC里是灰色地带它不代表pass也不代表fail但它比fail更容易被白白忽略。因为业界很多人看到“没有fail”就默认全绿这是大忌。处理abort的方向有几个先看abort的点是不是集中在某个复杂度极高的结构比如大的乘法器、大的地址译码器可以尝试调整引擎设置LEC有多种引擎有些适合算术比较有些适合随机逻辑也可以加大运行时间和资源上限。如果还不行就要考虑把逻辑锥切小一点或者从设计层面去看为什么这个锥这么复杂。总之abort必须被“处理”成一个可解释的状态最后报告里不能带着一堆未解决的问题去签核。5. 从Batch脚本到签核报告——把LEC跑成可靠流程5.1 一份可复用的TCL批处理脚本骨架等你在GUI里把流程跑通、跑明白之后真正的日常迭代会用到批量命令行方式。同一个项目每天改几行网表就要重新跑一遍LEC谁有耐心天天点界面我习惯维护一个相对固定的TCL脚本核心流程如下细节根据项目改# log set_log_file ./lec.log # library read_library -file ./lib/std_cell.lib read_library -file ./lib/sram_256x32.lib # load design read_design -golden -rtl -filelist ./rtl_filelist.f read_design -revised -verilog -filelist ./netlist_filelist.f # top set_root_module top # svf from synthesis add_svf ./syn/top.svf # constants for functional mode set_constant scan_en 0 set_constant rst_n 1 # compile and compare compile compare # report report_compare_data -report ./out/compare.rpt report_abort_data -report ./out/abort.rpt这段脚本是示意写法不同LEC版本的选项措辞不完全一样但主线是一致的日志→库→设计→顶层→SVF→常量→编译→比较→报告。注意我没有用中文注释里的“rtl”选项细节具体以你项目里已有的do file为准直接改路径和文件list即可。跑批量脚本时一定要盯住退出码和log里的error关键字别让脚本“看起来跑完”就以为成功了。5.2 修完ECO后的增量重跑思路ECO之后跑LEC我一般不直接打开整个设计重新全量Compare而是先确认ECO到底动了哪些地方。Cadence LEC有比较并输出两个网表差异的功能你可以先做增量分析把ECO涉及的逻辑锥单独列为重点对象。这能大幅缩短周转时间尤其当设计上千万门全量跑一趟要几个小时的情况下。当然增量跑的前提是你能明确界定受到影响的区域而且你的改动足够局部。如果ECO牵扯到顶层模块接口的修改、寄存器增加或删除那么该全量跑还是全量跑不要为了图快把验证精度牺牲掉。签核这种东西宁可多花两小时也不能给流片留一丝不确定。5.3 报告与日志归档让结论可追溯LEC跑完不是自己看一眼就算完还需要把报告和日志留下来作为签核材料的一部分。我的习惯是每次跑完自动归档一套文件LEC的TCL脚本、完整log、compare report、abort report以及运行环境和库版本记录。这样任何时候有人问“这个版本的网表跑LEC了吗、结果是什么”我能直接拿出一整套可回溯的数据。归档格式上文件命名里带上时间戳和网表版本号比如lec_top_20250511_v3.2.rpt。判定的结论必须体现在报告里全部match、或者有fail但已经逐项document并确认不影响功能模式。这类材料在项目评审、客户审计和高层review时会非常有用千万别临时再补跑。5.4 个人经验这几个地方最容易犯浑最后集中说几个我踩过的坑希望你看完能少走几趟弯路。第一别忽视Setup阶段的warning。很多人跑LEC只看Compare的最终结果中间一堆warning当没看见。事实是那些warning通常预告了后面的问题。宁可前面多花十几分钟把warning逐条看过也不要等Compare跑完再痛苦debug。第二库文件的版本一致性怎么强调都不过分。综合库、PR库、LEC库三者必须来自同一套工艺和版本。我见过一个项目LEC用的是老版本库里面某个AOI cell的功能定义和新库对不上结果一片逻辑全报不等价浪费了一整天。第三区分设计变更和验证环境变更。跑ECO前后的LEC时如果出现大量失败先确认是不是由于你在Setup里新增了某种约束或者换了SVF版本导致的而不是网表真的有问题。验证环境自身的变更必须和设计变更分开排查。第四对abort保持敬畏。我看到太多团队report里的fail清干净了却留着一堆abort说是“工具算不完”这跟没验证基本没区别。正规流程里每种abort都要有成因解释能消除的尽量消除。Cadence LEC这套工具用熟练之后其实会上瘾。它给你的不是一堆仿真波形而是一个可以用数学保证的“等价”结论。拿一次真实项目经验来说有一次前端改完RTL综合后跑LEC报出某条路径不等价前端看了半天RTL觉得没问题最后发现是综合工具没完全遵守某个keep语句——如果没有LEC这道关卡这个bug大概率会带着进流片。做数字IC确认“形式等价”这一关永远值得你认真对待。