數字集成電路設計驗證︰量化評估、激勵生成、形式化驗證

FOREWORD
前言
第1章 緒論
1.1 設計驗證簡介
1.2 設計驗證中的關鍵問題
1.2.1 量化評估
1.2.2 激勵生成
1.2.3 形式化驗證
1.3 章節組織結構
參考文獻
第2章 寄存器傳輸級行為描述抽象方法
2.1 硬件描述語言概述
2.1.1 硬件描述語言的產生與發展
2.1.2 硬件描述語言的描述特點
2.2 RTL行為描述的進程分析
2.2.1 語法與語義限制
2.2.2 組合進程
2.2.3 時鐘進程
2.2.4 異步進程
2.3 寄存器傳輸級行為描述抽象
2.3.1 行為描述中的進程
2.3.2 過程性語句
2.3.3 語句的語義行為
2.3.4 語句的執行條件
2.3.5 進程的相互關系
2.3.6 電路模型
2.3.7 行為模擬方式
2.4 本章總結
參考文獻
第3章 基于可觀測性的覆蓋率評估方法
第4章 缺項-設計錯誤模型
第5章 基于錯誤傳播概率的量化分析方法
第6章 模擬驗證的激勵生成概述
第7章 基于傳輸故障模型的寄存器傳輸級激勵生成
第8章 基于行為階段聚類的寄存器傳輸級激勵生成
第9章 覆蓋率驅動的寄存器傳輸級激勵生成
第10章 布爾函數與基于電路的布爾推理
第11章 基于可滿足性的增量等價性檢驗方法
第12章 驗證包含黑盒的電路設計的形式化方法
第13章 極小布爾不可滿足問題
第14章 模型檢驗在電路設計驗證中的應用研究
第15章 總結與展望
索引