全面的功能驗(yàn)證：完整的工業(yè)流程

譯者序
　　對(duì)本書的評(píng)論
　　原書序
　　前言
　　第1部分 驗(yàn)證簡介
　　第1章 芯片設(shè)計(jì)的驗(yàn)證5
　　1.1 功能驗(yàn)證簡介5
　　1.2 驗(yàn)證面臨的挑戰(zhàn)9
　　1.2.1 狀態(tài)空間爆炸的挑戰(zhàn)9
　　1.2.2 查找不正確行為的挑戰(zhàn)10
　　1.3 驗(yàn)證的任務(wù)和目標(biāo)12
　　1.4 驗(yàn)證的開銷15
　　1.4.1 工程開銷和對(duì)獨(dú)立驗(yàn)證團(tuán)隊(duì)的需求16
　　1.4.2 設(shè)計(jì)自動(dòng)化工具17
　　1.4.3 時(shí)間17
　　1.5 本書范疇以外的驗(yàn)證領(lǐng)域18
　　1.6 驗(yàn)證周期：一個(gè)結(jié)構(gòu)化的流程18
　　1.6.1 功能規(guī)范20
　　1.6.2 建立驗(yàn)證計(jì)劃20
　　1.6.3 開發(fā)環(huán)境20
　　1.6.4 調(diào)試硬件描述語言和環(huán)境21
　　1.6.5 回歸測(cè)試21
　　1.6.6 硬件制造22
　　1.6.7 調(diào)試流片后的硬件（系統(tǒng)測(cè)試）22
　　1.6.8 “逃逸”錯(cuò)誤分析22
　　1.6.9 常見的中斷驗(yàn)證周期的情況23
　　1.7 本章小結(jié)23
　　1.8 習(xí)題24
　　
　　第2章 驗(yàn)證流程26
　　2.1 驗(yàn)證層次26
　　2.1.1 驗(yàn)證等級(jí)26
　　2.1.2 怎樣選擇驗(yàn)證等級(jí)30
　　2.2 驗(yàn)證策略34
　　2.2.1 驅(qū)動(dòng)原理34
　　2.2.2 檢查策略37
　　2.2.3 檢查黑盒設(shè)計(jì)41
　　2.2.4 驗(yàn)證策略匯總44
　　2.2.5 通用的模擬驗(yàn)證環(huán)境46
　　2.2.6 驗(yàn)證方法學(xué)的進(jìn)展46
　　2.3 本章小結(jié)51
　　2.4 習(xí)題52
　　
　　第3章 基于模擬的驗(yàn)證基礎(chǔ)55
　　3.1 基本驗(yàn)證環(huán)境：測(cè)試平臺(tái)55
　　3.1.1 激勵(lì)模塊56
　　3.1.2 監(jiān)視器60
　　3.1.3 檢查器62
　　3.1.4 記分板62
　　3.1.5 待驗(yàn)證設(shè)計(jì)64
　　3.2 觀察點(diǎn)：黑盒、白盒和灰盒驗(yàn)證65
　　3.2.1 黑盒65
　　3.2.2 白盒65
　　3.2.3 灰盒66
　　3.3 基于斷言的驗(yàn)證概述67
　　3.3.1 斷言的重要性68
　　3.3.2 斷言表達(dá)設(shè)計(jì)意圖69
　　3.3.3 斷言的分類69
　　3.4 測(cè)試平臺(tái)和測(cè)試策略71
　　3.4.1 確定性的測(cè)試平臺(tái)72
　　3.4.2 自檢查的測(cè)試平臺(tái)73
　　3.5 本章小結(jié)76
　　3.6 習(xí)題76
　　
　　第4章 驗(yàn)證計(jì)劃78
　　4.1 功能規(guī)范78
　　4.2 驗(yàn)證計(jì)劃的演進(jìn)79
　　4.3 驗(yàn)證計(jì)劃的內(nèi)容80
　　4.3.1 驗(yàn)證層次的描述81
　　4.3.2 必需的工具81
　　4.3.3 風(fēng)險(xiǎn)和依賴82
　　4.3.4 待驗(yàn)證的功能83
　　4.3.5 細(xì)節(jié)測(cè)試及方法：環(huán)境84
　　4.3.6 覆蓋率要求88
　　4.3.7 測(cè)試用例場景：矩陣88
　　4.3.8 資源需求89
　　4.3.9 進(jìn)度細(xì)節(jié)90
　　4.4 驗(yàn)證實(shí)例：Calc191
　　4.4.1 設(shè)計(jì)描述91
　　4.4.2 為Calc1建立驗(yàn)證計(jì)劃94
　　4.4.3 Calc1設(shè)計(jì)的確定性驗(yàn)證99
　　4.5 本章小結(jié)102
　　4.6 習(xí)題103
　　
　　第2部分 基于模擬的驗(yàn)證
　　第5章 硬件描述語言和模擬引擎107
　　5.1 硬件描述語言108
　　5.1.1 硬件描述語言建模層次108
　　5.1.2 硬件描述語言在驗(yàn)證方面的應(yīng)用115
　　5.2 模擬引擎介紹119
　　5.2.1 速度與精度120
　　5.2.2 選擇正確的方法121
　　5.3 事件驅(qū)動(dòng)模擬122
　　5.3.1 層次化模型網(wǎng)絡(luò)122
　　5.3.2 隨時(shí)間變化進(jìn)行的模型評(píng)估124
　　5.3.3 模型評(píng)估中的事件驅(qū)動(dòng)控制125
　　5.3.4 實(shí)現(xiàn)一個(gè)事件驅(qū)動(dòng)的模擬引擎框架129
　　5.4 改善模擬吞吐量134
　　5.5 基于周期的模擬137
　　5.5.1 同步設(shè)計(jì)138
　　5.5.2 基于周期的模擬算法139
　　5.5.3 對(duì)基本的基于周期的模擬引擎進(jìn)行擴(kuò)展141
　　5.6 波形觀察器144
　　5.7 本章小結(jié)147
　　5.8 習(xí)題148
　　
　　第6章 創(chuàng)建環(huán)境149
　　6.1 測(cè)試平臺(tái)描述工具149
　　6.1.1 采用硬件描述語言作為測(cè)試平臺(tái)描述工具150
　　6.1.2 C/C++庫155
　　6.1.3 高級(jí)驗(yàn)證語言172
　　6.1.4 其它測(cè)試平臺(tái)描述工具180
　　6.2 驗(yàn)證覆蓋率181
　　6.2.1 概述182
　　6.2.2 功能驗(yàn)證覆蓋率與制造過程中的測(cè)試覆蓋率183
　　6.2.3 結(jié)構(gòu)覆蓋率184
　　6.2.4 功能覆蓋率186
　　6.2.5 大量覆蓋率數(shù)據(jù)的采集和管理189
　　6.2.6 正確的覆蓋率分析策略190
　　6.3 本章小結(jié)191
　　6.4 習(xí)題191
　　
　　第7章 基于模擬的測(cè)試激勵(lì)生成策略193
　　7.1 Calc2概述193
　　7.1.1 Calc2驗(yàn)證計(jì)劃196
　　7.1.2 Calc2及其測(cè)試激勵(lì)生成策略201
　　7.2 測(cè)試激勵(lì)生成策略201
　　7.2.1 測(cè)試激勵(lì)生成的類型201
　　7.2.2 激勵(lì)部件的通用算法205
　　7.2.3 在Calc2中應(yīng)用4種類型的測(cè)試激勵(lì)生成方法206
　　7.2.4 為隨機(jī)測(cè)試用例選取種子219
　　7.2.5 隨機(jī)環(huán)境中的約束求解策略221
　　7.2.6 隨機(jī)環(huán)境中的覆蓋率技術(shù)224
　　7.2.7 促進(jìn)“稀有”事件的發(fā)生226
　　7.2.8 “死鎖”和“活鎖”激勵(lì)的生成228
　　7.3 本章小結(jié)231
　　7.4 習(xí)題231
　　
　　第8章 基于模擬的驗(yàn)證中的結(jié)果檢查策略232
　　8.1 結(jié)果檢查的類型232
　　8.1.1 運(yùn)行時(shí)實(shí)時(shí)檢查與測(cè)試用例結(jié)束檢查233
　　8.1.2 預(yù)生成測(cè)試用例與實(shí)時(shí)生成測(cè)試用例238
　　8.1.3 在Calc2中應(yīng)用結(jié)果檢查策略238
　　8.2 調(diào)試247
　　8.2.1 調(diào)試過程248
　　8.2.2 不同類型的測(cè)試平臺(tái)對(duì)調(diào)試的影響258
　　8.3 本章小結(jié)259
　　8.4 習(xí)題260
　　
　　第9章 廣義的功能驗(yàn)證261
　　9.1 系統(tǒng)的復(fù)位和啟動(dòng)262
　　9.1.1 復(fù)位線初始化262
　　9.1.2 掃描初始化265
　　9.1.3 可測(cè)性和內(nèi)建自測(cè)試267
　　9.2 錯(cuò)誤和降級(jí)模式的處理270
　　9.2.1 錯(cuò)誤檢測(cè)機(jī)制的驗(yàn)證271
　　9.2.2 自修復(fù)硬件的驗(yàn)證273
　　9.3 對(duì)輔助的硬件調(diào)試機(jī)制進(jìn)行驗(yàn)證279
　　9.4 低功耗模式的驗(yàn)證282
　　9.4.1 通過關(guān)閉功能單元節(jié)省功耗283
　　9.4.2 通過周期降級(jí)節(jié)省功耗284
　　9.5 本章小結(jié)285
　　9.6 習(xí)題285
　　
　　第10章 重用策略與系統(tǒng)模擬287
　　10.1 重用策略287
　　10.1.1 重用準(zhǔn)則289
　　10.1.2 水平重用295
　　10.1.3 垂直重用296
　　10.1.4 在Calc2中應(yīng)用重用策略297
　　10.1.5 斷言重用299
　　10.2 系統(tǒng)模擬302
　　10.2.1 系統(tǒng)測(cè)試平臺(tái)302
　　10.2.2 單元的連接和交互303
　　10.2.3 可重用IP世界的驗(yàn)證挑戰(zhàn)306
　　10.3 通用邏輯模擬外的其它方法307
　　10.3.1 加速308
　　10.3.2 硬件仿真313
　　10.3.3 硬件/軟件協(xié)同驗(yàn)證313
　　10.3.4 協(xié)同仿真315
　　10.4 本章小結(jié)317
　　10.5 習(xí)題318
　　
　　第3部分 形式驗(yàn)證
　　第11章 形式驗(yàn)證簡介323
　　11.1 基礎(chǔ)知識(shí)324
　　11.1.1 設(shè)計(jì)的正確性及規(guī)范324
　　11.1.2 計(jì)算復(fù)雜性325
　　11.1.3 模擬線性擴(kuò)展的神話327
　　11.1.4 形式驗(yàn)證中的數(shù)學(xué)證明方法328
　　11.2 形式化的布爾等價(jià)性檢查329
　　11.2.1 等價(jià)性檢查在大規(guī)模集成電路設(shè)計(jì)流程中的作用330
　　11.2.2 等價(jià)性檢查工具的主要組成元素331
　　11.2.3 時(shí)序和組合布爾等價(jià)性檢查332
　　11.2.4 組合電路等價(jià)性檢查的核心算法334
　　11.2.5 現(xiàn)代等價(jià)性檢查工具的藍(lán)圖342
　　11.3 功能形式驗(yàn)證——性質(zhì)檢查344
　　11.3.1 性質(zhì)檢查與時(shí)序等價(jià)性檢查345
　　11.3.2 形式化方法完全驗(yàn)證設(shè)計(jì)的神話346
　　11.3.3 一個(gè)設(shè)計(jì)實(shí)例的性質(zhì)348
　　11.3.4 形式驗(yàn)證中待驗(yàn)證設(shè)計(jì)的驅(qū)動(dòng)351
　　11.3.5 狀態(tài)空間遍歷和時(shí)序邏輯353
　　11.3.6 功能形式驗(yàn)證工具的流程357
　　11.4 本章小結(jié)357
　　11.5 習(xí)題358
　　
　　第12章 形式驗(yàn)證的使用359
　　12.1 采用硬件描述語言庫描述性質(zhì)規(guī)范359
　　12.1.1 開放驗(yàn)證庫360
　　12.1.2 采用開放驗(yàn)證庫描述性質(zhì)365
　　12.2 性質(zhì)描述語言PSL368
　　12.2.1 概述369
　　12.2.2 PSL的布爾層370
　　12.2.3 PSL的時(shí)序?qū)?72
　　12.2.4 PSL的驗(yàn)證層375
　　12.2.5 PSL的建模層377
　　12.2.6 應(yīng)用PSL描述性質(zhì)378
　　12.2.7 高級(jí)PSL話題的討論及注意事項(xiàng)379
　　12.3 使用形式驗(yàn)證進(jìn)行性質(zhì)檢查384
　　12.3.1 模擬和形式驗(yàn)證之間的性質(zhì)復(fù)用384
　　12.3.2 模型編譯385
　　12.3.3 形式功能驗(yàn)證算法386
　　12.3.4 狀態(tài)空間爆炸問題的解決方法388
　　12.3.5 半形式驗(yàn)證391
　　12.3.6 提供形式和半形式驗(yàn)證工具的EDA供應(yīng)商392
　　12.4 本章小結(jié)392
　　12.5 習(xí)題393
　　
　　第4部分 全面的驗(yàn)證
　　第13章 完成驗(yàn)證周期397
　　13.1 回歸測(cè)試398
　　13.1.1 驗(yàn)證流程中的回歸測(cè)試398
　　13.1.2 回歸測(cè)試的質(zhì)量399
　　13.1.3 回歸測(cè)試的效率400
　　13.2 問題跟蹤403
　　13.3 流片前的準(zhǔn)備406
　　13.3.1 度量標(biāo)準(zhǔn)406
　　13.3.2 完成準(zhǔn)則410
　　13.4 “逃逸”錯(cuò)誤分析412
　　13.4.1 個(gè)體錯(cuò)誤分析412
　　13.4.2 “逃逸”錯(cuò)誤舉例418
　　13.4.3 “逃逸”錯(cuò)誤分析的趨勢(shì)422
　　13.5 本章小結(jié)423
　　13.6 習(xí)題424
　　
　　第14章 高級(jí)驗(yàn)證技術(shù)425
　　14.1 節(jié)省驗(yàn)證周期——引導(dǎo)驗(yàn)證的過程426
　　14.1.1 分離上電復(fù)位驗(yàn)證和主線驗(yàn)證426
　　14.1.2 引導(dǎo)待驗(yàn)證設(shè)計(jì)進(jìn)入高“潛誤”狀態(tài)427
　　14.1.3 調(diào)整待驗(yàn)證設(shè)計(jì)的配置以激發(fā)資源沖突的狀態(tài)430
　　14.2 高層建模概念430
　　14.2.1 高層模型的應(yīng)用430
　　14.2.2 高層建模的類型433
　　14.3 覆蓋率驅(qū)動(dòng)的測(cè)試生成436
　　14.4 本章小結(jié)439
　　14.5 習(xí)題439
　　
　　第5部分 驗(yàn)證實(shí)例研究
　　第15章 驗(yàn)證實(shí)例443
　　15.1 一個(gè)行刪除的“逃逸”錯(cuò)誤實(shí)例443
　　15.1.1 背景介紹443
　　15.1.2 驗(yàn)證環(huán)境444
　　15.1.3 “逃逸”錯(cuò)誤445
　　15.2 分支歷史表446
　　15.2.1 背景介紹446
　　15.2.2 分支歷史表的目標(biāo)及邏輯設(shè)計(jì)447
　　15.2.3 分支歷史表的驗(yàn)證450
　　15.2.4 結(jié)果458
　　15.3 網(wǎng)絡(luò)處理器458
　　15.3.1 系統(tǒng)簡介458
　　15.3.2 驗(yàn)證工作460
　　15.3.3 結(jié)果468
　　15.4 本章小結(jié)468
　　附錄驗(yàn)證術(shù)語表471
　　參考文獻(xiàn)482