企业官网建设流程全解析

流片时间已定，后端同事发来消息：“网表在时钟树综合后又改了几处，你确认一下功能没问题。”这种场景在数字IC项目里太常见了。几千个case的回归仿真能cover掉大部分功能点，但综合、修时序、插入扫描链这些步骤引入的问题，仿真不一定能暴露出来。可靠的解法其实很标准：跑一遍逻辑等价性验证，用Conformal LEC把修订版设计与基准版本做一次数学层面的全状态比较。

Conformal LEC（Logic Equivalence Checking）在数字IC设计流程里几乎是绕不开的一环。不管是流片前的RTL vs Gate signoff，还是ECO、时钟树修改、低功耗逻辑插入之后的一致性确认，它都是最有力的兜底手段之一。相比仿真需要人写testbench、看覆盖率，LEC是形式化验证，穷举处理所有输入状态，只要环境设置正确，它给出的结论就是数学结论，不是抽样统计。

这篇文章适合刚接触LEC的验证工程师、后端工程师，也适合已经跑了很长时间但一直靠老脚本、遇到问题只能发愁的工程师。我会把从库读入、设计设置、关键点映射、约束、验证、报告解读到常见fail排查这条完整链路讲清楚，再分享一些脚本和文档里不会写的实操细节。

1. 为什么每个流片项目都绕不开Conformal LEC

1.1 LEC到底验证什么

要理解LEC，先理解设计里“逻辑锥”的概念。任何一个寄存器的输入引脚，或者任何一组组合逻辑输出，都可以向上追溯它依赖的所有输入信号；这些信号追到头，是primary input、寄存器输出、存储器输出等起点。从起点到终点之间的组合逻辑，就叫一个逻辑锥。如果两个设计在对应的终点上，各自的逻辑锥函数完全一致，那么它们在功能上就是等价的。

Conformal LEC的工作方式大致分三步：第一，找到两个设计里应该对应的关键点，包括输入输出端口、触发器、锁存器、存储器输出等；第二，把整个设计切成大量逻辑锥；第三，用形式化引擎比较每个逻辑锥两边的函数。这是穷尽式比较，不是抽样，所以只要工具判定通过，理论上两边功能就是一致的，这点是仿真替代不了的。

有个生活化的类比很贴切：仿真像抽查作文，挑几段读一遍，感觉没问题就认为整体没问题；LEC像把两份文稿逐字比对，连标点符号都要一致。所以综合后、修timing、做ECO后，光靠回归仿真兜底是不够的，必须跑LEC从结构上保证功能没变化。

1.2 LEC与仿真、属性检查的分工

可能会有人问：既然LEC这么强，能不能完全替代仿真？不能。LEC只验证两个设计之间的等价关系，它不知道你的设计功能本身对不对。RTL一开始就写错了，LEC照样可以通过。仿真验证的是设计行为是否符合规格，LEC验证的是改动前后功能是否一致，两者职责完全不同。

另外，还有一类形式化验证叫属性检查（property checking），它是拿断言去证明某个逻辑性质在所有状态下都成立，跟LEC的“两个设计等价比较”也不是一回事。实际signoff实践中，这三者往往是组合使用的：仿真cover功能需求，属性检查抓边界条件，LEC保证每次综合或ECO后的改动都没把功能“改坏”。

这样看下来，LEC在整个流程里的定位就清晰了：它是最后的“安全网”。只要网表级有任何手改、工具改、ECO改，都要扔给它验证一遍，确保改前改后逻辑函数一致。

2. Setup阶段决定成败：库、设计与工具配置

很多人第一次跑LEC不顺利，十有八九是setup阶段出了问题，而不是验证本身跑不通。LEC工具很实在：前面给的信息不对，后面就会冒出一堆莫名其妙的fail。

2.1 库文件怎么读，有哪些讲究

RTL与门级网表做等价比较时，必须给工具提供标准单元库，工具才知道每个cell的逻辑功能。读库常用命令是read_library，可以读liberty格式，也能读db格式。个人习惯是统一用liberty，因为文本格式便于diff，想确认某个单元的真值表时直接打开看一眼很方便。

这里容易踩的坑至少有三种。第一，库不全，某些IO cell、特殊cell没读进来，工具只能把单元当黑盒处理，黑盒输出端口的功能无法判断，后面验证会大量失败。第二，corner给得跟综合不一致。比如综合用的是tt corner的库，LEC里却只读了ss corner。纯功能验证下不同corner逻辑功能基本一致，但有些单元库在不同电压、不同corner下的行为建模存在差异，建议还是跟综合保持同一套库。第三，有些库包含多电压域、隔离单元、level shifter等特殊单元，在低功耗设计时需要配合UPF一起读，否则工具对隔离逻辑的行为分析会出错。

读库之后可以用report_library检查读进来了多少module。初次跑项目时最好扫一眼，确认不是零记录。我见过有人跑到verify全fail，排查半天，最后发现读库命令里路径多了一个引号，lib一个都没进去，所有单元全成了黑盒。

2.2 golden和revised：谁是谁要搞清楚

Conformal LEC里，golden和revised是两个设计。golden是基准，可以理解成“参考答案”；revised是被验证的对象，工具会拿revised去跟golden比。通常做RTL vs Gate时，RTL是golden，综合网表是revised；做ECO验证时，ECO前的设计是golden，ECO后的设计是revised。

读设计的命令大致长这样：

# golden设计，通常是未实现版本 read_design -golden -verilog \ -define SYNTHESIS \ -filelist ./scripts/rtl.f set_top -golden chip_top # revised设计，通常是综合后网表 read_design -revised -verilog \ ./results/chip_top.gate.v set_top -revised chip_top

filelist里RTL的解析顺序很重要，如果顶层module依赖某些define或include，需要把搜索路径和宏定义指定全。一个比较笨但有效的做法，是从综合工具那边把filelist、define、include path整份拿过来，保证两边读进来的RTL语义一致。

set_top指定顶层，这里经常遇到低级错误。golden和revised的top名称写错，或者大小写不一致，会导致后面map出的关键点数量少得可怜。顶层名称、实例名、端口名在比对时是严格匹配的，建议先用report_design_info看看两边顶层是否正确，再继续往下走。

2.3 时钟与复位约束：不约束就等着爆fail

LEC的比对依赖时序元素，如果时钟和复位关系不清晰，工具无法正确切分逻辑锥。比如设计中存在多个时钟域，如果不告诉工具每个触发器的时钟是什么，工具会用默认方式猜测，一旦猜错，后面验证就会大面积fail。

常用方式是在读入设计后调用add_clk_constraints或相关命令，让工具自动识别时钟树并做约束。异步复位、异步置位信号也一样，工具需要知道这些信号是异步控制端，不会作为普通数据路径进行处理。setup期间还经常需要手动设置常数。比如某些测试信号在功能模式下应该固定为0或1，比如DFT的test_mode、scan_enable，这种信号不设常数，工具会把两条可测试性路径都当作功能路径来比，结果当然对不上。

这里我的经验是：约束宁可多写一点也不要少写。LEC确实存在误报，但误报大多是约束不足导致的，不是工具本身有问题。把约束点统一列成一个文件，跟RTL、网表一起纳入版本管理，新项目直接复用，省心很多。

3. 关键点映射：LEC启动后的第一道关

setup跑完，接下来是LEC最核心的环节之一：关键点（key points）映射。这个概念有点抽象，但它直接决定最终验证结果可不可信。

3.1 关键点为什么重要

前面提到，LEC会把设计切成逻辑锥。切分的“边界点”就是关键点。关键点至少包含四类：primary input/output、DFF或DLAT的输出引脚、存储器输出、黑盒的输出。工具默认会自动识别这些点，并把两个设计中的关键点做对应，对应不上的点在报告里会标记为unmapped。

为什么说这步决定成败？因为如果golden里某个寄存器和revised里的另一个寄存器没有对应上，意味着这个寄存器后面的逻辑锥在两边是分别独立验证的，相当于关键点之间出现“断链”。某个点的映射一旦错了，由此向后传播的逻辑锥可能全部fail，但根因可能只是早期的一个匹配错误。

3.2 自动映射与手动干预

多数情况下，如果RTL和网表之间寄存器数量和名称保持一致，工具靠名字能自动映射。比如data_q、addr_reg这类信号名，在综合网表里通常还保留着，直接就能对上。但修timing时，综合工具可能插入buffer、拆分扇出、加冗余逻辑，寄存器可能被重命名甚至合并，导致自动映射不全。

这时可以给工具加映射规则。比如用正则规则把golden侧和revised侧重名寄存器对应起来，或者在GUI里手动指定对应点。我见过一些老工程师更直接：在综合时以命名约束保持寄存器名不变，从源头减少mapping负担。日常维护中，这条经验非常管用。

跑完map之后，一定要看report_unmapped_points，尤其是DFF/DLAT这类时序点的unmapped数量。少量组合逻辑点unmapped还可以接受，时序点unmapped多了，验证结果基本不能信。

3.3 mapping后的检查清单

我每次mapping后必做三个动作：

• 用report_key_points确认关键点总数和分布；
• 用report_unmapped_points看失败侧有哪些点没对得上；
• 对比两侧DFF总数，确认没有大规模寄存器丢失。

一般建议golden和revised的DFF数量先对齐，再往verify走。如果DFF数量差太多，八成是复位或时钟约束处理有问题，先回头查setup，别浪费时间在验证阶段。这里多说一句，mapping阶段看到unmapped点也不要急着全手动补，有相当一部分unmapped点来自常量单元或测试逻辑，通过合理的set_constant反而更干净。

4. 完整运行与结果解读：从命令行到报告

前面这些步骤都理清楚了，正式验证的命令反而很简单，参数和模式选择才是重点。

4.1 一份可直接参考的LEC do文件

以比较常见的流程为例，完整脚本结构如下：

set_log_file ./logs/lec.log set_system_mode lec # 1. 读库 set search_path "/design/libs" read_library -sensitive -liberty \ /design/libs/tt_typ.lib # 2. 读golden RTL read_design -golden -verilog \ -define SYNTHESIS \ -filelist ./scripts/rtl.f set_top -golden chip_top # 3. 读revised netlist read_design -revised -verilog \ ./results/chip_top.gate.v set_top -revised chip_top # 4. 约束 add_clk_constraints set_constant test_mode 0 set_constant scan_enable 0 # 5. 映射与验证 map_key_points verify # 6. 输出报告 report_verification_engine > ./logs/engine.rpt report_unmapped_points > ./logs/unmapped.rpt report_fail 5 > ./logs/fail.rpt

命令本身不复杂，但有几个细节值得注意。第一是add_clk_constraints，工具默认按它自己识别到的时钟做约束，对于多时钟域设计，最好根据设计时钟信息手动指定，别完全依赖自动识别。第二是set_constant，它指定某信号恒为某值，这只是给工具一个验证前提，不是证明出来的结论，所以用错地方反而会掩盖真实问题。它更适合用于DFT测试信号这类功能模式下不参与比对的信号。

实际工程中，我习惯把脚本拆成setup、run、report三部分。setup部分负责库、设计、约束，run部分只有map_key_points和verify，report部分输出各类报告。这样RTL更新后只需要重新读一遍设计，不用把库和约束全部推倒重来。

4.2 verify之后的结论怎么看

运行结束后，工具会给出三类结论之一：verified、fail、undetermined。verified是等价；fail是逻辑锥不等价；undetermined是工具没能收敛，可能是设计太大、约束不够、或者存在黑盒导致逻辑锥无法分析。

对于undetermined，一般可以靠调整引擎或增加约束来转成verified或fail。Conformal有几个针对不同结构的验证引擎，比如专门处理datapath的引擎和专门处理随机逻辑的引擎，具体可以用set_engine_mode切换。如果逻辑锥包含大量乘法器、除法器这类datapath结构，选对引擎能显著降低abort数量。

还有一个常见问题是abort。工具处理超大逻辑锥时，如果没有及时切cut point，会撑爆内存或超时。解决办法是通过历史经验设置cut point或者做层次化比较，把大模块拆成小模块逐个验证。这也是很多大芯片项目坚持block level LEC的原因之一。

4.3 从Report到结论：怎么快速定位问题点

一个实用的习惯是：不要只盯着最终pass/fail。第一次跑fail时，先打开report_fail或者GUI，看fail点聚集在哪个模块、哪个时钟域、哪个corner。如果fail点集中在一小块区域，多半是那部分逻辑存在真实差异；如果fail点连成大片，先怀疑mapping或约束问题，而不是怀疑RTL本身被改错了。

我遇到过一个case，修订版网表出现大面积fail，检查后发现两边时钟门控结构不一致。一个版本的clock gating cell带latch-enable，另一个版本不带，导致某些寄存器在特殊时钟沿下捕获的数据不同。这种fail单看RTL是发现不了的，必须靠LEC形式的逻辑比较才能揪出来。

5. 不等价？先从这几个方向排查

5.1 常见fail原因速查表

这个表不是让你背，而是提醒你fail不一定是“逻辑真不对”。EDA工具的特点在于它能给出非常精确的变量，我们要做的是把“被验证对象”和“验证前提”分开看。前提错了，后面的所有比较都是空中楼阁。

5.2 逐步debug的路径

如果遇到无法解释的fail，我一般按这个顺序debug。

第一，查unmapped points。任何一个时序点没有对应，后面的验证结果就可能失真。先把映射问题解决，验证结果至少有一半会恢复正常。第二，在GUI里打开fail点，看两边的逻辑锥。Conformal的GUI能显示两类逻辑结构，对找问题作用很大。特别是datapath电路，cone display能帮助定位到是哪一级运算或者哪个mux选错了。第三，检查黑盒。如果网表里有库中不存在的cell，工具会当黑盒处理，黑盒输入输出端口就成了逻辑锥边界，功能无法验证。把黑盒报告拉出来，看有没有该被解析的cell漏掉。第四，检查异步逻辑。工具对异步set/reset的建模与RTL描述可能不匹配，导致验证fail。如果设计里有跨时钟域的异步FIFO，需要配合CDC约束或设置时序path，让工具知道哪些路径不需要比较。

5.3 真实不等价和工具误报的区分

做LEC越久，越会意识到一个词：合理怀疑。工具报fail时，先别慌，要分成两种情况：一种是设计确实被改坏了，需要回到RTL或网表修；另一种是约束或环境导致工具对同一逻辑采用了不同假设，属于误报。

比如某些算术单元，综合工具可能在代数变换下生成不同结构，逻辑函数理论等价，但工具在特定建模下判为fail。这时可以人工审查，调整引擎，或者改换比较层次。还有扫描链重排后的网表，如果没把scan_enable设为常数，工具会把shift路径也当功能路径比对，自然fail。把测试信号设好常数，fail马上消失。

反过来也要警惕另一种情况：工具报verified，但设计确实有问题。多数是因为约束过强，把有效路径当成常量或exclude掉了。所以每次verified后，我都会顺手看一下报告里的约束清单，确认没有多设、错设的常量。

6. 进阶场景：ECO、低功耗与层次化验证

6.1 前端ECO后验证

RTL ECO是LEC最高频的场景之一。改了几行RTL，想让综合工具重新生成网表，又担心改动影响其他逻辑，跑一遍LEC比跑全量回归快得多，也可靠得多。实践上，ECO前后比较时把ECO前的RTL作为golden，ECO后的RTL作为revised，也可以直接用原始网表和ECO后网表比较，目的是确认所有改动都只发生在预期区域。

我总结经验是：ECO验证时尽量保存一个干净的“当前版本”，与修改版做diff时一目了然，这样LEC的fail点还能对照diff检查，省很多精力。另外，ECO常伴随修cell、换buffer、调整驱动强度，这类改动不影响功能，LEC能自动吸收；真正需要关注的是加删逻辑或修改逻辑连接的部分。

6.2 低功耗设计与UPF

插入isolation cell、level shifter、power switch之后，RTL与网表的功能不再完全等价，如果直接跑LEC，会出现大量fail。标准做法是把UPF文件也交给工具，让工具知道这些低功耗cell在功能模式下如何工作、哪些信号固定为0或1、哪些状态是非法状态，从而正确地进行比较。这一步对后端低功耗signoff很重要，也最容易因为少给UPF而浪费一整天时间在奇怪的fail上。

6.3 层次化模块级LEC

芯片规模大时，全chip跑LEC可能非常耗时。常见的做法是block level分别验证，再在chip level做黑盒封装或用already proved的关键点来简化逻辑锥复杂度。这有点像分而治之：先证明各个小模块没错，再证明模块连接没错。关键是要保证block之间的接口约束一致，避免block内部已经proved后，又因为接口变化而失算。

我自己一直有个习惯：每次跑LEC都会把golden、revised、库、约束文件、工具版本、关键选项记录下来。因为LEC报出来的问题和设计、工具版本强相关，同一个设计换一个工具版本，结果可能完全不同。没有版本信息，事后排查会陷入被动。

做LEC这些年，我最深的体会是：这工具最大的价值不是“告诉你有没有错”，而是“告诉你哪里还有疑点”。它会把你从拍脑袋判断中解放出来，逼着你把每一个逻辑锥都看清楚。流片之前，这种踏实感是很难用别的东西替代的。如果你第一次跑就遇到大片fail，别慌，按前面这个排查顺序走一遍，大多时候都能找到答案。