在當(dāng)前復(fù)雜的數(shù)字設(shè)計(jì)開(kāi)發(fā)過(guò)程中，功能驗(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ì)過(guò)程中的主要瓶頸：高達(dá)70%的設(shè)計(jì)開(kāi)發(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)證具有非窮盡的固有特性，因此邊際情形無(wú)法被檢測(cè)到。事實(shí)上，不管你用多少時(shí)間仿真，也不管你的測(cè)試平臺(tái)和發(fā)生器有多么智能，通過(guò)仿真驗(yàn)證設(shè)計(jì)意圖對(duì)于電路以外的所有電路來(lái)說(shuō)都是不完整的?；镜姆抡?zhèn)蜗窨梢员环殖扇?lèi)：窮盡型、可控型和可觀察型。

　　形式驗(yàn)證是一個(gè)系統(tǒng)性的過(guò)程，將使用數(shù)學(xué)推理來(lái)驗(yàn)證設(shè)計(jì)意圖(指標(biāo))在實(shí)現(xiàn)(RTL)中是否得以貫徹。形式驗(yàn)證可以克服所有3種仿真挑戰(zhàn)，因?yàn)樾问津?yàn)證能夠從算法上窮盡檢查所有隨時(shí)間可能變化的輸入值。換句話說(shuō)，沒(méi)有必要表明如何激勵(lì)設(shè)計(jì)或創(chuàng)建多種條件來(lái)實(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è)彈性緩存例子(見(jiàn)圖1)。數(shù)據(jù)可以在時(shí)鐘域間改變，能夠根據(jù)兩個(gè)時(shí)鐘之間的相位和頻率偏移做出調(diào)整。數(shù)據(jù)必須無(wú)損地通過(guò)彈性緩存進(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ù)來(lái)縮短驗(yàn)證時(shí)間，同時(shí)改進(jìn)他們的整體驗(yàn)證工作。然而，一般采用的ABV專(zhuān)注于局部的、在仿真中使用的RTL實(shí)現(xiàn)相關(guān)斷言。所有內(nèi)部斷言的匯聚不會(huì)表征或完整規(guī)定微架構(gòu)定義的那種模塊的端到端行為。此外，當(dāng)設(shè)計(jì)實(shí)現(xiàn)改變時(shí)，這些局部性斷言不能重復(fù)使用。換句話說(shuō)，通過(guò)端到端屬性(包括數(shù)據(jù)完整性和包順序)和規(guī)定模塊必需的黑箱行為，高層斷言(我們?cè)诒疚闹兄父邔右?提供高得多的設(shè)計(jì)功能覆蓋率，并且能在各種設(shè)計(jì)實(shí)現(xiàn)和多個(gè)項(xiàng)目之間重復(fù)使用。更重要的是，通過(guò)形式性驗(yàn)證模塊的高層要求集，可以使驗(yàn)證完整性和產(chǎn)能得到顯著提高。因此，高層形式驗(yàn)證無(wú)需模塊級(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. 高層要求覆蓋了與工程師想要寫(xiě)入的數(shù)百條較低層斷言相同的設(shè)計(jì)空間

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

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

　　理想的形式驗(yàn)證工具要求具有一定的規(guī)模，以便窮盡地檢查所有可能的輸入條件以及設(shè)計(jì)中任意點(diǎn)的可控性和可視性(見(jià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)主義的做法，也就是說(shuō)，你通過(guò)反復(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)建功能覆蓋模型、開(kāi)發(fā)測(cè)試平臺(tái)、創(chuàng)建輸入激勵(lì)發(fā)生器、編寫(xiě)指導(dǎo)性測(cè)試以及執(zhí)行測(cè)試、分析覆蓋率指標(biāo)、調(diào)整激勵(lì)發(fā)生器以面向未驗(yàn)證的設(shè)計(jì)部分，然后反復(fù)這一過(guò)程。純形式驗(yàn)證技術(shù)則相反，專(zhuān)注于證實(shí)模塊的端到端、直接對(duì)應(yīng)微架構(gòu)規(guī)范的高層要求，幫助用戶戲極大提高項(xiàng)目的設(shè)計(jì)和驗(yàn)證產(chǎn)能，同時(shí)確保正確性。