系統(tǒng)級芯片設(shè)計語言和驗證語言的發(fā)展

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

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

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

　　1）形式化方法取得了長足進展，特別是等價性檢驗已經(jīng)集成到標準驗證流程中。模型檢驗技術(shù)以及定理證明等還不能成為設(shè)計環(huán)境的主流驗證方法的主要原因有［3］:
　?、偃狈V泛接受的性質(zhì)描述語言。
　　②缺乏商業(yè)化的工具。
　?、壑两袢狈τ行У厥褂眯问交椒▽W的指導(dǎo)原則。
　?、茉诟淖凃炞C方法帶來的收益是否明顯的問題上還在觀望。
　　2）形式化方法還需要和傳統(tǒng)的方法相結(jié)合才能發(fā)揮作用。設(shè)計和驗證方法的進步應(yīng)當是漸進的，不可能革命性的改變。因此在可以預(yù)見的幾年內(nèi)，混合驗證方法應(yīng)當成為主流的驗證方法。斷言對于表示接口限制、設(shè)計性質(zhì)和設(shè)計假設(shè)都具有很深刻的作用和影響。這些會對發(fā)現(xiàn)過去的方法不能發(fā)現(xiàn)的設(shè)計錯誤做出貢獻。特別適合測試覆蓋結(jié)合起來可以極大的改進驗證效率。
　　3）基于斷言的驗證是結(jié)合形式化驗證和傳統(tǒng)的模擬驗證可行的途徑［5］。支持這種途徑的統(tǒng)一的設(shè)計和驗證語言是SystemVerilog。他是在新的Verilog語言標準上擴充系統(tǒng)描述構(gòu)件而開發(fā)的一種過渡性的系統(tǒng)級設(shè)計語言。該語言可以統(tǒng)一的描述復(fù)雜的設(shè)計和測試方案（ testbenches）。SystemVerilog支持多級接口設(shè)計和斷言，充分利用了當前的設(shè)計驗證技術(shù)和實踐。他后向兼容verilog,具有繼承性，與其同時成為一個結(jié)合設(shè)計和驗證的語言。該語言已經(jīng)得到很多EDA廠商和用戶的支持，預(yù)計將會流行起來。
　　參考文獻
　　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］韓俊剛，杜慧敏.數(shù)字硬件的形式化驗證［M］.北京：北京大學出版社，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