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

第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語言調(diào)度和執(zhí)行語義簡介
1.7 本章小結(jié)
第2章 編寫驗(yàn)證的代碼
2.1 功能正確性
2.2 時序正確性
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 模擬器控制臺
3.7 本章小結(jié)
3.8 習(xí)題
第4章 測試基準(zhǔn)組成與設(shè)計(jì)
4.1 測試基準(zhǔn)的分類與測試環(huán)境
4.2 初始化機(jī)制
4.3 時鐘生成與同步
4.4 激勵生成
4.5 響應(yīng)評估
4.6 驗(yàn)證實(shí)用程序
4.7 測試基準(zhǔn)至系統(tǒng)設(shè)計(jì)接口
4.8 常見的實(shí)際技術(shù)與方法
4.9 本章小結(jié)
4.10 習(xí)題
第5章 測試構(gòu)想、斷言與覆蓋
5.1 分層驗(yàn)證
5.2 測試規(guī)劃
5.3 偽隨機(jī)測試生成程序
5.4 斷言
5.5 SystemVerilog斷言
5.6 驗(yàn)證覆蓋
5.7 本章小結(jié)
5.8 習(xí)題
第6章 調(diào)試進(jìn)程與驗(yàn)證周期
6.1 故障捕獲、范圍壓縮與錯誤跟蹤
6.2 模擬數(shù)據(jù)轉(zhuǎn)儲
6.3 潛在故障原因的隔離
6.4 系統(tǒng)設(shè)計(jì)更新與維護(hù)：修改控制
6.5 回歸、發(fā)布機(jī)制與流片標(biāo)準(zhǔn)
6.6 本章小結(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)自動機(jī)與語言
7.6 本章小結(jié)
7.7 習(xí)題
第8章 判定圖、等價檢驗(yàn)與符號模擬
8.1 二叉判定圖
8.2 判定圖的變異
8.3 基于判定圖的等價檢驗(yàn)
8.4 布爾可滿足性
8.5 符號模擬
8.6 本章小結(jié)
8.7 習(xí)題
第9章 模型檢驗(yàn)與符號計(jì)算
9.1 性質(zhì)、規(guī)范與邏輯
9.2 性質(zhì)檢驗(yàn)
9.3 符號計(jì)算與模型檢驗(yàn)
9.4 符號CTL模型檢驗(yàn)
9.5 計(jì)算改進(jìn)
9.6 模型檢驗(yàn)工具的使用
9.7 本章小結(jié)
9.8 習(xí)題
參考文獻(xiàn)
縮寫詞匯表