序言
本文是讀《Formal Verification An Essential Toolkit for Modern VLSI Design》這本書第二章，做的學(xué)習(xí)筆記。
(資料圖片僅供參考)
COMPARE SPECIFICATIONS
通常，我們會將spec和設(shè)計實現(xiàn)進(jìn)行比較。Spec相對來說比較抽象些，可以是些SVA的assertion，RTL model或者一些HVL，比如systemc等。而implemenation通常是RTL代碼或者網(wǎng)表。
圖1是一個簡單的checker，A和B分別表示兩種spec，它們接收相同的輸入(Input)，checker比較二者的輸出是否相等。如果找到一個輸入序列導(dǎo)致輸出比較失敗，就是找個了一個反例（CounterExample）,工具會將此反例，包括相應(yīng)的輸入記錄下來，呈現(xiàn)出來。這個checker其實是個黑盒（Black box），因為我們無法觀察A和B內(nèi)部的狀態(tài)或者信號（白盒White box則可以）。
如果A和B足夠簡單，那我們可以測到所有可能的情形，或者用Formal Verification來判定二者完全等價。同時，我們也可以借助這個等價來簡化一些復(fù)雜的的問題，例如圖2所示，一個更加復(fù)雜的系統(tǒng)，里面包含了A和B。
在這個例子中，因為我們先前已經(jīng)證明了A等價于B，我們可以做下簡化操作，把A和B從系統(tǒng)中拿掉，簡化成C和D的比較，如圖3所示。當(dāng)然，C和D的輸入(Inputs’) 與原始的輸入(Input)已經(jīng)有了很大的差別。這種divide and conquer 策略在FV中經(jīng)常使用，主要用來簡化分析大的design。
我們可以把上下方框想象成Spec和Implementation，這樣的比較輸入和輸入我們可以判定implementation與spec是等價的，設(shè)計符合我們的要求。這個一個典型的formal equivalence verification (FEV) 。不過，通常Spec和Implementation不會出現(xiàn)這種理想的等價情況。
CONES OF INFLUENCE
如果我們把一些把相干的邏輯分別考量，驗證復(fù)雜度能大大簡化。比如，我們有個硬件，實現(xiàn)加法和乘法運(yùn)算；在跑simulation的時候，我們可能造不同case側(cè)重不同的點，有點測加法，有的測乘法。如果我們加法和乘法拆分出來，單獨驗，效率定能大幅提升，但在simulation里面不太現(xiàn)實，因為這需要造幾套驗證環(huán)境。
FV則能比較好的支持這種拆分，F(xiàn)V工具讀取property，將設(shè)計里面一些與當(dāng)前property不相關(guān)的邏輯移移除掉。這個叫cone of influence 簡化。如圖4所示，我們只考量result輸出的時候，很多邏輯對這個輸出沒影響，我們可以把它們簡化掉。如果design特別大的話，這種可以極大的簡化復(fù)雜度。
FV工具也可以支持用戶自定義的簡化，而非自動簡化。例如有個輸入，我們可以綁定成某個固定的值。這樣邏輯也能大大簡化。
BDD
BDD(binary decision tree)，顧名思義，用樹形結(jié)果來表示電路的邏輯。如果去觀察一些電路的真值表如圖5，會發(fā)現(xiàn)有很多redundancy，很多行都是0。BDD可以表示相同設(shè)計的同時，移除一些冗余的邏輯。BDD是一種范式（canonical ），等價設(shè)計的BDD是一樣的；如果兩個電路的BDD一樣，那么可以判定二者等價。BDD算法是第一代Formal 工具常用的算法。
我們以一個MUX為例來說明BDD，如圖6所示，一個MUX邏輯的BDD算法， xyz為輸入，最下面一行為輸出。類似于紅黑樹，每一個分支左側(cè)代表下一輸入變量為0，右側(cè)代表輸入為1.
我們把輸出為0和1的做下merge，如圖7所示。
進(jìn)一步觀察，左側(cè)兩個z，無論取值如何，輸出都是一樣，說明父節(jié)點y不影響結(jié)果。同理，對于觀察右側(cè)，z節(jié)點多余。于是，我們可以進(jìn)一步簡化成圖8這樣的。
當(dāng)然，如果選擇變量的順序不一樣，我們得到的BDD的大小會有所不同。如果我們選擇z->x->y的順序的，我們將得到圖9這樣的BDD。對于一些大的design來說，如果順序選擇不當(dāng)，可能導(dǎo)致指數(shù)爆炸。通常用Heuristic-based 算法來尋找最佳的變量順序。比如根據(jù)電路的拓?fù)浣Y(jié)構(gòu)來，根據(jù)變量的相關(guān)性來映射。另一種方法是嘗試將每一個輸入變量替換0或者1，看看哪個精簡的程度更大些。
對于大而復(fù)雜的設(shè)計來說，提取BDD仍然是一件很艱難的工作，或許隨著輸入的增加而指數(shù)級增長。
COMPUTING A BDD FOR A CIRCUIT DESIGN
如果我們有真值表，我們可以很快速的提取出BDD。但大部分電路，我們沒那么容易算出真值表，尤其對RTL而言。慶幸的是，我們將根據(jù)基本的邏輯（與、或、非）的BDD組合起來，算出更大設(shè)計的BDD。
基本的與或非邏輯的BDD，參見圖10所示。
例如，我們以 (x&&y)||z 為例，電路如圖11所示。將這些基本門電路組合在一起，就是這個電路的BDD，參見圖12.
MODEL CHECKING
Model checking是FV工具分析一段時間內(nèi)時序邏輯的主要方法。給定properties ，model-checking 會去搜索可能的未來狀態(tài)，然后判定是否違反這些property。
首先創(chuàng)建初始狀態(tài)的BDD，然后根據(jù)相應(yīng)的邏輯推導(dǎo)出下一個狀態(tài)的BDD，不斷重復(fù)這個過程（reachability ），直到所有的狀態(tài)都加進(jìn)來。如果遇到vilation，F(xiàn)V會倒推回去，給出一個反例。
model checker 可能出出現(xiàn)三種情形：
設(shè)計符合spec
有violation，并給出反例
邏輯爆炸，無法證明；只能推測N個cycle沒有violation
BOOLEAN SATISFIABILITY
BOOLEAN SATISFIABILITY，即SAT，它可以更快的舉出反例。
假設(shè)我們有這樣的spec和implemenation：
implementation = !(!a&&c || a&&!b)requirement = !a&&!c || b&c即：
!(!a&&c || a&&!b) -> !a&&!c || b&cp -> q 等價于 !p || q
(!a&&c || a&&!b) || (!a&&!c || b&&c)SOLVING THE SAT PROBLEM
對于很多表達(dá)式，證明其成立可能比較困難，但找反例則會簡單的多。如果我們寫成AND形式，那只需要有一項為0，則表達(dá)式為0.
**Conjunctive normal form (CNF) **表達(dá)式是寫成||形式，各個item或在一起，也稱作product-of-sums ?？梢詫ND類比成乘法，OR類比成加法。比如下式就是個CNF：
(a||b||!d)&&(!b||c)&&(a||c)所有的bool邏輯都可以表達(dá)成CNF形式。
我們一個或門為例，輸入為a,b，輸出為c。它的基本邏輯是：
a -> cb -> c!(a||b) -> !c改寫一下：
(!a||c)&&(!b||c)&&(a||b||!c)我們建立一個真值表，把輸入一個個賦值進(jìn)去，看看是否成立。比如a=0, b= 0, c = 0。但如果變量比較的多的話，算法會指數(shù)爆炸。
THE DAVIS-PUTNAM SAT ALGORITHM
一個個枚舉顯然不太合理，一個簡單的思路是先考慮一個變量，這樣就拆分成兩個子問題：一個a=0和一個a=1的情形。不斷重復(fù)這個過程，直到證明或者有違規(guī)。
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)}最壞的情形是把所有的都遍歷一遍，但一般來說不需要。例如對于表達(dá)是(a||!b||c) 來說，如果將a賦值成1，整個表達(dá)等于1，不需要繼續(xù)分析了。
一個典型的列子如圖13所以
總結(jié)：
不要理解成formal是逐個枚舉輸入變量的值，formal實際上用的數(shù)學(xué)方法來證明的。
