基于PSA的集成電路形式驗證方法研究.pdf

1、現(xiàn)今社會已是海量信息的世界，而支持處理這些信息的最主要物質基礎是數(shù)字芯片。為了滿足日益復雜的系統(tǒng)功能需求，數(shù)字電路的設計工作遇到了前所未有的挑戰(zhàn)。在數(shù)字電路設計流程中，為確保數(shù)字電路功能的正確性與完整性，驗證工作的重要作用越來越突顯，特別是在設計過程中的早期階段，對系統(tǒng)進行正確的功能驗證對該系統(tǒng)的成功開發(fā)有著至關重要的意義。數(shù)字電路形式驗證方法由于具有抽象級別高、建模能力強的特點，特別適合數(shù)字電路設計流程中的頂層設計的功能驗證問題。目前

2、業(yè)界常用的驗證方法已經(jīng)不能完全滿足現(xiàn)代設計工作的需要，因此系統(tǒng)研究形式驗證方法有其特有的現(xiàn)實意義。本文以多項式符號代數(shù)(Polynomial Symbolic Algebra，PSA)理論為基礎，針對于數(shù)字電路，研究適合算術密集型產(chǎn)品的形式驗證方法。
　　 (1)為解決數(shù)字芯片設計中模型檢驗問題，提出基于多項式理論的定界模型檢驗方法。首先，給出基于多項式形式的電路功能的統(tǒng)一描述。為了能夠采用多項式形式描述電路功能，本文在傳統(tǒng)的電

3、路控制邏輯描述方法的基礎上，將其進一步擴展，將傳統(tǒng)方法中的原子命題轉化為多項式形式，將布爾特征函數(shù)轉化為多項式集合的形式。這樣，可以與電路數(shù)據(jù)通路部分建立統(tǒng)一的多項式描述形式。其次，通過建立高級語言的關系模型，給出了電路在高層次描述中目標性質的抽取方法，通過該方法形成待驗證性質的多項式形式描述，從而形成了待驗證性質與電路功能統(tǒng)一的多項式形式?；谝陨蟽牲c，本文將定界模型檢驗問題轉化為基于多項式理論的定理證明問題。并采用計算多項式集合良好

4、三角列的方法解決定理證明問題。與傳統(tǒng)方法相比，本文方法可在電路高級別抽象上直接進行定界模型檢驗。
　　 (2)為解決數(shù)字芯片的數(shù)據(jù)通路RTL級模型與優(yōu)化后的RTL級描述之間的等價性檢驗問題，提出基于多項式理論的等價性驗證方法。首先，證明了多項式集合零點集與數(shù)據(jù)通路等價的關系。將數(shù)據(jù)通路看作黑盒結構，只考慮輸入/輸出關系，因此，兩個數(shù)據(jù)通路功能等價，可看作對同一組輸入，兩個數(shù)據(jù)通路有相同輸出。為此，將多項式集合的解集合看作是多維空

5、間中的點，通過多項式代數(shù)簇理論，將空間的點向平面投影，從代數(shù)的角度證明了數(shù)據(jù)通路等價與多項式集合零點集的關系。其次，給出判定多項式集合零點集相等的代數(shù)方法。采用多項式理想理論處理零點集等價判定問題，并利用理想良性基的可計算性給出了具體的判定過程?；谝陨蟽牲c，本文提出驗證高級別數(shù)據(jù)通路功能等價性的求解算法。
　　 (3)為提高數(shù)字芯片的驗證速度，提出基于多項式理論的模塊化驗證方法。首先，采用模塊化的形式描述電路的結構。其次，給出

6、模塊化的電路功能計算方法。從基本門電路或電路基本部件出發(fā)，從電路模塊化的結構描述中獲得各個部件的相互約束關系，并以多項式代數(shù)中的消元與擴張原理為基礎，逐級遞歸地計算出每一個電路節(jié)點的多項式集合的消元理想的Grobner基，最終獲得電路的整體功能描述。基于以上兩點，提出基于模塊化思想的電路驗證問題的代數(shù)求解算法。
　　 基于Maple等工具建立實驗系統(tǒng)，針對上述算法進行了實驗研究。實驗結果表明，針對算術密集型電路，本文基于PSA的