1 前言

　解決系統級設計問題首先要解決系統及功能的描述問題。系統級設計語言的競爭正在如火如荼的展開。需要一種語言能夠描述包括嵌入的軟件和模擬電路在內的整個系統。而現在的寄存器級的硬件描述語言將成為硬件設計的匯編語言。設計和驗證工程師將只在關鍵的部分利用他們取得較高的性能，而一般情況下將主要利用系統及語言進行設計和驗證。

　　本文將對當前出現的系統級設計和驗證語言及其發展趨勢進行全面地綜述，在第2節和第3節將分別綜述系統及設計語言和驗證語言的發展情況。第4節論述當前主流的驗證方法。

　　2　系統級設計語言

　　2.1　對系統級設計語言的要求

　　系統級設計的特點是：更多更復雜的功能集成和綜合、功能模塊或IP核，包含存儲器、處理器、模擬模塊、接口模塊和高速、高頻輸入輸出及軟件模塊，因此要考慮軟件和硬件的劃分、優化等協同設計和協同驗證問題。根據系統級設計的特點，人們普遍認為系統級設計語言應當具有如下的特點：

　　1)具有形式化的語義。

　　2)支持特別領域規范的集成。

　　3)支持描述系統和部件的計算模型的復合。

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

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

　　6)從設計規范到設計實現整個設計過程中一致地、連續地探索設計空間。

　　7)支持在具體領域和多個交叉領域的預先分析和驗證。

　　2.2　系統級設計語言的發展

　　21世紀初期是系統級設計語言發展變化最迅速的時期。各種系統設計語言 如雨后春筍，已經出現的系統級語言可以分成3類。

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

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

　　我們認為，和C相比，C++顯然是比較好的選擇。因為C++是可以擴展的，也因為硬件中的并發概念易于用類庫表示，C++面向對象的本質與HDL的分層次特性可以很好地對應。

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

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

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

　　Rosetta的 facets語法對于現有的硬件描述語言的用戶來說，應當是容易熟悉的。他的語法和VHDL幾乎是一樣的。該語言設計的主要難點是要把多個領域的信息統一在一種設計活動中。對于不同的領域，例如模擬、數字、機械、和光部件，Rosetta 提供了定義和理解系統的機制。不僅如此，他還提供對于擴展新領域進行建模的技術，這對于將來語言的發展非常重要。不能正確理解不同領域的交互作用經常是引起系統失敗的根源。因此Rosetta提供顯式的交互建模和評價這些交互的方法。

　　3　系統級驗證語言

　　3.1　基于事務的驗證和基于斷言的驗證

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

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

　　3.2　目前的系統級驗證語言概況

　　IC設計和EDA 界需要一種標準化的具有公開接口的驗證方法學，在2000年，Open Verilog InternaTIonal和VHDL International聯合，組成了Accellera組織。其目的就是在系統、半導體和設計工具企業，推動、開發和培育新的國際標準。以便加強以語言為基礎的設計自動化進程。面對幾個在語法和語義方面都不夠完善的形式性質描述語言，Accellera進行了一個選舉過程，4個候選的語言是 Motorola的CBV，IBM的 Sugar，Intel的 ForSpec 和Verisity的e 語言。經過討論，集中到Sugar和 CBV上，在2002年4月選定了IBM的Sugar 2.0[3]。Sugar 2.0的獲勝造成了Accellera組織的分裂，包括Cadence在內的多數EDA工具供應商支持Accellera 的決定。另外一部分則轉向支持Syopsys的 OpenVera 2.0。作為一種真正的工業標準語言，Sugar 2.0語法和語義很簡單明了?；旧鲜腔诰€性時態邏輯語言(LTL),他是由基于分支時態邏輯(計算樹邏輯CTL)的Sugar1.0演化而來的。其關鍵思想是利用一種擴展的正則表達式的構件。因此對于形式驗證領域來說，理解Sugar是很容易的。

　　Sugar語言是由IBM的Haifa 實驗是經過8年研究開發的[4]，是一種說明性的形式化性質規范語言。其語義是嚴格的，但是易于理解和使用?？梢杂妙愃贫ɡ淼男问?描述要驗證的屬性，這些描述可以作為模型檢驗和定理證明的輸入，也可以做模擬程序中檢查程序的輸入。Sugar由4層結構組成：

　　布爾層由布爾表達式構成。

　　時態層描述邏輯值隨時間變化的性質。

　　驗證層由一些指示詞描述驗證軟件如何利用時態的性質。還有些驗證指示詞假設某種性質成立。驗證層也提供把Sugar的語句分成驗證單元的方式。

　　模型層提供對于輸入行為進行建模的方法，對于輔助信號和變量進行 說明并定義其行為。模型層也可以定義為時態層的性質和實體的名字。

　　Sugar具有3種風格，分別對應于硬件描述語言Verilog，VHDL和環境描述語言EDL( IBM的RuleBase 模型檢驗器使用的語言)。采用不同風格時，在布爾層和模型層的 語法可以不同，但是在時態層和驗證層相同。

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

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

　　指示詞描述所要檢查或監視的性質。

　　布爾表達式。

　　事件表達式表示時間序列。

　　公式表示表述時間序列之間的關系。

　　Sugar和 Open Vera 2.0 有2個層次是相同的，即布爾層和時態層。這些層構成了斷言的核心。他們的差別在其他層次上面。OpenVera 2.0 重視性質的細致結構，用戶能和斷言深入交互，以便考察和探索形式驗證的知識。Sugar的另外2個層次服務于性質的“格式化”，而簡化與用戶的交互?？傊还苡媚欠N語言，Open Vera 2.0 或者Sugar，他們都提供了高效驗證復雜系統芯片的手段。

　　4　對于當前驗證方法的評述

　　目前的設計驗證方法迅速發展，設計和驗證語言層出不窮。但是以下的觀點和結論是明確的：

　　1)形式化方法取得了長足進展，特別是等價性檢驗已經集成到標準驗證流程中。模型檢驗技術以及定理證明等還不能成為設計環境的主流驗證方法的主要原因有[3]:

　?、偃狈V泛接受的性質描述語言。

　?、谌狈ι虡I化的工具。

　　③至今缺乏有效地使用形式化方法學的指導原則。

　?、茉诟淖凃炞C方法帶來的收益是否明顯的問題上還在觀望。

　　2)形式化方法還需要和傳統的方法相結合才能發揮作用。設計和驗證方法的進步應當是漸進的，不可能革命性的改變。因此在可以預見的幾年內，混合驗證方法應當成為主流的驗證方法。斷言對于表示接口限制、設計性質和設計假設都具有很深刻的作用和影響。這些會對發現過去的方法不能發現的設計錯誤做出貢獻。特別適合測試覆蓋結合起來可以極大的改進驗證效率。

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