基于多項式模型的高層次形式化驗證.pdf

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

2、，人們發(fā)展了一種新方法——形式化驗證(FormalVerification)方法。這是VLSI(VeryLargeScaleIntegration)設計驗證的一種有希望的方法。形式化驗證意味著驗證過程是數(shù)學化的，而不是如模擬技術那樣，是試驗性質的。數(shù)學化的驗證克服了模擬的不足，因為它的覆蓋是完全的，并且可以減少驗證時間。形式化驗證可以對電路描述進行自動化的驗證，減少了驗證的復雜度。 本文研究基于多項式符號代數(shù)理論的形式化驗證方法

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

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