數(shù)字IC的設計流程及驗證方法介紹

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

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

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

　　等價性檢查（Equivalence Checking）

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

　　定理證明（Theory Prover）

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

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

　　比較產生等于、大于、大于的結果。

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

　　264 （all input patterns） X 10^-6

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

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

　　≈584，942 years

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

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

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

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

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

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

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

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

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

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

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

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

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

　　等價性檢查的問題是需要一個參考設計作為描述，而如何設計一個理想參考模型（gold design）又是一個很重的任務。

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

　　等價性檢查主要是比較兩種設計中相應的組合功能塊?？梢栽趨⒖荚O計中指定比較點，然后比較2種設計在該點的邏輯功能是否等價。比較點可以是輸出端口、寄存器、鎖存器、黑盒輸入pin或被驅動的線網等。

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

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

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

　　等價性檢查的工具有：

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

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

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