一文解析最嚴格的等價性比對驗證combinational equivalence

在我們開始詳細討論FEV 技術之前，我們需要有一個定義

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

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

1. 輸入

2. 輸出

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

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

基于對于這些關鍵點的不同比對方式，有三種類型的等價性比對：

1. combinational equivalence

2. sequential equivalence

3. transactional equivalence

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

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

Combinational equivalence

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

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

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

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

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

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

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

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