4、形式验证基础：逻辑等价性检查（LEC）、综合前后网表比对、验证流程
形式验证，说白了就是给芯片设计上把「数学锁」。
我刚开始做后端时，总觉得仿真跑通了就万事大吉。直到有一次，综合后的网表跟RTL对不上，仿真愣是没发现，结果流片回来功能全乱套。嗯，从那以后，我再也不敢轻视形式验证了。
4.1 逻辑等价性检查（LEC）是什么？
LEC的全称是Logic Equivalence Check。它的任务很简单：证明两个设计在功能上是完全一样的。
你想想看，RTL代码经过综合、优化、扫描链插入、时钟树综合……每一步都可能引入错误。LEC就是用来抓这些「漏网之鱼」的。
核心思想：把两个设计（比如RTL和综合后网表）都转换成布尔逻辑表达式，然后用数学方法证明它们是否等价。
我个人习惯把LEC比作「数字电路的DNA鉴定」。它不关心时序，只关心逻辑功能是否一致。
4.2 综合前后网表比对
这是LEC最经典的应用场景。我们通常比对三个版本：
- RTL vs 综合后网表：检查综合工具有没有「理解错」你的代码
- 综合后网表 vs 布局后网表：检查布局阶段有没有意外修改逻辑
- 布局后网表 vs 最终网表：检查时钟树、ECO等操作是否引入错误
我在项目中遇到过最坑的一次，是综合工具把某个case语句优化成了优先级编码器，而RTL里明明写的是并行逻辑。LEC直接报错，救了我一命。
注意：综合前后比对时，一定要处理好「未映射」和「未连接」的端口。我曾经因为一个悬空的输出端口，浪费了整整一天去排查。
4.3 验证流程
标准的LEC验证流程，我一般分四步走：
- 读入设计：把RTL和网表都读进工具里
- 设置匹配点：告诉工具哪些端口、寄存器是对应的
- 运行比对：工具自动进行逻辑锥分析
- 分析结果：通过则万事大吉，不通过则要debug
这里有个小技巧：匹配点设置得越精确，比对速度越快。我一般会先让工具自动匹配，再手动检查那些「模糊匹配」的点。
避坑指南：我曾经遇到过一个case，LEC报了几百个不匹配点。后来发现是综合工具把某些寄存器优化掉了，而RTL里还保留着。解决办法是给这些寄存器加 /* keep */ 属性。
4.4 常见问题与调试技巧
LEC报错时，别慌。先看这几点：
- 是不是黑盒问题？——有些IP核是加密的，LEC看不到内部逻辑
- 是不是时序问题？——LEC只比功能，不比时序。但有些工具会把时序优化后的逻辑当成「不等价」
- 是不是扫描链问题？——扫描链插入后，功能模式下的逻辑应该不变
说白了，LEC的debug过程就是「排除法」。我一般会先看报错点的逻辑锥，然后对比RTL和网表的扇入扇出。如果实在找不到原因，就重新跑一遍综合，加上 -no_dft 选项排除扫描链干扰。
4.5 知识体系总览
下面这张图，是我自己总结的形式验证知识框架。你可以把它当成一张「地图」，随时回来对照。
4.6 实用命令示例
我用的是Synopsys Formality工具，命令大致如下：
# 读入参考设计（RTL）
read_verilog -r {top.v} -format verilog
set_top r:/WORK/top
# 读入实现设计（综合后网表）
read_verilog -i {top_syn.v} -format verilog
set_top i:/WORK/top
# 设置匹配点
set_constant -type port r:/WORK/top/rst_n 0
set_constant -type port i:/WORK/top/rst_n 0
# 运行比对
verify
# 查看结果
report_passing -all
report_failing -all这里要注意：复位信号一定要设成常数，否则LEC会认为两个设计在复位状态下不等价。我刚开始就吃过这个亏。
4.7 总结
形式验证不是万能的，但没有它是万万不能的。它就像芯片设计的「安检门」——虽然麻烦，但能拦住大部分危险品。
我个人建议：每次综合后、布局后、时钟树综合后，都跑一遍LEC。别嫌麻烦，等流片回来再发现问题，那才叫真麻烦。
记住一句话：仿真只能证明有bug，形式验证才能证明没bug。