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

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

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

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

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

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

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

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

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

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

(Coverage-Driven Verification)

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

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

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

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

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

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

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

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

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

正式模型查驗

(Formal Model Checking)

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

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

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

正式模型查驗以及仿真

(Formal Model Checking and Simulation)

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

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

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

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

以斷語為根底的驗證

(Assertion-Based Verification)

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

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

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

技能價值的闡明

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

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

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

當(dāng)咱們將測驗平臺(Test-Bench)組合起來的時分,所謂的價值就可以用以下的條件歸納思考:

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

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

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

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

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

正式模型查驗

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

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

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

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

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

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

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

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

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

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

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

辦法論評論

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

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

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

買賣階級原型的刻畫

(Transaction-Level Modeling)

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

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

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

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

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