COMPARE SPECIFICATIONS

通常，我們會將spec和設計實現進行比較。Spec相對來說比較抽象些，可以是些SVA的assertion，RTL model或者一些HVL，比如systemc等。而implemenation通常是RTL代碼或者網表。

圖1是一個簡單的checker，A和B分別表示兩種spec，它們接收相同的輸入(Input)，checker比較二者的輸出是否相等。如果找到一個輸入序列導致輸出比較失敗，就是找個了一個反例（CounterExample）,工具會將此反例，包括相應的輸入記錄下來，呈現出來。這個checker其實是個黑盒（Black box），因為我們無法觀察A和B內部的狀態或者信號（白盒White box則可以）。

圖1simple checker

如果A和B足夠簡單，那我們可以測到所有可能的情形，或者用Formal Verification來判定二者完全等價。同時，我們也可以借助這個等價來簡化一些復雜的的問題，例如圖2所示，一個更加復雜的系統，里面包含了A和B。

在這個例子中，因為我們先前已經證明了A等價于B，我們可以做下簡化操作，把A和B從系統中拿掉，簡化成C和D的比較，如圖3所示。當然，C和D的輸入(Inputs’) 與原始的輸入(Input)已經有了很大的差別。這種divide and conquer 策略在FV中經常使用，主要用來簡化分析大的design。

我們可以把上下方框想象成Spec和Implementation，這樣的比較輸入和輸入我們可以判定implementation與spec是等價的，設計符合我們的要求。這個一個典型的formal equivalence verification (FEV) 。不過，通常Spec和Implementation不會出現這種理想的等價情況。

CONES OF INFLUENCE

如果我們把一些把相干的邏輯分別考量，驗證復雜度能大大簡化。比如，我們有個硬件，實現加法和乘法運算；在跑simulation的時候，我們可能造不同case側重不同的點，有點測加法，有的測乘法。如果我們加法和乘法拆分出來，單獨驗，效率定能大幅提升，但在simulation里面不太現實，因為這需要造幾套驗證環境。

FV則能比較好的支持這種拆分，FV工具讀取property，將設計里面一些與當前property不相關的邏輯移移除掉。這個叫cone of influence 簡化。如圖4所示，我們只考量result輸出的時候，很多邏輯對這個輸出沒影響，我們可以把它們簡化掉。如果design特別大的話，這種可以極大的簡化復雜度。

FV工具也可以支持用戶自定義的簡化，而非自動簡化。例如有個輸入，我們可以綁定成某個固定的值。這樣邏輯也能大大簡化。

BDD

BDD(binary decision tree)，顧名思義，用樹形結果來表示電路的邏輯。如果去觀察一些電路的真值表如圖5，會發現有很多redundancy，很多行都是0。BDD可以表示相同設計的同時，移除一些冗余的邏輯。BDD是一種范式（canonical ），等價設計的BDD是一樣的；如果兩個電路的BDD一樣，那么可以判定二者等價。BDD算法是第一代Formal 工具常用的算法。

我們以一個MUX為例來說明BDD，如圖6所示，一個MUX邏輯的BDD算法， xyz為輸入，最下面一行為輸出。類似于紅黑樹，每一個分支左側代表下一輸入變量為0，右側代表輸入為1.

我們把輸出為0和1的做下merge，如圖7所示。

進一步觀察，左側兩個z，無論取值如何，輸出都是一樣，說明父節點y不影響結果。同理，對于觀察右側，z節點多余。于是，我們可以進一步簡化成圖8這樣的。

當然，如果選擇變量的順序不一樣，我們得到的BDD的大小會有所不同。如果我們選擇z->x->y的順序的，我們將得到圖9這樣的BDD。對于一些大的design來說，如果順序選擇不當，可能導致指數爆炸。通常用Heuristic-based 算法來尋找最佳的變量順序。比如根據電路的拓撲結構來，根據變量的相關性來映射。另一種方法是嘗試將每一個輸入變量替換0或者1，看看哪個精簡的程度更大些。

對于大而復雜的設計來說，提取BDD仍然是一件很艱難的工作，或許隨著輸入的增加而指數級增長。

COMPUTING A BDD FOR A CIRCUIT DESIGN

如果我們有真值表，我們可以很快速的提取出BDD。但大部分電路，我們沒那么容易算出真值表，尤其對RTL而言。慶幸的是，我們將根據基本的邏輯（與、或、非）的BDD組合起來，算出更大設計的BDD。

基本的與或非邏輯的BDD，參見圖10所示。

例如，我們以 (x&&y)||z 為例，電路如圖11所示。將這些基本門電路組合在一起，就是這個電路的BDD，參見圖12.

MODEL CHECKING

Model checking是FV工具分析一段時間內時序邏輯的主要方法。給定properties ，model-checking 會去搜索可能的未來狀態，然后判定是否違反這些property。

首先創建初始狀態的BDD，然后根據相應的邏輯推導出下一個狀態的BDD，不斷重復這個過程（reachability ），直到所有的狀態都加進來。如果遇到vilation，FV會倒推回去，給出一個反例。

model checker 可能出出現三種情形：

設計符合spec

有violation，并給出反例

邏輯爆炸，無法證明；只能推測N個cycle沒有violation

BOOLEAN SATISFIABILITY

BOOLEAN SATISFIABILITY，即SAT，它可以更快的舉出反例。

假設我們有這樣的spec和implemenation：

implementation =  !(!a&&c || a&&!b)
requirement = !a&&!c || b&c

即：

!(!a&&c || a&&!b) -> !a&&!c || b&c

p -> q 等價于 !p || q

(!a&&c || a&&!b) || (!a&&!c || b&&c)

SOLVING THE SAT PROBLEM

對于很多表達式，證明其成立可能比較困難，但找反例則會簡單的多。如果我們寫成AND形式，那只需要有一項為0，則表達式為0.

**Conjunctive normal form (CNF) **表達式是寫成||形式，各個item或在一起，也稱作product-of-sums 。可以將AND類比成乘法，OR類比成加法。比如下式就是個CNF：

(a||b||!d)&&(!b||c)&&(a||c)

所有的bool邏輯都可以表達成CNF形式。

我們一個或門為例，輸入為a,b，輸出為c。它的基本邏輯是：

a -> c
b -> c
!(a||b) -> !c

改寫一下：

(!a||c)&&(!b||c)&&(a||b||!c)

我們建立一個真值表，把輸入一個個賦值進去，看看是否成立。比如a=0, b= 0, c = 0。但如果變量比較的多的話，算法會指數爆炸。

THE DAVIS-PUTNAM SAT ALGORITHM

一個個枚舉顯然不太合理，一個簡單的思路是先考慮一個變量，這樣就拆分成兩個子問題：一個a=0和一個a=1的情形。不斷重復這個過程，直到證明或者有違規。

SATDivide&Conquer(formula)

If the formula evaluates to 1
{Return Success!}
If the formula evaluates to 0,
{Return Failure, hope another assignment works.}
Else
{split the problem on some variable, v.
SATDivide&Conquer (formula replacing v with 0)
SATDivide&Conquer (formula replacing v with 1)
}

最壞的情形是把所有的都遍歷一遍，但一般來說不需要。例如對于表達是(a||!b||c) 來說，如果將a賦值成1，整個表達等于1，不需要繼續分析了。

一個典型的列子如圖13所以

總結：

不要理解成formal是逐個枚舉輸入變量的值，formal實際上用的數學方法來證明的。

審核編輯：劉清