SOC設計驗證方法的探索

一、引言

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

　　二、SOC驗證的特點(diǎn)

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

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

　　2.軟硬件協(xié)同驗證：處理器中運行的軟件必須和硬件部分產(chǎn)生關(guān)聯(lián)才能進(jìn)行驗證?；蛘呶覀儜摪衍浻布斪饕粋€(gè)完整的測試中元件(Device Under Test),對涉及軟硬件結合狀態(tài)的方案進(jìn)行測試。所以我們要找到一種方法來(lái)檢驗我們編寫(xiě)的測試，以及在涵蓋的測試范圍中，軟硬件之間的關(guān)聯(lián)性。

　　3.IP核復用：對于可重用的IP核要建立可重用的驗證元件。建立可重用的驗證元件，會(huì )遇到重大挑戰，但同時(shí)也會(huì )因此而獲得更大利益。

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

　　三、當前常用的驗證方法

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

　　1、模擬驗證

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

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

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

　　2、仿真驗證

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

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

　　缺點(diǎn)：代價(jià)昂貴，靈活性差。

　　3、形式驗證

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

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

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

　　類(lèi)型：

　　(1)等價(jià)性檢驗[5]

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

　　從整個(gè)數字系統的設計流程看，等價(jià)性問(wèn)題幾乎存在于每個(gè)上下相鄰的設計層次中，見(jiàn)圖2。

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

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

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

　　四、新型的驗證方法

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

　　五.結論

　　形式化方法最近幾年取得了長(cháng)足進(jìn)展，特別是等價(jià)性檢驗已經(jīng)集成到標準驗證流程中。設計和驗證方法的進(jìn)步應當是漸進(jìn)的，不可能發(fā)生革命性的改變。因此在可以預見(jiàn)的幾年內，混合驗證方法應當成為主流的驗證方法。

　　基于斷言的驗證是結合形式化驗證和傳統的模擬驗證可行的途徑。支持這種途徑的統一的設計和驗證語(yǔ)言是SystemVerilog。該語(yǔ)言已經(jīng)得到很多EDA廠(chǎng)商和用戶(hù)的支持，預計將會(huì )流行起來(lái)。