1 前言

　解決系統(tǒng)級(jí)設(shè)計(jì)問題首先要解決系統(tǒng)及功能的描述問題。系統(tǒng)級(jí)設(shè)計(jì)語言的競(jìng)爭(zhēng)正在如火如荼的展開。需要一種語言能夠描述包括嵌入的軟件和模擬電路在內(nèi)的整個(gè)系統(tǒng)。而現(xiàn)在的寄存器級(jí)的硬件描述語言將成為硬件設(shè)計(jì)的匯編語言。設(shè)計(jì)和驗(yàn)證工程師將只在關(guān)鍵的部分利用他們?nèi)〉幂^高的性能，而一般情況下將主要利用系統(tǒng)及語言進(jìn)行設(shè)計(jì)和驗(yàn)證。

　　本文將對(duì)當(dāng)前出現(xiàn)的系統(tǒng)級(jí)設(shè)計(jì)和驗(yàn)證語言及其發(fā)展趨勢(shì)進(jìn)行全面地綜述，在第2節(jié)和第3節(jié)將分別綜述系統(tǒng)及設(shè)計(jì)語言和驗(yàn)證語言的發(fā)展情況。第4節(jié)論述當(dāng)前主流的驗(yàn)證方法。

　　2　系統(tǒng)級(jí)設(shè)計(jì)語言

　　2.1　對(duì)系統(tǒng)級(jí)設(shè)計(jì)語言的要求

　　系統(tǒng)級(jí)設(shè)計(jì)的特點(diǎn)是：更多更復(fù)雜的功能集成和綜合、功能模塊或IP核，包含存儲(chǔ)器、處理器、模擬模塊、接口模塊和高速、高頻輸入輸出及軟件模塊，因此要考慮軟件和硬件的劃分、優(yōu)化等協(xié)同設(shè)計(jì)和協(xié)同驗(yàn)證問題。根據(jù)系統(tǒng)級(jí)設(shè)計(jì)的特點(diǎn)，人們普遍認(rèn)為系統(tǒng)級(jí)設(shè)計(jì)語言應(yīng)當(dāng)具有如下的特點(diǎn)：

　　1)具有形式化的語義。

　　2)支持特別領(lǐng)域規(guī)范的集成。

　　3)支持描述系統(tǒng)和部件的計(jì)算模型的復(fù)合。

　　4)支持更加抽象的建模。

　　5)支持對(duì)于限制信息的表示和集成。

　　6)從設(shè)計(jì)規(guī)范到設(shè)計(jì)實(shí)現(xiàn)整個(gè)設(shè)計(jì)過程中一致地、連續(xù)地探索設(shè)計(jì)空間。

　　7)支持在具體領(lǐng)域和多個(gè)交叉領(lǐng)域的預(yù)先分析和驗(yàn)證。

　　2.2　系統(tǒng)級(jí)設(shè)計(jì)語言的發(fā)展

　　21世紀(jì)初期是系統(tǒng)級(jí)設(shè)計(jì)語言發(fā)展變化最迅速的時(shí)期。各種系統(tǒng)設(shè)計(jì)語言 如雨后春筍，已經(jīng)出現(xiàn)的系統(tǒng)級(jí)語言可以分成3類。

　　第一類是通過對(duì)于經(jīng)典語言的擴(kuò)展得到的語言如SystemVerilog[1]。SystemVerilog 在向高層次發(fā)展方面，對(duì)于原來的Verilog進(jìn)行了根本性的修改。他混合了Verilog, C/C++和 CoDesign AutomaTIon′s SuperLog 給設(shè)計(jì)者提供了最強(qiáng)的能力。SystemVerilog是對(duì)于IEEE 13642001 Verilog的擴(kuò)展，以便輔助提供產(chǎn)生并驗(yàn)證抽象的系統(tǒng)結(jié)構(gòu)級(jí)的模型。在接口方面突出的特點(diǎn)是在高層抽象可以實(shí)現(xiàn)模塊的連接。類似于C語言的結(jié)構(gòu)，如斷言結(jié)構(gòu)支持性質(zhì)的檢驗(yàn)。主要擴(kuò)展的目的是使得Verilog語言能夠支持大規(guī)模的設(shè)計(jì)并達(dá)到更高級(jí)的抽象。他還借用了C的數(shù)據(jù)類型 “char”,“int”等。凡是C的編碼可以直接用在Verilog模型和驗(yàn)證程序中。這類對(duì)傳統(tǒng)語言擴(kuò)展的方法的優(yōu)點(diǎn)是有利于設(shè)計(jì)者的平穩(wěn)過渡，但是主張完全用C語言作為系統(tǒng)級(jí)語言的人們懷疑這種“改良”的方法在進(jìn)行模擬時(shí)的效率不能得到滿意結(jié)果。

　　第二類是利用軟件領(lǐng)域的語言和方法，如C/C++,Java,UML等等。主張用C/C++作為系統(tǒng)級(jí)設(shè)計(jì)語言的人們認(rèn)為隨著時(shí)間的推移，最終將會(huì)利用C的自動(dòng)編譯程序和其他自動(dòng)化的工具來實(shí)現(xiàn)從C/C++的模型到芯片的編譯。在目前工具不完善的情況下必須進(jìn)行人工逐步求精的設(shè)計(jì)。也就是說，目前C/C++要擴(kuò)展硬件表達(dá)成分而不是只在算法級(jí)描述。例如 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類：一類是在標(biāo)準(zhǔn)C語言上進(jìn)行擴(kuò)充，以SpecC為代表;另一類是利用C++可擴(kuò)充性，以SystemC為代表，他提供一組硬件的基本元件，這些元件可以擴(kuò)充，以便在更高的層次上支持硬件。這2種互補(bǔ)的方法都在4個(gè)層次上即算法、模塊、按照周期(cycle accurate)和寄存器傳輸(RTL)級(jí)別上支持硬件描述。在SystemC20之前，有些人認(rèn)為SystemC是側(cè)重于模擬，SpecC是側(cè)重于規(guī)范和結(jié)構(gòu)建模，以綜合和驗(yàn)證為目標(biāo)，但是在SystemC20之后，這些說法也不準(zhǔn)確了，因?yàn)楝F(xiàn)在的SystemC2.0已經(jīng)能夠支持所有系統(tǒng)級(jí)的要求。 SystemC填補(bǔ)了在傳統(tǒng)的HDL和基于C/C++的軟件開發(fā)方法之間的鴻溝。他包含C++類庫和一個(gè)模擬內(nèi)核，這個(gè)內(nèi)核用來產(chǎn)生行為級(jí)和寄存器級(jí)的模型。有領(lǐng)先的EDA廠家管理和支持，并與商用的綜合工具相結(jié)合。他支持通用的軟件和硬件開發(fā)環(huán)境。

　　我們認(rèn)為，和C相比，C++顯然是比較好的選擇。因?yàn)镃++是可以擴(kuò)展的，也因?yàn)橛布械牟l(fā)概念易于用類庫表示，C++面向?qū)ο蟮谋举|(zhì)與HDL的分層次特性可以很好地對(duì)應(yīng)。

　　人們也在討論Java是否可以作為系統(tǒng)及語言和高級(jí)硬件描述語言的問題[2]。例如LavaLogic先提出JHDL，他把Java語言的描述轉(zhuǎn)換成為綜合的HDL程序，再用所提供的工具變成門級(jí)的描述。擁護(hù)Java作為系統(tǒng)級(jí)描述語言的人認(rèn)為Java可以提高描述和運(yùn)行效率，與現(xiàn)在的HDL相比，能夠以很簡(jiǎn)短的程序表達(dá)高層的概念。C/C++具有內(nèi)在的表達(dá)并發(fā)能力，相反Java可以用線程顯式的表達(dá)并發(fā)。但是Java不支持模板和操作符過載，因此可能產(chǎn)生大量的過程調(diào)用。

　　第三類是全新的系統(tǒng)級(jí)語言。例如Rosetta，用這一個(gè)語言，用戶可以描述幾乎任何工程領(lǐng)域的行為和限制，包括模擬、數(shù)字、軟件、微流體和機(jī)械等。但是并不能代替和實(shí)現(xiàn)Verilog，VHDL和C等。他由美國DARPA開發(fā)，目的是給設(shè)計(jì)者提供描述大型的、復(fù)雜的計(jì)算系統(tǒng)，特別是混合多種技術(shù)的系統(tǒng)的能力，他可以在高層次上定義、捕獲和驗(yàn)證系統(tǒng)的限制條件和需求條件及其部件。他提供定義和結(jié)合多個(gè)領(lǐng)域的語義模型，進(jìn)行建模和分析。他的語義是形式化的、可以擴(kuò)展的，并且能適應(yīng)新系統(tǒng)的要求。

　　Rosetta 的設(shè)計(jì)方法學(xué)是基于一種多面體的小平面(facet)的概念。facet是部件或系統(tǒng)的模型，他提供所關(guān)心領(lǐng)域具體的信息。為了支持異構(gòu)系統(tǒng)的設(shè)計(jì)，每個(gè)小平面提供具體領(lǐng)域的詞匯和語義。他用來從不同角度定義系統(tǒng)的視圖，然后把不同的小平面組合起來構(gòu)成部件的模型。部件的模型再組合成系統(tǒng)的模型。

　　Rosetta的 facets語法對(duì)于現(xiàn)有的硬件描述語言的用戶來說，應(yīng)當(dāng)是容易熟悉的。他的語法和VHDL幾乎是一樣的。該語言設(shè)計(jì)的主要難點(diǎn)是要把多個(gè)領(lǐng)域的信息統(tǒng)一在一種設(shè)計(jì)活動(dòng)中。對(duì)于不同的領(lǐng)域，例如模擬、數(shù)字、機(jī)械、和光部件，Rosetta 提供了定義和理解系統(tǒng)的機(jī)制。不僅如此，他還提供對(duì)于擴(kuò)展新領(lǐng)域進(jìn)行建模的技術(shù)，這對(duì)于將來語言的發(fā)展非常重要。不能正確理解不同領(lǐng)域的交互作用經(jīng)常是引起系統(tǒng)失敗的根源。因此Rosetta提供顯式的交互建模和評(píng)價(jià)這些交互的方法。

　　3　系統(tǒng)級(jí)驗(yàn)證語言

　　3.1　基于事務(wù)的驗(yàn)證和基于斷言的驗(yàn)證

　　驗(yàn)證語言的提出需要說明基于事務(wù)的驗(yàn)證和基于斷言的驗(yàn)證。解決所謂系統(tǒng)芯片的“驗(yàn)證危機(jī)”，策略之一是基于事務(wù)處理的驗(yàn)證(TBV)，事務(wù)是概念上單一的數(shù)據(jù)或控制的轉(zhuǎn)移，這種轉(zhuǎn)移有事務(wù)的開始時(shí)間，結(jié)束時(shí)間和所有相關(guān)的信息確定，這些信息和事務(wù)一起存儲(chǔ)，作為事務(wù)的屬性。事務(wù)處理可以是簡(jiǎn)單的存儲(chǔ)器讀寫，也可以是具有復(fù)雜的結(jié)構(gòu)數(shù)據(jù)報(bào)在網(wǎng)絡(luò)信道中的傳送。把驗(yàn)證的層次從信號(hào)層次提高到事務(wù)處理層次，讓測(cè)試具有更直觀的方式，有利于測(cè)試產(chǎn)生、糾錯(cuò)過程和功能覆蓋的度量。設(shè)計(jì)系統(tǒng)結(jié)構(gòu)不是想象使能信號(hào)和地址總線如何工作，而是想象數(shù)據(jù)如何在系統(tǒng)中流動(dòng)和存儲(chǔ)。TBV就是這種高層次設(shè)計(jì)過程的自然展開。定性的驗(yàn)證過程包含3個(gè)步驟：測(cè)試生成、設(shè)計(jì)查錯(cuò)和功能覆蓋分析。每個(gè)階段都要提高到事務(wù)處理的抽象層次。可以用Verilog語言的task 來構(gòu)成事務(wù)。這對(duì)于基本的測(cè)試也許還可以接受，但是當(dāng)要產(chǎn)生復(fù)雜的數(shù)據(jù)結(jié)構(gòu)、復(fù)雜的測(cè)試方案，動(dòng)態(tài)的測(cè)試生成時(shí)，就會(huì)產(chǎn)生太多的限制。高級(jí)驗(yàn)證語言(HLV)例如近年來開發(fā)TestBuilder(C++)、Vera和 E等，就是要解決這些復(fù)雜的問題。

　　基于斷言的驗(yàn)證(ABV)是把形式化方法集成到傳統(tǒng)模擬流程中的一種有效的方法。設(shè)計(jì)團(tuán)隊(duì)在RTL設(shè)計(jì)中插入設(shè)計(jì)意圖(斷言)并且進(jìn)行模擬，然后用形式化技術(shù)檢查斷言，限制條件，也就是合法接口行為的斷言，和其他斷言同時(shí)一同參加模擬。斷言檢查的結(jié)果改進(jìn)模擬的有效性。即使利用傳統(tǒng)的模擬驗(yàn)證，斷言也可以大大提高模擬的效率。基于斷言的驗(yàn)證要由用戶寫出斷言，斷言表示要驗(yàn)證的性質(zhì)，因此需要性質(zhì)描述語言。例如邏輯和時(shí)序方面的性質(zhì)。這些也是驗(yàn)證語言要解決的問題。

　　3.2　目前的系統(tǒng)級(jí)驗(yàn)證語言概況

　　IC設(shè)計(jì)和EDA 界需要一種標(biāo)準(zhǔn)化的具有公開接口的驗(yàn)證方法學(xué)，在2000年，Open Verilog InternaTIonal和VHDL International聯(lián)合，組成了Accellera組織。其目的就是在系統(tǒng)、半導(dǎo)體和設(shè)計(jì)工具企業(yè)，推動(dòng)、開發(fā)和培育新的國際標(biāo)準(zhǔn)。以便加強(qiáng)以語言為基礎(chǔ)的設(shè)計(jì)自動(dòng)化進(jìn)程。面對(duì)幾個(gè)在語法和語義方面都不夠完善的形式性質(zhì)描述語言，Accellera進(jìn)行了一個(gè)選舉過程，4個(gè)候選的語言是 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è)標(biāo)準(zhǔn)語言，Sugar 2.0語法和語義很簡(jiǎn)單明了。基本上是基于線性時(shí)態(tài)邏輯語言(LTL),他是由基于分支時(shí)態(tài)邏輯(計(jì)算樹邏輯CTL)的Sugar1.0演化而來的。其關(guān)鍵思想是利用一種擴(kuò)展的正則表達(dá)式的構(gòu)件。因此對(duì)于形式驗(yàn)證領(lǐng)域來說，理解Sugar是很容易的。

　　Sugar語言是由IBM的Haifa 實(shí)驗(yàn)是經(jīng)過8年研究開發(fā)的[4]，是一種說明性的形式化性質(zhì)規(guī)范語言。其語義是嚴(yán)格的，但是易于理解和使用。可以用類似定理的形式 描述要驗(yàn)證的屬性，這些描述可以作為模型檢驗(yàn)和定理證明的輸入，也可以做模擬程序中檢查程序的輸入。Sugar由4層結(jié)構(gòu)組成：

　　布爾層由布爾表達(dá)式構(gòu)成。

　　時(shí)態(tài)層描述邏輯值隨時(shí)間變化的性質(zhì)。

　　驗(yàn)證層由一些指示詞描述驗(yàn)證軟件如何利用時(shí)態(tài)的性質(zhì)。還有些驗(yàn)證指示詞假設(shè)某種性質(zhì)成立。驗(yàn)證層也提供把Sugar的語句分成驗(yàn)證單元的方式。

　　模型層提供對(duì)于輸入行為進(jìn)行建模的方法，對(duì)于輔助信號(hào)和變量進(jìn)行 說明并定義其行為。模型層也可以定義為時(shí)態(tài)層的性質(zhì)和實(shí)體的名字。

　　Sugar具有3種風(fēng)格，分別對(duì)應(yīng)于硬件描述語言Verilog，VHDL和環(huán)境描述語言EDL( IBM的RuleBase 模型檢驗(yàn)器使用的語言)。采用不同風(fēng)格時(shí)，在布爾層和模型層的 語法可以不同，但是在時(shí)態(tài)層和驗(yàn)證層相同。

　　OpenVera 1.0 是Synopsys捐獻(xiàn)出來公開的驗(yàn)證語言。對(duì)于模擬，他已經(jīng)具有描述斷言的能力。Synopsys公司和Intel公司的ForSpec相結(jié)合后產(chǎn)生的OpenVera 2.0也能夠支持形式化驗(yàn)證。和Intel公司聯(lián)合推出OpenVeraForespec 作為工業(yè)標(biāo)準(zhǔn)的斷言語言，但是因?yàn)閷?duì)于工程師來說難以接受，因此被拒絕。但是其概念還是有特點(diǎn)的。他的目標(biāo)是作為一種支持模擬和形式驗(yàn)證的性質(zhì)描述語言。從ForSpec借用的構(gòu)件和操作包括“assume”，“restrict”，“model”，“assert” 等，這些都為形式化驗(yàn)證服務(wù)。語言成分“ assumeguarantee”可以把斷言作為模塊的性質(zhì)，在高層上又作為監(jiān)視器。OpenVera 用來描述斷言時(shí)可以精確的描述在多個(gè)周期時(shí)間的時(shí)序行為。硬件描述語言例如Verilog和 VHDL是用來描述硬件的過程行為。這種過程模型難以有效地表述在多周期的時(shí)態(tài)行為。利用Ope nVera的斷言語言O(shè)VA，用戶可以方便直觀地描述輸入輸出行為、總線協(xié)議以及其他復(fù)雜的硬件行為和關(guān)系。和硬件描述語言的描述比較，要簡(jiǎn)潔3~5倍。和Sugar語言的4級(jí)結(jié)構(gòu)相比，OpenVera 2.0分為5個(gè)主要的級(jí)別：

　　上下文(環(huán)境)幫助定義斷言的轄域(或作用域)。

　　指示詞描述所要檢查或監(jiān)視的性質(zhì)。

　　布爾表達(dá)式。

　　事件表達(dá)式表示時(shí)間序列。

　　公式表示表述時(shí)間序列之間的關(guān)系。

　　Sugar和 Open Vera 2.0 有2個(gè)層次是相同的，即布爾層和時(shí)態(tài)層。這些層構(gòu)成了斷言的核心。他們的差別在其他層次上面。OpenVera 2.0 重視性質(zhì)的細(xì)致結(jié)構(gòu)，用戶能和斷言深入交互，以便考察和探索形式驗(yàn)證的知識(shí)。Sugar的另外2個(gè)層次服務(wù)于性質(zhì)的“格式化”，而簡(jiǎn)化與用戶的交互。總之，不管用那種語言，Open Vera 2.0 或者Sugar，他們都提供了高效驗(yàn)證復(fù)雜系統(tǒng)芯片的手段。

　　4　對(duì)于當(dāng)前驗(yàn)證方法的評(píng)述

　　目前的設(shè)計(jì)驗(yàn)證方法迅速發(fā)展，設(shè)計(jì)和驗(yàn)證語言層出不窮。但是以下的觀點(diǎn)和結(jié)論是明確的：

　　1)形式化方法取得了長(zhǎng)足進(jìn)展，特別是等價(jià)性檢驗(yàn)已經(jīng)集成到標(biāo)準(zhǔn)驗(yàn)證流程中。模型檢驗(yàn)技術(shù)以及定理證明等還不能成為設(shè)計(jì)環(huán)境的主流驗(yàn)證方法的主要原因有[3]:

　　①缺乏廣泛接受的性質(zhì)描述語言。

　　②缺乏商業(yè)化的工具。

　　③至今缺乏有效地使用形式化方法學(xué)的指導(dǎo)原則。

　　④在改變驗(yàn)證方法帶來的收益是否明顯的問題上還在觀望。

　　2)形式化方法還需要和傳統(tǒng)的方法相結(jié)合才能發(fā)揮作用。設(shè)計(jì)和驗(yàn)證方法的進(jìn)步應(yīng)當(dāng)是漸進(jìn)的，不可能革命性的改變。因此在可以預(yù)見的幾年內(nèi)，混合驗(yàn)證方法應(yīng)當(dāng)成為主流的驗(yàn)證方法。斷言對(duì)于表示接口限制、設(shè)計(jì)性質(zhì)和設(shè)計(jì)假設(shè)都具有很深刻的作用和影響。這些會(huì)對(duì)發(fā)現(xiàn)過去的方法不能發(fā)現(xiàn)的設(shè)計(jì)錯(cuò)誤做出貢獻(xiàn)。特別適合測(cè)試覆蓋結(jié)合起來可以極大的改進(jìn)驗(yàn)證效率。

　　3)基于斷言的驗(yàn)證是結(jié)合形式化驗(yàn)證和傳統(tǒng)的模擬驗(yàn)證可行的途徑[5]。支持這種途徑的統(tǒng)一的設(shè)計(jì)和驗(yàn)證語言是SystemVerilog。他是在新的Verilog語言標(biāo)準(zhǔn)上擴(kuò)充系統(tǒng)描述構(gòu)件而開發(fā)的一種過渡性的系統(tǒng)級(jí)設(shè)計(jì)語言。該語言可以統(tǒng)一的描述復(fù)雜的設(shè)計(jì)和測(cè)試方案( testbenches)。SystemVerilog支持多級(jí)接口設(shè)計(jì)和斷言，充分利用了當(dāng)前的設(shè)計(jì)驗(yàn)證技術(shù)和實(shí)踐。他后向兼容verilog,具有繼承性，與其同時(shí)成為一個(gè)結(jié)合設(shè)計(jì)和驗(yàn)證的語言。該語言已經(jīng)得到很多EDA廠商和用戶的支持，預(yù)計(jì)將會(huì)流行起來。