近些年在布爾可滿足性（SAT）領域取得了較大進展,一系列基于DPLL框架的優(yōu)化算法被提出,有效SAT解算器諸如zChaff等已可解決很大規(guī)模的SAT問題。SAT作為一個優(yōu)秀引擎在EDA領域已廣泛應用,本論文的主要方向就是探索如何有效地將SAT技術應用于等價性驗證和測試生成這兩類重要問題中。下面概括本論文的主要研究方向和創(chuàng)新點:1.基于輸出分組和電路SAT的組合等價性驗證技術。隨著芯片設計規(guī)模日益龐大復雜,功能驗證成為現階段IC設計過程中的瓶頸環(huán)節(jié),而傳統(tǒng)模擬技術已很難滿足現時集成電路設計的要求。作為模擬技術的補充,組合等價性驗證工具在IC功能驗證中使用已日益普遍。本文提出一種基于電路可滿足性和輸出分組技術的組合電路等價性驗證算法。算法首先使用與非圖結構哈希技術來簡化驗證任務。對那些具有較多輸出的復雜電路,為共享結構信息從而提高驗證速度,使用輸出分組技術將那些共享較多內部結點的輸出轉化為一個子問題,從而驗證問題可轉化為一系列驗證子問題。對每一個子問題,使用將電路SAT和BDD學習等技術結合的驗證算法來解決。實驗結果表明該類方法可有效用于解決大規(guī)模電路的驗證問題。2.結合不變量提取和時序S... 

【文章來源】：浙江大學浙江省 211工程院校 985工程院校 教育部直屬院校

【文章頁數】：124 頁

【學位級別】：博士

【部分圖文】：

IC設計流程中的等價性驗證

匹配時間比較結果

5832這12個電路，兩種方法算法均能在0.1秒內完成匹配，故這里只給出:1423到538584共10個測試電路的比較結果。圖4一5匹配時間比較結果圖4一5中給出文獻【571和本文算法匹配所用的CPU時間(單位為S)。圖4一6

【參考文獻】：
期刊論文
[1]基于切割法的時序電路等價驗證[J]. 黃偉,唐璞山.  復旦學報(自然科學版). 2006(01)
[2]改進的時間幀展開的時序電路等價驗證算法[J]. 丁敏,唐璞山.  計算機輔助設計與圖形學學報. 2006(01)
[3]使用輸出分組和電路可滿足性的等價性驗證算法[J]. 鄭飛君,嚴曉浪,葛海通,楊軍,盧永江.  計算機輔助設計與圖形學學報. 2005(11)
[4]基于增量可滿足性的等價性檢驗方法[J]. 李光輝,李曉維.  計算機學報. 2004(10)
[5]結合二叉判決圖和布爾可滿足性的等價性驗證算法[J]. 嚴曉浪,鄭飛君,葛海通,楊軍.  電子學報. 2004(08)



本文編號：3423592