4、等价性检查（EC）基础：组合逻辑等价性检查、时序逻辑等价性检查、带扫描链的等价性检查、EC工具的基本使用流程
等价性检查，说白了就是「比大小」。
只不过比的不是数字，而是两个电路设计是不是「一模一样」。我刚开始做验证那会儿，总觉得这玩意儿可有可无——功能仿真跑通了不就行了？直到有一次，综合后的网表跟RTL对不上，流片回来芯片直接罢工……嗯，从那以后，我再也不敢跳过EC了。
4.1 组合逻辑等价性检查
组合逻辑的EC，是最基础也是最容易理解的。它检查的是：同样的输入，是不是产生同样的输出。
举个例子，你写了一段RTL：
assign y = (a & b) | (c & d);综合工具可能给你优化成：
assign y = ~(~a | ~b) | (c & d); // 用了不同的门实现功能上完全等价，但结构不同。EC工具要做的，就是证明这两个网表在所有输入组合下，输出y都一致。
核心原理：EC工具会把两个设计转换成布尔函数，然后用BDD（二叉决策图）或SAT求解器来验证等价性。说白了，就是穷举所有输入，看输出是否匹配——只不过用了数学技巧，不用真的一个个跑。
我在项目中遇到过一种情况：RTL里写了个case语句，综合后变成了mux树。工具报「不等价」，我查了半天，发现是case的default分支没写全。综合工具默认补了x态，而RTL里是latch行为。嗯，这种坑踩过一次就记住了。
4.2 时序逻辑等价性检查
时序逻辑的EC，比组合逻辑复杂一个量级。它不光要看组合逻辑，还要看寄存器、状态机、时钟域这些东西。
你想想看，一个状态机在RTL里用三段式写的，综合后可能被优化成一段式。功能一样，但状态编码、跳转逻辑全变了。EC工具怎么比？
这里有个关键概念叫「状态映射」。工具需要先找到两个设计中对应的寄存器，然后证明它们在每个时钟周期后的状态和输出都一致。
我的个人习惯：在做时序EC之前，先确认两个设计的复位状态一致。如果复位值不同，工具大概率会报错。我曾经因为一个寄存器的复位值从0改成了1，导致整个EC跑不过，排查了整整两天。
时序EC的典型流程：
- 匹配寄存器：工具自动找对应关系，或者用户手动指定
- 建立时序模型：把时序逻辑展开成组合逻辑的迭代
- 验证等价性：用数学方法证明每个时钟周期都一致
- 报告不等价点：给出反例，方便调试
4.3 带扫描链的等价性检查
这个就有点意思了。扫描链是DFT（可测试性设计）的一部分，它把普通寄存器串成了移位寄存器。在测试模式下，你可以通过扫描链把数据灌进去，再把结果扫出来。
但问题来了：加了扫描链之后，功能逻辑变了吗？
理论上不应该变。扫描链只在测试模式下工作，正常模式下它应该「透明」——不影响功能。但实际中，扫描链的插入可能会引入额外的逻辑，比如mux、时钟门控等，这些都有可能改变功能行为。
注意：带扫描链的EC，需要分别验证两种模式：
- 功能模式：扫描链不工作，验证功能逻辑是否等价
- 测试模式：扫描链工作，验证扫描链本身是否正确
我曾经遇到一个案例：扫描链插入时，工具自动在某个寄存器的时钟端加了个门控。功能模式下没问题，但测试模式下时钟被意外关断了，导致扫描链数据传不过去。这种问题，不做EC根本发现不了。
带扫描链的EC，说白了就是多了一层约束。工具需要知道：
- 哪些信号是扫描使能（scan_enable）
- 哪些信号是扫描输入/输出（scan_in/scan_out）
- 测试模式下，功能输入怎么处理
把这些约束配对了，EC才能跑出正确结果。
4.4 EC工具的基本使用流程
市面上主流的EC工具有Synopsys的Formality、Cadence的Conformal等。虽然界面不同，但核心流程大同小异。我以Formality为例，说说基本步骤。
4.4.1 准备设计文件
你需要两个设计：
- 参考设计（Reference）：通常是RTL或综合前的网表
- 实现设计（Implementation）：通常是综合后的网表
工具会拿参考设计当「标准答案」，去比对实现设计。
4.4.2 设置环境
告诉工具：
- 库文件在哪里（比如标准单元库）
- 顶层模块叫什么
- 要不要忽略某些端口（比如测试模式下的额外引脚）
4.4.3 加载设计
用命令把两个设计读进来：
read_verilog -r reference.v # 读参考设计
read_verilog -i implementation.v # 读实现设计
set_top r:/WORK/top # 设置参考设计的顶层
set_top i:/WORK/top # 设置实现设计的顶层4.4.4 匹配点设置
工具会自动匹配寄存器、端口等。如果匹配不上，需要手动指定：
match # 自动匹配
report_unmatched_points # 查看未匹配的点经验之谈：匹配不上是最常见的报错。原因通常是：
- 寄存器名字被综合工具改了（比如加了_suffix）
- 某些寄存器被优化掉了（比如常数寄存器）
- 时钟或复位信号不一致
我一般先跑一下report_unmatched_points，看看哪些点没对上。如果数量不多，手动指定就行。如果一大堆，那八成是环境设置有问题。
4.4.5 运行验证
verify # 开始验证
report_passing_points # 查看通过的点
report_failing_points # 查看失败的点验证通过的话，工具会告诉你「All passing points verified successfully」。如果失败，它会给出反例——也就是一组输入值，能让两个设计的输出不一样。
4.4.6 调试失败点
拿到反例后，怎么调试？我的做法是：
- 先看反例的输入值，手动算一下两个设计的输出
- 如果算不明白，用仿真器跑一下RTL，看实际行为
- 对比综合后的网表，看是不是综合工具优化出了问题
- 如果都不是，那可能是EC工具的约束没设对
一个小技巧：EC工具通常支持「debug mode」，可以逐步展开逻辑锥，帮你定位到具体是哪一级逻辑出了问题。我习惯先跑debug mode，把问题范围缩小到几十个门，再手动分析。这样效率高很多。
知识体系总览
下面这张图，是我自己总结的EC知识框架。你可以把它当成一张「地图」，学完本章后对照着回顾一下：
这张图把EC分成了三大块：组合逻辑、时序逻辑、带扫描链。底部是工具流程，从准备文件到调试失败点，环环相扣。你可以在实际项目中对照着这张图，看看自己卡在了哪一步。
公众号:蓝海资料掘金营，微信deep3321