序言

本文是讀《Formal Verification An Essential Toolkit for Modern VLSI Design》這本書(shū)第二章，做的學(xué)習(xí)筆記。

(資料圖片僅供參考)

COMPARE SPECIFICATIONS

通常，我們會(huì)將spec和設(shè)計(jì)實(shí)現(xiàn)進(jìn)行比較。Spec相對(duì)來(lái)說(shuō)比較抽象些，可以是些SVA的assertion，RTL model或者一些HVL，比如systemc等。而implemenation通常是RTL代碼或者網(wǎng)表。

圖1是一個(gè)簡(jiǎn)單的checker，A和B分別表示兩種spec，它們接收相同的輸入(Input)，checker比較二者的輸出是否相等。如果找到一個(gè)輸入序列導(dǎo)致輸出比較失敗，就是找個(gè)了一個(gè)反例（CounterExample）,工具會(huì)將此反例，包括相應(yīng)的輸入記錄下來(lái)，呈現(xiàn)出來(lái)。這個(gè)checker其實(shí)是個(gè)黑盒（Black box），因?yàn)槲覀儫o(wú)法觀察A和B內(nèi)部的狀態(tài)或者信號(hào)（白盒White box則可以）。

如果A和B足夠簡(jiǎn)單，那我們可以測(cè)到所有可能的情形，或者用Formal Verification來(lái)判定二者完全等價(jià)。同時(shí)，我們也可以借助這個(gè)等價(jià)來(lái)簡(jiǎn)化一些復(fù)雜的的問(wèn)題，例如圖2所示，一個(gè)更加復(fù)雜的系統(tǒng)，里面包含了A和B。

在這個(gè)例子中，因?yàn)槲覀兿惹耙呀?jīng)證明了A等價(jià)于B，我們可以做下簡(jiǎn)化操作，把A和B從系統(tǒng)中拿掉，簡(jiǎn)化成C和D的比較，如圖3所示。當(dāng)然，C和D的輸入(Inputs’) 與原始的輸入(Input)已經(jīng)有了很大的差別。這種divide and conquer 策略在FV中經(jīng)常使用，主要用來(lái)簡(jiǎn)化分析大的design。

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

CONES OF INFLUENCE

如果我們把一些把相干的邏輯分別考量，驗(yàn)證復(fù)雜度能大大簡(jiǎn)化。比如，我們有個(gè)硬件，實(shí)現(xiàn)加法和乘法運(yùn)算；在跑simulation的時(shí)候，我們可能造不同case側(cè)重不同的點(diǎn)，有點(diǎn)測(cè)加法，有的測(cè)乘法。如果我們加法和乘法拆分出來(lái)，單獨(dú)驗(yàn)，效率定能大幅提升，但在simulation里面不太現(xiàn)實(shí)，因?yàn)檫@需要造幾套驗(yàn)證環(huán)境。

FV則能比較好的支持這種拆分，F(xiàn)V工具讀取property，將設(shè)計(jì)里面一些與當(dāng)前property不相關(guān)的邏輯移移除掉。這個(gè)叫cone of influence 簡(jiǎn)化。如圖4所示，我們只考量result輸出的時(shí)候，很多邏輯對(duì)這個(gè)輸出沒(méi)影響，我們可以把它們簡(jiǎn)化掉。如果design特別大的話，這種可以極大的簡(jiǎn)化復(fù)雜度。

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

BDD

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

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

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

進(jìn)一步觀察，左側(cè)兩個(gè)z，無(wú)論取值如何，輸出都是一樣，說(shuō)明父節(jié)點(diǎn)y不影響結(jié)果。同理，對(duì)于觀察右側(cè)，z節(jié)點(diǎn)多余。于是，我們可以進(jìn)一步簡(jiǎn)化成圖8這樣的。

當(dāng)然，如果選擇變量的順序不一樣，我們得到的BDD的大小會(huì)有所不同。如果我們選擇z->x->y的順序的，我們將得到圖9這樣的BDD。對(duì)于一些大的design來(lái)說(shuō)，如果順序選擇不當(dāng)，可能導(dǎo)致指數(shù)爆炸。通常用Heuristic-based 算法來(lái)尋找最佳的變量順序。比如根據(jù)電路的拓?fù)浣Y(jié)構(gòu)來(lái)，根據(jù)變量的相關(guān)性來(lái)映射。另一種方法是嘗試將每一個(gè)輸入變量替換0或者1，看看哪個(gè)精簡(jiǎn)的程度更大些。

對(duì)于大而復(fù)雜的設(shè)計(jì)來(lái)說(shuō)，提取BDD仍然是一件很艱難的工作，或許隨著輸入的增加而指數(shù)級(jí)增長(zhǎng)。

COMPUTING A BDD FOR A CIRCUIT DESIGN

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

基本的與或非邏輯的BDD，參見(jiàn)圖10所示。

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

MODEL CHECKING

Model checking是FV工具分析一段時(shí)間內(nèi)時(shí)序邏輯的主要方法。給定properties ，model-checking 會(huì)去搜索可能的未來(lái)狀態(tài)，然后判定是否違反這些property。

首先創(chuàng)建初始狀態(tài)的BDD，然后根據(jù)相應(yīng)的邏輯推導(dǎo)出下一個(gè)狀態(tài)的BDD，不斷重復(fù)這個(gè)過(guò)程（reachability ），直到所有的狀態(tài)都加進(jìn)來(lái)。如果遇到vilation，F(xiàn)V會(huì)倒推回去，給出一個(gè)反例。

model checker 可能出出現(xiàn)三種情形：

設(shè)計(jì)符合spec

有violation，并給出反例

邏輯爆炸，無(wú)法證明；只能推測(cè)N個(gè)cycle沒(méi)有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&c

p -> q 等價(jià)于 !p || q

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

SOLVING THE SAT PROBLEM

對(duì)于很多表達(dá)式，證明其成立可能比較困難，但找反例則會(huì)簡(jiǎn)單的多。如果我們寫成AND形式，那只需要有一項(xiàng)為0，則表達(dá)式為0.

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

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

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

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

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

改寫一下：

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

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

THE DAVIS-PUTNAM SAT ALGORITHM

一個(gè)個(gè)枚舉顯然不太合理，一個(gè)簡(jiǎn)單的思路是先考慮一個(gè)變量，這樣就拆分成兩個(gè)子問(wèn)題：一個(gè)a=0和一個(gè)a=1的情形。不斷重復(fù)這個(gè)過(guò)程，直到證明或者有違規(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)}

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

一個(gè)典型的列子如圖13所以

總結(jié)：

不要理解成formal是逐個(gè)枚舉輸入變量的值，formal實(shí)際上用的數(shù)學(xué)方法來(lái)證明的。