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

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

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

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

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

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

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