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

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

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

4、根據符號代數(shù)的特點，將PSL中邏輯規(guī)范中關于布爾邏輯的定義進行了修改，定義了信號邏輯與斷言邏輯以適應斷言驗證的要求。PSL布爾層斷言雖然簡單，但卻是本文驗證方法的起始點和基礎，在布爾斷言與組合電路模型分別代數(shù)化的基礎上，給出相應的Groebner基方法和吳方法的驗證算法，并通過實例驗證。
　　(2)PSL時序層的代數(shù)化符號模擬斷言驗證
　　提出了將基于PSL時序層斷言驗證的符號模擬驗證問題轉化為符號計算理論適用的代數(shù)問題方法

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

6、olicTrajectory Evaluation(STE)技術的斷言圖方法來解決PSL中時序層斷言的刻畫和驗證問題。
　　(3)SystemVerilog斷言的代數(shù)化符號模擬斷言驗證
　　提出了將基于SystemVerilog斷言驗證的符號模擬驗證問題轉化為符號計算理論適用的代數(shù)問題方法，首先定義了SystemVerilog斷言的約束子集，并給出了每個序列以及屬性的操作符代數(shù)化步驟。然后在布爾斷言以及時序電路斷言驗證的基礎

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