基于多項(xiàng)式符號(hào)代數(shù)的數(shù)字電路形式驗(yàn)證方法研究.pdf

1、隨著數(shù)字集成電路設(shè)計(jì)規(guī)模的增大和功能復(fù)雜性的提高，功能驗(yàn)證已經(jīng)成為設(shè)計(jì)流程中的瓶頸。傳統(tǒng)的模擬驗(yàn)證方法無(wú)法滿(mǎn)足現(xiàn)時(shí)復(fù)雜集成電路設(shè)計(jì)帶來(lái)的巨大的驗(yàn)證需求。形式驗(yàn)證技術(shù)，例如模型檢驗(yàn)和等價(jià)驗(yàn)證，因此發(fā)展成為模擬驗(yàn)證方法的一種重要補(bǔ)充，正日益受到學(xué)術(shù)界的關(guān)注?，F(xiàn)有的形式驗(yàn)證技術(shù)大多基于傳統(tǒng)的位級(jí)方法，例如BDD或布爾SAT，它們主要針對(duì)低層次門(mén)級(jí)電路和以控制流為主的電路的驗(yàn)證，難以勝任以數(shù)據(jù)流為主的高層次復(fù)雜電路設(shè)計(jì)的驗(yàn)證。作為一種新近提出的

2、電路表示和計(jì)算方法，多項(xiàng)式符號(hào)代數(shù)能夠克服BDD和布爾SAT方法的某些不足。本文深入研究了多項(xiàng)式符號(hào)代數(shù)方法在數(shù)字電路形式驗(yàn)證中的應(yīng)用，取得了如下創(chuàng)新性成果：
　　 (1)提出了基于多項(xiàng)式符號(hào)代數(shù)的模型檢驗(yàn)方法。首先，擴(kuò)展了傳統(tǒng)的Kripke結(jié)構(gòu)的概念，得到了所謂狀態(tài)轉(zhuǎn)換系統(tǒng)的新概念。用該狀態(tài)轉(zhuǎn)換系統(tǒng)代替?zhèn)鹘y(tǒng)的Kripke結(jié)構(gòu)來(lái)抽象高層次設(shè)計(jì)中的控制邏輯，并統(tǒng)一用多項(xiàng)式方法描述高層次設(shè)計(jì)中的數(shù)據(jù)通路和控制邏輯，從而有效地避免了數(shù)

3、據(jù)域和控制域之間頻繁的約束傳播和回溯操作。進(jìn)而，給出了一個(gè)高層次設(shè)計(jì)模型檢驗(yàn)的方法框架。在該方法框架之下，原有的模型檢驗(yàn)問(wèn)題被轉(zhuǎn)化為一個(gè)假設(shè)和結(jié)論均具有多項(xiàng)式形式的一階邏輯定理證明問(wèn)題，一個(gè)基于多項(xiàng)式符號(hào)計(jì)算的判定過(guò)程被用來(lái)有效地解決該定理證明問(wèn)題。針對(duì)典型高層次設(shè)計(jì)的實(shí)驗(yàn)結(jié)果表明，與現(xiàn)有的基于非線性求解器的高層次模型檢驗(yàn)方法相比，該方法在保證驗(yàn)證準(zhǔn)確性的情況下，平均要快1到5倍。
　　 (2)提出了基于多項(xiàng)式符號(hào)代數(shù)的等價(jià)驗(yàn)證

4、方法。該方法直接在高層次建模數(shù)據(jù)通路設(shè)計(jì)，給出了高層次數(shù)據(jù)通路的多項(xiàng)式集合表示的一般形式及構(gòu)造方法。由于避免了將高層次數(shù)據(jù)通路設(shè)計(jì)展開(kāi)為門(mén)級(jí)網(wǎng)表，對(duì)于同樣的驗(yàn)證問(wèn)題，該方法涉及的信號(hào)變量的數(shù)目和約束表達(dá)式的數(shù)目要比基于BDD和布爾SAT的等價(jià)驗(yàn)證方法少得多。進(jìn)而，從多項(xiàng)式集合公共零點(diǎn)的角度定義了高層次數(shù)據(jù)通路的功能等價(jià)性，并給出了一個(gè)基于多項(xiàng)式符號(hào)計(jì)算的有效的代數(shù)求解算法。針對(duì)高層次基準(zhǔn)數(shù)據(jù)通路的實(shí)驗(yàn)結(jié)果表明，與現(xiàn)有的基于*BMD和整數(shù)

5、線性規(guī)劃的高層次等價(jià)驗(yàn)證方法相比，該方法在保證錯(cuò)誤診斷能力的情況下，平均要快1倍到1個(gè)數(shù)量級(jí)。
　　 (3)提出了基于多項(xiàng)式符號(hào)代數(shù)的層次化驗(yàn)證方法。首先，引入了一種基于廣義表數(shù)據(jù)結(jié)構(gòu)的層次化電路表示模型。基于此種層次化表示，并應(yīng)用多項(xiàng)式代數(shù)中的消元定理和擴(kuò)張定理，得到了一種層次化的電路功能計(jì)算方法。該方法將原本規(guī)模較大的計(jì)算問(wèn)題劃分為一些小的計(jì)算問(wèn)題，并以一種逐層遞歸的方式完成原有計(jì)算，從而有效地提高了計(jì)算效率。進(jìn)而，將這種新