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

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

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

使用形式驗證之目的

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

形式驗證的優點包括:

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

形式驗證技術

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

20190715_formalverification_TA31P1

圖1:各種形式驗證技術。
(來源:Aijaz Fatima)

模型檢查

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

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

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

20190715_formalverification_TA31P2

圖2:模型檢查程序。
(來源:Aijaz Fatima)

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

定理證明

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

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

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

20190715_formalverification_TA31P3

圖3:定理證明程序。
(來源:Aijaz Fatima)

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

等價性檢查

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

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

20190715_formalverification_TA31P4

圖4:邏輯等效性檢查。
(來源:Aijaz Fatima)

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

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

20190715_formalverification_TA31P5

圖5:順序等效性檢查。
(來源:Aijaz Fatima)

總結

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

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

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

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