代數(shù)化符號(hào)模擬驗(yàn)證的應(yīng)用研究.pdf

1、傳統(tǒng)的模擬驗(yàn)證技術(shù)與形式化驗(yàn)證方法是集成電路驗(yàn)證理論中最重要的兩類(lèi)驗(yàn)證方法，模擬驗(yàn)證技術(shù)原理簡(jiǎn)單，可操作性強(qiáng)，應(yīng)用范圍廣，但無(wú)法進(jìn)行完全測(cè)試;形式化方法具備完全性，但應(yīng)用范圍受到局限。
　　而模擬技術(shù)與形式化方法混合驗(yàn)證是近十幾年來(lái)驗(yàn)證領(lǐng)域方興未艾的重要研究方向之一，它有機(jī)地結(jié)合了模擬驗(yàn)證方法的動(dòng)態(tài)性與形式化方法無(wú)需測(cè)試矢量的優(yōu)點(diǎn)，是一個(gè)既有理論依據(jù)又能實(shí)際運(yùn)用的方法。本文重點(diǎn)研究代數(shù)符號(hào)計(jì)算理論與模擬驗(yàn)證方法的交叉與融合。

2、>　　在數(shù)字集成電路設(shè)計(jì)驗(yàn)證領(lǐng)域，符號(hào)模擬通過(guò)系統(tǒng)的動(dòng)態(tài)符號(hào)執(zhí)行檢查預(yù)設(shè)條件或斷言的真假來(lái)進(jìn)行功能的正確性驗(yàn)證，是一種在工程實(shí)踐應(yīng)用中發(fā)揮了重要作用的有效方法。目前的符號(hào)模擬特別是高層符號(hào)模擬方法，存在著符號(hào)表達(dá)結(jié)果難以判定和空間爆炸等問(wèn)題，使得其本身的構(gòu)建理論和應(yīng)用都受到了很大的限制?；诖耍疚膶⒋鷶?shù)符號(hào)計(jì)算方法運(yùn)用到符號(hào)模擬驗(yàn)證領(lǐng)域，作為可驗(yàn)證計(jì)算的核心計(jì)算方法。并針對(duì)模擬驗(yàn)證計(jì)算的特點(diǎn)，著重研究基于斷言驗(yàn)證方法學(xué)下符號(hào)模擬算法的

3、代數(shù)化方法面臨的理論問(wèn)題，分別提出基于吳特征列方法和基于Groebner基的代數(shù)化算法。主要工作和取得的研究成果如下:
　　(1)PSL布爾層的代數(shù)化符號(hào)模擬斷言驗(yàn)證
　　提出了將基于PSL布爾層斷言驗(yàn)證的符號(hào)模擬驗(yàn)證問(wèn)題轉(zhuǎn)化為符號(hào)計(jì)算理論適用的代數(shù)問(wèn)題方法，并且初步建立代數(shù)化的模擬驗(yàn)證的基本理論框架。首先將待驗(yàn)證的布爾斷言表達(dá)式和系統(tǒng)符號(hào)執(zhí)行的結(jié)構(gòu)轉(zhuǎn)換為適當(dāng)?shù)姆蔷€性代數(shù)方程組的形式，本文采用基于數(shù)據(jù)流的多項(xiàng)式代數(shù)表達(dá)方法。

4、根據(jù)符號(hào)代數(shù)的特點(diǎn)，將PSL中邏輯規(guī)范中關(guān)于布爾邏輯的定義進(jìn)行了修改，定義了信號(hào)邏輯與斷言邏輯以適應(yīng)斷言驗(yàn)證的要求。PSL布爾層斷言雖然簡(jiǎn)單，但卻是本文驗(yàn)證方法的起始點(diǎn)和基礎(chǔ)，在布爾斷言與組合電路模型分別代數(shù)化的基礎(chǔ)上，給出相應(yīng)的Groebner基方法和吳方法的驗(yàn)證算法，并通過(guò)實(shí)例驗(yàn)證。
　　(2)PSL時(shí)序?qū)拥拇鷶?shù)化符號(hào)模擬斷言驗(yàn)證
　　提出了將基于PSL時(shí)序?qū)訑嘌则?yàn)證的符號(hào)模擬驗(yàn)證問(wèn)題轉(zhuǎn)化為符號(hào)計(jì)算理論適用的代數(shù)問(wèn)題方法

5、，并且初步建立時(shí)序電路代數(shù)化模擬驗(yàn)證的基本理論框架。針對(duì)符號(hào)模擬的特點(diǎn)以及通過(guò)Symbolic Trajectory Evaluation(STE)技術(shù)對(duì)比，重點(diǎn)研究符號(hào)斷言的刻畫(huà)和驗(yàn)證問(wèn)題。由于布爾值的真與假與電路信號(hào)的高與低在當(dāng)前PSL規(guī)范中未加以區(qū)分，從而導(dǎo)致符號(hào)代數(shù)驗(yàn)證方法無(wú)法實(shí)施，所以首先定義了SERE的簡(jiǎn)單約束子集以及對(duì)每種時(shí)序操作符代數(shù)化，在此基礎(chǔ)上，給出時(shí)序電路在時(shí)幀展開(kāi)基礎(chǔ)上參數(shù)化多項(xiàng)式集合的建模方法。最后借鑒Symb

6、olicTrajectory Evaluation(STE)技術(shù)的斷言圖方法來(lái)解決PSL中時(shí)序?qū)訑嘌缘目坍?huà)和驗(yàn)證問(wèn)題。
　　(3)SystemVerilog斷言的代數(shù)化符號(hào)模擬斷言驗(yàn)證
　　提出了將基于SystemVerilog斷言驗(yàn)證的符號(hào)模擬驗(yàn)證問(wèn)題轉(zhuǎn)化為符號(hào)計(jì)算理論適用的代數(shù)問(wèn)題方法，首先定義了SystemVerilog斷言的約束子集，并給出了每個(gè)序列以及屬性的操作符代數(shù)化步驟。然后在布爾斷言以及時(shí)序電路斷言驗(yàn)證的基礎(chǔ)

7、上，給出基于多項(xiàng)式理論的電路模型與SystemVerilog斷言模型建模方法，將基于模擬的驗(yàn)證問(wèn)題轉(zhuǎn)換為符號(hào)代數(shù)計(jì)算問(wèn)題。最后給出相應(yīng)的Groebner基方法和吳方法的驗(yàn)證算法，并通過(guò)實(shí)例驗(yàn)證。
　　綜上所述，本文基于斷言驗(yàn)證方法學(xué)，將符號(hào)模擬技術(shù)代數(shù)化，提出一種集成電路代數(shù)化符號(hào)模擬的斷言驗(yàn)證方法。該方法在代數(shù)符號(hào)計(jì)算與形式化驗(yàn)證方法以及模擬技術(shù)之間搭建起一座橋梁，將傳統(tǒng)模擬驗(yàn)證技術(shù)、形式化方法、代數(shù)符號(hào)計(jì)算相融合，有效避免純形