基于SAT的數(shù)字電路形式驗證方法研究.pdf

1、隨著半導(dǎo)體工藝突飛猛進(jìn)的發(fā)展，集成電路(integrated circuit,IC)設(shè)計的復(fù)雜度呈指數(shù)增長，對IC設(shè)計起決定性作用的電子設(shè)計自動化(electronic designautomation,EDA)技術(shù)的發(fā)展相對落后，特別是驗證已經(jīng)成為整個IC設(shè)計流程的瓶頸?；贐DD的形式化驗證方法是一種自動化的方法，但只適用于中、小規(guī)模的電路，對大規(guī)模的電路則會出現(xiàn)狀態(tài)空間爆炸問題。近幾年來，對可滿足性(satisfiability,

2、SAT)問題研究的進(jìn)步使得EDA中的一些問題可以轉(zhuǎn)化為SAT問題進(jìn)行解決。但是，通用SAT求解器對求解特定領(lǐng)域的問題并不是最有效的。本文對基于SAT的數(shù)字電路的形式驗證方法和FPGA工藝映射方法進(jìn)行深入研究，利用電路結(jié)構(gòu)和問題的特有信息，對SAT求解算法進(jìn)行改進(jìn)，取得了如下創(chuàng)新性成果：
　　 1)針對基于SAT的等價驗證中，已有SAT求解算法zChaff*對電路可觀無關(guān)性信息不能有效利用的問題，提出了一種改進(jìn)的可滿足性求解算法z

3、Chaff+。首先，根據(jù)邏輯門的輸入與輸出之間的關(guān)系，引入控制唯一性概念;其次，以帶可觀無關(guān)條件的CNF理論為基礎(chǔ)，先通過在可觀無關(guān)條件計算時不使用變量排序的方法，減少可觀無關(guān)條件丟失，再通過不對只出現(xiàn)在可觀無關(guān)條件中的變量賦值的方法，來保證電路的控制唯一性。理論分析和實驗結(jié)果表明，改進(jìn)的可滿足性求解算法zChaff+在解決等價驗證問題時，搜索空間大大減小，求解速度明顯提高。
　　 2)針對基于SAT的無界模型檢驗中的前像計算問

4、題，提出改進(jìn)的所有解可滿足性求解算法All-SAT+。首先，選用zChaff+作為標(biāo)準(zhǔn)求解器，并采用出現(xiàn)在無關(guān)條件中次數(shù)多的變量優(yōu)先賦值的變量決策策略對其進(jìn)行改進(jìn)，生成盡量大的解立方體或者小的沖突子句，降低阻塞子句或沖突學(xué)習(xí)存儲空間需求，并減少算法所需的總枚舉步數(shù)；其次，采用只對狀態(tài)變量進(jìn)行l(wèi)ifting檢查的改進(jìn)算法，對每個枚舉步求得的解立方體進(jìn)一步擴(kuò)展，使每個枚舉步獲得的解立方體捕捉到更多的解；再次，用ZBDD進(jìn)行解合并壓縮和存儲；

5、最后，利用無關(guān)狀態(tài)學(xué)習(xí)約束以避免對不必要狀態(tài)空間的搜索，并采用增量式技術(shù)通過學(xué)習(xí)子句共享提高算法效率。實驗結(jié)果表明，改進(jìn)算法All-SAT+有效地降低了解的個數(shù)和前像計算的時間，比文獻(xiàn)中的lifting算法、Lipi算法在求解速度上都有顯著的提高。
　　 3)針對由隨機(jī)搜索算法和DPLL算法組成的混合SAT算法在求解電路相關(guān)問題時存在的過度滿足問題，提出了改進(jìn)的混合SAT算法HBISAT+。利用電路可觀性對混合算法進(jìn)行改進(jìn)，局部

6、算法采用改進(jìn)算法WalkSAT+，DPLL算法則采用文獻(xiàn)中的算法zChaff*；采用改進(jìn)的啟發(fā)式策略選擇填充子句，協(xié)調(diào)兩種算法，減少算法的迭代次數(shù)，提高整個算法的效率。實驗結(jié)果說明，混合算法比只使用DPLL算法在求解速度上有很大提高，而改進(jìn)算法HBISAT+的速度比原算法平均提高27％，證明利用電路可觀性改進(jìn)的混合求解算法，可以更有效的求解難解電路的等價驗證問題。
　　 4)針對基于SAT的FPGA工藝映射算法中輸入置換帶來的計