System Verilog Assertions應用指南

定　價：￥39.80

作　者：	（美）維加亞拉哈文、拉門那斯
出版社：	清華大學出版社
叢編項：	國外電子信息經(jīng)典教材
標　簽：	計算

購買這本書可以去

ISBN：	9787302134411	出版時間：	2006-10-01	包裝：	平裝
開本：	32	頁數(shù)：	305	字數(shù)：

內(nèi)容簡介

　　2002年中期，我們的經(jīng)理給我們發(fā)了一個電子郵件，問道：“誰愿意去支持OVA？”我們從腦子中迸出的第一個想法就是“究竟什么是OVA？”和其他幾個工程師交談后，我們知道了它是OPEN VERA語言的一個子集。OVA是指“OPEN VERA斷言（Open VERA Assersions，簡寫OVA）”，它是一種描述性的語言，能描述時序上的條件。就如同過去一樣，為了滿足對技術的渴求，我們同意做OVA的支持。在兩個月內(nèi)，我們學習了這種語言，并開始培訓客戶，在六個月內(nèi)培訓了200個左右的客戶?？蛻艉樗阌窟M教室，給我們留下深刻的印象。我們確信這是驗證領域下一件最好的事情。當客戶們匆忙接受完培訓，他們并沒有開發(fā)任何OVA的代碼。這是因為驗證技巧和這種語言都是新的。一些工具剛開始支持這些語言結構。沒有多少IP（Intellectual Property）可以使用。很自然，客戶并沒有我們想像的那么滿意。同時，Synopsys公司把OPEN VERA語言捐獻給Accellera委員會，使其成為SystemVerilog語言的一部分，其他幾個公司為SystemVerilog語言的形成作了一些貢獻。在DAC 2004，Accellera委員會把SystemVerilog 3.1定為一個標準。斷言語言被納入SystemVerilog語言并成為了標準的一部分。這就是通常所說的“SystemVerilog Assertion（SVA）”。我們繼續(xù)培訓客戶基于斷言的驗證，不過現(xiàn)在僅僅教SVA。我們能清楚地看到客戶更習慣于使用預開發(fā)的斷言庫，而不樂意編寫定制的斷言代碼。是什么阻礙了他們？是工具嗎？不，工具是現(xiàn)成的。是語言嗎？或許，但它如今已是一個標準，所以不應該是它。經(jīng)過一番深入的討論，我們認識到，缺乏例子來演示SVA的結構可能是阻礙客戶使用這項新技術的原因。比較典型的是缺乏專家指導導致了如此低的采納率。這時我想到出版一本關于SVA的“烹飪書”可能有用——即一本充滿例子的書，這本書可以作為指導書，用來教授這種語言。這個項目就是這樣啟動的。我們努力把過去兩年中在教授這門科目時所學的東西寫出來。但是在這個領域還有很多東西需要去學，這本書只是把我們所學到的跟大家分享。如何閱讀這本書這本書的寫作方式可以使工程師快速掌握SystemVerilog斷言。第0、1和2章，可以使您充分了解基礎語法和一些通用的模擬技巧。閱讀完這三章，讀者應該能在他們的設計／驗證環(huán)境中寫斷言。第3、4、5和6章是不同類型的設計的“烹飪書”。讀者如果在他們自己的環(huán)境里遇到類似的設計可以參考這些章節(jié)，以這些章節(jié)作為起點開始寫斷言。這些章節(jié)也可以作為指導。如果您是基于斷言驗證的新手，則需要閱讀完第0章~第2章，才能開始其他章節(jié)。如果您熟悉SVA語言，就可以根據(jù)需要參考這些章節(jié)。第0章—— 這是關于基于斷言的驗證（ABV）方法論的白皮書。這一章介紹了ABV的方法學和功能覆蓋的重要性。第1章—— 用簡單的例子討論了SVA的語法和詳細分析了在動態(tài)模擬中執(zhí)行SVA結構的過程。包括了模擬波形和事件表以供讀者參考。要了解每個SVA結構的細節(jié)，用戶可以參考SystemVerilog 3.1 a 語言參考手冊（LRM）的第17章。第2章—— 用一個實例系統(tǒng)說明SVA模擬的方法。主題囊括了協(xié)議解析、模擬控制和功能覆蓋。第3章—— 用兩個不同的有限狀態(tài)機（FSM）模型作為例子，舉例說明如何用SVA驗證FSM。第4章—— 舉例說明用SVA驗證一個數(shù)據(jù)通道。用JPEG設計的一部分來演示如何用SVA驗證控制信號和數(shù)據(jù)。第5章—— 舉例用SVA驗證一個存儲控制器。這個控制器支持不同類型的存儲如：SDRAM、SRAM、FLASH等。第6章—— 舉例用SVA驗證一個基于PCI局部總線的系統(tǒng)。使用了一個PCI系統(tǒng)配置的例子，用SVA驗證不同的PCI協(xié)議。第7章—— 用一個測試平臺（testbench）的例子驗證斷言，也討論了在驗證斷言的精度背后的理論。隨書附一張光盤。本書中的所有例子都可以用VCS 2005.06發(fā)行版運行，也包括運行這些例子的腳本范例。VCS是Synopsys公司的注冊商標。

作者簡介

暫缺《System Verilog Assertions應用指南》作者簡介

圖書目錄

第0章基于斷言的驗證
第1章 SVA介紹
1.1什么是斷言
1.2為什么使用System Verilog斷言(SVA)
1.3System Verilog的調度
1.4SVA術語
1.4.1并發(fā)斷言
1.4.2即時斷言
1.5建立SVA塊
1.6一個簡單的序列
1.7邊沿定義的序列
1.8邏輯關系的序列
1.9序列表達式
1.10時序關系的序列
1.11SvA中的時鐘定義
1.12禁止屬性
1.13一個簡單的執(zhí)行塊
1.14蘊含操作符
1.14.1交疊蘊含
1.14.2非交疊蘊含
1.14.3后續(xù)算子帶固定延遲的蘊含
1.14.4使用序列作為先行算子的蘊含
1.15SvA檢驗器的時序窗口
1.15.1重疊的時序窗口
1.15.2無限的時序窗口
1.16“ended”結構
1.17使用參數(shù)的SVA檢驗器
1.18使用選擇運算符的SVA檢驗器
1.19使用true表達式的SVA檢驗器
1.20“$past”構造
1.21重復運算符
1.21.1連續(xù)重復運算符[*]
1.21.2用于序列的連續(xù)重復運算符[*]
1.21.3用于帶延遲窗口的序列的連續(xù)重復運算符[*]
1.21.4連續(xù)運算符[*]和可能性運算符
1.21.5跟隨重復運算符[->]
1.21.6非連續(xù)重復運算符[=]
1.22“and”構造
1.23“intersect”構造
1.24“or”構造
1.25“firstmatch”構造
1.26“throughout”構造
1.27“within”構造
1.28內(nèi)建的系統(tǒng)函數(shù)
1.29“disableiff”構造
1.30使用“intersect”控制序列的長度
1.31在屬性中使用形參
1.32嵌套的蘊含
1.33在蘊含中使用if/else
1.34SVA中的多時鐘定義
1.35“matched”構造
1.36“expect”構造
1.37使用局部變量的SVA
1.38在序列匹配時調用子程序
1.39將SVA與設計連接
1.40SVA與功能覆蓋
第2章 SVA模擬方法論
2.1一個被驗證的實例系統(tǒng)
2.1.1主控設備
2.1.2中間設備
2.1.3目標設備
2.2塊級驗證
2.2.1SVA在設計塊中的應用
2.2.2仲裁器的驗證
2.213模擬中針對仲裁器的SVA檢驗
2.2.4主控設備的驗證
2.2.5模擬中針對主控設備的SVA檢驗
2.2.6膠合(Glue)的驗證
2.2.7模擬中針對膠合邏輯(glue logic)的SVA檢驗
2.2.8目標設備的驗證
2.2.9模擬中針對目標設備的SVA檢驗
2.3系統(tǒng)級驗證
2.4功能覆蓋
2.4.1實例系統(tǒng)的覆蓋率計劃
2.4.2功能覆蓋小結
2.5用于創(chuàng)建事務日志的SVA
2.6用于FPGA原型測試的SVA
2.7SVA模擬方法的小結
第3章 SVA在有限狀態(tài)機中的應用
3.1設計例子——FSM1
3.1.1FSMl的功能描述
3.1.2FSMl的SVA檢驗器
3.2設計實例——FSM2
3.2.1FSM2的功能描述
3.2.2FSM2的SVA檢驗器
3.2.3有時序窗口協(xié)議的FSM2
3.3在FSM中應用SVA的小結
第4章 SVA用于數(shù)據(jù)集約型(DATA INIENSVE)的設計
4.1簡單乘法器的檢驗
4.2設計實例——算術單元
4.2.1WHT算術
4.2.2WHT硬件的實現(xiàn)
4.2.3WHT模塊的SVA檢驗器
4.3設計實例一PEG的數(shù)據(jù)通路設計
4.3.1三模塊的深入探討
4.3.2用于JPEG設計的SVA檢驗器
4.3.3.IPEG模型的數(shù)據(jù)檢驗
4.4數(shù)據(jù)集約型設計的小結
第5章 SVA儲存器
5.1存儲控制系統(tǒng)實例
5.1.1CPU—AHB接口操作
5.1.2存儲控制器的操作
5.2SDRAM的驗證
5.3SRAM／FLASH的驗證
5.4DDR-SDRAM的驗證
5.5存儲器SVA的小結
第6章 SVA協(xié)議接口
6.1PCI簡介
6.1.1一個PCI讀出事務的實例
6.1.2PCI寫入事務實例
6.2PCI系統(tǒng)實例
6.3情形1——主控DUT設備
6.4情形2——目標DUT設備
6.5情形3——系統(tǒng)級斷言
6.6用于標準協(xié)議的SVA小結
第7章對檢驗器的檢驗
7.1斷言驗證
7.2雙信號SVA Assenion Test
7.2.1雙信號的邏輯關系
7.2.2電平敏感邏輯關系激勵的產(chǎn)生
7.2.3邊沿敏感邏輯關系激勵的產(chǎn)生
7.2.4雙信號的時序關系
7.2.5時序關系激勵的產(chǎn)生
7.2.6雙信號的重復關系
7.2.7雙信號ATB環(huán)境
7.3一個PCI檢驗器的ATB實例
7.4檢驗器檢驗小結