數字集成電路設計驗證

前言

　　實現(xiàn)所期望的功能特性是集成電路設計需要滿足的最基本要求，功能驗證是集成電路設計驗證的基礎技術，是集成電路設計的關鍵技術之一，是確保集成電路功能正確性的主要技術手段?！　”緯侨嬲撌鰯底旨呻娐吩O計驗證方法的學術著作，匯集了自2000年以來中國科學院計算研究所（以下簡稱中科院計算所）在數字集成電路設計驗證方法學研究中取得的自主創(chuàng)新的重要研究成果和結論。內容涉及數字集成電路設計驗證的三個重要方面：量化評估、激勵生成和形式化驗證。　　全書共15章，其中技術內容可分為三大部分。第一部分（第2～5章）量化評估，從可觀測性信息和發(fā)現(xiàn)設計錯誤的能力兩個角度，論述數字集成電路設計驗證的量化評估方法。第二部分（第6～9章）激勵生成，針對寄存器傳輸級的激勵生成問題，從故障模型和覆蓋率導向兩個角度，論述確定性和非確定性的激勵生成方法。第三部分（第10～14章）形式化驗證，從提高處理速度的角度，論述形式化驗證中的等價性檢驗方法和模型檢驗方法。　　本書的主要技術內容匯集了李曉維研究員從2001年以來指導的博士生（李光輝、呂濤、魯巍、邵明等）和碩士生（劉領一、趙陽、王天成等）的學位論文工作的部分成果；也包括李華偉和尹志剛的博士學位論文的部分成果。這些研究成果部分已經在本領域相關學術刊物和學術會議上發(fā)表。本書由李曉維研究員主持撰寫，呂濤博士參與了第3～5章內容的整理；李華偉研究員參與了第2、6～9章內容的整理；李光輝教授參與了第10～14章內容的整理。清華大學計算機系邊計年教授審閱了全部書稿，美國LJCSB計算機系主任鄭光廷教授撰寫了序言。在此表示衷心的感謝。　　本書匯集的部分科研成果是在國家重點基礎研究計劃（973）課題“高性能處理芯片的設計驗證與測試”（2005CB321605）、國家自然科學基金重點項目“數字VLSI電路測試技術研究”（60633060）和“從行為級到版圖級的設計驗證與測試生成”（90207002）等資助下完成的。研究過程中得到了中科院計算所李國杰院士、閔應驊研究員、胡偉武研究員、李忠誠研究員等領導和同事的關心和支持，得到了清華大學邊計年教授、復旦大學唐璞山教授、浙江大學嚴曉浪教授、西安郵電大學韓俊剛教授等同行的支持和幫助，在此表示衷心的感謝?！　∮捎谧髡咚胶徒涷炗邢蓿瑫须y免存在不足之處，懇請讀者批評指正。

內容概要

　　《數字集成電路設計驗證：量化評估、激勵生成、形式化驗證》內容涉及數字集成電路設計驗證的三個主要方面：量化評估、激勵生成和形式化驗證。主要包括寄存器傳輸級（RTL）電路建模、基于可觀測性的覆蓋率評估方法、設計錯誤模型；基于故障模型的激勵生成、基于RTL行為模型的激勵生成、覆蓋率驅動的激勵生成；基于可滿足性的等價性檢驗、包含黑盒電路的形式化驗證，以及不可滿足問題?！　∪珪鴪D文并茂，闡述了作者及其科研團隊自主創(chuàng)新的研究成果和結論，對致力于數字集成電路設計驗證方法研究的科研人員（尤其是在讀研究生），具有較大的學術參考價值，也可用作集成電路專業(yè)的高等院校教師、研究生和高年級本科生的教學參考書。

書籍目錄

FOREWORD前言第1章 緒論1.1 設計驗證簡介1.2 設計驗證中的關鍵問題1.2.1 量化評估1.2.2 激勵生成1.2.3 形式化驗證1.3 章節(jié)組織結構參考文獻第2章 寄存器傳輸級行為描述抽象方法2.1 硬件描述語言概述2.1.1 硬件描述語言的產生與發(fā)展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 語句的執(zhí)行條件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 動態(tài)參數化引用一定值鏈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 優(yōu)化的覆蓋率評估算法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 實現(xiàn)框架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 軟件的變異測試系統(tǒng)Mothra4.4.2 基于Mothra的硬件設計變異測試系統(tǒng)4.4.3 獨立的硬件設計錯誤注入系統(tǒng)ErrorInjector4.5 本章總結參考文獻第5章 基于錯誤傳播概率的量化分析方法5.1 在量化評估方法中考慮錯誤效果的意義5.2 RTL操作的錯誤屏蔽概率分析5.2.1 一元操作的EMP分析5.2.2 二元操作的EMP分析5.2.3 常見字操作的錯誤屏蔽概率5.3 基于錯誤屏蔽概率的靜態(tài)可觀測性量化分析方法5.3.1 研究靜態(tài)可觀測性分析方法的動機5.3.2 HDL設計中內部信號的靜態(tài)可觀測性分析方法5.3.3 根據低觀測根源選擇內部觀測點的方法5.3.4 實驗及分析5.4 本章總結參考文獻第6章 模擬驗證的激勵生成概述6.1 簡介6.2 遺傳算法用于激勵生成6.2.1 遺傳算法的起源和發(fā)展6.2.2 遺傳算法的基本結構6.2.3 遺傳算法的技術要點6.2.4 基于模擬的激勵生成與遺傳算法6.2.5 ARTIST系統(tǒng)6.3 確定性激勵生成6.3.1 基于故障模型的測試生成6.3.2 基于錯誤模型的激勵生成6.4 本章總結參考文獻第7章 基于傳輸故障模型的寄存器傳輸級激勵生成7.1 行為傾向驅動引擎7.1.1 電路行為的表征與展現(xiàn)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 無回溯激勵生成及算法實現(xiàn)7.3.1 無回溯激勵生成7.3.2 基于行為傾向驅動引擎構造無回溯測試生成算法7.3.3 簡單實例分析7.3.4 算法特征小結7.4 實驗及分析7.4.1 擬定的實驗方案7.4.2 系統(tǒng)實現(xiàn)方式7.4.3 實驗結果比較分析7.5 本章總結參考文獻……第8章 基于行為階段聚類的寄存器傳輸級激勵生成第9章 覆蓋率驅動的寄存器傳輸級激勵生成第10章 布爾函數與基于電路的布爾推理第11章 基于可滿足性的增量等價性檢驗方法第12章 驗證包含黑盒的電路設計的形式化方法第13章 極小布爾不可滿足問題第14章 模型檢驗在電路設計驗證中的應用研究第15章 總結與展望索引

章節(jié)摘錄

　　第6章介紹了寄存器傳輸級的激勵自動生成方法的研究現(xiàn)狀，主要包括：將遺傳算法用于激勵生成的非確定性方法，以及基于故障模型／錯誤模型的確定性激勵生成方法。　　第7章研究了基于故障模型的寄存器傳輸級激勵生成方法。設計了行為傾向驅動引擎用于展現(xiàn)電路的行為，建立了一種新的故障模型——傳輸故障模型，基于行為傾向驅動引擎構造了傳輸故障的無回溯測試生成算法，實現(xiàn)了X_Pulling和TiDE兩個測試生成系統(tǒng)，并進行了相關實驗和數據分析?！　〉?章研究了從寄存器傳輸級行為描述出發(fā)，如何生成測試序列來檢測有限狀態(tài)機的狀態(tài)轉移關系。提出了有限狀態(tài)機的行為階段聚類描述，該描述可通過從寄存器傳輸級行為描述抽取狀態(tài)信息得到。建立了一種新的行為級故障模型——行為階段轉換故障模型，進一步提出了一種基于聚類的測試生成算法。實現(xiàn)了基于行為階段聚類的寄存器傳輸級自動測試生成系統(tǒng)ATCLUB，并進行了相關實驗和數據分析?！　〉?章研究了以有效的覆蓋率為導向的非確定性的激勵生成方法。介紹了兩種方法：第一種，采用設計驗證常用的覆蓋率評估準則，附加第7章提出的傳輸故障模型的覆蓋準則，設計了混合遺傳算法來進行激勵生成；第二種，針對第3章所提出的可觀測性覆蓋準則COC模型，使用第7章提出的請求一響應策略進行無回溯的激勵生成。對這兩種方法分別進行了相關實驗和數據分析。　　第三部分（第10～14章）介紹形式化驗證方法。形式化驗證方法使用嚴格的數學推理來證明設計滿足規(guī)范的部分或全部屬性，引起了學術界和產業(yè)界的廣泛關注。然而，形式化方法仍然受限于處理規(guī)模和運行時間，難以廣泛應用于實際設計。針對這一問題，本書的工作重點探討了增量等價性檢驗算法、包含黑盒的電路的設計驗證方法、極小布爾不可滿足子式的提取算法，以及針對電路設計的模型檢驗方法等?！　〉?0章介紹基于電路的布爾推理常用方法。簡介布爾函數的基本運算與數字硬件行為的建模方法。介紹布爾函數的規(guī)范表示方法——有序二叉判決圖的概念、運算、變量排序方法，并討論了BDD引擎在形式化驗證中的應用。介紹布爾可滿足性問題及其判定方法，并討論了基于SAT的測試產生方法、等價性檢驗方法和有界模型檢驗方法。最后討論靜態(tài)邏輯蘊涵的算法與應用。第10章的內容為后面的章節(jié)研究形式化驗證方法奠定了基礎。

編輯推薦

　　本書是全面論述數字集成電路設計驗證方法的學術著作，匯集了自2000年以來中國科學院計算研究所（以下簡稱中科院計算所）在數字集成電路設計驗證方法學研究中取得的自主創(chuàng)新的重要研究成果和結論。內容涉及數字集成電路設計驗證的三個重要方面：量化評估、激勵生成和形式化驗證?！　∪珪?5章，其中技術內容可分為三大部分。第一部分（第2～5章）量化評估，從可觀測性信息和發(fā)現(xiàn)設計錯誤的能力兩個角度，論述數字集成電路設計驗證的量化評估方法。第二部分（第6～9章）激勵生成，針對寄存器傳輸級的激勵生成問題，從故障模型和覆蓋率導向兩個角度，論述確定性和非確定性的激勵生成方法。第三部分（第10～14章）形式化驗證，從提高處理速度的角度，論述形式化驗證中的等價性檢驗方法和模型檢驗方法。

圖書封面

圖書標簽Tags

無

評論、評分、閱讀與下載

---

    數字集成電路設計驗證 PDF格式下載

---