數(shù)字集成電路設(shè)計(jì)驗(yàn)證

前言

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

內(nèi)容概要

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

書籍目錄

FOREWORD前言第1章 緒論1.1 設(shè)計(jì)驗(yàn)證簡介1.2 設(shè)計(jì)驗(yàn)證中的關(guān)鍵問題1.2.1 量化評(píng)估1.2.2 激勵(lì)生成1.2.3 形式化驗(yàn)證1.3 章節(jié)組織結(jié)構(gòu)參考文獻(xiàn)第2章 寄存器傳輸級(jí)行為描述抽象方法2.1 硬件描述語言概述2.1.1 硬件描述語言的產(chǎn)生與發(fā)展2.1.2 硬件描述語言的描述特點(diǎn)2.2 RTL行為描述的進(jìn)程分析2.2.1 語法與語義限制2.2.2 組合進(jìn)程2.2.3 時(shí)鐘進(jìn)程2.2.4 異步進(jìn)程2.3 寄存器傳輸級(jí)行為描述抽象2.3.1 行為描述中的進(jìn)程2.3.2 過程性語句2.3.3 語句的語義行為2.3.4 語句的執(zhí)行條件2.3.5 進(jìn)程的相互關(guān)系2.3.6 電路模型2.3.7 行為模擬方式2.4 本章總結(jié)參考文獻(xiàn)第3章 基于可觀測性的覆蓋率評(píng)估方法3.1 設(shè)計(jì)驗(yàn)證中的可觀測性3.1.1 研究設(shè)計(jì)驗(yàn)證中的可觀測性的意義3.1.2 設(shè)計(jì)驗(yàn)證中的可觀測性相關(guān)研究3.2 可觀測性的DFUDO模型3.2.1 工作基礎(chǔ)3.2.2 動(dòng)態(tài)參數(shù)化引用一定值鏈3.2.3 HDL設(shè)計(jì)中信號(hào)可觀測性的DFUD0模型3.3 基于DFUD0模型的語句覆蓋率評(píng)估方法3.3.1 基于DFUDO模型的語句覆蓋率（OSC）的定義3.3.2 覆蓋率評(píng)估算法3.3.3 實(shí)驗(yàn)及分析3.4 基于DFUDO模型的分支覆蓋率評(píng)估方法3.4.1 基于DFUDO模型的分支覆蓋率（OBC）的定義3.4.2 優(yōu)化的覆蓋率評(píng)估算法3.4.3 實(shí)驗(yàn)及分析3.5 兩種基于DFUDO模型的代碼覆蓋率評(píng)估方法的比較3.5.1 OSC與OBC的共性3.5.2 OSC與OBC的差異比較3.6 可觀測性的COC模型3.6.1 增強(qiáng)型進(jìn)程控制樹與數(shù)據(jù)流向圖3.6.2 控制－觀測鏈3.6.3 基于COC模型的可觀測性的定義3.7 基于COC模型的語句覆蓋率評(píng)估方法3.7.1 實(shí)現(xiàn)框架3.7.2 電路的行為模擬3.7.3 可觀測性分析過程3.7.4 基于COC模型的語句覆蓋率的計(jì)算3.7.5 實(shí)驗(yàn)及分析3.8 本章總結(jié)參考文獻(xiàn)第4章 缺項(xiàng)－設(shè)計(jì)錯(cuò)誤模型4.1 設(shè)計(jì)錯(cuò)誤模型介紹4.2 實(shí)際芯片的設(shè)計(jì)驗(yàn)證4.2.1 設(shè)計(jì)簡介4.2.2 接口邏輯的設(shè)計(jì)驗(yàn)證4.2.3 處理器邏輯的設(shè)計(jì)驗(yàn)證4.3 缺項(xiàng)－設(shè)計(jì)錯(cuò)誤模型4.3.1 設(shè)計(jì)錯(cuò)誤數(shù)據(jù)的分析4.3.2 缺項(xiàng)錯(cuò)誤模型4.3.3 缺項(xiàng)錯(cuò)誤模型的測試方法4.3.4 實(shí)驗(yàn)及分析4.4 設(shè)計(jì)錯(cuò)誤的注入4.4.1 軟件的變異測試系統(tǒng)Mothra4.4.2 基于Mothra的硬件設(shè)計(jì)變異測試系統(tǒng)4.4.3 獨(dú)立的硬件設(shè)計(jì)錯(cuò)誤注入系統(tǒng)ErrorInjector4.5 本章總結(jié)參考文獻(xiàn)第5章 基于錯(cuò)誤傳播概率的量化分析方法5.1 在量化評(píng)估方法中考慮錯(cuò)誤效果的意義5.2 RTL操作的錯(cuò)誤屏蔽概率分析5.2.1 一元操作的EMP分析5.2.2 二元操作的EMP分析5.2.3 常見字操作的錯(cuò)誤屏蔽概率5.3 基于錯(cuò)誤屏蔽概率的靜態(tài)可觀測性量化分析方法5.3.1 研究靜態(tài)可觀測性分析方法的動(dòng)機(jī)5.3.2 HDL設(shè)計(jì)中內(nèi)部信號(hào)的靜態(tài)可觀測性分析方法5.3.3 根據(jù)低觀測根源選擇內(nèi)部觀測點(diǎn)的方法5.3.4 實(shí)驗(yàn)及分析5.4 本章總結(jié)參考文獻(xiàn)第6章 模擬驗(yàn)證的激勵(lì)生成概述6.1 簡介6.2 遺傳算法用于激勵(lì)生成6.2.1 遺傳算法的起源和發(fā)展6.2.2 遺傳算法的基本結(jié)構(gòu)6.2.3 遺傳算法的技術(shù)要點(diǎn)6.2.4 基于模擬的激勵(lì)生成與遺傳算法6.2.5 ARTIST系統(tǒng)6.3 確定性激勵(lì)生成6.3.1 基于故障模型的測試生成6.3.2 基于錯(cuò)誤模型的激勵(lì)生成6.4 本章總結(jié)參考文獻(xiàn)第7章 基于傳輸故障模型的寄存器傳輸級(jí)激勵(lì)生成7.1 行為傾向驅(qū)動(dòng)引擎7.1.1 電路行為的表征與展現(xiàn)7.1.2 函數(shù)或映射的屬性7.1.3 抽象的行為值與RTL變量的行為7.1.4 行為傾向7.1.5 驅(qū)動(dòng)引擎7.2 傳輸故障模型7.2.1 電路故障的層次化抽象模型7.2.2 傳輸故障的定義與組織7.2.3 傳輸故障與邏輯故障的對(duì)應(yīng)關(guān)系7.3 無回溯激勵(lì)生成及算法實(shí)現(xiàn)7.3.1 無回溯激勵(lì)生成7.3.2 基于行為傾向驅(qū)動(dòng)引擎構(gòu)造無回溯測試生成算法7.3.3 簡單實(shí)例分析7.3.4 算法特征小結(jié)7.4 實(shí)驗(yàn)及分析7.4.1 擬定的實(shí)驗(yàn)方案7.4.2 系統(tǒng)實(shí)現(xiàn)方式7.4.3 實(shí)驗(yàn)結(jié)果比較分析7.5 本章總結(jié)參考文獻(xiàn)……第8章 基于行為階段聚類的寄存器傳輸級(jí)激勵(lì)生成第9章 覆蓋率驅(qū)動(dòng)的寄存器傳輸級(jí)激勵(lì)生成第10章 布爾函數(shù)與基于電路的布爾推理第11章 基于可滿足性的增量等價(jià)性檢驗(yàn)方法第12章 驗(yàn)證包含黑盒的電路設(shè)計(jì)的形式化方法第13章 極小布爾不可滿足問題第14章 模型檢驗(yàn)在電路設(shè)計(jì)驗(yàn)證中的應(yīng)用研究第15章 總結(jié)與展望索引

章節(jié)摘錄

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

編輯推薦

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

圖書封面

圖書標(biāo)簽Tags

無

評(píng)論、評(píng)分、閱讀與下載

---

    數(shù)字集成電路設(shè)計(jì)驗(yàn)證 PDF格式下載

---