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

到底什么才是我們所說的“等價”。

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

1. 輸入

2. 輸出

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

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

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

1. combinational equivalence

2. sequential equivalence

3. transactional equivalence

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

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

Combinational equivalence

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

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

上一篇文章已經(jīng)說過，這種類型的等價性比對幾乎和邏輯綜合同時出現(xiàn)，用來保證RTL和綜合后的門級網(wǎng)表一一對應(yīng)。

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

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

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

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

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