所謂形式驗證，是指從數學上完備地證明或驗證電路的實現方案是否確實實現了電路設計所描述的功能。形式驗證方法分為等價性驗證、模型檢驗和定理證明等。
基本介紹
- 中文名：形式驗證
- 外文名：Formal Verification
- 方法：等價性檢查、模型檢查等
- 優點：驗證時間短等
- 涉及領域：計算機、積體電路
- 學科：電子信息工程
原理,方法,優點,
原理
形式驗證時要確定電路在哪一級電路上的測試是正確的，使用模型檢驗的方法看兩個電路在描述上是否一致。
1．組合邏輯電路的邏輯驗證
對組合邏輯來說，不存在狀態暫存器，其輸出值Z[t]不依賴於前面的輸入值X[t-i](1≤i≤t)。這時只要對每個輸入向量證明其輸出向量相同。在組合邏輯驗證領域有以下兩類方法。
(1)轉換為單一抽象模型比較。通過對單一表示的結構進行比較，得出其功能等價的結論。在最壞的情況下，布爾函式為正，表示隨輸入個數指數增加，其過大的記憶體需求限制了一般布爾函式的驗證能力。
(2)利用測試輸入向量進行驗證。探尋使兩個電路具有不同輸出的輸入測試向量，若不存在這樣的測試向量，則電路在功能上等價。在最壞情況下，這種方法需要窮舉所有可能的輸入測試矢量，運行時間又成為一個主要問題。
2．時序邏輯電路的驗證
對一個時序電路而言，可以把它看成一個有限狀態機(FSM，finite-state machine)。電路功能的等價可以用有限狀態機的等價來判斷。假定有兩個狀態機A和B，要對它們進行比較。直觀的說，當A和B有相同的接口，而且從相同的初始狀態出發，兩者對有效輸入值序列產生相同的輸出值序列，則可以說A和B等價。
方法
形式驗證的方法有等價性檢查、模型檢查、定理證明等。形式驗證主要是用來在覆蓋所有可能的輸入情況下檢查是否與給定的規範一致。SoC驗證的形式化方法主要是等價性檢查和模型檢查。
模型檢查主要是檢查RTL代碼是否滿足規範中規定的一些特性。在規定這些特性時一般使用特性規範語言，目前一般也使用基於斷言的驗證語言。由於這種方法可以在不需要仿真的前提下檢查設計中所有可能出現的情況是否滿足規定的特性，所以使用這種方法不會遺漏任何的邊界情況。
等價性檢查主要是檢查兩個門級網表之間是否一致，保證網表處理後不會改變電路的功能，或者保證網表能正確地實現RTL代碼所描述的功能，或者保證兩種RTL描述邏輯一致。等價性檢查通過對比兩個描述來檢測它們的等價性。等價性檢查工具將兩個設計讀入記憶體，用形式化數據算法分析彼此的數據結構來進行比較。只要兩個設計的所有輸出管腳與每一個暫存器或鎖存器的功能是一樣的，那么就認為兩個設計的功能等效。它主要是用來尋找實現中的缺陷，而不是設計中的缺陷，與檢驗C語言到彙編語言的轉換的檢測類似。因此這種方法很難發現同時存在於兩種要比較的描述中的固有缺陷。
定理證明系統一般分為自動定理證明系統和互動定理證明系統，互動定理證明系統對硬體驗證來說最有價值。比較成熟的互動證明系統有Boyer-Moore定理證明器，它以遞歸函式論為基礎，以數學歸納法為核心技術；PVS原形驗證系統是基於高階邏輯和類型理論的；HOL定理證明器系統也是基於高階邏輯的系統；STEP是基於時態邏輯的定理證明系統；此外還有XYZ系統。定理證明器最適合為研究工作提供驗證工具和環境。
優點
形式驗證的優點如下：
(1)形式驗證是對指定描述的所有可能的情況進行驗證，覆蓋率達到了100%。
(2)形式驗證技術是借用數學上的方法將待驗證電路和功能描述或參考設計直接進行比較，不需要開發測試激勵。
(3)形式驗證的驗證時間短，可以很快發現和改正電路設計中的錯誤，可以縮短設計周期。
形式驗證主要驗證數字IC設計流程中的各個階段的代碼功能是否一致，包括綜合前RTL代碼和綜合後網表的驗證，因為如今IC設計的規模越來越大，如果對門級網表進行動態仿真，會花費較長的時間，而形式驗證只用幾個小時即可完成一個大型的驗證。另外，因為版圖後做了時鐘樹綜合，時鐘樹的插入意味著進入布圖工具的原來的網表已經被修改了，所以有必要驗證與原來的網表是邏輯等價的。
