在我們開始詳細討論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。