超大規模集成電路中組合電路的等價驗證方法
2023-05-26 22:27:51 1
專利名稱：超大規模集成電路中組合電路的等價驗證方法
技術領域：
本發明屬於超大規模集成電路設計技術領域，具體涉及一種超大規模集成電路的組合電路的等價驗證方法。
背景技術：
隨著集成電路設計技術的不斷發展，晶片的集成度越來越高，現在單個晶片上已經能集成幾千萬個門甚至上億個門。電路設計早已擺脫純圖紙的手工設計而藉助於計算機輔助設計(CAD)。從輸入、編譯、綜合、仿真、驗證到最後的版圖生成，每個環節都由於計算機輔助設計的加入而極大地加快了設計進程。
無論設計什麼晶片，一個最基本的要求是電路功能的正確性，其次才是對其功耗、速度、面積等指標進行考核。在實際設計中，工程師可能會因為電路的某項指標(比如功耗)不夠理想而對電路的結構進行了改動，這改動必須不能影響電路的正確性。由於電路巨大的複雜性，正確性的驗證通常是由計算機來完成。原先通常採用的方法是模擬(simulation)。但是基於模擬的方法有兩個缺點1.模擬通常是針對電路的某個特性而進行的。也就是說一次模擬成功結束只能保證這次模擬所測的這項特性是滿足設計要求的，但不能保證電路在別的地方不出錯。所以，基於模擬的經驗方法是不完備(not complete)的。
2.為了達到比較高的覆蓋率，模擬所用的激勵矢量往往還需要人為的手動產生，這種人工步驟的引入使得基於模擬的方法有時十分費時。
另外一種新穎的方法——形式化的等價驗證方法在理論上是完備(complete)的，而且驗證的整個過程無需人工的參與，克服了基於模擬的方法的弊端，因此這種方法得到越來越多的關注。
對於任意的電路，其中往往包含了大量的組合電路。對於其中時序電路部分的等價驗證，通常通過分割和轉化，可以將其分為多個組合電路的等價驗證。因此，組合電路的等價驗證技術是整個電路驗證的基礎。
目前國際上解決組合電路驗證問題的方法一般分為三大類基於學習的、基於轉換的和基於替換的。基於轉換的方法，由於要加入許多額外的門，一定程度上增大了問題的規模，現在使用較少。基於學習的方法，需要在輸入網表中探索可能得到的附加條件，再利用自動測試生成(ATPG)的方法完成驗證，這種方法在取得附加條件的搜索階段比較耗時，還沒有特別出色的啟發式算法。基於替換的方法比較直觀，它試圖找出兩張網表中相同功能的部分並加以替換，在本質上是一種分劃的方法，將一個大問題分劃為許多現有算法可以解決的子問題並進行逐個解決，整個問題的規模也隨之減小。代表算法有「W.Kunz，D.K.Pradhan，and S.M.Reddy，″A novel framework for logic verification in a synthesisenvironment″，IEEE Tran.on Computer Aided Design，vol.15，no.1，Jan.1996，pp.20-32」。在以往的算法實現中，由於分劃不夠有效，此類算法的潛力沒有很好得到發揮，而本發明在這一點上有所突破。
等價驗證的子問題，通常已經被劃分至可以接受的規模，具體的解決可以通過二分決策圖(BDD，Binary Decision Diagram)的算法或可滿足性問題(SAT，Satisfiability)的算法加以解決。此時，問題解決的速度正比於該算法的效率。
發明內容
本發明的目的在於提出一種可加快驗證速度的超大規模集成電路中組合電路的等價驗證方法。
本發明提出的超大規模集成電路中組合電路的等價驗證方法，是一種基於替換的分划算法，在分劃的技術上提出了逐層遞進的劃分思想，在驗證的回溯中提出了閾值控制的回溯方法，試驗結果證明這些創新舉措的引入對於整個等價驗證的加速十分有效。具體步驟如下1、配對點的生成。首先對電路進行層次分劃(劃分子電路)，並根據電路的特徵來確定每層的深度，使劃分的層次達到可以接受的規模。一般劃分層次深度為3-12。通常，對於異或邏輯比較多的電路(比如乘法器)每層的深度可以比較小，比如取3-5；對於普通電路，每層深度取9-12比較合適。根據經驗決定了分層之後，在各層中分別用隨機產生的方法得到所需的配對點。
2、配對點入棧。即將已生成的配對點按次序放入堆棧，該次序可以由某種啟發式算法來確定，比如按照距離輸入激勵的長度進行從小至大的排序。
3、尋找支持點集。即搜索棧頂配對點的支持點集(Support)，並同時遍歷該子問題所包含的所有的點，生成對應的連接範式(CNF，Conjunctive normal form)形式的可滿足性問題。
4、可滿足性問題計算。即將該連結範式交由可滿足問題解決器(SAT Solver)進行處理，來判斷該子電路是否等價。
5、回溯。具體過程如下若配對點對應的兩點不相等，則可能會發生錯反情況(FalseNegative)。為了進一步確定兩點是否等價，需要進行回溯。這時，要根據實際問題確定一個控制是否進行回溯的閾值，若當前連接範式的大小已經超過此閾值，該子問題被判定為沒有繼續回溯的價值(繼續回溯的時間代價將十分昂貴)而放棄該配對點。否則向原始輸入方向搜索新的支持點集，即為回溯，並重複第4步。此處的閾值一般取值為500-2000。
6、替換。若配對點對應的兩點被判定為相等，則將其中一點由另一點進行替換(如圖1(a)和圖1(b)所示)。
下面就第1步基於分層分劃的配對點的隨機生成和第5步基於閾值控制的回溯方法作進一步的說明，而其餘步驟與通常基於替換的方法的步驟相同。
基於層次分劃的配對點的隨機生成對於兩個待比較的電路，首先根據電路的特徵來決定每層的深度，對於異或邏輯比較多的電路(比如乘法器)每層的深度可以比較小，比如取4；對於普通電路，每層深度取10比較合適。假設待測的兩個電路層深都為100，大小都為10000個點(即都為10000門的規模)，採用早先的全電路整體生成方法，所需要做的比較將是10000*10000＝一億次。如果先將電路分層為10層，再將各個對應層之間的點進行隨機生成後的比較，那麼只需要1000*1000*10＝一千萬次。經過這樣的處理，計算量減少了10倍。當然分層後可能會有邊界兩邊相鄰部分交叉配對的潛在機會損失，但對於整體的加速，這樣的潛在機會損失還是可以忽略的。
在每一次循環中(也就是對於分層的每一層)，都在輸入點上給出N比特長度的隨機測試激勵向量，層中的每一點都對應生成一個N比特長度長的信號響應。這裡N取值為待測電路的規模但最大不超過8000。如果待測的兩個電路中分別有一點生成的信號響應完全相等，此兩點將產生一個待測點對。
基於閾值控制的回溯方法當該子電路在當前支持點集作為激勵輸入點的情況下若兩者不相等，則可能會是因為錯反問題導致的。如圖2所示，S1，S2，T1，T2，I1，I2，I3都為圖中的點。通過檢驗，可以肯定S1＝S2，T1＝T2，如果利用此兩點作為後面驗證配對點＜O1，O2＞的支持點集，會得到在＜S1＝0，T1＝1＞的情況下該配對點不相等的情況。而事實上，＜S1＝0，T1＝1＞是不可能由原始輸入I1，I2，I3得到，這樣的矛盾稱為錯反問題。為了解決錯反問題，通常採用的方法是進行回溯，將原支持點集中的每一點的支持點集合併成新的支持點集，再次進行等價判斷，如果相等則可以保證兩點的等價，若還是不相等則繼續回溯，直到當前支持點集已經是原始輸入。
那麼有可能一對事實上不相等的配對點，經過了許多次回溯直到到達原始輸入才能判斷它們確實不等，而且每次回溯都會使得該子問題的規模變大，從而浪費大量的時間。我們提出一利基於閾值控制的回溯方法，除非該配對點是原始輸出(也就是不得不得到準確相等與否的配對點)，如果該配對點對應的連接範式的規模已經超過了某個動態的閾值，我們認為此時繼續回溯時間代價將過於昂貴而放棄繼續回溯。根據經驗，此處的閾值一般取值為500-2000即可。
圖1為替換方法示意圖。其中，圖1(a)為替換前的比較電路圖，圖1(b)為替換後的電路圖。
圖2為錯反問題示意圖。其中，圖2(a)為示例電路1，圖2(b)為示例電路2。
圖3為算法框圖。
具體實施例方式
根據本發明，超大規模集成電路中組合電路的等價驗證技術主要分為六個步驟配對點生成、配對點入棧、尋找支持點集、可滿足性問題計算、回溯過程和替換過程。根據該方法，我們設計了具體的算法程序，具體步驟如下(圖3所示)1、將整個電路按照從輸入到輸出的方向進行分層劃分。首先根據電路的特徵來決定每層的深度，對於異或邏輯比較多的電路(比如乘法器)每層的深度可以比較小，比如取4；對於普通電路，每層深度取10比較合適。
2、在當前層的範圍內，向前進行隨機模擬。在輸入點上給出N比特長度的隨機測試激勵向量，層中的每一點都對應生成一個N比特長度長的信號響應。這裡N取值為待測電路的規模但最大不超過8000。如果待測的兩個電路中分別有一點生成的信號響應完全相等，此兩點將被配為一個待測點對。如此得到相當數量的配對點對。如果層數已經到達最後要驗證的原始輸出點，則將其也生成為配對點對。
3、將配對點對以某種策略放入執行堆棧，這裡的策略可以是按照距離輸入激勵的長度進行從小至大的排序。如果遇到原始輸出組成的配對點對，則將其直接放入堆棧的底部，最後對其進行操作。
4、取出堆棧頂部的配對點對，向後搜索它的支持點集(只有已經被證明為相等且替換過的點或者是整個電路的原始輸入可以作為支持點)。如果此時堆棧中已經沒有配對點對，則再考察是否還有沒有被檢驗的配對點對，如果有，則轉回步驟2；否則表明兩個待測電路相等，驗證結束。
5、將此配對點對到其支持點集的部分構成一個米特電路(Miter)，並轉化為連接範式的可滿足性問題，交由可滿足性問題解決器進行計算。
6、如果可滿足性問題解決器得到的結果為這兩個電路相同，則判定此配對點對中的兩點功能相同，將其中一點用另一點進行替換，返回步驟4；如果可滿足性問題解決器得到的結果為兩個電路不相同，進行步驟7。
7、如果此時的支持點集就是所有原始輸入點的集合，那麼如果該配對點為原始輸出配對點，則可以判定這兩個電路不相同，驗證結束；否則返回步驟4；如果此時的支持點集不是所有原始輸入點的集合，且該配對點對應的SAT問題的大小沒有超過規定的某個閾值的情況下，進行步驟8。
8、找出原配對點的支持點集中的每個元素的支持點集，並將其合併成新的支持點集。這個步驟也稱為回溯，完成後跳至步驟5。
國際上對於組合電路的等價驗證問題有許多供測試的實例，比如ISCAS』85系列，評價的標準看運行的時間，並對不同測試實例下的運行時間作比較以評價該算法的效率。
由本發明提出的解決組合電路等價驗證的方法記為FDCEC(可在計算機上實現)，在和原先整體分劃的方法結果比較如下，這裡所比較的電路(ISCAS』85系列)是國際上組合電路等價驗證中常用測試實例
*無法計算超過512M內存使用限制本發明方法和原先非閾值控制回溯的方法比較結果如下
可以看出本發明的基於分層的分劃方法和基於閾值控制的回溯方法使得組合電路的等價驗證過程大大加速。
權利要求
1.一種超大規模集成電路中組合電路的等價驗證方法，具體步驟如下(1)配對點的生成首先對電路進行層次分劃，並根據電路的特徵來確定每層的深度，使劃分的層次達到可以接受的規模；然後在各層中分別用隨機產生的方法得到所需的配對點；(2)配對點入棧將已生成的配對點按次序放入堆棧；(3)尋找支持點集搜索棧頂配對點的支持點集，並同時遍歷該子問題所包含的所有的點，生成對應的連接範式形式的可滿足性問題；(4)可滿足性問題計算將該連結範式交由可滿足問題解決器進行處理，來判斷該子電路是否等價；(5)回溯若配對點對應的兩點不相等，則根據實際問題確定一個控制是否進行回溯的閾值，若當前連接範式的大小已經超過此閾值，則不回溯；否則，向原始輸入方向搜索新的支持點集，並重複第(4)步驟；(6)替換若配對點對應的兩點被判定為相等，則將其中一點由另一點進行替換。
2.根據權利要求1所述的等價驗證方法，其特徵在於步驟(1)中所述的層次劃分的深度為3-12。
3.根據權利要求1所述的等價驗證方法，其特徵在於步驟(2)中配對點的次序按照距離輸入激勵的長度進行從小到大的排列。
4.根據權利要求1所述的等價驗證方法，其特徵在於步驟(4)中所述的控制閾值為500-2500。
5.根據權利要求1所述的等價驗證方法，其特徵在於在每一次循環中，都在輸入點上給出N比特長度的隨機測試激勵向量，層中的每一點都生成一個N比特長度長的信號響應，N為待測電路的規模，N≤8000。
全文摘要
本發明為一種超大規模集成電路中組合電路的等價驗證方法。它是一種基於替換的分划算法。其中，提出了逐層遞進的劃分方法和閾值控制回溯的方法，具體包括配對點生成，配對點入棧尋找支持點集、可滿足性問題計算、回溯過程和替換過程。本發明使組合電路的等價驗證過程大大加速。
文檔編號H01L21/82GK1529353SQ03151468
公開日2004年9月15日 申請日期2003年9月29日 優先權日2003年9月29日
發明者李亮, 唐璞山, 李 亮 申請人:復旦大學