數字積體電路設計驗證：量化評估、激勵生成、形式化驗證

內容簡介

主要包括暫存器傳輸級（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設計中信號可觀測性的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模型的可觀測性的定義

數字積體電路設計驗證：量化評估、激勵生成、形式化驗證

基本介紹

內容簡介

圖書目錄

相關詞條

熱門詞條