System Verilog Assertions應(yīng)用指南

定　價：￥39.80

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

購買這本書可以去

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

內(nèi)容簡介

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

作者簡介

暫缺《System Verilog Assertions應(yīng)用指南》作者簡介

圖書目錄

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