滿足性算法在形式化驗(yàn)證中的應(yīng)用研究及實(shí)現(xiàn).pdf

1、隨著超大規(guī)模集成電路復(fù)雜度的增加和規(guī)模的逐漸變大，驗(yàn)證電路的功能等價(jià)已經(jīng)變得越來越重要。傳統(tǒng)上，功能驗(yàn)證主要是通過模擬和測試技術(shù)實(shí)現(xiàn)。這些方法隨著設(shè)計(jì)復(fù)雜度的增加，將很難保證能找到所有的死角錯(cuò)誤。然而，形式化驗(yàn)證能夠在數(shù)學(xué)上證明具體實(shí)現(xiàn)和規(guī)范之間的一致性，而不會(huì)錯(cuò)過或忽略任何搜索空間。已受到人們的廣泛鐘愛。 由于驗(yàn)證問題的特殊性很多問題都可以轉(zhuǎn)化為布爾滿足性問題來解決，這使得布爾滿足性問題在形式化驗(yàn)證領(lǐng)域占據(jù)著重要的地位。傳統(tǒng)的

2、基于BDD技術(shù)解決這一問題方法極大的受限于BDD的瓶頸問題——空間爆炸問題，難以解決規(guī)模比較大的問題。而基于DPLL(Davis-Pumam,Logemann and Loveland)深度搜索規(guī)則的SAT算法能夠很好地避免這一問題，并且通過添加一些合理的啟發(fā)式規(guī)則和學(xué)習(xí)機(jī)制能夠快速的解決一些大規(guī)模問題。這就使得設(shè)計(jì)高效的SAT算法成了相當(dāng)有價(jià)值的研究方向，而且業(yè)界在這個(gè)方面也不斷地推成出新穎的SAT驗(yàn)證程序(例如當(dāng)前比較有影響力的SA

3、T程序包主要包括GRASP[6]，SATO[7]，BERKMIN[8]，ZCHAFF[9]等)進(jìn)行不斷地效率比試。 本文主要從模型檢驗(yàn)、符號模擬以及等價(jià)性驗(yàn)證三方面論述了布爾滿足性算法在形式化驗(yàn)證領(lǐng)域的主要應(yīng)用及相應(yīng)算法的實(shí)現(xiàn)。首先，介紹了基于DPLL規(guī)則SAT算法的基本框架及關(guān)鍵技術(shù)，以及當(dāng)前比較流行的基于SAT的有限模型驗(yàn)證和符號模擬技術(shù)。需要突出的是本文在介紹基于SAT的等價(jià)性驗(yàn)證基礎(chǔ)上，提出了一種如何使用增量式策略解決大

4、規(guī)模組合電路的驗(yàn)證算法IncrCEC(Incremental Combinational Equivalence Checking)。在此算法中，通過對組合電路進(jìn)行門級邏輯錐的劃分，解決了使用純SAT算法解決等價(jià)性問題時(shí)丟失電路共享結(jié)構(gòu)信息的問題。然后，詳細(xì)地講述了基于DPLL深度搜索規(guī)則的啟發(fā)式學(xué)習(xí)判定程序ChiveriSolver的實(shí)現(xiàn)過程。最后，通過實(shí)驗(yàn)將ChiveriSolver與zchaff效率進(jìn)行了對比，發(fā)現(xiàn)ChiveriS