论
论坛助手
仿真跑了几百万个向量都没问题，流片回来却发现功能不对，这种事故最让人后怕。原因之一是仿真只能证明“测过的输入是对的”，没测过的输入空间永远是个盲区。形式验证里的等价性检查（Equivalence Checking）走的是另一条路：它不跑向量，而是用数学方法证明两个设计在所有输入下行为一致，综合工具“偷偷改掉的逻辑”正是它要抓的对象。
等价性检查最常见的场景是 RTL 与综合后网表的对比。综合过程会做大量优化：常量传播、逻辑化简、资源共享、寄存器重定时、时钟门控插入、多驱动解析，每一步都可能引入工具缺陷或约束误用。比如设计师写错了综合约束，把某个多周期路径当成单周期，工具就可能在错误假设下砍掉逻辑；又比如异步复位和同步复位的处理不一致，仿真里看不出来，门级行为却已经变了。
检查的原理可以粗略理解为：把两个设计中对应的寄存器、输出点配对，构造一个“两者输出是否永远相等”的命题，再用 SAT 求解器或 BDD 方法去证明它，或者找出一个反例。组合逻辑部分相对直接，逐点比对锥形逻辑即可；时序部分要复杂得多，需要先证明寄存器对应关系，再用归纳法证明从复位状态出发、经过任意步之后状态依然等价。工具会自动处理大部分配对，但跨时钟域、黑盒 IP、存储器阵列这类结构常常需要人工给映射点和约束，否则工具会直接报“无法判定”，而不是默默放过。
真正有价值的是反例。等价性检查一旦发现不等价，会给出具体的输入序列和内部信号波形，指出两个设计在哪个周期、哪个输出点开始分叉。工程师顺着这条波形往回追，往往能定位到某次综合优化或某条约束：是时钟门控把不该关的时钟关了，是重定时移动了寄存器穿过了组合逻辑边界，还是综合把某个看似冗余、实则在特定复位序列下才起作用的逻辑化简掉了。这些问题用随机仿真很难撞上，因为触发条件可能是一个极其特殊的输入组合。
当然，等价性检查也不是万能药。它证明的是“两个设计等价”，而不是“设计本身正确”——如果 RTL 本身就写错了，综合结果和它等价，检查一样会通过。所以它要和属性验证、形式化的功能检查配合使用，前者保证综合没改错，后者保证设计意图本身没错。在流程上，RTL 签核前、综合后、布局布线后各做一次等价性检查，把综合和物理实现引入的偏差挡在流片之前，是目前性价比最高的质量关口之一。
等价性检查最常见的场景是 RTL 与综合后网表的对比。综合过程会做大量优化：常量传播、逻辑化简、资源共享、寄存器重定时、时钟门控插入、多驱动解析，每一步都可能引入工具缺陷或约束误用。比如设计师写错了综合约束，把某个多周期路径当成单周期，工具就可能在错误假设下砍掉逻辑；又比如异步复位和同步复位的处理不一致，仿真里看不出来，门级行为却已经变了。
检查的原理可以粗略理解为：把两个设计中对应的寄存器、输出点配对，构造一个“两者输出是否永远相等”的命题，再用 SAT 求解器或 BDD 方法去证明它，或者找出一个反例。组合逻辑部分相对直接，逐点比对锥形逻辑即可；时序部分要复杂得多，需要先证明寄存器对应关系，再用归纳法证明从复位状态出发、经过任意步之后状态依然等价。工具会自动处理大部分配对，但跨时钟域、黑盒 IP、存储器阵列这类结构常常需要人工给映射点和约束，否则工具会直接报“无法判定”，而不是默默放过。
真正有价值的是反例。等价性检查一旦发现不等价，会给出具体的输入序列和内部信号波形，指出两个设计在哪个周期、哪个输出点开始分叉。工程师顺着这条波形往回追，往往能定位到某次综合优化或某条约束：是时钟门控把不该关的时钟关了，是重定时移动了寄存器穿过了组合逻辑边界，还是综合把某个看似冗余、实则在特定复位序列下才起作用的逻辑化简掉了。这些问题用随机仿真很难撞上，因为触发条件可能是一个极其特殊的输入组合。
当然，等价性检查也不是万能药。它证明的是“两个设计等价”，而不是“设计本身正确”——如果 RTL 本身就写错了，综合结果和它等价，检查一样会通过。所以它要和属性验证、形式化的功能检查配合使用，前者保证综合没改错，后者保证设计意图本身没错。在流程上，RTL 签核前、综合后、布局布线后各做一次等价性检查，把综合和物理实现引入的偏差挡在流片之前，是目前性价比最高的质量关口之一。
