超大規模集成電路驗證的可滿足性問題的解決方法
2023-05-26 22:30:56 1
專利名稱：超大規模集成電路驗證的可滿足性問題的解決方法
技術領域：
本發明屬於超大規模集成電路技術領域，具體涉及一種超大規模集成電路驗證的可滿足性問題的解決方法。
背景技術：
超大規模集成電路發展到現在，單個晶片上已經能集成幾百萬門甚至千萬門的電路。設計這樣的電路是個十分複雜的問題，要驗證其正確性更是個十分困難的問題。大家知道做一次晶片試製要花費幾萬至幾十萬美元。如果不能驗證其100％的正確，只要有一、二個錯誤的晶片，就去進行試製，不僅造成經濟上的巨大損失，也帶來上市時間的損失。所以完成設計後的大規模集成電路晶片必須驗證其正確性，只有做到100％正確，才能進行試製性投片。目前驗證所需要的時間大約是設計時間的二倍，其難度可想而知。這裡所說的驗證是功能驗證，學術上稱之為形式驗證。即檢查設計的電路功能是否就是原來設想要實現的功能。
可滿足性(SAT)問題是形式驗證中的一個重要工具。所謂可滿足性問題是把電路用邏輯表達式(即布爾表達式)來描述。經處理後該表達式如果不滿足，電路是正確的，否則就不正確。可滿足性問題一般來說是一個NP完全問題，NP完全問題用現代計算機來計算，其計算複雜性隨著邏輯變量數的增加而成指數增加。一般幾百個邏輯變量所需的計算時間(即使使用最快的計算機)也是一個天文數字，因此無法對所有的情況進行正確性驗證。而在大規模集成電路的邏輯描述中至少要有幾萬個邏輯變量。這從一般意義上說是無法進行驗證計算的。近年來出現了某些啟發式方法，對於從實際問題轉化過來的可滿足性問題實例進行研究，確認有一定規律性，並在某些部分可作簡化處理。因而能解決相當數量的具有幾萬甚至幾十萬個邏輯變量的實際問題，為大規模集成電路的驗證打開了應用前景。
可滿足性問題的定義可以表述為，給定一個邏輯變量集合以及由這些邏輯變量或反變量構成的子句集合，問是否存在對於邏輯變量集合的一組賦值，使子句集合每個子句中至少有一個變量或反變量的值為真。若存在這樣的賦值，則稱問題可滿足，反之則問題不可滿足。目前在國際上對於解可滿足性問題的算法通常分為兩大類一類是基於深度優先搜索，另一類是基於局部查找。局部查找的算法是一種不完全算法，它只能在找到賦值後回答問題是可滿足的，而對於在規定的時間內沒有找到賦值的，並不能斷定問題的可滿足性。況且實際公布的運行結果表明，局部查找算法對於隨機問題的效果比對於實際例子的效果一般要好，因此在實際的應用特別是在電路設計領域中有一定的應用局限性。基於深度優先搜索(又稱分支回溯)的算法是當前解決可滿足性問題的主流趨勢(L.Zhang et al，「Efficient conflict driven learning in a Boolean Satisfiability solver」；F.Bacchus「EnhancingDavis Putnam with Extended Binary Clause Reasoning」；E.Goldberg et al，「A fast and robustSAT-solver」)。從最早的DP算法開始，算法能解決的問題規模越來越大，從一開始10個變量的規模到現在上萬變量的規模。單純的深度優先搜索算法從理論上來說是時間複雜性指數增長的算法，然而在實際運用中發現，實際問題轉化而來的可滿足性問題有規律性，比如子句的長度一般較短，變量在子句中的出現次數較為平均等等，這些都有利於搜索算法的應用。近年來，對於這類算法最大的改進是引入了所謂學習(learning)的技術，使搜索過程中的決策次數大大降低，提高了算法的效率。但是僅僅引入學習過程對於解決決策次數還不夠。雖然現在的算法注重於整體的運算時間，但是對於決策次數的考慮有利於對問題區分，同時也有利於如何進一步考慮提高工作效率。
發明內容
本發明的目的在於提出一種可大大減少決策次數、提高工作效率的超大規模集成電路驗證的可滿足性問題的解決方法。
本發明提出的超大規模集成電路驗證的可滿足性問題的解決方法，是以深度優先搜索算法為基礎，在其中加入了推理(Advanced Reasoning)過程，並利用推理過程，對決策的策略作相應改進，本發明可分成五個步驟，分別是①決策過程，②布爾約束的簡化過程，③回溯過程，④學習過程以及⑤推理過程。其中決策過程，即通過一種策略選取還未賦值的變量進行賦值；布爾約束的簡化就是利用已有的賦值，尋找受約束的單元子句，並對單元子句中的變量進行賦值；回溯過程就是在當前賦值遇到矛盾時(也就是出現某個子句，其所有變量的值均為假)，要改變最近賦值變量的值，從而解決矛盾，向另外的搜索空間搜索；學習過程，即當遇到矛盾時，分析之前賦過值的變量情況，在其中找到導致矛盾的一組變量，以子句的形式加入到原問題中，可以在以後的搜索中避免遇到相同的矛盾；推理過程，是指在布爾約束簡化過程完了以後，對於簡化後的問題(子問題)作進一步探索，以期望找到更多的已經可以確定的變量賦值(所謂的強制賦值的文字)，使搜索過程避免不必要的或無用的決策，從而大大降低決策次數。
下面進一步介紹推理過程、決策過程以及相關數據結構的實現方法。
推理過程
本發明採用了FLD技術(FLD即Failed Literal Detection，失敗性賦值檢查)，目的是通過對於還未賦值變量的檢測，找到那些受問題約束的強制賦值的文字，對他們進行賦值，從而在新決策之前避免不必要的探索過程。FLD最關鍵之處是如何確定待測變量集合。這個集合中包含強制賦值的文字的比例(命中率)越高，則算法的運行效率越高。由於實際可滿足性問題的多樣性，本發明提出了所謂的動態篩選的策略。也就是在每一步FLD之前動態篩去一些不可能成為強制賦值的文字的變量，縮小集合中變量的數目，從而提高FLD的運行效率。具體說來分成兩步1、收集待測變量。
只對出現在所謂的二元子句(即子句中有且僅有兩個變量未賦值)的變量進行收集，成為初始的待測變量集合。
2、篩選策略有兩種情況的篩選(1)如果待測變量x中某個相位受其它測試變量的布爾約束，則變量x的這個相位的賦值無需再測。
比如初始的待測變量為a，b，c，設其測試的順序也是abc，通常情況下必須對每個測試變量賦值0和1來測試該變量是否是強制賦值的文字，但是如果問題中存在這樣的子句(a+b)，則當測試a＝0時由子句可滿足性約束b必須為1，b＝1這個相位就受到變量a的布爾約束，因此在測完a以後，b＝1這個相位就無需再測。而在一般地實際問題中，變量之間的布爾約束是非常多的，因此利用此策略可以大大降低無用的測試過程，提高FLD的效率。
(2)如果待測變量沒有出現在新產生的二元子句中，則該變量也不在本次FLD中測試。
比如變量a在上次的FLD中測試過並且沒有成為強制賦值的文字，在本次FLD時，雖然它也出現在二元子句中，但是這些二元子句是上次FLD時已經存在的，而在新產生的二元子句中並沒有a，因此在我們的FLD篩選策略中將a篩去。
採用了有篩選的策略後，FLD的執行效率提高了。例如在例子par16-1-c(16位奇偶校驗電路)，沒有採用篩選策略時總的測試變量次數為308456，而其命中率為0.8％，採用了篩選策略後總的測試次數為105630，命中率為1.6％，不僅測試數減少了，而且命中率也提高了，因此程序的運行時間也由原來的28.1秒提高到5.4秒。又如在例子ssa2670-130中，沒有用篩選策略時總測試變量次數為306558，命中率為0.09％，採用篩選策略後，測試數為3392，命中率為2.5％，運行時間從15.8秒提高到0.12秒。充分說明了動態篩選在FLD測試中的重要性。
決策過程對於決策過程，我們發現，原有的策略雖然計算量小，但考慮的不夠「深」。原因在於原來的策略中，沒有引入推理過程，對於變量所隱含的「效果」沒能計算在內。本發明利用FLD的結果對原有的策略進行了改進。對於每一個變量作選取時，會有一個所謂選取的權值，每次決策選取權值最大的變量作為決策變量。這個權值可以靜態的也可以是動態改變的。對於每個變量，我們把原有的策略所產生的權值作為初始值，累加上受該變量布爾約束變量的權值作為該變量新的權值(稱為當前值)。決策時就選取具有最大當前值的變量作為決策變量。例如待決策的變量有a，b，c，d，其初始權值為4，10，2，8，然而對於變量c，在作FLD時發現變量b和d都受其布爾約束，因此c的當前值為10+2+8＝20。而其餘三個變量由於沒有受約束的變量，當前值就是原來的權值，因此在我們的決策過程中會選取c作為我們的決策變量。
在數據結構的實現上，根據布爾約束簡化過程和FLD過程的綜合要求，設計了2-3混合型變量監測數據結構。所謂變量監測結構，就是在每個子句中挑選沒有被賦值的變量作為子句狀態的監測變量。當被監測的變量在任何賦值過程中被賦值後，監測指針將指向子句中下一個沒有被賦值的變量。而2-3混合型結構就是指在布爾約束簡化過程中每個子句監測3個變量；在FLD過程中每個子句只監測2個變量。見
圖1所示。
從圖1中可以看到，當程序對變量x8賦值時，由於x8並不是該子句的監測變量，因此布爾約束簡化過程或FLD過程並不會訪問該子句。只有當監測變量賦值以後才訪問到該子句，使賦值運算的效率大大提高。同時，3變量監測可以確保FLD對變量收集的要求。混合型結構既保證了FLD收集變量的需要，又在最大限度上保留了賦值運算的高效性。
具體實施例方式
根據本發明，解決超大規模集成電路驗證的可滿足性問題的方法包括五個步驟決策過程、布爾約束的簡化過程、回溯過程、學習過程和推理過程。根據該方法，我們設計了相應的算法程序。具體計算步驟如下1、掃描原問題的子句，初始化所有變量的當前值；2、選擇具有最大當前值的變量作為本次的決策變量，並根據變量當前值的情況賦值。比如變量x為決策變量，而x比x』具有更高的當前值，則令x＝1，反之，令x＝0；如果在此過程中發現所有的變量已經賦值完畢，表示原問題可滿足的，輸出變量的賦值情況，退出。
3、根據決策變量的賦值，對問題中還沒有滿足的子句進行變量賦值。比如x＝1，則所有包含x的子句都滿足。所有包含x』的子句中尋找單元子句，根據布爾約束簡化這些單元子句，即對單元子句中的變量賦值。
4、如果賦值過程中出現矛盾，就直接回溯到上一次決策變量處，改變該變量的原有賦值並執行步驟3；5、根據二元子句收集候選的測試變量，根據篩選策略去除不用測試的變量。然後對每個變量作FLD測試。一旦發現強制賦值的文字，對其相反的文字作學習過程。比如x是強制賦值的文字，x』就是相反的文字，對x』學習得到一個子句，根據子句的情況回溯到相應的決策變量處，改變該變量的值並執行步驟3，否則反覆執行5直到沒有強制賦值的文字，執行7；6、如果4、5在回溯過程中發現所有的搜索空間已經搜索完畢，則表示原問題不可滿足，退出。
7、根據FLD的結果，根據決策策略中當前值計算法則更新所有變量的當前值，執行2。
上述實施步驟具體見圖2所示。
國際上對於可滿足問題算法提供了許多供測試的實例。評價的標準是看運行時間，並對不同的測試實例下的運行時間作比較以評價算法的效率。
由本發明提出的解決可滿足性問題的方法記為FD1SAT(已編製成相應算法程序)，與國外兩個先進方法比較，其中zchaff(』02)是沒有採用推理過程的程序，2cls+eq(』02)雖然採用了一定的推理過程，但沒有採用FLD技術。運用的典型算例和運行結果見下表。而且在文章「Enhancing Davis Putnam with Extended Binary Clause Reasoning」(Fahiem Bacchus)中指出FLD效率不高，我們的程序運行結果否定了這樣的結論。另外決策數比不採用推理過程的程序大大降低。
綜上，本發明的算法模型是建立在深度優先搜索的框架上，但是對其中的重要環節提出了新的算法和數據結構，特別是引入了推理過程，採用了具有動態篩選的FLD技術，使算法的運行效率大大提高。
權利要求
1.一種超大規模集成電路驗證的可滿足性問題的解決方法，以深度優先搜索算法為基礎，其特徵在於加入了推理過程，並利用推理過程對決策的策略作相應改進，具體步驟如下(1)決策過程通過一種策略選取還未賦值的變量進行賦值；(2)布爾約束的簡化過程利用已有的賦值，尋找受約束的單元子句，並對單元子句中的變量賦值；(3)回溯過程在當前賦值遇到矛盾時，改變最近賦值變量的值，從而解決矛盾，向另外的搜索空間搜索；(4)學習過程當遇到矛盾時，分析之前賦過值的變量情況，在其中找到導致矛盾的一組變量，以子句的形式加入到原問題中，可以在以後的搜索中避免遇到相同的矛盾；(5)推理過程在布爾約束簡化過程完了以後，對於簡化後的問題(子問題)作進一步探索，以期望找到更多的已經可以確定的變量賦值(所謂的強制賦值的文字)，使搜索過程避免不必要的或無用的決策，從而大大降低決策次數。
2.根據權利要求所述的解決方法，其特徵在於推理過程採用了失敗性賦值檢查(FLD)技術，通過對於還未賦值變量的檢測，找到那些受問題約束的強制賦值的文字，對它們對應的變量賦值，具體分如下兩步(1)收集待測變量只對出現在二元子句的變量進行收集，成為初始的待測變量集合；(2)篩選策略①如果待測變量x中某個相位受其它測試變量的布爾約束，則變量x的這個相位的賦值無需再測；②如果待測變量沒有出現在新產生的二元子句中，則該變量也不在本次FLD中測試。
3.根據權利要求1所述的解決方法，其特徵在於決策過程中把原有的策略所產生的權值作為初始值，累加上受該變量布爾約束變量的權值作為該變量的當前值；決策時選取具有最大當前值的變量作為決策變量。
4.根據權利要求2或3所述的解決方法，其特徵在於採用2-3混合型變量監測數據結構在每個子句中挑選沒有被賦值的變量作為子句狀態的監測變量，當被監測的變量在任何賦值過程中被賦值後，監測指針將指向子句中下一個沒有被賦值的變量，在布爾約束簡化過程中每個子句監測3個變量；在FLD過程中每個子句只監測2個變量。
全文摘要
本發明為一種解決超大規模集成電路驗證的可滿足性問題方法。它以深度優先搜索為基礎，加入了推理過程，並利用推理過程對決策的策略做了相應的改進。具體步驟包括決策過程、布爾約束的簡化過程、回溯過程、學習過程和推理過程。其數據結構採用了2－3混合型變量監測數據結構形式。本發明方法可大大降低決策次數，提高工作效率。
文檔編號H01L21/82GK1525550SQ0315103
公開日2004年9月1日 申請日期2003年9月18日 優先權日2003年9月18日
發明者丁敏, 唐璞山, 丁 敏 申請人:復旦大學