基于布爾可滿足性的邏輯電路等價性驗證和測試生成技術(shù)研究.pdf

1、近些年在布爾可滿足性（SAT）領域取得了較大進展，一系列基于DPLL框架的優(yōu)化算法被提出，有效SAT解算器諸如zChaff等已可解決很大規(guī)模的SAT問題。SAT作為一個優(yōu)秀引擎在EDA領域已廣泛應用，本論文的主要方向就是探索如何有效地將SAT技術(shù)應用于等價性驗證和測試生成這兩類重要問題中。 下面概括本論文的主要研究方向和創(chuàng)新點： 1．基于輸出分組和電路SAT的組合等價性驗證技術(shù)。隨著芯片設計規(guī)模日益龐大復雜，功能驗證成為

2、現(xiàn)階段IC設計過程中的瓶頸環(huán)節(jié)，而傳統(tǒng)模擬技術(shù)已很難滿足現(xiàn)時集成電路設計的要求。作為模擬技術(shù)的補充，組合等價性驗證工具在IC功能驗證中使用已日益普遍。本文提出一種基于電路可滿足性和輸出分組技術(shù)的組合電路等價性驗證算法。算法首先使用與非圖結(jié)構(gòu)哈希技術(shù)來簡化驗證任務。對那些具有較多輸出的復雜電路，為共享結(jié)構(gòu)信息從而提高驗證速度，使用輸出分組技術(shù)將那些共享較多內(nèi)部結(jié)點的輸出轉(zhuǎn)化為一個子問題，從而驗證問題可轉(zhuǎn)化為一系列驗證子問題。對每一個子問題

3、，使用將電路SAT和BDD學習等技術(shù)結(jié)合的驗證算法來解決。實驗結(jié)果表明該類方法可有效用于解決大規(guī)模電路的驗證問題。 2．結(jié)合不變量提取和時序SAT的時序等價性驗證技術(shù)。應用組合等價性驗證工具的重要的限制是兩個待驗證電路的觸發(fā)器之間存在一一對應關(guān)系。然而對一個復雜設計，通常在調(diào)用綜合工具時會進行重定時等時序優(yōu)化，這些優(yōu)化容易破壞綜合前后設計觸發(fā)器間對應關(guān)系。因此，驗證這些類型設計就必須使用時序等價性驗證技術(shù)。本文提出一種時序等價性

4、驗證框架：為探索驗證任務間結(jié)構(gòu)相似性，算法使用不變量提取引擎來提前識別電路中有效不變量；為減少不變量提取時的誤判幾率，提出了時間幀擴展和動態(tài)選擇候選集兩種優(yōu)化策略，同時提出了不變量提取過程中的快速查找反例啟發(fā)式方法。對使用不變量引擎后尚未解決任務，可進一步使用完整的時序SAT引擎來解決。從對部分ISCAS89電路和工業(yè)實例的實驗結(jié)果表明，提出技術(shù)對驗證復雜時序電路提供了一種可能方案。 3．基于改進聯(lián)接電路模型的時序自動測試生成技

5、術(shù)。面向時序電路的ATPG問題是EDA領域中具有高度計算復雜性問題之一，運行傳統(tǒng)時序ATPG的觀察發(fā)現(xiàn)大部分計算開銷用于解決那些較難觀測故障。針對使用傳統(tǒng)SAT方法需要對每個故障構(gòu)建一次聯(lián)接電路的不足，本文中提出了可同時注入多個候選故障的電路模型。使用該改進模型的關(guān)鍵好處在于：（1）之前SAT求解過程中獲得的有用信息可在測試其他故障時完全重用，這樣可大大降低求解的計算開銷；（2）當SAT求解結(jié)果顯示為不可滿足時，可以斷定剩余所有故障是不

6、可測試的，因此查找那些不可測故障僅僅是SAT求解的副產(chǎn)品。此外，將不變量提取、邊界模型檢驗和時序SAT解算器結(jié)合并充分發(fā)揮各自引擎的優(yōu)點，可進一步提高時序ATPG求解的效率。實驗表明，該算法是一種有效的算法，尤其適用于測試那些常規(guī)方法無法解決的較難觀測故障。 4．支持多故障和不同故障類型的診斷測試生成技術(shù)。時序ATPG的改進聯(lián)接電路模型可擴展到診斷測試生成（DTPG）應用中，本文提出了一種基于SAT的DTPG技術(shù)。基于擴展的模型