形式驗證(formal verification)是使用數學方法驗證設計正確性的過程，其工具使用各種演算法來驗證設計，但不執行任何時序檢查。這些工具不需要激勵(stimulus)或測試平台，在IC設計週期初期即可執行，也就是說，只要有RTL碼即可執行形式驗證。問題發現越早，修復就越容易。

形式驗證的普及得益於在英特爾(Intel) Pentium處理器發現漏洞的業界知名事件；該事件導致故障處理器召回，英特爾也不得不承擔近5億美元的損失。還有其他各種事故，例如Ariane 5號運載火箭爆炸，以及巴拿馬癌症研究所(Panama Cancer Institute)輻射量超標事故等；這些事故實際上都可以利用形式驗證以避免。

硬體系統有許多應用都至關重要，其產生的任何故障都可能導致極大的財務或實體損失。本文將討論形式驗證，以及該技術的各種「分身」。

使用形式驗證之目的

形式驗證技術可以追蹤標準驗證技術檢測不到的錯誤，而且若使用標準技術檢測可以檢測到錯誤，形式驗證通常可以以明顯更快的速率識別錯誤。在利用軟體模擬(simulation)和硬體模擬(emulation)工具對設計進行功能驗證之前，通常就已執行了形式驗證。

形式驗證的優點包括：

• 在設計週期初期發現bug；
• 花費時間更少；
• 可靠；
• 更快速；
• 更詳盡。

形式驗證技術

圖1是各種形式驗證技術，以下將一一說明。

圖1：各種形式驗證技術。
（來源：Aijaz Fatima）

模型檢查

模型檢查(Model checking)，也稱為屬性檢查(property)，是一種基於狀態(state-based)的形式驗證方法；參考圖2。

以下步驟說明了模型檢查的程序：

1. 對系統進行建模以得到模型M；具體來說，系統被建模為一組狀態，以及狀態之間的轉換(transitions)，用以描述系統如何回應內部或外部刺激、從一種狀態轉換至另一種狀態。
2. 使用屬性規範語言(property specification language)，如PSL或SVA，來建立要驗證的屬性，以得到公式Φ。屬性是設計行為的描述。
3. 運行模型檢查器以確定模型M是否滿足公式Φ。
4. 如果模型不滿足屬性，則生成反例(counterexample)；反例是違反屬性的激勵，通常在模擬軟體工具中以波形來表示。
5. 在模擬軟體中使用系統模型執行反例以查找錯誤位置。

圖2：模型檢查程序。
（來源：Aijaz Fatima）

模型檢查的優/缺點包括：一旦將系統模型和屬性規範提供給模型檢查器，驗證過程就將是完全自動的；但是從模型檢查器要處理的狀態數來看，模型檢查適用於小型系統。

定理證明

定理證明(theorem proving)是使用數學推理方法驗證所實現的系統是否滿足設計要求(或規範)的過程，是一種基於證據(proof-based)的形式驗證方法；參考圖3。

以下步驟解釋了定理證明的程序：

1. 在形式數學邏輯中將系統建模為一組數學定義。
2. 從數學定義中匯出系統的屬性。
3. 使用定理證明器(theorem prover)驗證系統是否符合規範；定理證明器或許也可以被稱為證明助理(proof assistant)，目前有各種可用的定理證明器，根據其基礎邏輯來分類。

圖3：定理證明程序。
（來源：Aijaz Fatima）

定理證明優/缺點：其最大優點是可以處理非常複雜的系統，但是定理證明並非全自動，需要人工干預才能完成，這需要時間以及專業。而且在證明失敗的情況下不會生成反例，這會使得定位錯誤相對困難。

等價性檢查

等價性檢查(Equivalence checking)是驗證兩個設計在功能上是否相同的過程；兩種類型的等價性檢查技術說明如下：

邏輯等價性檢查(Logical equivalence checking，LEC)：也稱為組合(combinational)等價性檢查，是驗證兩個設計在暫存器之間具有相同組合邏輯的過程，兩個被比較的設計也應具有相同數量的暫存器。該技術用於驗證不同抽象等級的兩個設計在功能上是否相同；例如，邏輯閘層級網表(gate-level netlist)，是否在功能上與電路佈局網表(layout netlist)相同；參考圖4。

圖4：邏輯等效性檢查。
（來源：Aijaz Fatima）

順序等價性檢查(Sequential equivalence checking，SEC)：順序等價性檢查是驗證兩個設計在功能上是否相同的過程，並且在提供相同輸入時驗證是否有相同的輸出。它用於比較兩種設計的順序邏輯(sequential logic)，而這兩種設計可能有不同的實現。SEC是一個複雜的過程，因此非常受設計規模的限制；參考圖5。

有時IC設計會在最後一刻進行修改，以合併某些功能、時序、電源或其他修正，或者包括一些額外的邏輯，如掃描邏輯、電源控制電路等；這些變化也需要驗證。標準驗證程式會耗費大量時間，會推因此遲產品上市時間；順序等效性檢查會將修改後的設計與標準設計進行比較，並驗證它們在功能上是否一致。

圖5：順序等效性檢查。
（來源：Aijaz Fatima）

總結

形式驗證是一種自動檢查方法，可以捕獲許多常見的設計錯誤，並且可以發現設計中的歧義。它是一種詳盡的方法，涵蓋了所有輸入場景，還可以檢測極端案例異常。

形式驗證可以節省設計工程師的時間和精力，因為潛在問題甚至可在測試環境被開發之前即被發現。它可用於設計的高階描述、RTL或GLS表示等階段。市場上有各種各樣複雜的形式驗證工具，其中許多工具還提供簡易的按鈕方式來查找設計中的問題。

本文同步刊登於電子工程專輯2019年7月號；編譯：Judith Cheng

(原文出自EE Times姊妹刊，ASPENCORE旗下EEWeb網站；參考連結：Introduction to Formal Verification，by Aijaz Fatim)

活動簡介

未來寬能隙半導體元件會在哪些應用成為主流？元件供應商又會開發出哪些新的應用寬能隙元件的電路架構，以協助電力系統開發商進一步簡化設計複雜度、提升系統整體效率？TechTaipei「寬能隙元件市場與技術發展研討會」將邀請寬能隙半導體的關鍵供應商一一為與會者解惑。

贊助廠商

立即報名