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

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

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