數字積體電路設計驗證

《數字積體電路設計驗證》是2010年科學出版社出版的圖書，作者是李曉維。本書闡述了作者及其科研團隊自主創新的研究成果和結論，對致力於數字積體電路設計驗證方法研究的科研人員提供教學參考書。

基本介紹

• 書名：數字積體電路設計驗證
• 作者：李曉維
• ISBN：9787030276094
• 定價：58.00元
• 出版社：科學出版社
• 出版時間：2010年5月1日
• 開本：16開

內容簡介

《數字積體電路設計驗證:量化評估、激勵生成、形式化驗證》內容涉及數字積體電路設計驗證的三個主要方面：量化評估、激勵生成和形式化驗證。主要包括暫存器傳輸級(RTL)電路建模、基於可觀測性的覆蓋率評估方法、設計錯誤模型；基於故障模型的激勵生成、基於RTL行為模型的激勵生成、覆蓋率驅動的激勵生成；基於可滿足性的等價性檢驗、包含黑盒電路的形式化驗證，以及不可滿足問題。

全書圖文並茂，闡述了作者及其科研團隊自主創新的研究成果和結論，對致力於數字積體電路設計驗證方法研究的科研人員(尤其是在讀研究生)，具有較大的學術參考價值，也可用作積體電路專業的高等院校教師、研究生和高年級本科生的教學參考書。

圖書目錄

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章 基於可觀測性的覆蓋率評估方法

3.1 設計驗證中的可觀測性

3.1.1 研究設計驗證中的可觀測性的意義

3.1.2 設計驗證中的可觀測性相關研究

3.2 可觀測性的DFUDO模型

3.2.1 工作基礎

3.2.2 動態參數化引用一定值鏈

3.2.3 HDL設計中信號可觀測性的DFUD0模型

3.3 基於DFUD0模型的語句覆蓋率評估方法

3.3.1 基於DFUDO模型的語句覆蓋率（OSC）的定義

3.3.2 覆蓋率評估算法

3.3.3 實驗及分析

3.4 基於DFUDO模型的分支覆蓋率評估方法

3.4.1 基於DFUDO模型的分支覆蓋率（OBC）的定義

3.4.2 最佳化的覆蓋率評估算法

3.4.3 實驗及分析

3.5 兩種基於DFUDO模型的代碼覆蓋率評估方法的比較

3.5.1 OSC與OBC的共性

3.5.2 OSC與OBC的差異比較

3.6 可觀測性的COC模型

3.6.1 增強型進程控制樹與數據流向圖

3.6.2 控制－觀測鏈

3.6.3 基於COC模型的可觀測性的定義

3.7 基於COC模型的語句覆蓋率評估方法

3.7.1 實現框架

3.7.2 電路的行為模擬

3.7.3 可觀測性分析過程

3.7.4 基於COC模型的語句覆蓋率的計算

3.7.5 實驗及分析

3.8 本章總結

參考文獻

第4章 缺項－設計錯誤模型

4.1 設計錯誤模型介紹

4.2 實際晶片的設計驗證

4.2.1 設計簡介

4.2.2 接口邏輯的設計驗證

4.2.3 處理器邏輯的設計驗證

4.3 缺項－設計錯誤模型

4.3.1 設計錯誤數據的分析

4.3.2 缺項錯誤模型

4.3.3 缺項錯誤模型的測試方法

4.3.4 實驗及分析

4.4 設計錯誤的注入

4.4.1 軟體的變異測試系統Mothra

4.4.2 基於Mothra的硬體設計變異測試系統

4.4.3 獨立的硬體設計錯誤注入系統ErrorInjector

4.5 本章總結

參考文獻

第5章 基於錯誤傳播機率的量化分析方法

5.1 在量化評估方法中考慮錯誤效果的意義

5.2 RTL操作的錯誤禁止機率分析

5.2.1 一元操作的EMP分析

5.2.2 二元操作的EMP分析

5.2.3 常見字操作的錯誤禁止機率

5.3 基於錯誤禁止機率的靜態可觀測性量化分析方法

5.3.1 研究靜態可觀測性分析方法的動機

5.3.2 HDL設計中內部信號的靜態可觀測性分析方法

5.3.3 根據低觀測根源選擇內部觀測點的方法

5.3.4 實驗及分析

5.4 本章總結

參考文獻

第6章 模擬驗證的激勵生成概述

6.1 簡介

6.2 遺傳算法用於激勵生成

6.2.1 遺傳算法的起源和發展

6.2.2 遺傳算法的基本結構

6.2.3 遺傳算法的技術要點

6.2.4 基於模擬的激勵生成與遺傳算法

6.2.5 ARTIST系統

6.3 確定性激勵生成

6.3.1 基於故障模型的測試生成

6.3.2 基於錯誤模型的激勵生成

6.4 本章總結

參考文獻

第7章 基於傳輸故障模型的暫存器傳輸級激勵生成

7.1 行為傾向驅動引擎

7.1.1 電路行為的表征與展現

7.1.2 函式或映射的屬性

7.1.3 抽象的行為值與RTL變數的行為

7.1.4 行為傾向

7.1.5 驅動引擎

7.2 傳輸故障模型

7.2.1 電路故障的層次化抽象模型

7.2.2 傳輸故障的定義與組織

7.2.3 傳輸故障與邏輯故障的對應關係

7.3 無回溯激勵生成及算法實現

7.3.1 無回溯激勵生成

7.3.2 基於行為傾向驅動引擎構造無回溯測試生成算法

7.3.3 簡單實例分析

7.3.4 算法特徵小結

7.4 實驗及分析

7.4.1 擬定的實驗方案

7.4.2 系統實現方式

7.4.3 實驗結果比較分析

7.5 本章總結

參考文獻

……

第8章 基於行為階段聚類的暫存器傳輸級激勵生成

第9章 覆蓋率驅動的暫存器傳輸級激勵生成

第10章 布爾函式與基於電路的布爾推理

第11章 基於可滿足性的增量等價性檢驗方法

第12章 驗證包含黑盒的電路設計的形式化方法

第13章 極小布爾不可滿足問題

第14章 模型檢驗在電路設計驗證中的套用研究

第15章 總結與展望

索引