等价性比对验证之equivalence（1）

等价性比对验证

在我们开始详细讨论FEV 技术之前，我们需要有一个定义

到底什么才是我们所说的“等价”？

一般我们将等价定义为一组关键点之间的匹配，也就是说比较两个模型在相同的激励下，这些关键点是否完全具有相同的逻辑。关键点可能包括：

熟悉数字芯片实现的人可能发现，这不就是一个寄存器传输级电路的几个属性么。

基于对于这些关键点的不同比对方式，有三种类型的等价性比对：

从上到下，比对的方式越来越宽松，但是整个模块的端到端功能都能囊括在内的。

具体的差异性，见后续。

Combinational equivalence是使用EDA工具进行等价性比对中最成熟的FEV技术，一般情况下是将RTL和原理图网表进行等价性比对

上图中每个SPEC模型中的触发器都对应于IMP模型中的特定触发器并且两两触发器之间的组合逻辑功能都是完全等价的。换句话说，这两个模型之前的所有关键点都存在一一对应的关系，中间不存在任何其他的操作。

上一篇文章已经说过，这种类型的等价性比对几乎和逻辑综合同时出现，用来保证RTL和综合后的门级网表一一对应。（现代IC研发流程中形式化等价性验证的重要性）

这种方式的好处是：EDA工具不需要考虑寄存器之间的时序关系，只需要关心组合逻辑锥是否等价，也有它的局限性：只适合于RTL和门级网表之间的寄存器数量一一对应的场景。熟悉逻辑综合技术的人想必都知道，很多逻辑综合技术会改变寄存器的位置和数量。

上面电路图中，如果使用的是Combinational equivalence等价性验证，那么需要比对的关键点就是输入（a,b,Ck）、寄存器（F1、F2）和输出（Out）

很明显Combinational equivalence比对最严格，但是在很多场景下有限制（不适应于时序单元变化的场景）。

实际上，我们其实只要证明在相同的输入下，输出能够比对上就可以了，不需要太关心中间的时序逻辑单元个数，所以后面我们将介绍放宽这种约束的等价性比对sequential equivalence和transactional equivalence。

我们在时序单元数量或者位置发生变化，但是整体功能不变的场景下对于Combinational equivalence进行一定程度的放松。

Sequential equivalence被某些EDA工具称之为周期精确等价（cycle-accurate equivalence），名字不重要，关键的是理解它和combinational equivalence的区别。

Sequential equivalence是使用EDA工具形式化地确认是否SPEC模型和IMP模型能否在相同的激励下产生相同的输出（这是最基本的要求）。另外不同于combinational equivalence，它不要求电路中每个时序单元都能够精确地比对，最终只要输出的时序一致即可。

如此，就可能在综合工具进行一些特殊优化使得时序单元数量、位置和流水线深度发生变化时依然能够比对通过。

其实伴随着对于combinational equivalence的要求的放松，
sequential equivalence以及后面即将介绍的transaction-based equivalence.越来越贴近FPV。

作者：验证哥布林
原文来源：芯片验证工程师
链接：https://mp.weixin.qq.com/s/eTPkyUiIuXCmx2A7UDUcxw
https://mp.weixin.qq.com/s/MP6egh0fqQ-88Dd6cudT6w

推荐阅读

更多数字IC设计技术干货等请关注数字芯片实验室专栏。添加极术小姐姐（微信：aijishu20)微信可申请加入IC设计交流群。