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

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

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

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

目的

形式驗(yàn)證技術(shù)跟蹤標(biāo)準(zhǔn)驗(yàn)證技術(shù)未檢測到的錯誤。此外，對于可以使用標(biāo)準(zhǔn)技術(shù)檢測到的錯誤，形式驗(yàn)證通常以明顯更快的速度識別它們。在通過仿真和仿真對設(shè)計進(jìn)行功能驗(yàn)證之前，先進(jìn)行形式驗(yàn)證。

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

在設(shè)計周期早期檢測錯誤

耗時少

可靠的

快點(diǎn)

詳盡無遺

形式驗(yàn)證技術(shù)

模型檢查

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

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

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

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

運(yùn)行模型檢查器以找出模型 M 是否滿足公式 ?。

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

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

優(yōu)缺點(diǎn)

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

定理證明

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

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

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

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

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

優(yōu)點(diǎn)和缺點(diǎn)

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

等價檢查

等價檢查是驗(yàn)證兩個設(shè)計在功能上是否相同的過程。兩種類型的等價檢查技術(shù)如下：

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

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

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

總結(jié)

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

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

審核編輯：湯梓紅