數(shù)字IC的設(shè)計(jì)流程，如下圖所示：

　　形式驗(yàn)證（Formal Verification）是一種IC設(shè)計(jì)的驗(yàn)證方法，它的主要思想是通過使用數(shù)學(xué)證明的方式來驗(yàn)證一個(gè)設(shè)計(jì)的功能是否正確。

　　形式驗(yàn)證可以分為三大類：

　　等價(jià)性檢查（Equivalence Checking）

　　形式模型檢查（Formal Model Checking）（也被稱作特性檢查）

　　定理證明（Theory Prover）

　　為什么要做形式驗(yàn)證？電路不也是工具綜合出來的嗎？為什么不能保證一致性？因?yàn)楣ぞ咭彩侨俗龀鰜淼?，也有可能?huì)出錯(cuò)，所以要確認(rèn)。

　　我們平時(shí)做的最多的模擬仿真，就是給各種case的輸入，窮盡各種組合，總是希望100%的驗(yàn)證到所有的情況。但是有些情況下，你不太可能達(dá)到這一個(gè)目的。假如有一個(gè)32位的比較器：

　　比較產(chǎn)生等于、大于、大于的結(jié)果。

　　假設(shè)采用一個(gè)快速模擬器，每微秒運(yùn)行一個(gè)向量，則用模擬器模擬完全部模擬向量需要的時(shí)間為：

　　264 （all input patterns） X 10^-6

　　---------------------------------------------------

　　3600 （seconds） X 24 （hours） X 365 （days）

　　≈584，942 years

　　顯然這是一個(gè)不切實(shí)際的驗(yàn)證時(shí)間。而形式驗(yàn)證使用嚴(yán)格的數(shù)學(xué)推理來證明待測(cè)試設(shè)計(jì)的正確性，由于其靜態(tài)、數(shù)學(xué)的特性，避免了對(duì)所有可能測(cè)試向量的枚舉，而且能夠達(dá)到100%無死角的檢測(cè)。

　　定理證明是形式驗(yàn)證技術(shù)中最高大上的，它需要設(shè)計(jì)行為的形式化描述，通過嚴(yán)格的數(shù)學(xué)證明，比較HDL描述的設(shè)計(jì)和系統(tǒng)的形式化描述在所有可能輸入下是否一致。這種驗(yàn)證方法需要非常深厚的數(shù)學(xué)功底，而且不能完全自動(dòng)化，所以應(yīng)用案例較少。

　　當(dāng)然還是有一些例子，例如HOL系統(tǒng)、PVS系統(tǒng)和ACL2系統(tǒng)等，并且都有成功應(yīng)用案例。Moore等人驗(yàn)證了AMD5K86芯片的除法算法的微碼，Brock等驗(yàn)證了Motorola的CAP處理器，Clark等驗(yàn)證了SRT除法算法。

　　模型檢驗(yàn)是一種檢測(cè)設(shè)計(jì)是否具有所需屬性的方法，如安全性、活性和公平性。模型檢驗(yàn)所針對(duì)的對(duì)象是同步時(shí)序設(shè)計(jì)。系統(tǒng)的設(shè)計(jì)spec用時(shí)序狀態(tài)邏輯公式來描述。而通過對(duì)有限狀態(tài)系統(tǒng)的所有可能的狀態(tài)空間遍歷來證明設(shè)計(jì)是符合規(guī)范的，增強(qiáng)設(shè)計(jì)者的信心；或者是通過提供違反spec的反例，以幫助設(shè)計(jì)者來發(fā)現(xiàn)早期設(shè)計(jì)的錯(cuò)誤。

　　反例給出的方式是從系統(tǒng)的初始狀態(tài)出發(fā)到“壞”的狀態(tài)的路徑。系統(tǒng)的狀態(tài)空間能夠用有效的抽象符號(hào)算法來隱含地描述。抽象符號(hào)算法包括有向遷移圖、二叉決策圖（BDD- binary decision diagram）、合取范式（CNF- conjunctive normal form）等有效手段。

　　目前比較著名的模型檢驗(yàn)工具：

　　Carnegie Mellon大學(xué)的符號(hào)模型檢驗(yàn)工具SMV、Stanford 研究所的原型驗(yàn)證系統(tǒng)PVS、U.C.Berkerley的驗(yàn)證和綜合工具VIS和Bell實(shí)驗(yàn)室的軟件和協(xié)議驗(yàn)證工具Spin等。

　　等價(jià)性檢查用于比較設(shè)計(jì)的兩種實(shí)現(xiàn)是否一致，可分為組合等價(jià)性檢查和時(shí)序等價(jià)性檢查。目前是我們?cè)O(shè)計(jì)驗(yàn)證過程中用得最多的方法。

　　它也是利用數(shù)學(xué)技術(shù)來驗(yàn)證參考設(shè)計(jì)與改動(dòng)后的設(shè)計(jì)等價(jià)，主要目的是在一個(gè)設(shè)計(jì)經(jīng)過變換之后，窮盡地檢驗(yàn)變換前后的功能一致性，即證明設(shè)計(jì)的變換沒有產(chǎn)生功能的變化，如下圖所示：

　　等價(jià)性檢查被廣泛應(yīng)用到設(shè)計(jì)流程中的各個(gè)不同階段，用于驗(yàn)證不同設(shè)計(jì)層次之間的功能一致性。

　　或者用來驗(yàn)證RTL級(jí)對(duì)RTL級(jí)、RTL級(jí)對(duì)門級(jí)以及門級(jí)實(shí)現(xiàn)之間是否等價(jià)。

　　等價(jià)性檢查的主要優(yōu)點(diǎn)是比窮舉式的模擬仿真更快，通常可在數(shù)小時(shí)內(nèi)驗(yàn)證數(shù)百萬門規(guī)模集成電路的一致性，這對(duì)模擬仿真是不可能的。

　　比如我們?cè)趖apeout前突然因?yàn)橐粋€(gè)bug改動(dòng)比較大，看仿真已經(jīng)來不及了，但怎么能放心的出去呢，只能靠等價(jià)性檢查。因此，等價(jià)性檢查工具已經(jīng)被主流的設(shè)計(jì)流程所采用。

　　等價(jià)性檢查的問題是需要一個(gè)參考設(shè)計(jì)作為描述，而如何設(shè)計(jì)一個(gè)理想?yún)⒖寄Ｐ停╣old design）又是一個(gè)很重的任務(wù)。

　　此外，等價(jià)性驗(yàn)證是為了找出實(shí)現(xiàn)的不一致性，而不能找出參考設(shè)計(jì)原先就可能存在的bug。另外等價(jià)性檢查不能驗(yàn)證設(shè)計(jì)對(duì)象的時(shí)序，只能驗(yàn)證功能，因此它通常需要和時(shí)序分析工具配合在一起使用。

　　等價(jià)性檢查主要是比較兩種設(shè)計(jì)中相應(yīng)的組合功能塊。可以在參考設(shè)計(jì)中指定比較點(diǎn)，然后比較2種設(shè)計(jì)在該點(diǎn)的邏輯功能是否等價(jià)。比較點(diǎn)可以是輸出端口、寄存器、鎖存器、黑盒輸入pin或被驅(qū)動(dòng)的線網(wǎng)等。

　　邏輯錐（logical cone）是一組可驅(qū)動(dòng)比較點(diǎn)的信號(hào)，它有n個(gè)輸入（基本輸入，狀態(tài)點(diǎn)）和一個(gè)輸出（基本輸出，狀態(tài)點(diǎn)），也可以包含其他邏輯錐，如下圖所示：

　　最右邊是一個(gè)輸出端口，可以將它將作為一個(gè)比較點(diǎn)，與參考設(shè)計(jì)中相應(yīng)的對(duì)象進(jìn)行比較，比較的過程實(shí)際上就是考察它們的邏輯錐是否等價(jià)。所以對(duì)于報(bào)告出來的不匹配的點(diǎn)，我們也可以通過對(duì)它們邏輯錐進(jìn)行分析，來找出具體的原因。

　　因此，等價(jià)性檢查的具體工作就是比較兩種設(shè)計(jì)中的關(guān)鍵點(diǎn)的等價(jià)性并將兩種設(shè)計(jì)中任何不匹配之處標(biāo)記、報(bào)告出來。

　　等價(jià)性檢查的工具有：

　　Synopsys的Formality，Cadence的Incisive Conformal，Mentor Graphics公司的FormalPro等。

　　最后，總結(jié)一下模擬仿真和形式驗(yàn)證的比較：

　　形式驗(yàn)證目前還不能完全取代模擬仿真驗(yàn)證。兩者各有所長(zhǎng)，技術(shù)互補(bǔ)，在驗(yàn)證過程中應(yīng)該結(jié)合使用，爭(zhēng)取找出設(shè)計(jì)中所有的bug！