系統級芯片設計語(yǔ)言和驗證語(yǔ)言的發(fā)展

作者：韓俊剛 時(shí)間：2006-02-11 17:08:15來(lái)自：西安郵電學(xué)院 ASIC設計中心

簡(jiǎn) 介：由于微電子技術(shù)的迅速發(fā)展和系統芯片的出現，包含微處理器和存儲器甚至模擬電路和射頻電路在內的系統芯片的規模日益龐大，復雜度日益增加。人們用傳統的模擬方法難以完成設計驗證工作，出現了所謂“驗證危機”。為了適應這種形勢，電子設計和驗證工具正在發(fā)生迅速而深刻的變革?，F在基于RTL級的設計和驗證方法必須向系統級的設計和驗證方法過(guò)渡，導致了驗證語(yǔ)言的出現和標準化，本文將對當前出現的系統級設計和驗證語(yǔ)言進(jìn)行全面綜述，并論述驗證語(yǔ)言標準化的情況。分析他們的優(yōu)缺點(diǎn)和發(fā)展趨勢。最后簡(jiǎn)單評述當前的驗證方法，說(shuō)明基于斷言的驗證是結合形式化驗證和傳統模擬驗證可行的途徑。

1　引言 　　在二十多年前中小規模集成電路的設計向大規模和超大規模集成電路過(guò)渡時(shí)，設計方法經(jīng)歷了由門(mén)級向寄存器傳輸級過(guò)渡。當時(shí)各種硬件描述語(yǔ)言如DDL,CDL層出不窮，在RTL級的設計描述語(yǔ)言曾經(jīng)歷了“春秋戰國”時(shí)代，逐漸形成了VHDL和Verilog稱(chēng) 霸的局面。隨著(zhù)微電子技術(shù)的發(fā)展，集成在一個(gè)芯片上的電路的功能日益復雜化。系統芯片的時(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)變得不可接受了。因此設計驗證出現了所謂的“驗證危機”?，F在基于RTL級的設計和驗證方法必須向系統級的設計和驗證方法過(guò)渡。
　　解決系統級設計問(wèn)題首先要解決系統及功能的描述問(wèn)題。系統級設計語(yǔ)言的競爭正在如火如荼的展開(kāi)。需要一種語(yǔ)言能夠描述包括嵌入的軟件和模擬電路在內的整個(gè)系統。而現在的寄存器級的硬件描述語(yǔ)言將成為硬件設計的匯編語(yǔ)言。設計和驗證工程師將只在關(guān)鍵的部分利用他們取得較高的性能，而一般情況下將主要利用系統及語(yǔ)言進(jìn)行設計和驗證。
　　本文將對當前出現的系統級設計和驗證語(yǔ)言及其發(fā)展趨勢進(jìn)行全面地綜述，在第2節和第3節將分別綜述系統及設計語(yǔ)言和驗證語(yǔ)言的發(fā)展情況。第4節論述當前主流的驗證方法。
　　2　系統級設計語(yǔ)言
　　2.1　對系統級設計語(yǔ)言的要求
　　系統級設計的特點(diǎn)是：更多更復雜的功能集成和綜合、功能模塊或IP核，包含存儲器、處理器、模擬模塊、接口模塊和高速、高頻輸入輸出及軟件模塊，因此要考慮軟件和硬件的劃分、優(yōu)化等協(xié)同設計和協(xié)同驗證問(wèn)題。根據系統級設計的特點(diǎn)，人們普遍認為系統級設計語(yǔ)言應當具有如下的特點(diǎn)：
　　1)具有形式化的語(yǔ)義。
　　2)支持特別領(lǐng)域規范的集成。
　　3)支持描述系統和部件的計算模型的復合。
　　4)支持更加抽象的建模。
　　5)支持對于限制信息的表示和集成。
　　6)從設計規范到設計實(shí)現整個(gè)設計過(guò)程中一致地、連續地探索設計空間。
　　7)支持在具體領(lǐng)域和多個(gè)交叉領(lǐng)域的預先分析和驗證。
　　2.2　系統級設計語(yǔ)言的發(fā)展
　　21世紀初期是系統級設計語(yǔ)言發(fā)展變化最迅速的時(shí)期。各種系統設計語(yǔ)言 如雨后春筍，已經(jīng)出現的系統級語(yǔ)言可以分成3類(lèi)。
　　第一類(lèi)是通過(guò)對于經(jīng)典語(yǔ)言的擴展得到的語(yǔ)言如SystemVerilog［1］。SystemVerilog 在向高層次發(fā)展方面，對于原來(lái)的Verilog進(jìn)行了根本性的修改。他混合了Verilog, C/C++和 CoDesign Automation′s SuperLog 給設計者提供了最強的能力。SystemVerilog是對于IEEE 13642001 Verilog的擴展，以便輔助提供產(chǎn)生并驗證抽象的系統結構級的模型。在接口方面突出的特點(diǎn)是在高層抽象可以實(shí)現模塊的連接。類(lèi)似于C語(yǔ)言的結構，如斷言結構支持性質(zhì)的檢驗。主要擴展的目的是使得Verilog語(yǔ)言能夠支持大規模的設計并達到更高級的抽象。他還借用了C的數據類(lèi)型“char”,“int”等。凡是C的編碼可以直接用在Verilog模型和驗證程序中。這類(lèi)對傳統語(yǔ)言擴展的方法的優(yōu)點(diǎn)是有利于設計者的平穩過(guò)渡，但是主張完全用C語(yǔ)言作為系統級語(yǔ)言的人們懷疑這種“改良”的方法在進(jìn)行模擬時(shí)的效率不能得到滿(mǎn)意結果。
　　第二類(lèi)是利用軟件領(lǐng)域的語(yǔ)言和方法，如C/C++,Java,UML等等。主張用C/C++作為系統級設計語(yǔ)言的人們認為隨著(zhù)時(shí)間的推移，最終將會(huì )利用C的自動(dòng)編譯程序和其他自動(dòng)化的工具來(lái)實(shí)現從C/C++的模型到芯片的編譯。在目前工具不完善的情況下必須進(jìn)行人工逐步求精的設計。也就是說(shuō)，目前C/C++要擴展硬件表達成分而不是只在算法級描述。例如 SpecC（the University of California, Irvine），ardwareC（Stanford University）HandelC（原先是在 Oxford University，現在轉移到Embedded Solutions Ltd）SystemC++（C Level Design Inc）SystemC（Synopsys Inc）Cynlib（CynApps）等?？梢园堰@些語(yǔ)言分成2類(lèi)：一類(lèi)是在標準C語(yǔ)言上進(jìn)行擴充，以SpecC為代表；另一類(lèi)是利用C++可擴充性，以SystemC為代表，他提供一組硬件的基本元件，這些元件可以擴充，以便在更高的層次上支持硬件。這2種互補的方法都在4個(gè)層次上即算法、模塊、按照周期（cycle accurate）和寄存器傳輸（RTL）級別上支持硬件描述。在SystemC20之前，有些人認為SystemC是側重于模擬，SpecC是側重于規范和結構建模，以綜合和驗證為目標，但是在SystemC20之后，這些說(shuō)法也不準確了，因為現在的SystemC2.0已經(jīng)能夠支持所有系統級的要求。SystemC填補了在傳統的HDL和基于C/C++的軟件開(kāi)發(fā)方法之間的鴻溝。他包含C++類(lèi)庫和一個(gè)模擬內核，這個(gè)內核用來(lái)產(chǎn)生行為級和寄存器級的模型。有領(lǐng)先的EDA廠(chǎng)家管理和支持，并與商用的綜合工具相結合。他支持通用的軟件和硬件開(kāi)發(fā)環(huán)境。
　　我們認為，和C相比，C++顯然是比較好的選擇。因為C++是可以擴展的，也因為硬件中的并發(fā)概念易于用類(lèi)庫表示，C++面向對象的本質(zhì)與HDL的分層次特性可以很好地對應。
　　人們也在討論Java是否可以作為系統及語(yǔ)言和高級硬件描述語(yǔ)言的問(wèn)題［2］。例如LavaLogic先提出JHDL，他把Java語(yǔ)言的描述轉換成為綜合的HDL程序，再用所提供的工具變成門(mén)級的描述。擁護Java作為系統級描述語(yǔ)言的人認為Java可以提高描述和運行效率，與現在的HDL相比，能夠以很簡(jiǎn)短的程序表達高層的概念。C/C++具有內在的表達并發(fā)能力，相反Java可以用線(xiàn)程顯式的表達并發(fā)。但是Java不支持模板和操作符過(guò)載，因此可能產(chǎn)生大量的過(guò)程調用。
　　第三類(lèi)是全新的系統級語(yǔ)言。例如Rosetta，用這一個(gè)語(yǔ)言，用戶(hù)可以描述幾乎任何工程領(lǐng)域的行為和限制，包括模擬、數字、軟件、微流體和機械等。但是并不能代替和實(shí)現Verilog，VHDL和C等。他由美國DARPA開(kāi)發(fā)，目的是給設計者提供描述大型的、復雜的計算系統，特別是混合多種技術(shù)的系統的能力，他可以在高層次上定義、捕獲和驗證系統的限制條件和需求條件及其部件。他提供定義和結合多個(gè)領(lǐng)域的語(yǔ)義模型，進(jìn)行建模和分析。他的語(yǔ)義是形式化的、可以擴展的，并且能適應新系統的要求。
　　Rosetta 的設計方法學(xué)是基于一種多面體的小平面（facet）的概念。facet是部件或系統的模型，他提供所關(guān)心領(lǐng)域具體的信息。為了支持異構系統的設計，每個(gè)小平面提供具體領(lǐng)域的詞匯和語(yǔ)義。他用來(lái)從不同角度定義系統的視圖，然后把不同的小平面組合起來(lái)構成部件的模型。部件的模型再組合成系統的模型。
　　Rosetta的 facets語(yǔ)法對于現有的硬件描述語(yǔ)言的用戶(hù)來(lái)說(shuō)，應當是容易熟悉的。他的語(yǔ)法和VHDL幾乎是一樣的。該語(yǔ)言設計的主要難點(diǎn)是要把多個(gè)領(lǐng)域的信息統一在一種設計活動(dòng)中。對于不同的領(lǐng)域，例如模擬、數字、機械、和光部件，Rosetta 提供了定義和理解系統的機制。不僅如此，他還提供對于擴展新領(lǐng)域進(jìn)行建模的技術(shù)，這對于將來(lái)語(yǔ)言的發(fā)展非常重要。不能正確理解不同領(lǐng)域的交互作用經(jīng)常是引起系統失敗的根源。因此Rosetta提供顯式的交互建模和評價(jià)這些交互的方法。
　　3　系統級驗證語(yǔ)言
　　3.1　基于事務(wù)的驗證和基于斷言的驗證
　　驗證語(yǔ)言的提出需要說(shuō)明基于事務(wù)的驗證和基于斷言的驗證。解決所謂系統芯片的“驗證危機”，策略之一是基于事務(wù)處理的驗證（TBV），事務(wù)是概念上單一的數據或控制的轉移，這種轉移有事務(wù)的開(kāi)始時(shí)間，結束時(shí)間和所有相關(guān)的信息確定，這些信息和事務(wù)一起存儲，作為事務(wù)的屬性。事務(wù)處理可以是簡(jiǎn)單的存儲器讀寫(xiě)，也可以是具有復雜的結構數據報在網(wǎng)絡(luò )信道中的傳送。把驗證的層次從信號層次提高到事務(wù)處理層次，讓測試具有更直觀(guān)的方式，有利于測試產(chǎn)生、糾錯過(guò)程和功能覆蓋的度量。設計系統結構不是想象使能信號和地址總線(xiàn)如何工作，而是想象數據如何在系統中流動(dòng)和存儲。TBV就是這種高層次設計過(guò)程的自然展開(kāi)。定性的驗證過(guò)程包含3個(gè)步驟：測試生成、設計查錯和功能覆蓋分析。每個(gè)階段都要提高到事務(wù)處理的抽象層次?？梢杂肰erilog語(yǔ)言的task 來(lái)構成事務(wù)。這對于基本的測試也許還可以接受，但是當要產(chǎn)生復雜的數據結構、復雜的測試方案，動(dòng)態(tài)的測試生成時(shí)，就會(huì )產(chǎn)生太多的限制。高級驗證語(yǔ)言（HLV）例如近年來(lái)開(kāi)發(fā)TestBuilder(C++)、Vera和 E等，就是要解決這些復雜的問(wèn)題。
　　基于斷言的驗證(ABV)是把形式化方法集成到傳統模擬流程中的一種有效的方法。設計團隊在RTL設計中插入設計意圖（斷言）并且進(jìn)行模擬，然后用形式化技術(shù)檢查斷言，限制條件，也就是合法接口行為的斷言，和其他斷言同時(shí)一同參加模擬。斷言檢查的結果改進(jìn)模擬的有效性。即使利用傳統的模擬驗證，斷言也可以大大提高模擬的效率?；跀嘌缘尿炞C要由用戶(hù)寫(xiě)出斷言，斷言表示要驗證的性質(zhì)，因此需要性質(zhì)描述語(yǔ)言。例如邏輯和時(shí)序方面的性質(zhì)。這些也是驗證語(yǔ)言要解決的問(wèn)題。
　　3.2　目前的系統級驗證語(yǔ)言概況
　　IC設計和EDA界需要一種標準化的具有公開(kāi)接口的驗證方法學(xué)，在2000年，Open Verilog International和VHDL International聯(lián)合，組成了Accellera組織。其目的就是在系統、半導體和設計工具企業(yè)，推動(dòng)、開(kāi)發(fā)和培育新的國際標準。以便加強以語(yǔ)言為基礎的設計自動(dòng)化進(jìn)程。面對幾個(gè)在語(yǔ)法和語(yǔ)義方面都不夠完善的形式性質(zhì)描述語(yǔ)言，Accellera進(jìn)行了一個(gè)選舉過(guò)程，4個(gè)候選的語(yǔ)言是 Motorola的CBV，IBM的 Sugar，Intel的 ForSpec 和Verisity的e 語(yǔ)言。經(jīng)過(guò)討論，集中到Sugar和 CBV上，在2002年4月選定了IBM的Sugar 2.0［3］。Sugar 2.0的獲勝造成了Accellera組織的分裂，包括Cadence在內的多數EDA工具供應商支持Accellera 的決定。另外一部分則轉向支持Syopsys的 OpenVera 2.0。作為一種真正的工業(yè)標準語(yǔ)言，Sugar 2.0語(yǔ)法和語(yǔ)義很簡(jiǎn)單明了?；旧鲜腔诰€(xiàn)性時(shí)態(tài)邏輯語(yǔ)言（LTL）,他是由基于分支時(shí)態(tài)邏輯(計算樹(shù)邏輯CTL）的Sugar1.0演化而來(lái)的。其關(guān)鍵思想是利用一種擴展的正則表達式的構件。因此對于形式驗證領(lǐng)域來(lái)說(shuō)，理解Sugar是很容易的。
　　Sugar語(yǔ)言是由IBM的Haifa 實(shí)驗是經(jīng)過(guò)8年研究開(kāi)發(fā)的［4］，是一種說(shuō)明性的形式化性質(zhì)規范語(yǔ)言。其語(yǔ)義是嚴格的，但是易于理解和使用?？梢杂妙?lèi)似定理的形式 描述要驗證 的屬性，這些描述可以作為模型檢驗和定理證明的輸入，也可以做模擬程序中檢查程序的輸入。Sugar由4層結構組成：
　　布爾層由布爾表達式構成。
　　時(shí)態(tài)層描述邏輯值隨時(shí)間變化的性質(zhì)。
　　驗證層由一些指示詞描述驗證軟件如何利用時(shí)態(tài)的性質(zhì)。還有 些驗證指示詞假設某種性質(zhì)成立。驗證層也提供把Sugar的語(yǔ)句分成驗證單元的方式。
　　模型層提供對于輸入行為進(jìn)行建模的方法，對于輔助信號和變量進(jìn)行 說(shuō)明并定義其行為。模型層也可以定義為時(shí)態(tài)層的性質(zhì)和實(shí)體的名字。
　　Sugar具有3種風(fēng)格，分別對應于硬件描述語(yǔ)言Verilog，VHDL和環(huán)境描述語(yǔ)言EDL（ IBM的RuleBase 模型檢驗器使用的語(yǔ)言）。采用不同風(fēng)格時(shí)，在布爾層和模型層的 語(yǔ)法可以不同，但是在時(shí)態(tài)層和驗證層相同。
　　OpenVera 1.0 是Synopsys捐獻出來(lái)公開(kāi)的驗證語(yǔ)言。對于模擬，他已經(jīng)具有描述斷言的能力。Synopsys公司和Intel公司的ForSpec相結合后產(chǎn)生的OpenVera 2.0也能夠支持形式化驗證。和Intel公司聯(lián)合推出OpenVeraForespec 作為工業(yè)標準的斷言語(yǔ)言，但是因為對于工程師來(lái)說(shuō)難以接受，因此被拒絕。但是其概念還是有特點(diǎn)的。他的目標是作為一種支持模擬和形式驗證的性質(zhì)描述語(yǔ)言。從ForSpec借用的構件和操作包括“assume”，“restrict”，“model”，“assert” 等，這些都為形式化驗證服務(wù)。語(yǔ)言成分“ assumeguarantee”可以把斷言作為模塊的性質(zhì)，在高層上又作為監視器。OpenVera 用來(lái)描述斷言時(shí)可以精確的描述在多個(gè)周期時(shí)間的時(shí)序行為。硬件描述語(yǔ)言例如Verilog和 VHDL是用來(lái)描述硬件的過(guò)程行為。這種過(guò)程模型難以有效地表述在多周期的時(shí)態(tài)行為。利用Ope nVera的斷言語(yǔ)言OVA，用戶(hù)可以方便直觀(guān)地描述輸入輸出行為、總線(xiàn)協(xié)議以及其他復雜的硬件行為和關(guān)系。和硬件描述語(yǔ)言的描述比較，要簡(jiǎn)潔3~5倍。和Sugar語(yǔ)言的4級結構相比，OpenVera 2.0分為5個(gè)主要的級別：
　　上下文（環(huán)境）幫助定義斷言的轄域（或作用域）。
　　指示詞描述所要檢查或監視的性質(zhì)。
　　布爾表達式。
　　事件表達式表示時(shí)間序列。
　　公式表示表述時(shí)間序列之間的關(guān)系。
　　Sugar和 Open Vera 2.0 有2個(gè)層次是相同的，即布爾層和時(shí)態(tài)層。這些層構成了斷言的核心。他們的差別在其他層次上面。OpenVera 2.0 重視性質(zhì)的細致結構，用戶(hù)能和斷言深入交互，以便考察和探索形式驗證的知識。Sugar的另外2個(gè)層次服務(wù)于性質(zhì)的“格式化”，而簡(jiǎn)化與用戶(hù)的交互?？傊?，不管用那種語(yǔ)言，Open Vera 2.0 或者Sugar，他們都提供了高效驗證復雜系統芯片的手段。
　　4　對于當前驗證方法的評述
　　目前的設計驗證方法迅速發(fā)展，設計和驗證語(yǔ)言層出不窮。但是以下的觀(guān)點(diǎn)和結論是明確的：

　　1）形式化方法取得了長(cháng)足進(jìn)展，特別是等價(jià)性檢驗已經(jīng)集成到標準驗證流程中。模型檢驗技術(shù)以及定理證明等還不能成為設計環(huán)境的主流驗證方法的主要原因有［3］:
　?、偃狈V泛接受的性質(zhì)描述語(yǔ)言。
　?、谌狈ι虡I(yè)化的工具。
　?、壑两袢狈τ行У厥褂眯问交椒▽W(xué)的指導原則。
　?、茉诟淖凃炞C方法帶來(lái)的收益是否明顯的問(wèn)題上還在觀(guān)望。
　　2）形式化方法還需要和傳統的方法相結合才能發(fā)揮作用。設計和驗證方法的進(jìn)步應當是漸進(jìn)的，不可能革命性的改變。因此在可以預見(jiàn)的幾年內，混合驗證方法應當成為主流的驗證方法。斷言對于表示接口限制、設計性質(zhì)和設計假設都具有很深刻的作用和影響。這些會(huì )對發(fā)現過(guò)去的方法不能發(fā)現的設計錯誤做出貢獻。特別適合測試覆蓋結合起來(lái)可以極大的改進(jìn)驗證效率。
　　3）基于斷言的驗證是結合形式化驗證和傳統的模擬驗證可行的途徑［5］。支持這種途徑的統一的設計和驗證語(yǔ)言是SystemVerilog。他是在新的Verilog語(yǔ)言標準上擴充系統描述構件而開(kāi)發(fā)的一種過(guò)渡性的系統級設計語(yǔ)言。該語(yǔ)言可以統一的描述復雜的設計和測試方案（ testbenches）。SystemVerilog支持多級接口設計和斷言，充分利用了當前的設計驗證技術(shù)和實(shí)踐。他后向兼容verilog,具有繼承性，與其同時(shí)成為一個(gè)結合設計和驗證的語(yǔ)言。該語(yǔ)言已經(jīng)得到很多EDA廠(chǎng)商和用戶(hù)的支持，預計將會(huì )流行起來(lái)。
　　參考文獻
　　1］Goering R.Nextgeneration Verilog Rises to Higher Abstraction LevelsEE Times, March 2002
　　2］Habibi A，Tahar S.A Survey:Systemonachip Design and VerificationTechnical Report, Electrical Computer Engineering Department, Concordia University,Montreal, Quebec, Canada, January 2003
　　3］Assertionbased VerificationSynopsys,Inchttp://www.synopsys.com/products/simulation/ova_wp.html,March， 2003
　　4］Goering R. Accellera Picks IBM′s Formal Property Language as StandardEE Times, April， 2002
　　5］韓俊剛，杜慧敏.數字硬件的形式化驗證［M］.北京：北京大學(xué)出版社，2001
　　6］Habibi A，Tahar S. A Survey on Systemonachip Design Languages.Technical Report, Electrical Computer Engineering Department, Concordia University,Montreal,Quebec,Canada,January 2003.Canada,2003