形式驗證是一種自動檢查方法，可以捕捉許多常見的設計錯誤，并可以發(fā)現(xiàn)設計中的歧義。

形式驗證是使用數(shù)學技術驗證設計正確性的過程。形式驗證工具使用各種算法來驗證設計并且不執(zhí)行任何時序檢查。這些工具不需要激勵或測試臺，因此，形式驗證在 IC 設計周期的早期執(zhí)行——即，只要 RTL 代碼可用。越早發(fā)現(xiàn)錯誤，就越容易修復。

在英特爾處理器中發(fā)現(xiàn)著名的奔騰漏洞后，形式驗證開始流行，導致召回有故障的處理器，英特爾不得不承擔近 5 億美元的損失。通過正式驗證，可以避免各種其他事件，例如 Ariane 5 爆炸和巴拿馬癌癥研究所的輻射過度暴露。

硬件系統(tǒng)的許多應用都很關鍵，其中任何故障都可能導致高額的財務或物理損失。本文討論形式驗證及其各種化身。

目的

形式驗證技術跟蹤標準驗證技術未檢測到的錯誤。此外，對于可以使用標準技術檢測到的錯誤，形式驗證通常以明顯更快的速度識別它們。在通過仿真和仿真對設計進行功能驗證之前，先進行形式驗證。

形式驗證的一些優(yōu)點如下：

在設計周期早期檢測錯誤

耗時少

可靠的

快點

詳盡無遺

形式驗證技術

模型檢查

模型檢查，也稱為屬性檢查，是一種基于狀態(tài)的形式驗證方法。

以下步驟解釋了模型檢查的過程：

對系統(tǒng)建模以獲得模型 M。系統(tǒng)被建模為一組狀態(tài)，其中包含一組狀態(tài)之間的轉(zhuǎn)換，這些轉(zhuǎn)換描述了系統(tǒng)如何響應內(nèi)部或外部刺激從一個狀態(tài)移動到另一個狀態(tài)。

使用屬性規(guī)范語言(例如 PSL 或 SVA)創(chuàng)建要驗證的屬性，以得出公式 ?。屬性是對設計行為的描述。

運行模型檢查器以找出模型 M 是否滿足公式 ?。

如果模型不滿足該性質(zhì)，則生成反例。反例是違反屬性的刺激，通常顯示為可在仿真中使用的波形。

用仿真中的系統(tǒng)模型運行反例，找出錯誤的位置。

優(yōu)缺點

一旦系統(tǒng)模型和屬性規(guī)范被提供給模型檢查器，驗證過程是全自動的。但是，就模型檢查器要處理的狀態(tài)數(shù)量而言，系統(tǒng)應該很小。

定理證明

定理證明是使用數(shù)學推理驗證實現(xiàn)的系統(tǒng)是否滿足設計要求(或規(guī)范)的過程。它是一種基于證明的形式驗證方法。

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

將系統(tǒng)建模為形式數(shù)學邏輯中的一組數(shù)學定義。

從數(shù)學定義中推導出系統(tǒng)的屬性。

使用定理證明器來驗證系統(tǒng)是否符合規(guī)范。有各種可用的定理證明器按其基礎邏輯分類。定理證明者也可以稱為證明助手。

優(yōu)點和缺點

定理證明的最大優(yōu)點是它可以處理非常復雜的系統(tǒng)。但是，定理證明不是全自動的，需要人工干預才能完成證明，這需要時間和專業(yè)知識。此外，在證明失敗的情況下，不會生成反例，這使得定位錯誤變得困難。

等價檢查

等價檢查是驗證兩個設計在功能上是否相同的過程。兩種類型的等價檢查技術如下：

邏輯等效檢查(LEC)：也稱為組合等效檢查，邏輯等效檢查是驗證兩個設計在寄存器之間具有相同組合邏輯的過程。兩個比較的設計也應該具有相同數(shù)量的寄存器。該技術用于驗證不同抽象級別的兩個設計在功能上是否相同;例如，門級網(wǎng)表在功能上與布局網(wǎng)表相同。

順序等價檢查 (SEC)：順序等價檢查是驗證兩個設計在功能上相同以及在提供相同輸入時提供相同輸出的過程。SEC 比較了兩種設計的時序邏輯，這兩種設計可能具有不同的實現(xiàn)方式。這是一個復雜的過程，因此非常受限于設計的大小。

有時，IC 的設計會在最后一刻進行修改，以包含一些功能、時序、電源或其他修復，或者包含一些額外的邏輯，例如掃描邏輯、電源控制電路等。此類更改需要驗證。標準驗證程序會耗費大量時間，因此會增加上市時間。順序等效檢查將修改后的設計與黃金設計進行比較，并驗證它們在功能上是否相同。

總結(jié)

形式驗證是一種自動檢查方法，可以發(fā)現(xiàn)許多常見的設計錯誤，并可以發(fā)現(xiàn)設計中的歧義。這是一種詳盡的方法，涵蓋所有輸入場景并檢測極端情況錯誤。

這種形式的驗證節(jié)省了設計人員的時間和精力，因為甚至在開發(fā)測試環(huán)境之前就發(fā)現(xiàn)了潛在的錯誤。它可用于設計的高級、RTL 或 GLS 表示。市場上有各種各樣復雜的形式化工具，其中許多提供了一種按鈕方式來查找設計中的錯誤。

審核編輯：湯梓紅