《數字積體電路設計驗證——量化評估、激勵生成、形式化驗證》是2010年5月出版社出版的圖書，作者是劉寶莉。
基本介紹
- 書名：數字積體電路設計驗證——量化評估、激勵生成、形式化驗證
- 作者：劉寶莉
基本信息,內容簡介,目錄,
基本信息
李曉維,呂濤,李華偉,李光輝 著 | ||||
科學出版社 | 2010年5月出版 | |||
定價：58.00 | 語種：中文 | |||
標準書號：978-7-03-027609-4 | 裝幀：平裝 | |||
版本：第一版 | 開本：B5 | |||
責任編輯：劉寶莉 | 字數：518千字 | |||
讀者對象：本科以上文化程度 | 頁數：411 | |||
書類：理論專著/研究生教育 | 冊/包： | |||
編輯部： 工程技術分社 | ||||
附註： | ||||
內容簡介
本書內容涉及數字積體電路設計驗證的三個主要方面：量化評估、激勵生成和形式化驗證。主要包括暫存器傳輸級（RTL）電路建模、基於可觀測性的覆蓋率評估方法、設計錯誤模型；基於故障模型的激勵生成、基於RTL行為模型的激勵生成、覆蓋率驅動的激勵生成；基於可滿足性的等價性檢驗、包含黑盒電路的形式化驗證，以及不可滿足問題。
全書圖文並茂，闡述了作者及其科研團隊自主創新的研究成果和結論，對致力於數字積體電路設計驗證方法研究的科研人員（尤其是在讀研究生），具有較大的學術參考價值，也可用作積體電路專業的高等院校教師、研究生和高年級本科生的教學參考書。
全書圖文並茂，闡述了作者及其科研團隊自主創新的研究成果和結論，對致力於數字積體電路設計驗證方法研究的科研人員（尤其是在讀研究生），具有較大的學術參考價值，也可用作積體電路專業的高等院校教師、研究生和高年級本科生的教學參考書。
目錄
前言
第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設計中信號可觀測性的DFUDO模型
3.3 基於DFUDO模型的語句覆蓋率評估方法
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章 模擬驗證的激勵生成概述
第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設計中信號可觀測性的DFUDO模型
3.3 基於DFUDO模型的語句覆蓋率評估方法
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章 基於行為階段聚類的暫存器傳輸級激勵生成
8.1 暫存器傳輸級行為描述與有限狀態機
8.1.1 有關RTL行為描述的若干定義
8.1.2 有限狀態機
8.1.3 小結
8.2 電路的行為階段
8.2.1 階段變數
8.2.2 行為階段轉換函式
8.2.3 小結
8.3 行為階段的聚類
8.3.1 對電路狀態聚類的動機
8.3.2 基於RTL行為描述的狀態聚類:行為階段聚類
8.3.3 小結
8.4 基於聚類的激勵生成
8.4.1 故障模型
8.4.2 基於聚類的測試生成算法
8.4.3 基於聚類的ATG系統ATCLUB
8.5 實驗及分析
8.6 本章總結
參考文獻
第9章 覆蓋率驅動的暫存器傳輸級激勵生成
9.1 基於混合遺傳算法的激勵生成
9.1.1 遺傳算法的改進方法
9.1.2 RTL模型和系統實現框架
9.1.3 遺傳算法設計
9.1.4 實驗及分析
9.2 可觀測性語句覆蓋率驅動的激勵生成
9.2.1 無回溯的激勵生成方案
9.2.2 以基於可觀測性的語句覆蓋率為驅動的激勵生成過程
9.2.3 停止判斷機制
9.2.4 選擇閾值
9.2.5 實驗及分析
9.3 本章總結
參考文獻
第10章 布爾函式與基於電路的布爾推理
10.1 布爾函式
10.1.1 布爾函式的運算
10.1.2 硬體行為的模擬
10.2 二叉判決圖
10.2.1 有序二叉判決圖
10.2.2 有序二叉判決圖的運算
10.2.3 有序二叉判決圖的變數排序
10.2.4 BDD在形式化驗證中的套用
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章 基於行為階段聚類的暫存器傳輸級激勵生成
8.1 暫存器傳輸級行為描述與有限狀態機
8.1.1 有關RTL行為描述的若干定義
8.1.2 有限狀態機
8.1.3 小結
8.2 電路的行為階段
8.2.1 階段變數
8.2.2 行為階段轉換函式
8.2.3 小結
8.3 行為階段的聚類
8.3.1 對電路狀態聚類的動機
8.3.2 基於RTL行為描述的狀態聚類:行為階段聚類
8.3.3 小結
8.4 基於聚類的激勵生成
8.4.1 故障模型
8.4.2 基於聚類的測試生成算法
8.4.3 基於聚類的ATG系統ATCLUB
8.5 實驗及分析
8.6 本章總結
參考文獻
第9章 覆蓋率驅動的暫存器傳輸級激勵生成
9.1 基於混合遺傳算法的激勵生成
9.1.1 遺傳算法的改進方法
9.1.2 RTL模型和系統實現框架
9.1.3 遺傳算法設計
9.1.4 實驗及分析
9.2 可觀測性語句覆蓋率驅動的激勵生成
9.2.1 無回溯的激勵生成方案
9.2.2 以基於可觀測性的語句覆蓋率為驅動的激勵生成過程
9.2.3 停止判斷機制
9.2.4 選擇閾值
9.2.5 實驗及分析
9.3 本章總結
參考文獻
第10章 布爾函式與基於電路的布爾推理
10.1 布爾函式
10.1.1 布爾函式的運算
10.1.2 硬體行為的模擬
10.2 二叉判決圖
10.2.1 有序二叉判決圖
10.2.2 有序二叉判決圖的運算
10.2.3 有序二叉判決圖的變數排序
10.2.4 BDD在形式化驗證中的套用
10.3 布爾可滿足性
10.3.1 布爾可滿足性問題
10.3.2 布爾可滿足性問題的算法
10.3.3 SAT在基於電路的布爾推理中的套用
10.4 靜態邏輯蘊涵
10.4.1 靜態邏輯蘊涵的基本概念
10.4.2 靜態邏輯蘊涵的算法
10.4.3 靜態邏輯蘊涵的套用
10.5 本章總結
參考文獻
第11章 基於可滿足性的增量等價性檢驗方法
11.1 等價性檢驗介紹
11.1.1 研究背景及意義
11.1.2 等價性檢驗綜述
11.2 基於可滿足性的增量等價性檢驗方法
11.2.1 SAT在等價性檢驗中的套用
11.2.2 基於可滿足性的增量等價性檢驗方法
11.2.3 實驗及分析
11.3 本章總結
參考文獻
第12章 驗證包含黑盒的電路設計的形式化方法
12.1 積體電路設計中的黑盒問題
12.2 驗證包含黑盒的電路設計的常用方法
12.2.1 基於BDD的方法
12.2.2 基於SAT的方法
12.3 結合邏輯模擬與布爾可滿足性的驗證方法
12.3.1 基於量化的布爾可滿足性驗證方法
12.3.2 邏輯模擬與布爾可滿足性算法的結合
12.3.3 算法的改進
12.3.4 實驗及分析
12.4 包含黑盒的電路設計驗證方法在邏輯錯誤診斷中的套用
12.4.1 錯誤診斷方法的相關研究
12.4.2 結合邏輯模擬與布爾可滿足性的錯誤診斷方法
12.4.3 實驗及分析
12.5 本章總結
參考文獻
第13章 極小布爾不可滿足問題
13.1 引言
13.2 識別MU式的算法
13.3 提取MU子式的近似算法
13.3.1 自適應核搜尋算法
13.3.2 利用蘊涵圖的近似提取算法
13.3.3 利用蘊涵圖提取MU子式的算法誤差模擬實驗
13.3.4 AMUSE方法
13.4 提取MU子式的精確算法
13.4.1 利用線性規劃的提取算法
13.4.2 遍歷子句的算法及預先局部賦值最佳化策略
13.4.3 實驗及分析
13.5 本章總結
參考文獻
第14章 模型檢驗在電路設計驗證中的套用研究
14.1 模型檢驗簡介
14.1.1 有限狀態轉移模型
14.1.2 時態邏輯
14.1.3 模型檢驗
14.1.4 滿足時態邏輯公式狀態集合的不動點表征
14.2 符號模型檢驗中轉移關係的分組策略
14.2.1 布爾函式的支撐變數
14.2.2 二叉判決圖的結點與支撐向量
14.2.3 基於支撐向量海明距離的轉移關係分組策略
14.2.4 實驗及分析
14.3 結合ATG和SAT的無界模型檢驗前像計算方法
14.3.1 系統前像計算方法及動機
14.3.2 ATG過程減少狀態變數上的賦值
14.3.3 實驗及分析
14.4 基於SAT的電路屬性檢驗
14.4.1 RTL設計到CNF的轉化
14.4.2 針對電路的SAT求解器最佳化
14.4.3 多時幀搜尋策略
14.4.4 實驗及分析
14.5 本章總結
參考文獻
第15章 總結與展望
15.1 總結
15.2 展望
參考文獻
索引
10.3.1 布爾可滿足性問題
10.3.2 布爾可滿足性問題的算法
10.3.3 SAT在基於電路的布爾推理中的套用
10.4 靜態邏輯蘊涵
10.4.1 靜態邏輯蘊涵的基本概念
10.4.2 靜態邏輯蘊涵的算法
10.4.3 靜態邏輯蘊涵的套用
10.5 本章總結
參考文獻
第11章 基於可滿足性的增量等價性檢驗方法
11.1 等價性檢驗介紹
11.1.1 研究背景及意義
11.1.2 等價性檢驗綜述
11.2 基於可滿足性的增量等價性檢驗方法
11.2.1 SAT在等價性檢驗中的套用
11.2.2 基於可滿足性的增量等價性檢驗方法
11.2.3 實驗及分析
11.3 本章總結
參考文獻
第12章 驗證包含黑盒的電路設計的形式化方法
12.1 積體電路設計中的黑盒問題
12.2 驗證包含黑盒的電路設計的常用方法
12.2.1 基於BDD的方法
12.2.2 基於SAT的方法
12.3 結合邏輯模擬與布爾可滿足性的驗證方法
12.3.1 基於量化的布爾可滿足性驗證方法
12.3.2 邏輯模擬與布爾可滿足性算法的結合
12.3.3 算法的改進
12.3.4 實驗及分析
12.4 包含黑盒的電路設計驗證方法在邏輯錯誤診斷中的套用
12.4.1 錯誤診斷方法的相關研究
12.4.2 結合邏輯模擬與布爾可滿足性的錯誤診斷方法
12.4.3 實驗及分析
12.5 本章總結
參考文獻
第13章 極小布爾不可滿足問題
13.1 引言
13.2 識別MU式的算法
13.3 提取MU子式的近似算法
13.3.1 自適應核搜尋算法
13.3.2 利用蘊涵圖的近似提取算法
13.3.3 利用蘊涵圖提取MU子式的算法誤差模擬實驗
13.3.4 AMUSE方法
13.4 提取MU子式的精確算法
13.4.1 利用線性規劃的提取算法
13.4.2 遍歷子句的算法及預先局部賦值最佳化策略
13.4.3 實驗及分析
13.5 本章總結
參考文獻
第14章 模型檢驗在電路設計驗證中的套用研究
14.1 模型檢驗簡介
14.1.1 有限狀態轉移模型
14.1.2 時態邏輯
14.1.3 模型檢驗
14.1.4 滿足時態邏輯公式狀態集合的不動點表征
14.2 符號模型檢驗中轉移關係的分組策略
14.2.1 布爾函式的支撐變數
14.2.2 二叉判決圖的結點與支撐向量
14.2.3 基於支撐向量海明距離的轉移關係分組策略
14.2.4 實驗及分析
14.3 結合ATG和SAT的無界模型檢驗前像計算方法
14.3.1 系統前像計算方法及動機
14.3.2 ATG過程減少狀態變數上的賦值
14.3.3 實驗及分析
14.4 基於SAT的電路屬性檢驗
14.4.1 RTL設計到CNF的轉化
14.4.2 針對電路的SAT求解器最佳化
14.4.3 多時幀搜尋策略
14.4.4 實驗及分析
14.5 本章總結
參考文獻
第15章 總結與展望
15.1 總結
15.2 展望
參考文獻
索引
