在我們開(kāi)始詳細(xì)討論FEV 技術(shù)之前，我們需要有一個(gè)定義

到底什么才是我們所說(shuō)的“等價(jià)”。

一般我們將等價(jià)定義為一組關(guān)鍵點(diǎn)之間的匹配，也就是說(shuō)比較兩個(gè)模型在相同的激勵(lì)下，這些關(guān)鍵點(diǎn)是否完全具有相同的邏輯。關(guān)鍵點(diǎn)可能包括：

1. 輸入

2. 輸出

3. 時(shí)序單元輸出（鎖存器和觸發(fā)器）

熟悉數(shù)字芯片實(shí)現(xiàn)的人可能發(fā)現(xiàn)，這不就是一個(gè)寄存器傳輸級(jí)電路的幾個(gè)屬性么。

基于對(duì)于這些關(guān)鍵點(diǎn)的不同比對(duì)方式，有三種類(lèi)型的等價(jià)性比對(duì)：

1. combinational equivalence

2. sequential equivalence

3. transactional equivalence

從上到下，比對(duì)的方式越來(lái)越寬松，但是整個(gè)模塊的端到端功能都能囊括在內(nèi)的。

具體的差異性，見(jiàn)后續(xù)的幾篇文章。

Combinational equivalence

Combinational equivalence是使用EDA工具進(jìn)行等價(jià)性比對(duì)中最成熟的FEV技術(shù)，一般情況下是將RTL和原理圖網(wǎng)表進(jìn)行等價(jià)性比對(duì)

上圖中每個(gè)SPEC模型中的觸發(fā)器都對(duì)應(yīng)于IMP模型中的特定觸發(fā)器并且兩兩觸發(fā)器之間的組合邏輯功能都是完全等價(jià)的。換句話說(shuō)，這兩個(gè)模型之前的所有關(guān)鍵點(diǎn)都存在一一對(duì)應(yīng)的關(guān)系，中間不存在任何其他的操作。

上一篇文章已經(jīng)說(shuō)過(guò)，這種類(lèi)型的等價(jià)性比對(duì)幾乎和邏輯綜合同時(shí)出現(xiàn)，用來(lái)保證RTL和綜合后的門(mén)級(jí)網(wǎng)表一一對(duì)應(yīng)。

1. 這種方式的好處是：EDA工具不需要考慮寄存器之間的時(shí)序關(guān)系，只需要關(guān)心組合邏輯錐是否等價(jià)，

2. 也有它的局限性：只適合于RTL和門(mén)級(jí)網(wǎng)表之間的寄存器數(shù)量一一對(duì)應(yīng)的場(chǎng)景。熟悉邏輯綜合技術(shù)的人想必都知道，很多邏輯綜合技術(shù)會(huì)改變寄存器的位置和數(shù)量。
   

上面電路圖中，如果使用的是Combinational equivalence等價(jià)性驗(yàn)證，那么需要比對(duì)的關(guān)鍵點(diǎn)就是輸入（a,b,Ck）、寄存器（F1、F2）和輸出（Out）

很明顯Combinational equivalence比對(duì)最嚴(yán)格，但是在很多場(chǎng)景下有限制（不適應(yīng)于時(shí)序單元變化的場(chǎng)景）。

實(shí)際上，我們其實(shí)只要證明在相同的輸入下，輸出能夠比對(duì)上就可以了，不需要太關(guān)心中間的時(shí)序邏輯單元個(gè)數(shù)，所以后面我們將介紹放寬這種約束的等價(jià)性比對(duì)sequential equivalence和transactional equivalence。