基于PSA的集成電路形式驗(yàn)證方法研究.pdf

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

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

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

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

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

6、模塊化的電路功能計(jì)算方法。從基本門電路或電路基本部件出發(fā)，從電路模塊化的結(jié)構(gòu)描述中獲得各個(gè)部件的相互約束關(guān)系，并以多項(xiàng)式代數(shù)中的消元與擴(kuò)張?jiān)頌榛A(chǔ)，逐級遞歸地計(jì)算出每一個(gè)電路節(jié)點(diǎn)的多項(xiàng)式集合的消元理想的Grobner基，最終獲得電路的整體功能描述?；谝陨蟽牲c(diǎn)，提出基于模塊化思想的電路驗(yàn)證問題的代數(shù)求解算法。
　　 基于Maple等工具建立實(shí)驗(yàn)系統(tǒng)，針對上述算法進(jìn)行了實(shí)驗(yàn)研究。實(shí)驗(yàn)結(jié)果表明，針對算術(shù)密集型電路，本文基于PSA的