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

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

　　形式驗證可以分為三大類：

　　等價性檢查（Equivalence Checking）

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

　　定理證明（Theory Prover）

　　為什么要做形式驗證？電路不也是工具綜合出來的嗎？為什么不能保證一致性？因為工具也是人做出來的，也有可能會出錯，所以要確認。

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

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

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

　　264 （all input patterns） X 10^-6

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

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

　　≈584，942 years

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

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

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

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

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

　　目前比較著名的模型檢驗工具：

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

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

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

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

　　或者用來驗證RTL級對RTL級、RTL級對門級以及門級實現(xiàn)之間是否等價。

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

　　比如我們在tapeout前突然因為一個bug改動比較大，看仿真已經(jīng)來不及了，但怎么能放心的出去呢，只能靠等價性檢查。因此，等價性檢查工具已經(jīng)被主流的設(shè)計流程所采用。

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

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

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

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

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

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

　　等價性檢查的工具有：

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

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

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