硬件設(shè)計(jì)驗(yàn)證（基于模擬與形式的方法）

定　價(jià)：￥45.00

作　者：	（美）蘭姆
出版社：	機(jī)械工業(yè)出版社
叢編項(xiàng)：	電子與電氣工程叢書
標(biāo)　簽：	計(jì)算機(jī)結(jié)構(gòu)、設(shè)計(jì)與制造計(jì)算機(jī)科學(xué)理論計(jì)算機(jī)與互聯(lián)網(wǎng)

購(gòu)買這本書可以去

ISBN：	9787111195023	出版時(shí)間：	2007-01-01	包裝：	平裝
開本：	16	頁(yè)數(shù)：	359	字?jǐn)?shù)：

內(nèi)容簡(jiǎn)介

　　本書全面介紹硬件系統(tǒng)設(shè)計(jì)驗(yàn)證的技術(shù)和方法，主要涉及基于模擬和形式驗(yàn)證的方法，內(nèi)容涵蓋靜態(tài)檢驗(yàn)、模擬器體系結(jié)構(gòu)、測(cè)試基準(zhǔn)設(shè)計(jì)、模擬規(guī)劃與策略、調(diào)試進(jìn)程與驗(yàn)證周期，形式驗(yàn)證背景知識(shí)、判定圖與SAT問題、符號(hào)計(jì)算與模型檢驗(yàn)。書中匯集大量設(shè)計(jì)驗(yàn)證的基本概念與技術(shù)，內(nèi)容深入淺出，敘述詳盡，既討淪一般的測(cè)試原則又展示具體的實(shí)踐方法，包含作者多午實(shí)踐經(jīng)驗(yàn)，實(shí)用性強(qiáng)。每章最后還配有各類習(xí)題，瀆者可用來(lái)鞏固所學(xué)的知識(shí)。. 本書可作為高等院校電子科學(xué)與技術(shù)、計(jì)算機(jī)科學(xué)與技術(shù)等專業(yè)高年級(jí)本科生或低年級(jí)研究生教材，也可供相關(guān)專業(yè)工程師參考。.. 隨著數(shù)字邏輯設(shè)計(jì)的規(guī)模越來(lái)越大，復(fù)雜度越來(lái)越高，功能驗(yàn)證已經(jīng)成為設(shè)計(jì)過程中的首要瓶頸。縮短驗(yàn)證時(shí)間是項(xiàng)目取得成功的關(guān)鍵。本書系統(tǒng)地闡述了當(dāng)今最具價(jià)值的基于模擬和形式方法的驗(yàn)證技術(shù)，幫助測(cè)試工程師和設(shè)計(jì)工程師為每個(gè)項(xiàng)目選擇最佳的解決方法，最快地在設(shè)計(jì)中建立起自信，并將它移植到更快的制造過程中。本書作者William K．Lam是設(shè)計(jì)驗(yàn)證方面的世界級(jí)一流專家，書中匯聚了作者廣博的實(shí)踐經(jīng)驗(yàn)，既討論一般的測(cè)試原則，也展示具體的實(shí)踐方法，有些內(nèi)容還提供了偽代碼形式的算法，讀者只需簡(jiǎn)單地改寫為具體的程序設(shè)計(jì)語(yǔ)言，即可上機(jī)調(diào)試。無(wú)論高校學(xué)生還是企業(yè)的驗(yàn)證工程師都可以從本書獲益。...

作者簡(jiǎn)介

　　本書提供作譯者介紹William K．Lam是Sun公司實(shí)驗(yàn)室的資深經(jīng)理兼高級(jí)工程主管，曾獲得2002年度Sun公司最高技術(shù)成就獎(jiǎng)——總裁創(chuàng)新獎(jiǎng)。他擁有加州大學(xué)伯克利分校電氣與計(jì)算機(jī)工程系博士學(xué)位，曾獲得1994年優(yōu)秀博士論文D．J，Sakrison獎(jiǎng)。他發(fā)表過大量論文及兩部專著，并擁有多項(xiàng)美國(guó)專利。.王維維博士，浙江大學(xué)副教授，碩士生導(dǎo)師。目前主要從事電子設(shè)計(jì)自動(dòng)化、計(jì)算機(jī)科學(xué)等領(lǐng)域的教學(xué)與科研工作。曾參與多項(xiàng)國(guó)家自然科學(xué)基金、浙江省自然科學(xué)基金項(xiàng)目，發(fā)表論文多篇，參與教材編寫兩部。...

圖書目錄

第1章設(shè)計(jì)驗(yàn)證的緣由
1. 1 什么是設(shè)計(jì)驗(yàn)證
1. 2 驗(yàn)證的基本原理
1. 3 驗(yàn)證方法學(xué)
1. 4 基于模擬的驗(yàn)證與形式驗(yàn)證的比較
1. 5 形式驗(yàn)證的局限性
1. 6 Verilog語(yǔ)言調(diào)度和執(zhí)行語(yǔ)義簡(jiǎn)介
1. 7 本章小結(jié)
第2章編寫驗(yàn)證的代碼
2. 1 功能正確性
2. 2 時(shí)序正確性
2. 3 模擬的性能
2. 4 可移植性與可維護(hù)性
2. 5 可綜合性. 可調(diào)試性與通用工具兼容性
2. 6 基于周期的模擬
2. 7 硬件模擬／仿真
2. 8 2狀態(tài)與4狀態(tài)模擬
2. 9 linter程序的設(shè)計(jì)與使用
2. 10 本章小結(jié)
2. 11 習(xí)題
第3章模擬器體系結(jié)構(gòu)與操作
3. 1 編譯器
3. 2 模擬器
3. 3 模擬器的分類與比較
3. 4 模擬器的操作與應(yīng)用
3. 5 增量式編譯
3. 6 模擬器控制臺(tái)
3. 7 本章小結(jié)
3. 8 習(xí)題
第4章測(cè)試基準(zhǔn)組成與設(shè)計(jì)
4. 1 測(cè)試基準(zhǔn)的分類與測(cè)試環(huán)境
4. 2 初始化機(jī)制
4. 3 時(shí)鐘生成與同步
4. 4 激勵(lì)生成
4. 5 響應(yīng)評(píng)估
4. 6 驗(yàn)證實(shí)用程序
4. 7 測(cè)試基準(zhǔn)至系統(tǒng)設(shè)計(jì)接口
4. 8 常見的實(shí)際技術(shù)與方法
4. 9 本章小結(jié)
4. 10 習(xí)題
第5章測(cè)試構(gòu)想. 斷言與覆蓋
5. 1 分層驗(yàn)證
5. 2 測(cè)試規(guī)劃
5. 3 偽隨機(jī)測(cè)試生成程序
5. 4 斷言
5. 5 System Verilog斷言
5. 6 驗(yàn)證覆蓋
5. 7 本章小結(jié)
5. 8 習(xí)題
第6章調(diào)試進(jìn)程與驗(yàn)證周期
6. 1 故障捕獲. 范圍壓縮與錯(cuò)誤跟蹤..
6. 2 模擬數(shù)據(jù)轉(zhuǎn)儲(chǔ)
6. 3 潛在故障原因的隔離
6. 4 系統(tǒng)設(shè)計(jì)更新與維護(hù)：修改控制
6. 5 回歸. 發(fā)布機(jī)制與流片標(biāo)準(zhǔn)
6,596 本章小結(jié)
6. 7 習(xí)題
第7章形式驗(yàn)證初步
7. 1 集合與運(yùn)算
7. 2 關(guān)系. 劃分. 偏序集與格
7. 3 布爾函數(shù)與表示
7. 4 布爾函數(shù)運(yùn)算符
7. 5 有限狀態(tài)自動(dòng)機(jī)與語(yǔ)言
7. 6 本章小結(jié)
7. 7 習(xí)題
第8章判定圖. 等價(jià)檢驗(yàn)與符號(hào)
模擬
8. 1 二叉判定圖
8. 2 判定圖的變異
8. 3 基于判定圖的等價(jià)檢驗(yàn)
8. 4 布爾可滿足性
8. 5 符號(hào)模擬
8. 6 本章小結(jié)
8. 7 習(xí)題
第9章模型檢驗(yàn)與符號(hào)計(jì)算
9. 1 性質(zhì). 規(guī)范與邏輯
9. 2 性質(zhì)檢驗(yàn)
9. 3 符號(hào)計(jì)算與模型檢驗(yàn)
9. 4 符號(hào)CTL模型檢驗(yàn)
9. 5 計(jì)算改進(jìn)
9. 6 模型檢驗(yàn)工具的使用
9. 7 本章小結(jié)
9. 8 習(xí)題
參考文獻(xiàn)
縮寫詞匯表...