《SystemVerilog驗證方法學》

《SystemVerilog驗證方法學》,作者夏宇聞、楊雷、陳先勇、徐偉俊,北京航空航天大學出版社2007年5月1日出版。

基本信息

內容簡介

本書藉助許多用SystemVerilog編寫的例子,介紹和說明一套完整的驗證方法學。它涵蓋了所有最新的驗證技術,其中包括:驗證計畫制定、testbench架構、受約束隨機激勵產生、以覆蓋率為主導(coverage-driven)的驗證、基於斷言(assertion-based)的驗證、形式化分析,以及基於一個開放、完善的方法學上的系統級驗證。此外,本書也包括標準程式庫VMM和VMM檢查器,從而可幫助縮短驗證開發的時間。本書可作為電子工程類、自動控制類、計算機類的大學本科高年級學生及研究生教學用書,亦可供其他工程人員自學與參考。

前言

當初VHDL剛成為IEEE標準時,人們普遍認為VHDL足以對付硬體設計的建模。然而事實表明並非完全如此,因為VHDL沒有預定義的4種狀態邏輯類型,所以各仿真器和模型的供應商不得不自己創建這些狀態類型,而這些類型與VHDL的邏輯類型並不兼容。這種情況很快促使一個小組的成立,該小組的宗旨是為VHDL開發一個能支持多值邏輯的補充標準。最後終於制定了IEEE1164標準。有了這樣一個修正的標準,模型就變成了可移植的,並且仿真器能夠最佳化運行已定義好的操作。

本書的作者希望在SystemVerilog語言的範疇內,為驗證組件創建一個類似於IEEE1164的標準。在附錄中指定的那些基礎結構元素,能夠為形成標準化的驗證接口打下基礎。若模型供應商用這樣的標準驗證接口來構建他們的驗證組件,則這些驗證組件一旦完成設計後,就是可移植的。若仿真器的供應商對自己設計的標準函式的執行進行最佳化,則仿真器的運行性能就能得到改進。本書是如何組織的本書由9個章節和4個附錄組成。這些章節描述了在實現驗證方法學時必須和應該遵循的一些指導原則。附錄詳細說明了套用類的支撐元素,以幫助實現新的驗證過程。第3章提供了編寫斷言的指導原則。與第3章配套的附錄B詳細說明了一套預定義的檢測器,可用來代替編寫新的斷言。第4章描述了驗證環境的組件,以及如何實現這些組件。與第4章對應的附錄A詳細說明了一套基礎和實用類,該類可用於實現各種環境和組件所需的一般功能。第5章描述了如何為被驗證的設計提供測試激勵,以及如何才能對激勵的生成加以約束,以便創建特定的感興趣的測試驗證條件。在附錄A中詳細加以說明的發生器類,能幫助讀者迅速地創建符合VMM要求的發生器組件。第6章描述了如何找到驗證的重點,用比較少的測試完成必要的驗證,以達到所需要的覆蓋率指標,使用(由前面幾章介紹的指導原則建立起來的)可約束的隨機驗證環境,有效地完成驗證的全過程。第7章描述了如何配合形式化技術來使用斷言。附錄B描述的檢查器中只有一個子集能用於這種場合。第8章描述了如何把前面幾章中介紹的原則擴大套用到系統級的驗證中。與其對應的附錄C指定了一種命令語言和可擴展組件的基礎結構,可以實現塊和系統級的驗證環境。第9章描述了如何利用附錄D中預定義的C函式,對由以通用可程式處理器為主構成的系統進行整體的驗證。從附錄A到附錄D,通過描述每個元素的接口和功能,詳細地說明了支撐基礎結構,但並不提供實現方案。具體合適的實現方案有待於廠商提供。這為EDA或IP廠商,對特定平台基礎結構的最佳化實現提供了機會。這也消除了在特定“引用”實現方案時,把不想要的副作用誤認為期望行為的風險。有關接口技術細節的代碼可在以下的網址查到……

請注意:不使用附錄中指定的支撐元素(supportelements),也可使用本方法學。任何功能等價的元素集合都能提供類似的功能。然而,若使用不同的支撐元素,有可能降低用不同的支撐基礎結構(differentsupportinfrastructures)編寫的驗證組件及環境的可移植性。

如何閱讀本書

編寫本書的宗旨不是想把本書編寫成可以邊閱讀邊做練習的教科書。雖然作者盡了最大的努力以合乎邏輯的順序介紹課本的材料,但如果讀者沒有把握驗證的全局總圖,還是很難完全理解該方法學中某些元素的重要性和其中包含的智慧。不幸的是,在尚未介紹搭建整體環境的各個元素前,勾畫出全局總圖又是不可能的。在介紹方法學時總伴隨著先有雞還是先有蛋的悖論。方法學研究的問題是,關於今天我們採取什麼步驟才能使未來的生活變得更容易一些。成功的方法學將通過早期的投入而提供更多的回報,從而有助於降低項目的總開銷。在方法學的實際描述中,因為未來所能取得的回報不可能馬上看得很清楚,所以很難證明早期的投入是否值得。同樣,若未曾描述過元素,也沒有研究過把這些元素放在一起將會產生的價值,描述未來的好處也是不可能的。對類似的方法學不熟悉的讀者,一般需要把整本書從頭到尾讀兩遍。第一遍閱讀能幫助讀者建立起方法學的整體概念,了解不同的元素是如何結合起來的,以及它們的功效。第二遍閱讀能幫助讀者全面地理解該方法學的具體實現步驟和支撐庫。

雖然每個讀者都能從閱讀整本書中受益,但是其中有些章節與某些特定的驗證任務有更大的關聯。設計工程師必須閱讀第3章,若他們想用形式化技術來驗證自己的設計,則還應該閱讀第7章。驗證項目的帶頭人和項目經理應該閱讀第2章和第6章。負責驗證環境的維護和實現的驗證工程師必須閱讀第4章和第5章,還應該閱讀第8章。IP驗證的開發人員應該閱讀第4章和第8章。負責測試事件實施的驗證工程師應該閱讀第5章的前半部分。若還負責功能覆蓋點的實施,他們還應該閱讀第6章的後半部分。嵌入式軟體的驗證工程師應該閱讀第9章。

附加資料來源

編寫本書時,SystemVerilog正在批准成為IEEE標準的處理過程中。除了幾本已經出版和正在出版的書外,關於SystemVerilog的更多資料可從下列網址下載……

本書假設讀者已經具有使用SystemVerilog語言的經驗。編寫本書的宗旨不是編寫一本培訓驗證和斷言結構的教科書和入門教材。下列按字母順序排列的書可用於獲得關於Sys-temVerilog語言結構的知識和必要的經驗:JanickBergeron,WritingTestbenchesUsingSystemVerilog,SpringerBenCohen,SrinivasanVenkataramananandAjeethaKumari,SystemVerilogAssertionsHandbook,VhdlCohenPublishingChrisSpearandArturoSalz,SystemVerilogforVerification,Springer

本書舉例用到的一些代碼段都是作者想要說明的各關鍵點。書中沒有提供完整的方法學套用舉例。這樣的例子需要幾十頁的SystemVerilog代碼才能寫完,而且這樣的代碼很難讀懂,並且隨著方法學的改進很有可能過時,而不可能真正地進行仿真。讀者可用下列與本書配套的網址找到幾個完整的例子及其代碼……

該配套網址上還有本書最新的勘誤表。隨著驗證方法不斷的演變和擴展,網站上也會發布一些新的指導原則。這些添加的指導原則將會被收入未來的新版本中。關於本方法學的解釋和使用中的討論以及改進的建議刊登在下面網址的論壇上……

感 謝

作者衷心地感謝HolgerKeding對第8章的貢獻,也感激下列各位詳盡的審閱及建設性的意見。名單排列如下:PierreAulagnier,OliverBell,MichaelBenjamin,JonathanBradford,CraigDeaton,JeffDelChiaro,GeoffHall,WolfgangEcker,RémiFrancard,ChristianGlaβner,OlivierHaller,TakashiKambe,MasamichiKawarabayashi,MichaelKeating,DaveMatt,AdityaMukherjee,SeiichiNishio,ZenjiOka,MichaelR⒐der,KostasSiomalas,StefanSojka,JasonSprott,STARCIPVerificationswg(MasahiroFuruya,HiroyukiFukuyama,KohkichiHashimoto,MasanoriImai,MasaharuKimura,HiroshiKoguchi,Hi-rohisaKotegawa,YouichiroKumazaki,YoshikazuMori,TadahikoNakamura,SanaeSai-tou,MasayukiShono,TsuneoToba,HideakiWashimi,TakeruYonaga),RobSwan,Yo-shiotakamine,GaryVrckovnikandFrazerWorley。

技術編輯KyleSmith的熱心關懷使本書獲益匪淺。

還有許多人為本書的內容和出版作出了貢獻。他們的名單按照字母順序排列如下:JayAlphey,TomAnderson,TomBorgstrom,DanBrook,DanColey,TomFitz-patrick,MikeGlasscock,JohnGoodenough,BadriGopalan,DavidGwilt,TimHolden,GhassanKhoory,FrameMaker,MehdiMohtashemi,PhilMoorby,DaveRich,SpencerSaunders,DavidSmith,MichaelSmith,ManojKumarThottasseri以及VCSandMagellan執行小組。

目錄

專家推薦
譯者序
序言
前言
本書是如何組織的
如何閱讀本書
附加資料來源
感謝

第1章導論
驗證生產率2
提高生產率2
驗證組件3
基於接口的設計4
針對驗證的設計5
使用斷言的好處6
方法學的實現7
方法學的採納7
指導原則9
基本的編碼指導原則10
術語的定義11

第2章驗證計畫
計畫過程14
功能驗證的需求15
驗證環境的需求18
驗證計畫的實現方案22
回響檢查24
嵌入式監視器25
斷言26
精確性28
記分板30
參考模型30
離線檢查31
總結32

第3章斷言
斷言的指定33
斷言語言基本知識35
DUT(被測設計)內部信號上的斷言39
外部接口上的斷言47
斷言編碼的指導原則50
覆蓋率屬性58
基於斷言的可重用檢查器63
簡單檢查器63
基於斷言的驗證IP71
基於斷言的IP結構74
文檔與發行內容82
斷言的鑑定83
總結84

第4章測試平台的基本結構
測試平台的架構86
信號層89
指令層96
功能層98
場景層101
測試層102
仿真控制104
訊息服務111
數據和事務115
類屬性/數據成員118
方法126
約束條件129
事務處理器132
物理層接口138
事務層接口139
完成和回響模型144
基元按序執行模型145
亂序基元執行模型149
非基元事務執行151
被動回響154
從動回響156
時序接口159
回調方法161
特定的測試平台164
傳統的匯流排功能模型168
VMM兼容升級168
VMM兼容接口169
總結171

第5章激勵與回響
激勵的生成173
隨機激勵174
定向激勵180
異常的生成182
嵌入式激勵186
對隨機生成的控制187
基元生成190
場景生成191
多流生成195
基於狀態的生成197
應選用哪種發生器202
自檢查結構203
記分板206
與事務處理器的集成209
異常的處理211
總結212

第6章針對覆蓋率的驗證
覆蓋率度量指標214
覆蓋率模型215
結構覆蓋率建模216
功能覆蓋率建模216
功能覆蓋率分析218
覆蓋率評級219
功能覆蓋率實現方案219
覆蓋率組221
覆蓋率屬性228
反饋機制228
總結230

第7章用於形式化驗證的斷言
模型檢查和斷言233
對數據的斷言242
不使用局部變數242
使用局部變數245
形式化驗證工具的兼容性250
總結250

第8章系統級驗證
可擴展的驗證組件252
XVC的結構253
XVC的實現255
動作的實現257
XVC管理器261
預定義的XVC管理器262
系統級驗證環境263
塊互聯結構的驗證267
基本集成驗證269
低層次系統功能驗證271
系統認證驗證272
驗證事務層模型274
事務層接口276
硬體輔助的驗證277
外設測試塊的結構279
總結281

第9章處理器集成驗證
軟體測試環境283
基本軟體集成驗證285
全系統驗證環境286
軟體測試結構289
測試動作292
編譯過程296
測試的運行298
引導模組299
總結300

附錄AVMM標準庫技術說明書
VMM_VERSION302
VMM_ENV303
VMM_LOG306
vmm_log_msg319
vmm_log_format320
vmm_log_callbacks322
VMM_DATA324
VMM_CHANNEL330
VMM_BROADCAST342
VMM_SCHEDULER346
vmm_scheduler_election350
VMM_NOTIFY352
vmm_notification357
VMM_XACTOR358
vmm_xactor_callbacks364
VMM_ATOMIC_GEN364
VMM_SCENARIO_GEN368

附錄BVMM檢查器庫
OVL等價的檢查器(SVL)381
高級檢查器387

附錄CXVC標準庫技術說明書
XVC_MANAGER393
XVC_XACTOR395
XVC_ACTION397
VMM_XVC_MANAGER399
注意400
檔案結構401
命令403

附錄D軟體驗證框架
基本類型417
系統描述符418
外設描述符418
中斷描述符421
DMA通道描述符422
測試動作423
低層次服務429
高速快取鎖定434
中斷控制器436
與XVC的軟體接口的連線440
索引441
作者介紹468

相關詞條

相關搜尋

熱門詞條

聯絡我們