基于可滿足性問(wèn)題解算器的有界模型檢驗(yàn)——子句規(guī)則和沖突分析研究.pdf

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

2、數(shù)十萬(wàn)變量規(guī)模的SAT問(wèn)題，并且作為一個(gè)優(yōu)秀的計(jì)算引擎在集成電路驗(yàn)證領(lǐng)域有著廣泛的應(yīng)用。本文分析了有界模型檢驗(yàn)在子句規(guī)則和沖突分析上的優(yōu)缺點(diǎn)，并提出了改進(jìn)的方法，能夠加速有界模型檢驗(yàn)的執(zhí)行。 本文主要的創(chuàng)新之處在于：(1)對(duì)重命名子旬規(guī)則進(jìn)行了改進(jìn)，引入了邏輯化簡(jiǎn)、處理多元運(yùn)算、合并相鄰結(jié)點(diǎn)等方法，減小了輸入到SAT解算器的問(wèn)題規(guī)模，有效的提高了有界模型檢驗(yàn)的執(zhí)行效率。(2)分析了有界模型檢驗(yàn)問(wèn)題沖突蘊(yùn)涵圖的特征，引入輔助學(xué)習(xí)子