做数字IC验证的朋友一定听过“Conformal LEC”这个名词。它全称是Logic Equivalence Checking逻辑等价性检查属于形式化验证Formal Verification里最基础、也是最实用的一类工具。简单说它拿一个功能正确的参考设计Reference通常是综合前的RTL再拿一个经过综合、扫描插入、时钟树综合甚至ECO修改后的实现网表Implementation用严谨的数学方法去证明两个设计在所有可能的输入组合下输出逻辑完全一致。在芯片项目里LEC的地位几乎和时序收敛并列。后端工程师改时钟树、修eco、动扫描链每做一步都要跑一遍LEC确认逻辑没被改坏。但凡某个点报Fail芯片流片回来大概率是废片。所以LEC不是“可跑可不跑”的辅助检查而是Tapeout前的头号质量关。这篇内容我尽量按照“先懂原理再讲实操最后讲踩坑”的节奏来写面向刚接触LEC的验证工程师、对形式化验证感兴趣的后端工程师以及想系统性了解LEC流程的IC学习者。全程站在这几年一线项目经验的角度把从环境配置、约束文件写法到Fail点调试的完整过程拆开讲清楚。1. 内容整体设计与思路拆解1.1 为什么要做等价性检查动态仿真的盲区做功能验证的时候大多数人习惯用仿真Simulation灌激励、比对波形。但仿真有一个天然缺陷你只能证明“你灌过的那几条激励是对的”不能证明“所有激励都对”。芯片里动辄几百万个触发器、上亿个组合逻辑节点输入空间完全跑尽了宇宙毁灭都跑不完。那综合工具、时钟树工具改过的网表怎么确认功能没被改坏靠仿真灌用例效率太低尤其在时钟树综合之后网表里多了几百个ICG单元Integrated Clock Gating集成门控时钟单元仿真模型复杂、速度慢还需要额外的时序约束才能跑得动。LEC的价值就在这里它不依赖激励而是通过形式化引擎把参考设计和实现设计做数学级的等价性判定。等价性检查的过程相当于把两个个设计“在逻辑函数层面画等号”只要函数一致无论内部结构怎么翻新结论都是Pass。项目中的通行做法是动态仿真在RTL阶段重点验证功能综合阶段之后全面转向LEC做等价性验证。这两种手段一个负责“验功能对不对”一个负责“验功能有没有在实现过程中被改坏”互补关系非常明确。1.2 LEC的核心定位网表转换过程中的“守护者”LEC在数字后端流程里最常见的应用是综合后的功能确认、时钟树综合后的功能确认、ECO修改后的功能确认。这三件事的核心都是回答同一个问题“网表在这步改动之后还是不是原来那个函数”拿ECO举例后端基于金属层的ECO修改往往只改了几根连线或几个标准单元工程师有意为之。但改动过程中工具可能会通过Spare Cell备用单元替换、逻辑重组、布线连通性变化等操作引入非预期差异。如果只靠Diff文件比对网表那些“看起来不同但功能相同”的变化会报出一大堆误报如果完全不管又怕“看起来没改但逻辑变了”。LEC恰恰能把“结构差异”和“功能差异”严格区分开结构上怎么改都行只要函数等价。所以LEC的定位总结成一句话它是贯穿综合、物理实现、ECO全过程的形式化安全网专门盯住“逻辑一致性”这条红线。1.3 文章参考范围的说明这份攻略以Synopsys Conformal LEC工具为主流程版本横跨近几代主流的LEC版本。文中涉及的命令、选项、报告格式基于我实际用过的典型版本环境编写不同版本之间可能略有差别但核心流程和排错思路大体通用。2. 核心概念拆解Reference、Implementation与映射2.1 两个设计之间的“翻译官”Key PointLEC最关键的思路就是先找到参考设计和实现设计之间的“共同点”再比较从这些“共同点”到输出之间的逻辑函数。这些共同点叫作Key Point也有人叫Compare Point比较点。通俗地理解可以把参考设计看成一份标准答案把实现设计看成考生作答的试卷。LEC要做的是找出试卷和标准答案里都有的“题号”Key Point然后逐题核对答案。如果所有题目答案都一致考试就通过了。Key Point一般包括主输入Primary InputPI比如芯片的输入端口主输出Primary OutputPO芯片的输出端口触发器DFF时钟沿驱动的存储单元锁存器、三态门等特殊存储节点黑盒Black Box的输入端和输出端。在这些共同点上LEC会比较参考设计和实现设计的功能而共同点内部的逻辑结构不管你怎么综合、优化、重组工具都不关心。所以LEC的效率远比“逐节点比对网表”高得多它把大问题拆解成若干小问题逐一证明。2.2 常见术语扫盲SVF、黑盒、Cut Point真正用Conformal LEC你会反复遇到下面几个术语提前理解比硬背命令重要得多。SVF文件Setup Verification File综合工具或物理实现工具在转换设计的过程中自动记录了各种名字映射关系、常量寄存器信息、扫描链信息等。LEC读入这些信息可以大幅度提高映射成功率。这个文件由DC综合时的write_svf命令或者后端工具的相应命令产生是连接综合工具和形式化验证工具的“翻译词典”。黑盒Black Box当某个子模块的详细信息不可见时LEC只能把它看成一个功能未知的盒子只保留它的输入输出端口。典型场景是第三方IP、存储器编译器生成的SRAM、模拟宏单元。黑盒会影响验证的完备性因为从黑盒输出往后的逻辑无法做到“结构无关的等价性证明”所以在条件允许的情况下黑盒越少越好。Cut Point切割点当某些内部节点的映射不明确或产生大量无效比对时工具会把一个内部节点当作临时的“等价点”就像在逻辑锥中间切一刀把一个大锥拆成两个小锥来证明。这个机制非常有用在时序逻辑相互变换较多的时候经常能解决阻塞问题。Unmapped Point未映射点参考设计和实现设计里有部分节点没有互相找到对应关系。这种情况一般会伴随Fail或者Abort是排查的重点区域。2.3 竞赛流程的本质把问题拆小不需要把LEC的内部引擎想得太玄乎。它的基本步骤是读入参考设计和实现设计根据网表名字、SVF文件、名称映射规则把两边的Key Point对上在每对Key Point上建立一个“逻辑锥”Fan-in Cone即从该点往前追溯到PI或DFF输出端的组合逻辑区域用BDD二叉决策图、SAT布尔可满足性问题求解器等引擎判断两个锥体代表的布尔函数是否相同输出Pass、Fail或Abort结果。这套思路最关键的一点它不是把两个设计整体去做等价性比对而是一对点一对点地证明。因此任何一个点报Fail都能精准定位到具体的逻辑锥调试范围非常小。3. 全流程实操从环境准备到拿到Pass3.1 数据准备需要哪些输入文件跑LEC前先把输入文件搞定。常见清单如下文件类型内容来源Reference设计RTL代码或综合后的参考网表代码仓库 / 项目交付Implementation设计综合后网表、CTS后网表、ECO后网表后端工具SVF文件设计转换过程中的映射关系和约束信息DC / Genus / 后端工具库文件标准单元库.db或. lib格式、IP库Foundry / IP供应商约束文件SDC约束、LEC专用的guide/constraint文件前端/后端协同实际项目中Reference设计通常就是综合用的RTL。有些场景会用“综合后网表当作Reference”再用“ECO后网表当作Implementation”做法一样谁功能是“基准”谁就是Reference。库文件必须同时包含逻辑功能描述和单元信息。注意读库的时候库里的连线延迟、单元延迟对LEC没有意义LEC只关心布尔逻辑功能和状态行为。3.2 第一次运行一个最精简的LEC脚本拿一个最简单的例子假设RTL顶层叫soc_top.v综合后网表叫soc_top_syn.vSVF文件叫soc_top.svf。LEC脚本可以写成这样# 设置日志文件和结果文件 set log file lec.log -replace set result file lec.result -replace # 指定库文件 set search_path ./lib ./rtl ./netlist read_db -technology lib typ.db # 读入Reference设计RTL read_design -ref -verilog ../rtl/soc_top.v -define {SYNTHESIS} -root soc_top # 读入Implementation设计综合网表 read_design -impl -verilog ../netlist/soc_top_syn.v -root soc_top # 设置SVF文件帮助映射 set_svf ../syn/soc_top.svf # 设置隐含的映射选项 set mapping mode parallel? auto set system mode lec add_compare_points -all run_lec report_verification_result -compare_point这段脚本里有几个地方值得说明read_db -technology lib typ.db这个库是标准单元库的“逻辑库”读进来之后LEC才知道网表里每个单元是AND门还是OR门是上升沿触发器还是下降沿触发器。-root soc_top的意思是只选择顶层模块做验证。如果设计里有子模块需要确认是整体比还是部分比。set_svf的时机没有严格规定必须在读网表之前还是之后一个兼容性最好的做法是先读设计再设SVF然后跑到映射阶段自动生效。add_compare_points -all表示让工具自动把PI、PO、DFF等都设置为比较点。在大多数网表验证场景中这就够了。跑完之后结果保存在result文件里同时在终端会打印汇总。一个纯Pass的结果一般会看到类似“All compare points are passing”或者“Verification Summary: Pass”。3.3 结果文件怎么看result文件里最关键的一张表是“Verification Result”它列出了每一类比较点的数量以及各自的结果归属Pass、Fail、Abort、Unverified。下面是一个典型的输出片段 Verification Result Reference Design: soc_top Implementation Design: soc_top_syn Mode: LEC Key Points: Primary Inputs : 128 Primary Outputs : 36 D Flip-Flops : 1024 Unmapped PI : 0 Unmapped PO : 0 Unmapped DFF : 2 Result: PASS : 1188 FAIL : 1 ABORT : 3 看到FAIL和ABORT先别慌也别急着改网表。90%的情况是映射、约束或环境配置的问题真正常见的逻辑不等价反而少。后面第4章会详细讲排查方法。3.4 用SVF和Guide文件提升映射率跑LEC时最头疼的事情之一就是“映射不完全”两边一大片DFF没有对应上。这个时候SVF文件的价值就体现出来了。SVF里最核心的信息包括名称映射表Name Mapping Table、常量寄存器Constant Register、未被逻辑重用的寄存器Deleted Register、扫描链和门控时钟信息等。读入SVF之后工具可以自动把参考设计里的寄存器名字对应到综合网表里的寄存器名字哪怕DC做了寄存器重命名、合并、常量折叠也能找回对应关系。在复杂的SoC项目里一般还会加一个Guide文件这是LEC侧手工声明的映射规则。常见写法比如add_name_mapping -ref { u_cpu/r_abc } -impl { scan_reg_123_/Q }当自动映射失败而你又确认真名对应关系时手动指定映射非常有效。提示SVF和Guide文件里的映射关系只起到“提速”和“辅助”作用。若映射错误之后跑的Pass结果也不可信。修改Guide文件之后务必重新查看报告中的映射数量。4. 常见问题与排查技巧实录4.1 Fail点排查首先排除“假Fail”碰到Fail我习惯的排查顺序是先看Fail点集中在哪些模块、哪些类型再看是否所有Fail点都连到某几个公共模块或某个黑盒再看是不是因为约束缺失比如某条路径被后端工具设为false_path但LEC没感知。有一个特别典型的“假Fail”场景Reference是RTLImplementation是综合网表综合时把某个常量寄存器优化掉了比如RTL里有一个寄存器的初始值一直是0DC把它替换成直接接地。此时SVF里会记录这是一个Constant Register。如果你没读SVF或者SVF不完整LEC会拿一个寄存器去比对一根地线结果必然Fail。解决办法也简单补一句话告诉工具这条线的逻辑是常数。在LEC里常见做法是读入SVF后它自动处理手工的话可以用add_constant_value -ref { u_dut/r_stuck_0 } -value 0还有一类高频“假Fail”是扫描链带来的。插入扫描链后DFF会多出SEScan Enable、SIScan Input端口还有正常功能输入D。LEC会自动把SE、SI当作额外输入但有些场景需要工具忽略扫描相关引脚。若报告中Fail点全部集中在扫描链相关逻辑上就要检查是否设置了对扫描相关约束的识别或者在add_compare_points阶段把扫描相关的比较点排除掉。4.2 Abort点排查当工具“算不动”的时候Abort不同于Fail。Fail是工具明确告诉你“两边逻辑不一样”Abort是工具算半天没有收敛在资源或时间用完的情况下放弃证明。有些同学一看到Abort就慌其实Abort不一定代表逻辑不等价也可能只是逻辑锥太大、解法过于复杂。处理Abort最常用的手段增大超时时间或内存限制把大逻辑锥用Cut Point切小对特殊结构做黑盒或约束处理调整引擎策略比如从BDD切到SAT或设置混合引擎修改比较粒度只比较出问题的子模块。实际操作中我经常用的一条是set system mode lec set compile verification force -abort_limit 3000这个abort_limit是控制单次证明的资源上限。调大之后部分原本Abort的点能转成Pass但代价是运行时间线性增加。如果调大上限后依然Abort又确认没有逻辑变化就需要考虑是不是该点所在逻辑锥创建了太多中间变量可以通过Cut Point来辅助。Cut Point操作示例add_cut_point -impl { u_dut/U_ADD_1/n1 } -type internal把它当成一个比较点来看待逻辑锥就会从这里断开前后各证各的。这个方案在处理乘法器、桶形移位器这类大规模组合逻辑时特别管用。4.3 黑盒处理不当导致“假Pass”比Fail和Abort更危险的是黑盒处理不当造成的假Pass。因为黑盒覆盖掉了内部逻辑工具只验证了黑盒连接的逻辑如果黑盒内部有改动LEC是感知不到的。我见过一个真实案例验证工程师把一块CPU子核在两边都设成了黑盒LEC报告全Pass团队就签核了。结果ECO时有人改动了该子核内部一个寄存器的极性没有同步更新黑盒设定最终流片回来功能异常。后来复盘就是因为黑盒太粗把改动藏在了盲区里。避免假Pass的几条经验黑盒清单要由前端和后端共同确认任何一方都不能单独拍板能精确到单元级黑盒的就不要把整个模块黑掉每次ECO后都要重新审视黑盒列表尤其是涉及改动的模块在报告中核对“Verified by BlackBox”或者“Unverified”点数量异常数量突然增加时警惕。4.4 ECO验证中常见的LEC误报与解决方法ECO网表验证是LEC应用的重灾区。后端经常做双孔金属ECO改完扫描链、时钟树之类然后拿ECO网表和综合后网表比时常会冒出一堆看起来“莫名其妙”的Fail。最常见的原因是时钟树综合后时钟偏斜和门控逻辑导致DFF的时钟引脚两边不对齐Reference侧DFF时钟来自理想时钟Implementation侧时钟来自ICG和时钟缓冲树。LEC对于时钟引脚的处理有一套默认规则但如果时钟逻辑太复杂工具可能无法自动找到对应关系。处理办法是给工具提供明确的时钟定义或者在比对时设置忽略时钟树的时钟结构差异set_constant -type clock -ref {clk} -impl {clk_leaf_latency_3}风格上不用照抄我这里核心是说清楚哪根时钟对应哪根时钟。这个方法在应对时钟复杂性时非常有效。另外一个ECO后常见的误报来自“dont care”状态。RTL里的case语句如果带有default条件综合工具经常利用这些dont care条件做逻辑优化。Reference侧未定义的行为在实现侧可能已经变成了具体逻辑。此时LEC报Fail其实是两边在未定义区域的行为不一致但这种不一致不影响芯片功能。解决办法是给LEC设置适当的约束告知特定条件下的输出不关心Dont Care。4.5 报告分析与GUI调试遇到复杂Fail光靠命令行日志效率偏低。Conformal LEC自带GUI调试界面可以通过start_gui启动也可以用report_failing_points命令把Fail点列出来。GUI里面最有价值的功能是原理图查看Schematic Viewer。点开任意一个Fail比较点它会画出两边从PI和DFF一直到该比较点的完整逻辑锥。鼠标点某个节点可以直接看它的逻辑表达式、电压值状态还能联动高亮比对两边的差异节点。这种可视化调试在定位“多了一个反相器”“少了一个与非门”“两根信号接反了”这类问题上比盯报告快得多。我个人的调试习惯先用report_failing_points -not_verified掌握Fail和Abort的总量再用GUI看1~2个代表性Fail点观察差异模式如果所有Fail点都表现为“同样一根信号在两个锥里极性不同”往往指向一个公共前级的极性异常如果Fail点散布毫无规律优先考虑约束和映射问题而非真实功能差异。5. 把LEC跑得更高效脚本与管理经验5.1 用DO文件管理复杂验证任务Conformal LEC支持把所有命令写到一个DO File类似Tcl脚本里项目里我的习惯是建三层结构setup.dofile定义库、路径、全局选项各模块共用design.dofile指定Ref/Impl的设计文件、SVF、Top名字按模块区分run.dofile定义比较点、运行选项、输出报告。这样每次验证后只需要改design.dofile几个变量即可效率和可维护性都提升明显。举例在顶层dofile里通过变量传入设计名set DESIGN soc_top set REF_FILE ../rtl/${DESIGN}.v set IMPL_FILE ../netlist/${DESIGN}_syn.v set SVF_FILE ../syn/${DESIGN}.svf source -echo setup.dofile source -echo design.dofile run_lec report_verification_result -compare_point -list5.2 一个比较完整的实用脚本参考这里给出一份简化但可实际运行的项目级参考脚本读者可以依据实际环境修改。# --------------------------------------------------------------- # Conformal LEC script template # --------------------------------------------------------------- set log file ./logs/${DESIGN}_lec.log -replace set result file ./results/${DESIGN}_lec.result -replace # libraries set search_path [list ./lib ./rtl ./netlist ./svf] read_db -technology lib slow.db read_db -technology lib fast.db # Reference design read_design -ref -verilog ./rtl/${DESIGN}.v -root ${DESIGN} # Implementation design read_design -impl -verilog ./netlist/${DESIGN}_cts.v -root ${DESIGN} # SVF set_svf ./svf/${DESIGN}.svf # constraints # 若存在LEC专用约束文件则source进来 if {[file exists ./constraints/${DESIGN}_lec.const]} { source ./constraints/${DESIGN}_lec.const } # Mapping options set mapping mode parallel set mapping method name set mapping auto -all # compare points add_compare_points -all # run run_lec # report report_verification_result -compare_point report_failing_points -not_verified -limit 100脚本里值得注意的细节是读库方式用了多个corner的库。LEC虽然是逻辑验证但不同corner里单元功能一致跑出来的结果应该完全一样读多个库并不影响结果。之所以要列出来是因为库不全时工具会因为读不到某个单元的function而报错。5.3 运行时间和资源的动态平衡大型SoC网表跑LEC动不动就要跑几个小时甚至更久。实际项目中对效率的追求往往需要调整运行模式。比如set verification mode hybrid混合引擎以及通过set mapping mode parallel启用并行映射都能明显提速。但有一点要提醒优化运行速度的前提是验证结果的稳定性和可重复性。我见过有团队为了速度快把验证引擎切到最简模式结果跑出一个看似Pass实则漏报的结果。个人经验是在项目初期用穷尽性更强的模式比如BDD模式跑一遍作为基线确认逻辑等价后再用更快的模式做常规回归这样既保证了质量又节省了时间。6. 写在最后的实战心得做LEC验证这几年最深刻的一个体会是这个工具本身门槛不高真正难的是把设计意图翻译成约束条件再把工具报出来的结果解读成有用的信息。很多Fail和Abort背后不是引擎不够聪明而是使用者在输入侧没有把环境告诉它。SVF要保真、黑盒要谨慎、约束要齐全这三点做到位LEC的成功率自然高。另一个心得是LEC结果一定要和整个设计流程串起来看。跑LEC之前先看综合报告里有没有dont_use、dont_touch、timing loop这些信息跑完LEC之后还要结合形式属性验证比如Conformal Property Equivalence、静态时序分析的结果一起回归。形式化验证工具再强也只是一个环节整个团队之间信息透明、脚本版本统一才是芯片质量最可靠的保证。如果你刚开始接触LEC建议拿一个小模块从RTL和综合网表开始比对把映射、Pass、Fail、Abort、黑盒这些概念全部过一遍再逐步向复杂设计推进。等你有过一次从一脸懵到成功定位一个棘手Fail点的经历Conformal LEC的框架就算是真正建立起来了。后面碰到更大规模、更复杂的ECO场景无非是反复应用这套思路而已。
