基于多項(xiàng)式模型的高層次形式化驗(yàn)證.pdf

1、當(dāng)今微電子學(xué)技術(shù)的發(fā)展，使得含有數(shù)千萬(wàn)元件的集成電路已經(jīng)能夠大批量地生產(chǎn)出來(lái)，真正的SoC(SystemonaChip)正在成為現(xiàn)實(shí)。集成電路的設(shè)計(jì)能力滯后于集成電路的工藝水平。設(shè)計(jì)VLSI中的關(guān)鍵問(wèn)題之一是如何檢查設(shè)計(jì)的正確性，即設(shè)計(jì)驗(yàn)證。因?yàn)樵O(shè)計(jì)驗(yàn)證的復(fù)雜度隨著芯片的規(guī)模呈指數(shù)增加，傳統(tǒng)的驗(yàn)證手段，如模擬、測(cè)試和仿真技術(shù)，對(duì)于大型的系統(tǒng)都不是完全的。由于集成電路工藝的復(fù)雜性，它的試制費(fèi)用相當(dāng)昂貴。為解決設(shè)計(jì)驗(yàn)證這一難題，過(guò)去二十年中

2、，人們發(fā)展了一種新方法——形式化驗(yàn)證(FormalVerification)方法。這是VLSI(VeryLargeScaleIntegration)設(shè)計(jì)驗(yàn)證的一種有希望的方法。形式化驗(yàn)證意味著驗(yàn)證過(guò)程是數(shù)學(xué)化的，而不是如模擬技術(shù)那樣，是試驗(yàn)性質(zhì)的。數(shù)學(xué)化的驗(yàn)證克服了模擬的不足，因?yàn)樗母采w是完全的，并且可以減少驗(yàn)證時(shí)間。形式化驗(yàn)證可以對(duì)電路描述進(jìn)行自動(dòng)化的驗(yàn)證，減少了驗(yàn)證的復(fù)雜度。 本文研究基于多項(xiàng)式符號(hào)代數(shù)理論的形式化驗(yàn)證方法

3、。關(guān)于多項(xiàng)式符號(hào)代數(shù)理論在形式化驗(yàn)證方面的研究，人們給出了WGLs(WeightedGeneralizedLists)和TEDs(TaylorExpansionDiagrams)兩個(gè)多項(xiàng)式表示模型，并給出了相應(yīng)的等價(jià)性驗(yàn)證算法。本文的主要工作如下。 1)基于WGLs模型，給出了高層的數(shù)據(jù)通路的規(guī)格說(shuō)明與相應(yīng)的電路實(shí)現(xiàn)之間的等價(jià)性驗(yàn)證算法。由于WGLs不能應(yīng)用于含有布爾變量和字級(jí)變量電路描述的表示，所以給出一個(gè)基于WGLs的新模型

4、LWGLs(LabeledandWeghhtedGeneralizedLists)。LWGLs可以應(yīng)用于含有布爾變量和字級(jí)變量電路描述的表示，并應(yīng)用于高層次電路描述與電路實(shí)現(xiàn)或不同的電路實(shí)現(xiàn)之間的等價(jià)性驗(yàn)證。 2)改進(jìn)了TEDs的加法和乘法的算法描述，并對(duì)算法的復(fù)雜度進(jìn)行分析。為了對(duì)電路的邏輯行為和時(shí)序行為進(jìn)行統(tǒng)一表示，給出了一個(gè)基于TEDs的新的模型，稱為時(shí)序泰勒展開(kāi)圖(TimedTaylorExpansionDiagrams