IC設(shè)計(jì)復(fù)雜化加劇先進(jìn)驗(yàn)證方式重要性倍增

跟著一些新科技的呈現(xiàn)，例如Constrained-random Data Generation、Assertion-based Verification、Coverage-driven Verification以及Formal Model Checking等，衡量功用驗(yàn)證(Functional
Verification)作業(yè)功率的辦法現(xiàn)已大大不一樣。盡管模仿(Simulation)仍將繼續(xù)扮演實(shí)務(wù)上驗(yàn)證作業(yè)中不行或缺的部份，但當(dāng)咱們?cè)谠u(píng)價(jià)整個(gè)驗(yàn)證進(jìn)程的時(shí)分，仿真的速度現(xiàn)已不再是最首要的思考基準(zhǔn)。運(yùn)用者可以藉由上述多項(xiàng)新科技的幫忙，調(diào)配原先所獨(dú)自憑借的模仿，完結(jié)更領(lǐng)先的驗(yàn)證作業(yè)。如此一來(lái)，盡管今天世上的描繪繼續(xù)以驚人速度雜亂化，描繪者依然可以因本人的驗(yàn)證作業(yè)能找出各式各樣的偏遠(yuǎn)個(gè)案(Corner cases)而充溢決心。

可是，單純讓作業(yè)「跑得更快」現(xiàn)已不夠了，眼前可以看到的描繪現(xiàn)已變得太大且太雜亂，無(wú)法成功猜測(cè)一切的偏遠(yuǎn)個(gè)案(Corner cases)，因而，驗(yàn)證戰(zhàn)略有必要批改，而為了要清晰界說(shuō)出怎樣改動(dòng)才干正確且滿足地到達(dá)政策，有必要先界說(shuō)清晰幾件作業(yè)，也就是一個(gè)成功的驗(yàn)證次序一切必要到達(dá)的根本政策如下:

?有必要通知運(yùn)用者上述兩項(xiàng)政策何時(shí)現(xiàn)已被到達(dá)了。

長(zhǎng)久以來(lái)，模仿就是驗(yàn)證(Verification)的核心技能。驗(yàn)證工程師對(duì)準(zhǔn)需求驗(yàn)證的描繪，發(fā)展出測(cè)驗(yàn)檔來(lái)發(fā)作所需求的測(cè)驗(yàn)鼓勵(lì)(Stimuli)寫(xiě)入在描繪里邊，在完結(jié)模仿之后查看作用是不是得到正確的反響。一切的測(cè)驗(yàn)都需求花時(shí)刻來(lái)編寫(xiě)、除錯(cuò)還有實(shí)行。當(dāng)咱們斷定某一個(gè)測(cè)驗(yàn)可以成功地被實(shí)行而且掩蓋某特定功用之后，咱們會(huì)將它參加回歸測(cè)驗(yàn)群組(Regression Suite)傍邊，然后著手編撰下一個(gè)測(cè)驗(yàn)檔，當(dāng)然又得顛末編寫(xiě)、除錯(cuò)以及實(shí)行等步調(diào)。這樣的辦法使得擔(dān)任測(cè)驗(yàn)的工程師為了可以掩蓋描繪里邊一切不一樣的特性而編撰出不一樣的測(cè)驗(yàn)檔，這是為了完結(jié)驗(yàn)證作業(yè)的第一個(gè)政策。當(dāng)參加越多功用在描繪里時(shí)，就得花更多時(shí)刻并參加更多的測(cè)驗(yàn)文件來(lái)到達(dá)政策。

在以仿真為主的流程里，驗(yàn)證工程師首要須把描繪里邊的根底架構(gòu)(Infrastructure)先串好，再想辦法編寫(xiě)測(cè)驗(yàn)檔，然后灌入描繪里邊，紀(jì)錄并查看作用。這種樹(shù)立測(cè)驗(yàn)平臺(tái)(Test-Bench)的辦法可以會(huì)占去絕大多數(shù)的驗(yàn)證時(shí)刻，乃至變成整個(gè)企劃的要害要徑。一般所謂的測(cè)驗(yàn)平臺(tái)主動(dòng)化指的是藉由EDA東西的幫忙，運(yùn)用某些辦法論來(lái)樹(shù)立上述的驗(yàn)證環(huán)境，意圖是讓驗(yàn)證者在最短的時(shí)刻內(nèi)檢測(cè)完最多的特性。因而，測(cè)驗(yàn)平臺(tái)主動(dòng)化的質(zhì)量好壞就決議于可以在多短的時(shí)刻內(nèi)樹(shù)立起所需求的環(huán)境，并發(fā)展出一切的測(cè)驗(yàn)檔。

若將測(cè)驗(yàn)平臺(tái)比方作一臺(tái)大機(jī)器，上面有許多的開(kāi)關(guān)和旋鈕，而測(cè)驗(yàn)檔就是一連串實(shí)行「操控開(kāi)關(guān)」和「改動(dòng)旋鈕」的特定次序指令作業(yè)。可想而知，若是機(jī)器上面有越多的開(kāi)關(guān)和旋鈕，而它們上面又各自有越多的刻度，那測(cè)驗(yàn)檔編撰者就有必要得花更多的時(shí)刻來(lái)描繪一切可以的情境。每個(gè)情境會(huì)經(jīng)由不一樣的途徑跑過(guò)描繪里邊不一樣的情況，也一同測(cè)完特定的一些功用。在如此的情況底下，若是想要得到更高的生產(chǎn)力，好像就得想辦法讓驗(yàn)證東西可以主動(dòng)地操控旋鈕和開(kāi)關(guān)，以樹(shù)立更多種的情境來(lái)完結(jié)測(cè)驗(yàn)。

上述的測(cè)驗(yàn)平臺(tái)主動(dòng)化可以運(yùn)用受束縛型隨機(jī)(Constrained-Random, CR)調(diào)配模仿來(lái)完結(jié)，其精力是：每一個(gè)測(cè)驗(yàn)檔的確描繪一堆可以的情境，而仿真器自身在每次被發(fā)動(dòng)(Invocation)時(shí)會(huì)主動(dòng)挑選其間的一種來(lái)實(shí)行。而為了幫忙咱們可以有用操控開(kāi)關(guān)及旋鈕，市面上所看到如SystemVerilog和SystemC這樣的驗(yàn)證言語(yǔ)供給可運(yùn)用束縛條件(Constraints)的辦法來(lái)描繪測(cè)驗(yàn)鼓勵(lì)的情境。藉以操控驅(qū)動(dòng)描繪信號(hào)和買賣的數(shù)值在必定的合法(Valid)規(guī)模。因而，仿真器便能隨機(jī)發(fā)作影響所需求的數(shù)值，而且在此一同束縛條件(Constraints)包管生出來(lái)的情境都是正確的。要跑下一個(gè)情境時(shí)，咱們可以很輕松地在仿真器中調(diào)配另一個(gè)不一樣的隨機(jī)種子，生出不一樣但合法的影響，然后查驗(yàn)另一個(gè)新的特性。

幻想一個(gè)Bus-Based的描繪，其規(guī)矩(Protocol)答應(yīng)單字組(Single-Word)和脈沖(Burst)兩種類型的存取?？梢赃\(yùn)用描繪發(fā)作在總線上面的處置(Transaction)來(lái)建構(gòu)一個(gè)測(cè)驗(yàn)，然后讓處置讀寫(xiě)辦法和總線形式(Bus mode)可以被隨機(jī)決議。運(yùn)用「CR」，運(yùn)用者可以僅用一個(gè)測(cè)驗(yàn)就驗(yàn)證完一切的總線形式，更有時(shí)機(jī)發(fā)掘出一些偏遠(yuǎn)個(gè)案，例如在一個(gè)Single Write之后立刻來(lái)了一個(gè)Burst-Read的情況。而若是在Bus上面的多個(gè)設(shè)備都對(duì)應(yīng)到不一樣的地址規(guī)模(Address
Range)，或是某些設(shè)備并不撐持一切的總線形式，咱們所要做的僅僅更改本來(lái)的束縛條件來(lái)隨機(jī)發(fā)作地址信息，而且束縛總線的形式，讓測(cè)驗(yàn)只會(huì)在合理地址規(guī)模內(nèi)成為供給的形式之一。這樣一來(lái)，便可以測(cè)驗(yàn)總線上每一個(gè)設(shè)備是在一切被撐持形式之下的行動(dòng)，而且可以包管不包羅任何所沒(méi)有被撐持的情況會(huì)發(fā)作。

包羅率導(dǎo)向驗(yàn)證法

(Coverage-Driven Verification)

藉由上述比如，在真實(shí)開(kāi)端進(jìn)行測(cè)驗(yàn)之前并無(wú)法得知會(huì)被選用的地址(address)和形式(mode)，由于它們是被隨機(jī)發(fā)作出來(lái)的，所以在進(jìn)行仿真的時(shí)分記載下某些信息是必要的，意圖是弄清晰哪些情境是真實(shí)被實(shí)行過(guò)的，這樣紀(jì)錄的舉措一般被稱作「功用包羅率(Functional Coverage)」剖析，所得出的數(shù)據(jù)關(guān)于驗(yàn)證進(jìn)程的功率性一望而知。假使咱們可以運(yùn)用包羅率剖析的數(shù)據(jù)來(lái)厘清某一個(gè)特定的測(cè)驗(yàn)測(cè)能否測(cè)到某個(gè)想測(cè)的功用，或是終究測(cè)的好不好，接下來(lái)再將此數(shù)據(jù)報(bào)答給處置次序來(lái)決議驗(yàn)證的下一步該怎樣進(jìn)行，這樣的辦法稱為「包羅率導(dǎo)向驗(yàn)證(Coverage-Driven Verification, CDV)」。在本文所謂「高階的驗(yàn)證辦法」里，CDV的首要精力在于能主動(dòng)化紀(jì)錄并剖析某些測(cè)驗(yàn)情境能否現(xiàn)已被實(shí)行，然后運(yùn)用這些信息幫忙剩下來(lái)的驗(yàn)證作業(yè)可以更有用率地被完結(jié)。

CDV是運(yùn)用單一測(cè)驗(yàn)隨機(jī)發(fā)作出測(cè)驗(yàn)鼓勵(lì)，進(jìn)而主動(dòng)生產(chǎn)出多樣的情境，由于其與生俱來(lái)的「隨機(jī)」特性可以讓本來(lái)簡(jiǎn)略的一些測(cè)驗(yàn)有才干找出偏遠(yuǎn)個(gè)案的過(guò)錯(cuò)(Corner Case Bugs)，也就是一些描繪者壓根兒也不會(huì)想到的情況。當(dāng)包羅率(Coverage)的信息被搜集結(jié)束后，新的測(cè)驗(yàn)可以被主動(dòng)化或是用人工樹(shù)立出來(lái)，其樹(shù)立的原則為更改束縛條件(Constraints)，把未被掩蓋的功用或情境作為驗(yàn)證政策。一個(gè)杰出的CDV運(yùn)用會(huì)需求運(yùn)用者運(yùn)用斷語(yǔ)(Assertions)或是其它機(jī)制來(lái)具體指定其所必要實(shí)行到之包羅點(diǎn)(Coverage Points)或是特定行動(dòng)(Behavior)。

功用包羅率(Functional Coverage)這個(gè)用語(yǔ)，在不一樣的文章與引用途會(huì)有不一樣的寓意。在最根本的情況之下，包羅率剖析就是紀(jì)錄一些數(shù)據(jù)，以斷定能否一切情境都被測(cè)驗(yàn)結(jié)束，其實(shí)，運(yùn)用一些簡(jiǎn)略的Checkbox加上EXCEL次序就可以完結(jié)一個(gè)包羅率剖析的表格，而一個(gè)缺乏經(jīng)歷的工程師可以就會(huì)運(yùn)用這個(gè)表格調(diào)配波形圖的辦法來(lái)調(diào)查一個(gè)Bus-Based描繪，辛苦地剖析某些地址和形式能否被實(shí)行過(guò)。

正如所謂次序代碼包羅率(Code Coverage)存在許多不一樣的類型，如Line、Toggle、Path、Expression等，功用包羅率也有許多的細(xì)分類，其決議于所要量測(cè)的政策，像測(cè)驗(yàn)包羅率(Test Coverage)以及標(biāo)準(zhǔn)包羅率(Specification
Coverage)別離是依據(jù)驗(yàn)證方案(Verification Plan)或是功用標(biāo)準(zhǔn)(Functional Specification)來(lái)量測(cè)某些特性能否已被測(cè)驗(yàn)。值得注重的是，這種類型的包羅率剖析其實(shí)很簡(jiǎn)略用上述的淺顯「表格法」來(lái)完結(jié)，而其重點(diǎn)是將所謂「記載數(shù)據(jù)」及「就數(shù)據(jù)提出陳述的才干」建構(gòu)入驗(yàn)證次序傍邊。

布局包羅率(Structural Coverage)是一種比擬領(lǐng)先的次分類，它是由0-IN與Mentor Graphics所提出。在描繪內(nèi)有一些較為艱難驗(yàn)證的部份，例如Arbiters、FIFOs、還有跨頻率規(guī)模(Clock-Domain Crossings)的描繪及一些相似的問(wèn)題?？墒秋L(fēng)趣的是，此類組件的行動(dòng)相對(duì)來(lái)說(shuō)比擬廣為咱們所曉得，

事實(shí)上，可以簡(jiǎn)略界說(shuō)出承認(rèn)其已被包羅結(jié)束所需求的規(guī)矩，而所謂的布局包羅率就是在描繪里辨別出這些組件，然后主動(dòng)地依據(jù)「功用包羅率」的數(shù)據(jù)提出陳述。

除了「剖析」功用包羅率數(shù)據(jù)的作業(yè)之外，咱們可以先就怎樣搜集這些信息來(lái)評(píng)論。這有必要先認(rèn)清一點(diǎn)，搜集數(shù)據(jù)的作業(yè)自身也是功用包羅率的一種，所以要當(dāng)心厘清評(píng)論的政策終究是什么。在上面所說(shuō)到的搜集包羅紀(jì)錄兩種根本型的功用包羅率：所謂的數(shù)據(jù)導(dǎo)向包羅率(Data-Oriented Coverage)以及分配導(dǎo)向包羅率(Control-Oriented
Coverage)。

數(shù)據(jù)導(dǎo)向包羅率指的是在模仿中某一特守時(shí)刻點(diǎn)，紀(jì)錄下一連串變量的值。舉例來(lái)說(shuō)，在一個(gè)網(wǎng)絡(luò)運(yùn)用上，它可以運(yùn)用來(lái)紀(jì)錄某些封包在進(jìn)入某描繪之前和之后的內(nèi)容。上述曾說(shuō)到的總線架構(gòu)描繪里，也答應(yīng)代表在每一個(gè)總線周期(Bus Cycle)的起始點(diǎn)掃描出地址和總線形式(Bus Mode)的信息。如此紀(jì)錄的作業(yè)一般樹(shù)立影響的進(jìn)程中完結(jié)，以包管運(yùn)用者已的確把一切的處置類型(Transaction Types)都標(biāo)準(zhǔn)正確。除此之外，也可以會(huì)在查看作用的時(shí)分做完紀(jì)錄，其優(yōu)點(diǎn)是每個(gè)組件的呼應(yīng)都是正確的。無(wú)論怎樣「數(shù)據(jù)導(dǎo)向包羅率」的紀(jì)錄都是在測(cè)驗(yàn)平臺(tái)里邊完結(jié)，而非待測(cè)組件(Device Under Test, DUT)。作用一般會(huì)以矩陣的辦法呈現(xiàn)，其內(nèi)在是當(dāng)每一個(gè)變量在其它變量固定于特定數(shù)值時(shí)，有多少次時(shí)機(jī)可以到達(dá)某一特定數(shù)字，得出來(lái)的每一種特別組合會(huì)被紀(jì)錄其呈現(xiàn)的次數(shù)，最終東西再幫你把這些組合呈現(xiàn)的總和數(shù)據(jù)報(bào)答出來(lái)。

分配導(dǎo)向包羅率指的是紀(jì)錄bu上或是DUT里邊某些特定時(shí)刻短行動(dòng)(Temporal Behaviors)發(fā)作的次數(shù)。根本上,
Control-Oriented Coverage大都是運(yùn)用者在運(yùn)用斷語(yǔ)(Assertions)的時(shí)分，東西會(huì)紀(jì)錄下某些被實(shí)行的特定通訊協(xié)議(protocols),或是某特定情境(scenarios)發(fā)作的情況。舉例來(lái)說(shuō)，一個(gè)retry發(fā)作在某訊框傳輸(frame transfer)的第n個(gè)封包，或是當(dāng)CPU正在實(shí)行jump的時(shí)分卻來(lái)了一個(gè)攪擾(interrupt)等情況。典型的Control-Oriented Coverage的作用是一連串的數(shù)據(jù)代表每一種序列(sequence)發(fā)作的次數(shù)為何。Assertions所界說(shuō)出來(lái)的序列可所以有彈性的,也就是例如「某b在某a的1~3個(gè)clock之后發(fā)作」。若是咱們可以曉得某b在a之后一個(gè)clock呈現(xiàn)的次數(shù)和三個(gè)clock之后呈現(xiàn)的次數(shù)各為何，這樣的信息就適當(dāng)有參考價(jià)值了。上例中的包羅率次分類一般被稱作斷語(yǔ)包羅率(Assertion Coverage)。

正式模型查驗(yàn)

(Formal Model Checking)

正式模型查驗(yàn)(Formal Model Checking, FMC)又可以稱作特點(diǎn)查驗(yàn)(Property Checking)，其寓意和同屬正式驗(yàn)證(formal
verification)的等效查驗(yàn)(Equivalence Checking)完全不一樣，盡管都是依托具體的數(shù)值剖析來(lái)完結(jié)。所謂的Equivalence Checking是比擬兩種不一樣的導(dǎo)入辦法能否為功用性等效(Functional Equivalence)?？墒?，F(xiàn)MC是徹完全底地查看過(guò)描繪中一切可以的情況，看看能否有任何可以違背某特定特點(diǎn)(property)的情況發(fā)作。

一般會(huì)運(yùn)用Assertions來(lái)表達(dá)所謂的Properties，而內(nèi)在則是表明在一個(gè)描繪里邊一些準(zhǔn)確的序列型(Sequential)行動(dòng)或是不變化(Invariant)行動(dòng)，前者例如「某甲發(fā)作在某乙之后」，而后者則例如某甲「永不發(fā)作」或是某乙「必定發(fā)作」。因而，可以把每一個(gè)Property當(dāng)成標(biāo)準(zhǔn)(specification)的一個(gè)小碎片?？梢詫roperty描繪為描繪的某些行動(dòng)，或是把property描繪成關(guān)于輸入描繪的inpu其行動(dòng)上的束縛，也就是所謂的束縛條件(Constraints)。在此Constraints其實(shí)跟咱們?cè)u(píng)論「CR Simulation」時(shí)提及的Constraints是一樣的，盡管引出這個(gè)詞匯在運(yùn)用流程上的來(lái)龍去脈有點(diǎn)不一樣。

就理論上來(lái)說(shuō)，可以運(yùn)用FMC成功驗(yàn)證任何一個(gè)極點(diǎn)雜亂的描繪。可是當(dāng)咱們實(shí)踐來(lái)看，由于FMC牽扯到的數(shù)學(xué)剖析可以雜亂到難以幻想，有些時(shí)分可以會(huì)影響FMC運(yùn)用到描繪里邊的一些小區(qū)塊。不過(guò)，由于FMC有本領(lǐng)剖分出一切描繪里邊可以到達(dá)的情況，因而即便省去運(yùn)用者本人編撰測(cè)驗(yàn)檔的步調(diào)，運(yùn)用它來(lái)完全驗(yàn)證一些特定的功用是完全沒(méi)有問(wèn)題的，在此情況底下，Properties反而扮演了驗(yàn)證政策的人物，調(diào)配Constraints來(lái)界說(shuō)某描繪的環(huán)境條件。以下將會(huì)評(píng)論FMC在bBlock Level中所供給的更多優(yōu)點(diǎn)。

正式模型查驗(yàn)以及仿真

(Formal Model Checking and Simulation)

Formal Model Checking可以被視為模仿技能的互補(bǔ)，一同也扮演CDV辦法論中不行或缺的一環(huán)。FMC可以完全驗(yàn)證完描繪中的一切可以情況，也就是可包管契合一切運(yùn)用者界說(shuō)之Assertions的標(biāo)準(zhǔn)，一同也包管順暢到達(dá)一切的包羅點(diǎn)(Coverage
Point)。把FMC技能與模仿技能調(diào)配運(yùn)用的時(shí)分，可看到一個(gè)簇新的驗(yàn)證辦法－動(dòng)態(tài)正式驗(yàn)證(Dynamic Formal Verification ,DFV)，這概念是由0-IN所提出，其呈現(xiàn)大大地晉升了CDV內(nèi)在與價(jià)值。

首要把一些FMC與模仿的根本概念從頭思考，大多數(shù)的仿真器包羅Mentor的ModelSim，新思科技的VCS還有利華核算機(jī)的NCSim都是運(yùn)用「Event-Based」的語(yǔ)義實(shí)行描繪行動(dòng)，而正式東西(Formal Tools)是運(yùn)用Cycle-Based的辦法來(lái)作業(yè)。將這兩種形式分隔運(yùn)用來(lái)驗(yàn)證描繪時(shí)，可以會(huì)使得作用發(fā)作一些意想不到的不一樣，運(yùn)用者得要十分當(dāng)心，不然常常會(huì)使得Formal Tool跟仿真器對(duì)準(zhǔn)特定的Property實(shí)行出不一樣的作用。也就是由于這種潛在的風(fēng)險(xiǎn)，0-IN的正式驗(yàn)證(Formal Verification)功用會(huì)主動(dòng)從頭實(shí)行一切仿真器體現(xiàn)出的FMC反例以包管兩種詮釋辦法作用最終是異曲同工。

為了可以包管仿真器與FMC的作用共同，將SystemVerilog與PSL兩種驗(yàn)證言語(yǔ)標(biāo)準(zhǔn)化就顯得很重要了。由于如此一來(lái)才可以包管不一樣言語(yǔ)的Properties之間具有一樣的語(yǔ)義。如此的共同性促進(jìn)可以運(yùn)用經(jīng)過(guò)block level正式驗(yàn)證的Properties來(lái)作為模仿進(jìn)程中的監(jiān)督者(Monitor)，尤其是在仿真大型的體系時(shí)更有作用。例如當(dāng)給予某個(gè)區(qū)塊指定的一些Constraints，若是它能成功經(jīng)過(guò)正式驗(yàn)證，承認(rèn)其會(huì)有某些特定的行動(dòng)之后，接下來(lái)需求做的就是承認(rèn)體系中與此區(qū)塊有關(guān)聯(lián)性的其它部份也契合一樣的Constraints。由于Assertion Monitor會(huì)在體系仿真時(shí)主動(dòng)查看block的輸入，咱們可以藉此驗(yàn)證一切的輸入Constraints是正確的，一同F(xiàn)MC剖析也毫無(wú)瑕庛。

若是FMC可以正式證明某個(gè)區(qū)塊在給予的一串輸入行動(dòng)之下可運(yùn)轉(zhuǎn)正確，而且整個(gè)體系也只會(huì)讓這個(gè)區(qū)塊在上述輸入行動(dòng)的標(biāo)準(zhǔn)內(nèi)作業(yè)，那咱們就可以百分之百斷定此區(qū)塊在這個(gè)體系里邊永久不會(huì)犯錯(cuò)。因而不需求在Full-Chip模仿的時(shí)分，費(fèi)盡心機(jī)想生出一堆雜亂Stimulus，就為了使得區(qū)塊可以跑到某些特別的情況。而咱們就可把模仿作業(yè)專心于整個(gè)芯片End-to-End的正常行動(dòng)，由于單一區(qū)塊的行動(dòng)現(xiàn)已可以包管咱們無(wú)憂無(wú)慮。

以斷語(yǔ)為根底的驗(yàn)證

(Assertion-Based Verification)

比擬常看到的情況是咱們都把所謂的Assertion-Based Verification(ABV)視為運(yùn)用Assertions來(lái)當(dāng)模仿時(shí)的監(jiān)督器，盡管這沒(méi)有太大的過(guò)錯(cuò)，不過(guò)更正確的解說(shuō)應(yīng)該是將Assertions別離運(yùn)用在模仿以及正式驗(yàn)證中。由于Assertions在模仿和Formal Model Checking內(nèi)都可以扮演極重要的人物。所謂的Assertions讓咱們可以運(yùn)用簡(jiǎn)略的數(shù)學(xué)概念來(lái)準(zhǔn)確描繪某區(qū)塊需求恪守的行動(dòng)，或是束縛其運(yùn)作環(huán)境。除此之外，Assertions還可以被運(yùn)用來(lái)描繪包羅點(diǎn)(Coverage Points)，所謂包羅點(diǎn)指的是不管運(yùn)用任何的技能，在驗(yàn)證進(jìn)程里邊都有必要要實(shí)行到的某些特定情境。

Assertion常常會(huì)被分類成「White-Box Assertions」和「Black-Box Assertions」。White-Box
Assertions讓咱們可以關(guān)于描繪的內(nèi)部情況一望而知，而且一般可以反映出描繪者所決斷出的特定實(shí)行(Implement)辦法，例如某特定情況機(jī)被設(shè)定為「one-hot」。而B(niǎo)lack-Box Assertions則是拿來(lái)描繪「End-to-End」的行動(dòng)，也因而它與描繪者怎樣做內(nèi)部描繪沒(méi)有關(guān)聯(lián)。Assertions的最大優(yōu)點(diǎn)是可以讓描繪者在驗(yàn)證進(jìn)程傍邊，輕松地檢核描繪或是環(huán)境有沒(méi)有照著原先幻想的辦法。風(fēng)趣的作業(yè)是，咱們常聽(tīng)到的問(wèn)題是：「我怎樣曉得這樣就夠了呢？」。

若是Assertions被賦予的任務(wù)是驗(yàn)證描繪的行動(dòng)能否契合標(biāo)準(zhǔn)的標(biāo)準(zhǔn)，有兩種辦法來(lái)評(píng)斷「是不是真的夠了」。首要是要斷定有滿足的Assertions來(lái)驗(yàn)證咱們想要驗(yàn)證的一切要害行動(dòng)，一般這也就是驗(yàn)證方案的一個(gè)部份。第二點(diǎn)是要斷定描繪里邊的「每一個(gè)部份」都充分地與「至少一個(gè)Assertion」有關(guān)聯(lián)，有關(guān)這部份就可以視為所謂的「Assertion密度」，其估計(jì)的辦法是核算需求多少Clock Cycles才干讓緩存器數(shù)值傳送到一個(gè)Assertion。若是所需求的Clock Cycle越少，就代表咱們可以更簡(jiǎn)略關(guān)于某些Assertions能否有被違背來(lái)做正式剖析。假使整個(gè)描繪里邊的每一個(gè)部份都可以在兩個(gè)到三個(gè)Clock Cycles里邊被Assertions測(cè)過(guò)(這是經(jīng)歷規(guī)律里邊比擬成功的事例數(shù)字)，或許就能答復(fù)你：「是的，這樣現(xiàn)已夠了?！?/p>

技能價(jià)值的闡明

包羅率導(dǎo)向驗(yàn)證法

(Coverage-Driven Verification Value
Statement)的價(jià)值闡明

所謂CDV的價(jià)值，可從往兩個(gè)方向思考，第一是所提出來(lái)的處理方案終究可以縮短多少樹(shù)立Test-Bench的時(shí)刻；第二是關(guān)聯(lián)的測(cè)驗(yàn)終究能多有用地被實(shí)行并驗(yàn)證描繪里的待測(cè)特性。

當(dāng)咱們將測(cè)驗(yàn)平臺(tái)(Test-Bench)組合起來(lái)的時(shí)分,所謂的價(jià)值就可以用以下的條件歸納思考:

?能否供給滿足且具水平的IP縮短編寫(xiě)次序代碼的時(shí)刻？

?有沒(méi)有優(yōu)秀的政策指引咱們樹(shù)立一個(gè)可重復(fù)運(yùn)用而且撐持多樣籠統(tǒng)(Abstraction)層級(jí)的驗(yàn)證環(huán)境？

當(dāng)咱們建好Test-Bench而且承認(rèn)其可以正常作業(yè)今后，接下來(lái)就是要運(yùn)用CR技能的長(zhǎng)處來(lái)幫忙調(diào)配模仿。而為了可以順暢完結(jié)任務(wù)，在CR模仿需求注重三個(gè)根本政策，首要，已然某些言語(yǔ)可以描繪隨機(jī)數(shù)值的束縛條件(constraints)，就得挑選一個(gè)能撐持這些言語(yǔ)的仿真器。第二、仿真器自身得要具有所謂束縛條件處理器(Constraint Solver)的附加功用，所謂的Constraint
Solver功用指的是可以忠于原味地將咱們下在Constraints里邊指定的隨機(jī)數(shù)值體現(xiàn)出來(lái)，無(wú)庸置疑的，若是一個(gè)Constraint Solver可以把這些隨機(jī)數(shù)值組成功地盡量擴(kuò)大，就可以幫忙咱們發(fā)作出更多不一樣且具有含義的情境出來(lái)。接下來(lái)第三點(diǎn)，需求調(diào)配Functional Coverage的功用來(lái)監(jiān)督包管咱們所想要的情境真的都已被有用實(shí)行。而就整個(gè)辦法論的觀念來(lái)看，CDV也一同需求Test自身可以做自我檢測(cè)(Self-Checking)。

一個(gè)好的CDV辦法論當(dāng)然要可以撐持驗(yàn)證的第一個(gè)政策，也就是成功驗(yàn)證某個(gè)描繪能否完結(jié)一切希望中有必要到達(dá)的一切事項(xiàng)。而其重點(diǎn)是要可以更簡(jiǎn)略樹(shù)立整個(gè)驗(yàn)證環(huán)境而且發(fā)作某些測(cè)驗(yàn)，這些tests可以包管咱們測(cè)完描繪自身被希望到達(dá)的某些特性。在此很重要的概念是或許描繪里有些特性可直接用手寫(xiě)測(cè)驗(yàn)反而較易測(cè)，也就是寫(xiě)測(cè)驗(yàn)的工程師直接供給一些Scenarios來(lái)測(cè)驗(yàn)就可以?？墒顷P(guān)于大多數(shù)的特性而言，運(yùn)用CDV概念運(yùn)用Constrained-Random Tests來(lái)發(fā)作出各種不一樣卻合理的情境并完結(jié)測(cè)驗(yàn)，才是一種有用率的驗(yàn)證法。

CDV也能顧及到驗(yàn)證的第二個(gè)政策，成功驗(yàn)證某個(gè)描繪能否沒(méi)有做出任何希望中不應(yīng)到達(dá)的任何事項(xiàng)。試想描繪者可以沒(méi)有辦法將描繪與次體系互動(dòng)的一切情況都思考進(jìn)去，可是由于隨機(jī)數(shù)值的不行猜測(cè)性，促進(jìn)更有時(shí)機(jī)可以發(fā)掘出一些偏遠(yuǎn)個(gè)案。

正式模型查驗(yàn)

(Formal Model Checking Value Statement)法的價(jià)值闡明

關(guān)于CDV也答應(yīng)以幫忙找出一些在模仿作業(yè)的時(shí)分，描繪者疏忽思考到的一些情境。而就界說(shuō)上來(lái)說(shuō)，正式剖析的根本精力就是可以包管一切的情境都可以被測(cè)到。因而，咱們可以運(yùn)用FMC的辦法，給予一些輸入Constraints來(lái)正式驗(yàn)證一個(gè)block，然后調(diào)查它能否正確地作業(yè)。如此一來(lái)，咱們就可以省去在block
level做模仿的時(shí)刻，這樣一來(lái)，不管是用Constrained-Random或是直接做測(cè)驗(yàn)都可以省掉。所以，當(dāng)一切的區(qū)塊兜在一同做驗(yàn)證，看看作業(yè)能否正常的時(shí)分再來(lái)運(yùn)用模仿即可。

另一種觀點(diǎn)表明，可以運(yùn)用FMC把整個(gè)芯片階級(jí)給完全驗(yàn)證結(jié)束而省掉掉模仿的步調(diào)。這樣的說(shuō)法有必要在下列的條件之下才干包管不會(huì)犯錯(cuò)：若是你給某區(qū)塊A一些輸入行動(dòng)，然后承認(rèn)它可以作業(yè)無(wú)誤，接下來(lái)你也得承認(rèn)與區(qū)塊A有相互作用的區(qū)塊B并不會(huì)有任何「違背」上述輸入行動(dòng)的情況呈現(xiàn)。這樣的正式驗(yàn)證被稱做為「Assume-Guarantee典范」，而且理論上這種辦法是十分可行的。接下來(lái)要證明那些「區(qū)塊B的輸入」也契合上面的假定內(nèi)容，然后依序往前推。回到實(shí)際面來(lái)看，想要有用地辦理properties與區(qū)塊之間的相互關(guān)系并非如抱負(fù)中那么簡(jiǎn)略，理論里的大同世界在實(shí)務(wù)上可所以艱難重重。

但也不必因而而太失望，有一個(gè)人數(shù)不少且繼續(xù)生長(zhǎng)中的運(yùn)用者聯(lián)盟大力認(rèn)可FMC的潛在優(yōu)點(diǎn)，尤其是對(duì)準(zhǔn)描繪里邊占有重要要害方位的一些組件，例如Arbiters、Clock-Domain Crossings還有FIFOs等等。FMC的真實(shí)價(jià)值在于完全剖析的才干，關(guān)于找出不管是描繪中或是標(biāo)準(zhǔn)中的過(guò)錯(cuò)適當(dāng)有用。當(dāng)正式剖析找出了問(wèn)題之后，除錯(cuò)機(jī)能會(huì)開(kāi)端斷定這個(gè)問(wèn)題終究是「描繪出了錯(cuò)」或是「Assertion的瑕疵」。別疏忽一種可以性，寫(xiě)Assertion的人很可以把標(biāo)準(zhǔn)的精力詮釋過(guò)錯(cuò)，在這種情況發(fā)作的時(shí)分，犯錯(cuò)Assertion就有必要要被修正。可是一般的問(wèn)題大部份會(huì)出在描繪里邊的過(guò)錯(cuò)。由于FMC完全剖析的特性，上述的任何情況都難逃高眼，而且會(huì)一一被修復(fù)，由于當(dāng)所謂的「被驗(yàn)證過(guò)的Assertions」被運(yùn)用在模仿上的時(shí)分，咱們關(guān)于這樣買了雙保險(xiǎn)的驗(yàn)證次序才愈加的有決心。

包羅率導(dǎo)向驗(yàn)證調(diào)配正式模型驗(yàn)證

(Coverage-Driven Verification and Formal
Model Checking)的價(jià)值闡明

CDV是藉由隨機(jī)發(fā)作Stimulus的辦法來(lái)使得一個(gè)單一的測(cè)驗(yàn)可以主動(dòng)創(chuàng)造出多種不一樣的情境。測(cè)驗(yàn)正因隨機(jī)與生俱來(lái)的優(yōu)點(diǎn)，咱們有時(shí)機(jī)可以找到一些描繪者原先沒(méi)有想到的Corner Case Bugs。
FMC則是完全判定完一切描繪里邊可以的情況來(lái)包管描繪與標(biāo)準(zhǔn)里的描繪具有共同性。FMC運(yùn)用Properties或是Assertions來(lái)做實(shí)務(wù)上的檢測(cè)，擔(dān)?？梢园岩磺械腃orner
Case Bugs給抓出來(lái)。事實(shí)上咱們可以把Constrained Random
Simulation就當(dāng)作FMC的近似類型，僅僅它運(yùn)用模仿來(lái)替代正式剖析。

想想上面提過(guò)的一個(gè)問(wèn)題，是不是FMC只能拿來(lái)做小區(qū)塊的停止剖析呢(Static Analysis)？其實(shí)所謂的束縛大多數(shù)是來(lái)自內(nèi)存和運(yùn)算資源的缺乏。還好，「動(dòng)態(tài)正式驗(yàn)證(Dynamic Formal Verification, DFV)」可以增強(qiáng)追尋模仿作業(yè)，進(jìn)步CDV辦法論的價(jià)值。

給定一些政策行動(dòng)(或許是運(yùn)用Assertions或是Coverage Points來(lái)體現(xiàn))，DFV運(yùn)用了正式剖析的辦法來(lái)追尋模仿作業(yè)里發(fā)現(xiàn)的一些「令人重視的情況(Interesting
States)」，然后判別它們會(huì)不會(huì)違背任何一個(gè)Assertions或者是能不能觸及到某一個(gè)Coverage Point。關(guān)于功用驗(yàn)證的進(jìn)程來(lái)說(shuō)，所謂的「令人重視的情況(Interesting States)」是指發(fā)現(xiàn)某個(gè)「新的」或是「稀有的」描繪行動(dòng)發(fā)作的情況。

讓咱們解說(shuō)一下這個(gè)概念，幻想一個(gè)過(guò)錯(cuò)在模仿開(kāi)端好久今后才呈現(xiàn)，而這個(gè)過(guò)錯(cuò)只要在某一特定FIFO滿了，而且某特定FSM處于「FOO」情況時(shí)分才會(huì)發(fā)作，若只透過(guò)模仿，咱們需求想辦法讓灌入的測(cè)驗(yàn)去喂飽那個(gè)FIFO，然后再用同一個(gè)或是別的一個(gè)測(cè)驗(yàn)去驅(qū)動(dòng)政策FSM進(jìn)入FOO情況。若是僅運(yùn)用隨機(jī)影響去等待兩個(gè)事情會(huì)一同發(fā)作，這樣的機(jī)率恐怕不高。也就是說(shuō)Constrained-Random Stimulus或許需求測(cè)驗(yàn)平臺(tái)具有一大堆的「旋鈕」和「開(kāi)關(guān)」，來(lái)到達(dá)這樣細(xì)密的操控，才干找出一切相似的偏遠(yuǎn)個(gè)案。假使此刻導(dǎo)入DFV的概念，當(dāng)模仿作業(yè)走到FIFO是充溢的情況時(shí)，正式剖析會(huì)開(kāi)端查看所由此刻刻點(diǎn)所推演出來(lái)的一切情況，所以可以順暢發(fā)現(xiàn)而且揭露出發(fā)作此情況而且招致過(guò)錯(cuò)的特別次序終究為何。因而，運(yùn)用DFV調(diào)配CR運(yùn)用比起只單純運(yùn)用CR來(lái)做測(cè)驗(yàn)的優(yōu)點(diǎn)在于可以省去許多樹(shù)立額定測(cè)驗(yàn)平臺(tái)次序代碼的時(shí)刻。

若是沒(méi)有DFV，一個(gè)CDV的運(yùn)用者得要思考可以會(huì)有潛在的過(guò)錯(cuò)存在，然后想辦法更動(dòng)Stimulus Constraints以設(shè)法扶引測(cè)驗(yàn)到達(dá)特定的一些情況。清楚明了的這并不大簡(jiǎn)略。就實(shí)際情況而言，DFV一般可以將單一的情境擴(kuò)大成適當(dāng)許多且有用的測(cè)驗(yàn)(或許超越一萬(wàn)個(gè))。這樣一來(lái)，真實(shí)的測(cè)驗(yàn)平臺(tái)束縛條件就可以變得簡(jiǎn)略的多，由于咱們毋需為了上述的「細(xì)密操控情況」費(fèi)盡心機(jī)以建出抱負(fù)中的Constraint環(huán)境。

辦法論評(píng)論

前面的評(píng)論首要都是著重在驗(yàn)證流程中所謂樹(shù)立測(cè)驗(yàn)平臺(tái)主動(dòng)化，以及正式特點(diǎn)查驗(yàn)技能的概念。為了可以真實(shí)在實(shí)務(wù)上發(fā)揚(yáng)功效，接下來(lái)就要評(píng)論怎樣運(yùn)用這些技能，而且看看終究在實(shí)務(wù)上可以或是可以可以做些什么作業(yè)。其實(shí)所謂「怎樣運(yùn)用」完全決議于描繪者自身，驗(yàn)證的作業(yè)其實(shí)就是包管怎樣運(yùn)用，以符合標(biāo)準(zhǔn)所指定要做的什么作業(yè)。須注重的是，在從擬定的標(biāo)準(zhǔn)移動(dòng)到真實(shí)邏輯閘的進(jìn)程里，一般城市運(yùn)用到多個(gè)不一樣程度的籠統(tǒng)層級(jí)(Levels of Abstraction)?？墒?，想要成為一個(gè)成功的驗(yàn)證辦法論，其間之一的條件就是可以簡(jiǎn)略地在籠統(tǒng)階級(jí)之間搬運(yùn)，而且保持功用上的共同性。

實(shí)施驗(yàn)證(Implementation Verification)指的是包管RTL到閘口層之間的共同性。一般來(lái)說(shuō),咱們關(guān)于組成(Synthesis)進(jìn)程的精力曉得頗豐，想要查看RTL到閘口的共同性相對(duì)來(lái)說(shuō)比擬直觀。在此情況傍邊，所謂的「RTL」就可以被看作是與「閘口階級(jí)描繪」相比擬時(shí)的「標(biāo)準(zhǔn)(Specification)」。別的一方面，關(guān)于一切功用驗(yàn)證的進(jìn)程來(lái)說(shuō)，一切意圖都是為了可以包管RTL描繪可以準(zhǔn)確反映出咱們希望中的功用，因而也可以成為要比擬閘口階級(jí)功用時(shí)的正確政策。所以本階段所說(shuō)到的功用驗(yàn)證里，RTL的人物就被視為拿來(lái)跟標(biāo)準(zhǔn)相比擬的導(dǎo)入進(jìn)程。

不管是評(píng)論到「Implementation Verification」或是「Functional Verification」，驗(yàn)證的根本作業(yè)都是去比擬兩種行動(dòng)各自的體現(xiàn)，有許多辦法描繪希望中的行動(dòng)，其間之一是運(yùn)用Properties或是Assertions，然后運(yùn)用它們來(lái)做FMC，拿來(lái)跟RTL做比擬，完全驗(yàn)證描繪里邊的次區(qū)塊的功用能否正確，另一方面，assertions也可以拿來(lái)運(yùn)用在模仿傍邊監(jiān)控現(xiàn)已被實(shí)行過(guò)的行動(dòng)，當(dāng)然眾所周知模仿自身也需求別的一種體現(xiàn)希望中行動(dòng)的政策，就是測(cè)驗(yàn)平臺(tái)。

買賣階級(jí)原型的刻畫(huà)

(Transaction-Level Modeling)

可以常常思考驗(yàn)證流程怎樣比擬有用率是一件功德，而堅(jiān)信最有用的辦法就是讓測(cè)驗(yàn)平臺(tái)永久聚集在描繪被希望到達(dá)的政策上。想要到達(dá)這個(gè)政策，最合理的辦法或許就是讓測(cè)驗(yàn)平臺(tái)在「買賣階級(jí)(Transaction level)」里邊被完結(jié)。所謂「Transaction」指的是描繪里邊某個(gè)恣意活動(dòng)的體現(xiàn)。而且可以被體如今各種不一樣的籠統(tǒng)層級(jí)之中，例如un-timed、cycle-accurate、pin-accurate等等。因而一個(gè)買賣層級(jí)的測(cè)驗(yàn)有必要可以描繪政策買賣所應(yīng)該實(shí)行的作業(yè)。而驗(yàn)證環(huán)境這時(shí)所扮演的人物是擔(dān)任變換這些transactions成為清晰的行動(dòng)，使這些行動(dòng)可以契合將進(jìn)行仿真形式的籠統(tǒng)層級(jí)。咱們常常會(huì)運(yùn)用所謂的「Transactors」或是「Bus-functional models, BFM」等組件，它們都是運(yùn)用來(lái)做上述變換的作業(yè)。在此可以界說(shuō)一個(gè)好的驗(yàn)證環(huán)境：答應(yīng)咱們樹(shù)立買賣層級(jí)的測(cè)驗(yàn)，而且供給完善的機(jī)能，即便描繪里邊有不一樣籠統(tǒng)層級(jí)的運(yùn)用，這些測(cè)驗(yàn)依然可以被成功地運(yùn)用。

首要，讓咱們?cè)u(píng)論一下仿真，不管買賣是被運(yùn)用在哪一種籠統(tǒng)層級(jí)之內(nèi)，總是會(huì)有一些信息是與這些層級(jí)關(guān)聯(lián)的，例如地址或是數(shù)據(jù)等?？梢哉f(shuō)測(cè)驗(yàn)是用來(lái)描繪買賣，而Transactors則是用來(lái)實(shí)施這些買賣。在本文說(shuō)到許多關(guān)于CDV的優(yōu)點(diǎn)，這些優(yōu)點(diǎn)都可以在買賣描繪符號(hào)(Transaction Descriptor)的身上找到，這些符號(hào)可以通知Transactors該做些什么，還有該指定哪些的隨機(jī)束縛條件。假使咱們可以樹(shù)立標(biāo)準(zhǔn)接口群組，用來(lái)辦理測(cè)驗(yàn)、Transactors還有描繪之間的通訊，就可以簡(jiǎn)略地透過(guò)交流架構(gòu)中比擬低階的部份，而毋需想辦法改動(dòng)較高的階級(jí)。如此一來(lái)，一個(gè)一樣的測(cè)驗(yàn)可以透過(guò)一組Transactors來(lái)驅(qū)動(dòng)描繪中的一個(gè)買賣階級(jí)形式，也可以透過(guò)別的一組不一樣可是卻兼容的Transactors來(lái)驅(qū)動(dòng)一個(gè)RTL形式。

當(dāng)咱們?cè)谂芤粋€(gè)買賣階級(jí)形式的仿真時(shí)，「黑箱(black box)」的Assertions可以用來(lái)指定在此階級(jí)的某些特定行動(dòng)，而當(dāng)咱們修正描繪下到RTL階級(jí)的時(shí)分，黑箱的Assertions也可以一同做相似程度的修正。因而，當(dāng)描繪和Assertions都現(xiàn)已成功下到RTL階級(jí)時(shí)，這些一樣的Assertions(或許修正過(guò))就可以拿來(lái)當(dāng)作動(dòng)態(tài)正式剖析的政策物，其意圖是為了可以幫忙買賣階級(jí)測(cè)驗(yàn)的主動(dòng)化。

到達(dá)完善修復(fù)的終極驗(yàn)證

若是可以一同運(yùn)用Dynamic Formal Verification以及Constrained-Random的測(cè)驗(yàn)平臺(tái)，將可以大幅晉升CDV的價(jià)值，由于可以運(yùn)用一樣的影響來(lái)衍生出許多的情境。除此之外，運(yùn)用DFV來(lái)剖析某模仿作業(yè)里多重的情境，代表可以削減附加在測(cè)驗(yàn)平臺(tái)上面的旋鈕以及開(kāi)關(guān)的數(shù)量，也因而DFV幫運(yùn)用者省去了極可觀自行生出次序代碼的時(shí)刻，如此一來(lái)讓寫(xiě)測(cè)驗(yàn)平臺(tái)的作業(yè)簡(jiǎn)化了許多。另一方面，運(yùn)用Constrained Random Simulation調(diào)配Dynamic Formal Analysis更可以讓每一個(gè)測(cè)驗(yàn)自身可以到達(dá)更高的功用性包羅率。綜上所述，皆是為了完結(jié)驗(yàn)證的終極意圖，不管在多么雜亂的描繪里邊，偏遠(yuǎn)個(gè)案過(guò)錯(cuò)都可以更簡(jiǎn)略地被發(fā)現(xiàn)而且被修復(fù)之。