1、引言

在片上系統(tǒng)的設(shè)計與實現(xiàn)中，驗證這一環(huán)節(jié)日益重要，整個過程中花在驗證的時間比重越來越大，主要原因在于隨著SOC 芯片復(fù)雜度的提高，驗證的規(guī)模也成指數(shù)級的增加。系統(tǒng)芯片的時代已經(jīng)到來，在RTL級硬件設(shè)計的抽象層次上已經(jīng)無法應(yīng)付數(shù)以百萬和千萬門系統(tǒng)的設(shè)計和驗證。據(jù)統(tǒng)計，兩年來，一次投片成功率已經(jīng)由50%降低到39%。不能一次成功的設(shè)計必須再投入幾個月的設(shè)計驗證時間和數(shù)十萬美元的費用。這種風(fēng)險已經(jīng)變得不可接受了。因此設(shè)計驗證出現(xiàn)了所謂的“驗證危機(jī)”［2］。功能驗證已經(jīng)成為集成電路設(shè)計和開發(fā)的瓶頸，這就使得驗證的方法逐漸受到業(yè)界人士的高度重視。工程師們在設(shè)計時不可能考慮到萬無一失，所以很多系統(tǒng)行為是不能緊緊通過測試文件就能保證系統(tǒng)功能的正確性。

?

2、SOC驗證的特點

片上系統(tǒng)（SoC）是一種建構(gòu)技術(shù)，主要由處理器（MCU）以及一些外圍設(shè)備如UART，MAC，控制器等構(gòu)成，系統(tǒng)結(jié)構(gòu)圖如圖1。SoC的驗證和ASIC的驗證工作有很多相同地方：首先都要進(jìn)行模擬，檢查設(shè)計是否符合規(guī)則，使用各種方法對芯片進(jìn)行測試。但是，SOC的驗證又比較特殊，存在一些特殊挑戰(zhàn)。

2.1 整合

驗證SoC的首要重點就是檢查各種元件之間的整合程度，這里隱含的基本假設(shè)就是每一部件都已經(jīng)完成自我檢查。

2.2.軟硬件協(xié)同驗證

處理器中運行的軟件必須和硬件部分產(chǎn)生關(guān)聯(lián)才能進(jìn)行驗證?；蛘呶覀儜?yīng)該把軟硬件當(dāng)作一個完整的測試中元件（Device Under Test），對涉及軟硬件結(jié)合狀態(tài)的方案進(jìn)行測試。所以我們要找到一種方法來檢驗我們編寫的測試，以及在涵蓋的測試范圍中，軟硬件之間的關(guān)聯(lián)性。

2.3.IP核復(fù)用

對于可重用的IP核要建立可重用的驗證元件。建立可重用的驗證元件，會遇到重大挑戰(zhàn)，但同時也會因此而獲得更大利益。

SoC代表的是一類極其復(fù)雜的系統(tǒng)。一個典型的SoC需要一個或多個微處理器，還需要一些其他部件，如DSP、Memory等。為驗證SoC，首先需要驗證每個部件的正確性，然后要驗證部件間連接和通信的正確性。SoC驗證問題實際上就是：如何針對具體的驗證任務(wù)，選擇適當(dāng)?shù)尿炞C工具并加以整合。

3、當(dāng)前常用的驗證方法

關(guān)于驗證的方法有很多，但是到現(xiàn)在為止還沒有任何一種方法可以非常有效地對系統(tǒng)芯片進(jìn)行功能驗證。概括來看，迄今的驗證方法可分為模擬、仿真和形式驗證三種［3］。

3.1、模擬驗證

模擬驗證是將激勵信號施加于設(shè)計，進(jìn)行計算并觀察輸出結(jié)果，并判斷該結(jié)果是否與預(yù)期一致。

優(yōu)點：模擬驗證是傳統(tǒng)的驗證方法，而且目前仍然是主流的驗證方法。

缺點：非完備性，即只能證明有錯而不能證明無錯。因此，模擬一般適用于在驗證初期發(fā)現(xiàn)大量和明顯的設(shè)計錯誤，而難以勝任復(fù)雜和微妙的錯誤。模擬驗證還嚴(yán)重依賴于測試向量的選取，而合理而充分地選取測試向量，達(dá)到高覆蓋率是一個十分艱巨的課題。由于設(shè)計者不能預(yù)測所有錯誤的可能模式，所以尚未發(fā)現(xiàn)某個最好的覆蓋率度量。即使選定了某個覆蓋率度量，驗證時間也是一個瓶頸。

3.2、仿真驗證

從電路的描述抽象出模型，然后將外部激勵信號或數(shù)據(jù)施加到此模式中，通過觀察該模型在外部激勵信號作用下的反應(yīng)來判斷該電子系統(tǒng)是否達(dá)到了設(shè)計目標(biāo)。仿真的方法是目前進(jìn)行設(shè)計時常用的方法，根據(jù)不同的仿真層次，有不同的仿真工具。

優(yōu)點：仿真比模擬的驗證速度快得多，

缺點：代價昂貴，靈活性差。

3.3、形式驗證

形式化驗證是不同于仿真方法的對邏輯設(shè)計結(jié)果進(jìn)行的另一種驗證方法［4］。在 自上而下的設(shè)計過程中，在設(shè)計的各個階段和級別，每一級設(shè)計都是以上一級的設(shè)計作為設(shè)計目標(biāo)，得到本級的設(shè)計結(jié)果的結(jié)構(gòu)描述，這是設(shè)計和綜合的過程。

優(yōu)點：完備性，能夠完全斷定設(shè)計的正確性。

缺點：首先要對原始設(shè)計進(jìn)行模型抽取，這對使用者有數(shù)學(xué)技能和經(jīng)驗上的要求。而且，有的工具需要人工引導(dǎo)（如定理證明），有的工具存在狀態(tài)空間爆炸 問題（如模型檢驗）。

類型：

（1）等價性檢驗［5］

它是用數(shù)學(xué)方法驗證參考設(shè)計與修改設(shè)計之間的等價性。（如圖2）利用等價性驗證工具可對這兩種設(shè)計方案進(jìn)行徹底的檢驗以保證它們在所有可能的條件下都有一樣的性能。還可利用等價性驗證來驗證不同的RTL或門級實施方案的等價性。

從整個數(shù)字系統(tǒng)的設(shè)計流程看，等價性問題幾乎存在于每個上下相鄰的設(shè)計層次中，見圖2。

（2）定理證明技術(shù)。

運用公理和已經(jīng)證明的定理證明電路的描述是正確的。

這兩種方法各有特點，其中定理證明雖然能夠給出設(shè)計是否正確的一個確切的回答，但由于涉及很多數(shù)學(xué)推理方面的知識，這就要求用戶有很強(qiáng)的數(shù)學(xué)功底，這也是這種方法不能推廣的一個原因。而等價性驗證是驗證不同階段的設(shè)計是否相互等價的一個很好的方法。一個SOC設(shè)計是分為多個階段進(jìn)行的，那么下一個階段的與上一個階段的等價是設(shè)計的正確的一個保證。

4、新型的驗證方法

針對SOC驗證出現(xiàn)的各種問題現(xiàn)在還沒有一種完全行之有效的方法出現(xiàn)，解決辦法之一是基于斷言的驗證（ABV）［6］，它是把形式化方法集成到傳統(tǒng)模擬流程中的一種有效的方法。設(shè)計團(tuán)隊在RTL設(shè)計中插入設(shè)計意圖（斷言）并且進(jìn)行模擬，然后用形式化技術(shù)檢查斷言，限制條件，也就是合法接口行為的斷言，和其他斷言同時一同參加模擬。斷言檢查的結(jié)果改進(jìn)模擬的有效性。即使利用傳統(tǒng)的模擬驗證，斷言也可以大大提高模擬的效率?；跀嘌缘尿炞C要由用戶寫出斷言，斷言表示要驗證的性質(zhì)，因此需要性質(zhì)描述語言。例如邏輯和時序方面的性質(zhì)。這就需要盡快找到一種能實現(xiàn)上述功能的語言。SystemVerilog正是在這種情況下產(chǎn)生的，正逐漸被業(yè)界人士接受。

5.小結(jié)

形式化方法最近幾年取得了長足進(jìn)展，特別是等價性檢驗已經(jīng)集成到標(biāo)準(zhǔn)驗證流程中。設(shè)計和驗證方法的進(jìn)步應(yīng)當(dāng)是漸進(jìn)的，不可能發(fā)生革命性的改變。因此在可以預(yù)見的幾年內(nèi)，混合驗證方法應(yīng)當(dāng)成為主流的驗證方法。基于斷言的驗證是結(jié)合形式化驗證和傳統(tǒng)的模擬驗證可行的途徑。支持這種途徑的統(tǒng)一的設(shè)計和驗證語言是SystemVerilog。該語言已經(jīng)得到很多EDA廠商和用戶的支持，預(yù)計將會流行起來。