介紹放寬約束的等價性比對sequential equivalence

在上一篇文章《等價性比對驗證之combinational?equivalence》中，我們說過Combinational equivalence比對最嚴(yán)格，但是在很多場景下有限制（不適應(yīng)于時序單元變化的場景）。

本章我們在時序單元數(shù)量或者位置發(fā)生變化，但是整體功能不變的場景下對于Combinational equivalence進行一定程度的放松。

SEQUENTIAL EQUIVALENCE

Sequential equivalence被某些EDA工具稱之為周期精確等價（cycle-accurate equivalence），名字不重要，關(guān)鍵的是理解它和combinational?equivalence的區(qū)別。

Sequential equivalence是使用EDA工具形式化地確認(rèn)是否SPEC模型和IMP模型能否在相同的激勵下產(chǎn)生相同的輸出（這是最基本的要求）。另外不同于combinational?equivalence，它不要求電路中每個時序單元都能夠精確地比對，最終只要輸出的時序一致即可。

如此，就可能在綜合工具進行一些特殊優(yōu)化使得時序單元數(shù)量、位置和流水線深度發(fā)生變化時依然能夠比對通過。

其實伴隨著對于combinational?equivalence的要求的放松，

sequential?equivalence以及后面即將介紹的transaction-based equivalence.
越來越貼近FPV。

審核編輯：劉清