形式驗(yàn)證簡(jiǎn)介

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

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

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

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

目的

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

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

在設(shè)計(jì)周期早期檢測(cè)錯(cuò)誤

耗時(shí)少

可靠的

快點(diǎn)

詳盡無(wú)遺

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

模型檢查

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

以下步驟解釋了模型檢查的過(guò)程：

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

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

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

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

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

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

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

定理證明

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

以下步驟解釋了定理證明的過(guò)程：

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

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

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

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

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

等價(jià)檢查

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

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

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

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

總結(jié)

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

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

審核編輯：湯梓紅