第三章 形式验证：Formality/LEC等价性检查

等价性检查，圈里人常说的「Formality」或「LEC」。说白了，就是确保你综合前后的代码逻辑一模一样。

我见过不少工程师，综合后仿真通过就以为万事大吉。结果流片回来，芯片功能就是不对。查到最后，往往是综合工具把某个电路优化「变形」了。嗯，形式验证就是抓这种问题的。

为什么需要等价性检查？

综合工具会把你的 RTL 代码映射成门级网表。这个过程里，工具会做大量优化：

• 资源共享
• 状态机编码重排
• 常数传播
• 逻辑等价变换

优化本身没问题。但工具也是软件，也有 bug。我曾经遇到过一次，DC 综合时把一个多路选择器优化成了错误的结构。仿真波形全对，形式验证才揪出来。

等价性检查的两种场景

场景	对比对象	典型工具
RTL-to-Gate	综合前 RTL vs 综合后网表	Synopsys Formality
Gate-to-Gate	修改前后网表	Cadence LEC

RTL-to-Gate 是流片前必做的。Gate-to-Gate 常用于 ECO 阶段，确认手动改网表没改坏功能。

Formality 实战流程

我习惯把流程分成四步。每一步都有坑，咱们一个一个说。

第一步：准备参考设计（Golden）

参考设计就是综合前的 RTL。注意，这里要用综合工具读入的同一个版本。

# Formality 脚本示例 - 读入参考设计
set_svf {./output/top.svf}
read_verilog -golden -01 -lib {./rtl/top.v}
read_verilog -golden -01 -lib {./rtl/sub_module.v}

第二步：准备实现设计（Implementation）

实现设计就是综合后的门级网表。通常还要带上工艺库。

# 读入实现设计
read_verilog -implementation -01 -lib {./output/top_synth.v}
read_db -implementation {./lib/slow.db}

第三步：设置匹配点

工具需要知道哪些端口和寄存器是对应的。大部分情况下，工具能自动匹配。但遇到复杂设计，就得手动指定。

# 手动设置匹配点
match
set_matched_points -golden {top.clk} -implementation {top.clk}
set_matched_points -golden {top.rst_n} -implementation {top.rst_n}

第四步：运行验证

# 运行等价性检查
verify
report_passing_points
report_failing_points

如果所有点都通过，恭喜你。如果有失败的，别慌，往下看。

常见失败原因与调试方法

我整理了一个表格，方便你快速定位问题。

失败现象	可能原因	调试方法
所有点都失败	端口不匹配或时钟域错误	检查 set_top 和端口映射
部分寄存器失败	综合优化导致结构变化	查看 SVF 文件是否完整
组合逻辑失败	资源共享或常数传播问题	使用 analyze_points 查看扇入
黑盒模块失败	库单元缺失或模型不匹配	检查 lib 文件是否完整

LEC 的特殊注意事项

Cadence LEC 和 Synopsys Formality 原理类似，但脚本语法不同。我简单列几个关键点：

• LEC 用 read design 读入设计
• LEC 用 add compare point 设置匹配点
• LEC 的调试命令是 report compare data

工具不同，但思路一样。核心都是：确认参考设计和实现设计在功能上等价。

等价性检查的知识体系

下面这张图，帮你理清形式验证在整个流程中的位置。

调试失败的实用技巧

遇到失败点，别急着改代码。先做这几步：

1. 查看失败点的扇入逻辑：用 analyze_points 命令，看哪些信号影响了这个点。
2. 对比两个设计的扇入结构：工具通常能显示 RTL 和网表的逻辑锥。对比一下，差异一目了然。
3. 检查 SVF 文件：如果 SVF 文件不完整或版本不对，工具会误报。
4. 尝试增加匹配点：手动指定一些关键寄存器，帮助工具建立对应关系。

等价性检查的覆盖率

形式验证的覆盖率是 100%。这是它比仿真强的地方。但要注意，这个 100% 只针对你设置的匹配点。如果某个寄存器没被匹配，工具就不会检查它。

所以，验证完成后，一定要检查匹配报告。确认所有关键寄存器都被覆盖到了。

检查项	要求
匹配点数量	与 RTL 中寄存器数量一致
通过率	100%
未匹配点	0 个（除非手动排除）
黑盒模块	确认已正确处理

写在最后

等价性检查是流片前的最后一道防线。别嫌麻烦，别图省事。我见过太多因为跳过这步而翻车的案例。

嗯，记住一句话：形式验证通过的网表，不一定是对的；但形式验证没通过的网表，一定有问题。