一文解析最严格的等价性比对验证combinational equivalence

在我们开始详细讨论FEV 威廉希尔官方网站 之前，我们需要有一个定义

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

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

1. 输入

2. 输出

3. 时序单元输出（锁存器和触发器）

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

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

1. combinational equivalence

2. sequential equivalence

3. transactional equivalence

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

具体的差异性，见后续的几篇文章。

Combinational equivalence

Combinational equivalence是使用EDA工具进行等价性比对中最成熟的FEV威廉希尔官方网站 ，一般情况下是将RTL和原理图网表进行等价性比对

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

上一篇文章已经说过，这种类型的等价性比对几乎和逻辑综合同时出现，用来保证RTL和综合后的门级网表一一对应。

1. 这种方式的好处是：EDA工具不需要考虑寄存器之间的时序关系，只需要关心组合逻辑锥是否等价，

2. 也有它的局限性：只适合于RTL和门级网表之间的寄存器数量一一对应的场景。熟悉逻辑综合威廉希尔官方网站 的人想必都知道，很多逻辑综合威廉希尔官方网站 会改变寄存器的位置和数量。
   

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

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

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