基于電路可滿足性的組合電路等價(jià)驗(yàn)證方法研究.pdf

1、隨著集成電路技術(shù)和制造技術(shù)不斷進(jìn)步，電路的規(guī)模也不斷增大，電路驗(yàn)證領(lǐng)域面臨著前所未有的挑戰(zhàn)。傳統(tǒng)的基于模擬的驗(yàn)證方法不能滿足電路復(fù)雜度增大的需要，具有完備性特點(diǎn)的形式化驗(yàn)證方法開(kāi)始得到人們的關(guān)注，成為當(dāng)前的研究熱點(diǎn)。 本文研究工作是針對(duì)組合電路的等價(jià)驗(yàn)證展開(kāi)的。由于近些年來(lái)，作為驗(yàn)證基本問(wèn)題的可滿足性問(wèn)題(SAT)研究取得了重大進(jìn)展，有效的SAT解算器諸如zChaff，BerkMin和C．SAT等已可解決很大規(guī)模SAT問(wèn)題，并且

2、作為一個(gè)優(yōu)秀搜索引擎在電路驗(yàn)證問(wèn)題方面有著廣泛應(yīng)用。本文分析了現(xiàn)有的電路可滿足性驗(yàn)證工具的優(yōu)缺點(diǎn)，針對(duì)驗(yàn)證中學(xué)習(xí)效率的瓶頸提出了改進(jìn)的方法，能夠更加合理地利用電路現(xiàn)有的信息。 本文主要的創(chuàng)新之處在于：(1)對(duì)待驗(yàn)證電路進(jìn)行與／非圖同構(gòu)簡(jiǎn)化，合并待驗(yàn)證兩電路的相似部分，以減小待驗(yàn)證電路產(chǎn)生的數(shù)據(jù)結(jié)構(gòu)規(guī)模。(2)根據(jù)電路的拓?fù)浣Y(jié)構(gòu)，合理選擇學(xué)習(xí)子句，避免重復(fù)無(wú)用的學(xué)習(xí)過(guò)程。(3)通過(guò)模擬蘊(yùn)含學(xué)習(xí)，能夠避免過(guò)深層次搜索，從而快速得到電