深層解析形式驗(yàn)證

　　等價(jià)性檢查的驗(yàn)證用于驗(yàn)證RTL設(shè)計(jì)與門級(jí)網(wǎng)表、門級(jí)網(wǎng)表與門級(jí)網(wǎng)表是否一致。在進(jìn)行掃描鏈重排、時(shí)鐘樹綜合等過程中，都可以用等價(jià)性檢查保證網(wǎng)表的一致性。等價(jià)性檢查已經(jīng)融入IC標(biāo)準(zhǔn)設(shè)計(jì)流程中。等價(jià)性檢查在檢查ECO時(shí)非常有用。例如，設(shè)計(jì)者在修改門級(jí)網(wǎng)表時(shí)，由于手誤，錯(cuò)將一個(gè)或門寫成或非門，等價(jià)性檢查工具通過比較RTL設(shè)計(jì)與門級(jí)網(wǎng)表，可以很容易地發(fā)現(xiàn)這種錯(cuò)誤。

　　模型檢查用時(shí)態(tài)邏輯來描述規(guī)范，通過有效的搜索方法來檢查給定的系統(tǒng)是否滿足規(guī)范。模型檢查是目前研究的熱點(diǎn)，但其驗(yàn)證的電路規(guī)模受限制這一問題還沒有得到很好的解決。

　　定理證明把系統(tǒng)與規(guī)范都表示成數(shù)學(xué)邏輯公式，從公理出發(fā)尋求描述。定理證明驗(yàn)證的電路模型不受限制，但需要使用者的人工干預(yù)和較多的背景知識(shí)。

在當(dāng)前復(fù)雜的數(shù)字設(shè)計(jì)開發(fā)過程中，功能驗(yàn)證十分重要。雖然硬件的復(fù)雜度仍遵循摩爾定律持續(xù)增長(zhǎng)，但是驗(yàn)證的復(fù)雜性更具挑戰(zhàn)。事實(shí)上，隨著硬件復(fù)雜性隨時(shí)間呈雙指數(shù)增長(zhǎng)，驗(yàn)證復(fù)雜性理論上也呈指數(shù)增長(zhǎng)。驗(yàn)證已被公認(rèn)為是設(shè)計(jì)過程中的主要瓶頸：高達(dá)70%的設(shè)計(jì)開發(fā)時(shí)間和資源花在功能驗(yàn)證上。Collett International Research認(rèn)為，即使在驗(yàn)證上花費(fèi)如此巨大的精力和資源，功能性缺陷仍是芯片重新流片的頭號(hào)原因。

　　功能性驗(yàn)證挑戰(zhàn)

　　邊際情形(corner-case)的缺陷是仿真?zhèn)蜗瘢捎谝苑抡鏋榛A(chǔ)的驗(yàn)證具有非窮盡的固有特性，因此邊際情形無法被檢測(cè)到。事實(shí)上，不管你用多少時(shí)間仿真，也不管你的測(cè)試平臺(tái)和發(fā)生器有多么智能，通過仿真驗(yàn)證設(shè)計(jì)意圖對(duì)于最小電路以外的所有電路來說都是不完整的?；镜姆抡?zhèn)蜗窨梢员环殖扇悾焊F盡型、可控型和可觀察型，如下表1所示。

　　形式驗(yàn)證是一個(gè)系統(tǒng)性的過程，將使用數(shù)學(xué)推理來驗(yàn)證設(shè)計(jì)意圖(指標(biāo))在實(shí)現(xiàn)(RTL)中是否得以貫徹。形式驗(yàn)證可以克服所有3種仿真挑戰(zhàn)(表1)，因?yàn)樾问津?yàn)證能夠從算法上窮盡檢查所有隨時(shí)間可能變化的輸入值。換句話說，沒有必要表明如何激勵(lì)設(shè)計(jì)或創(chuàng)建多種條件來實(shí)現(xiàn)較高的可觀察性。

　　雖然從理論上講，仿真測(cè)試平臺(tái)的輸入端口針對(duì)待驗(yàn)證設(shè)計(jì)(DUV)具有較高的可控性，但測(cè)試平臺(tái)對(duì)內(nèi)部點(diǎn)的可控性一般較差。為了使用基于仿真的方法識(shí)別設(shè)計(jì)錯(cuò)誤，以下條件必須保持：

　　* 必須產(chǎn)生正確的輸入激勵(lì)，以激活(也就是敏感化)設(shè)計(jì)中某個(gè)點(diǎn)的缺陷

　　* 必須產(chǎn)生正確的輸入激勵(lì)，以便將源自缺陷的所有效果傳送到輸出端口

　　在使用基于仿真的驗(yàn)證時(shí)，需要規(guī)劃設(shè)計(jì)中需要驗(yàn)證的對(duì)象：

　　* 定義需要測(cè)試的各種輸入條件

　　* 創(chuàng)建功能性覆蓋模型(確定是否做了足夠的仿真)

　　* 搭建測(cè)試平臺(tái)(檢查器，測(cè)試樁，發(fā)生器等)

　　* 創(chuàng)建特定的直接測(cè)試

　　* 成年累月的仿真

　　現(xiàn)實(shí)中，工程師一直在反復(fù)做著這些事：運(yùn)行測(cè)試、調(diào)試故障、再次仿真回歸組、觀察各種覆蓋率指標(biāo)，以及調(diào)整激勵(lì)(例如操控輸入發(fā)生器)以覆蓋以前未覆蓋的設(shè)計(jì)部分。

　　這里我們討論一個(gè)彈性緩存例子(見圖1)。數(shù)據(jù)可以在時(shí)鐘域間改變，能夠根據(jù)兩個(gè)時(shí)鐘之間的相位和頻率偏移做出調(diào)整。數(shù)據(jù)必須無損地通過彈性緩存進(jìn)行傳送，即使在設(shè)計(jì)允許時(shí)鐘不完全同步的情況下。在這個(gè)案例中的一個(gè)功能性缺陷例子是在時(shí)鐘有效沿對(duì)齊時(shí)由于數(shù)據(jù)的變化而出現(xiàn)的緩存溢出。這就可能要求對(duì)所有可能的輸入條件進(jìn)行大量的仿真和考慮，以建模和仿真這種錯(cuò)誤行為。

　　圖1：彈性緩存框圖

　　高層要求

　　許多公司已經(jīng)采用基于斷言的驗(yàn)證(ABV)技術(shù)來縮短驗(yàn)證時(shí)間，同時(shí)改進(jìn)他們的整體驗(yàn)證工作。然而，一般采用的ABV專注于局部的、在仿真中使用的RTL實(shí)現(xiàn)相關(guān)斷言。所有內(nèi)部斷言的匯聚不會(huì)表征或完整規(guī)定微架構(gòu)定義的那種模塊的端到端行為。此外，當(dāng)設(shè)計(jì)實(shí)現(xiàn)改變時(shí)，這些局部性斷言不能重復(fù)使用。換句話說，通過端到端屬性(包括數(shù)據(jù)完整性和包順序)和規(guī)定模塊必需的黑箱行為，高層斷言(我們?cè)诒疚闹兄父邔右?提供高得多的設(shè)計(jì)功能覆蓋率，并且能在各種設(shè)計(jì)實(shí)現(xiàn)和多個(gè)項(xiàng)目之間重復(fù)使用。更重要的是，通過形式性驗(yàn)證模塊的高層要求集，可以使驗(yàn)證完整性和產(chǎn)能得到顯著提高。因此，高層形式驗(yàn)證無需模塊級(jí)仿真，可極大地縮短系統(tǒng)級(jí)驗(yàn)證時(shí)間。讓我們?cè)敿?xì)地看看圖2所示的高層要求。

　　圖2：要求與RTL斷言對(duì)比。

　　Y軸代表抽取層，X軸代表被某個(gè)特殊斷言或要求覆蓋的設(shè)計(jì)數(shù)量。沿Y軸越往上走，被高層要求覆蓋的設(shè)計(jì)空間就越大。證實(shí)這些高層要求具有很高價(jià)值，原因有很多：

　　1. 高層要求關(guān)系到微架構(gòu)中的要求

　　2. 高層要求關(guān)系到測(cè)試平臺(tái)中的輸出檢查器組

　　3. 高層要求覆蓋了與工程師想要寫入的數(shù)百條較低層斷言相同的設(shè)計(jì)空間

　　4. 高層要求覆蓋了由于工程師遺漏的較低層斷言的缺失而未被覆蓋的設(shè)計(jì)空間

　　最后一點(diǎn)我們這里舉個(gè)例子，假如設(shè)計(jì)包含一個(gè)FIFO，并且工程師忘了編寫一個(gè)斷言來檢查FIF從不下溢。這種安全性違例將由高層要求加以識(shí)別。然而，通過形式性地驗(yàn)證高層要求，高層要求違例的根源就能得以跟蹤。例如，如果針對(duì)高層要求在影響錐中包含了FIFO，那么導(dǎo)致高層要求不能滿足的下溢條件將被檢測(cè)到。

　　理想的形式驗(yàn)證工具要求具有一定的規(guī)模，以便窮盡地檢查所有可能的輸入條件以及設(shè)計(jì)中任意點(diǎn)的可控性和可視性(見表1)。我們的旗艦產(chǎn)品，例如JasperGold，就采用了高性能和大規(guī)模的形式驗(yàn)證技術(shù)，能夠窮盡地驗(yàn)證模塊是否滿足源自微架構(gòu)的高層要求。這款產(chǎn)品使用數(shù)學(xué)算法，因?yàn)椴恍枰褂梅抡鏈y(cè)試平臺(tái)或激勵(lì)。

　　表1：仿真與形式驗(yàn)證的比較

　　本文小結(jié)

　　形式驗(yàn)證要求你以不同的方式思考。例如，仿真是完全經(jīng)驗(yàn)主義的做法，也就是說，你通過反復(fù)試驗(yàn)試圖查明缺陷，這要花相當(dāng)多的時(shí)間嘗試所有可能的組合，因此永遠(yuǎn)不會(huì)完整。另外，由于工程師必須定義和產(chǎn)生大量輸入條件，他們的工作重點(diǎn)將是如何在非設(shè)計(jì)目標(biāo)基礎(chǔ)上分解設(shè)計(jì)。另一方面，形式驗(yàn)證是窮盡式數(shù)學(xué)技術(shù)，允許工程師僅關(guān)注設(shè)計(jì)意圖，或“什么是設(shè)計(jì)的正確行為?”。

　　驗(yàn)證實(shí)現(xiàn)工作包括將多種輸入條件定義為測(cè)試計(jì)劃的一部分、創(chuàng)建功能覆蓋模型、開發(fā)測(cè)試平臺(tái)、創(chuàng)建輸入激勵(lì)發(fā)生器、編寫指導(dǎo)性測(cè)試以及執(zhí)行測(cè)試、分析覆蓋率指標(biāo)、調(diào)整激勵(lì)發(fā)生器以面向未驗(yàn)證的設(shè)計(jì)部分，然后反復(fù)這一過程。純形式驗(yàn)證技術(shù)則相反，專注于證實(shí)模塊的端到端、直接對(duì)應(yīng)微架構(gòu)規(guī)范的高層要求，幫助用戶戲極大提高項(xiàng)目的設(shè)計(jì)和驗(yàn)證產(chǎn)能，同時(shí)確保正確性。