介绍放宽约束的等价性比对sequential equivalence

在上一篇文章《等价性比对验证之combinational equivalence》中，我们说过Combinational equivalence比对最严格，但是在很多场景下有限制（不适应于时序单元变化的场景）。

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

SEQUENTIAL EQUIVALENCE

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

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

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

其实伴随着对于combinational equivalence的要求的放松，

sequential equivalence以及后面即将介绍的transaction-based equivalence.
越来越贴近FPV。

审核编辑：刘清