本文關(guān)鍵詞：代數(shù)化符號模擬驗證的應(yīng)用研究

  更多相關(guān)文章： 符號模擬 斷言驗證 代數(shù)符號計算 屬性描述語言 數(shù)字系統(tǒng)驗證

【摘要】：傳統(tǒng)的模擬驗證技術(shù)與形式化驗證方法是集成電路驗證理論中最重要的兩類驗證方法,模擬驗證技術(shù)原理簡單,可操作性強,應(yīng)用范圍廣,但無法進(jìn)行完全測試：形式化方法具備完全性,但應(yīng)用范圍受到局限。 而模擬技術(shù)與形式化方法混合驗證是近十幾年來驗證領(lǐng)域方興未艾的重要研究方向之一,它有機地結(jié)合了模擬驗證方法的動態(tài)性與形式化方法無需測試矢量的優(yōu)點,是一個既有理論依據(jù)又能實際運用的方法。本文重點研究代數(shù)符號計算理論與模擬驗證方法的交叉與融合。 在數(shù)字集成電路設(shè)計驗證領(lǐng)域,符號模擬通過系統(tǒng)的動態(tài)符號執(zhí)行檢查預(yù)設(shè)條件或斷言的真假來進(jìn)行功能的正確性驗證,是一種在工程實踐應(yīng)用中發(fā)揮了重要作用的有效方法。目前的符號模擬特別是高層符號模擬方法,存在著符號表達(dá)結(jié)果難以判定和空間爆炸等問題,使得其本身的構(gòu)建理論和應(yīng)用都受到了很大的限制。基于此,本文將代數(shù)符號計算方法運用到符號模擬驗證領(lǐng)域,作為可驗證計算的核心計算方法。并針對模擬驗證計算的特點,著重研究基于斷言驗證方法學(xué)下符號模擬算法的代數(shù)化方法面臨的理論問題,分別提出基于吳特征列方法和基于Groebner基的代數(shù)化算法。主要工作和取得的研究成果如下： (1)PSL布爾層的代數(shù)化符號模擬斷言驗證 提出了將基于PSL布爾層斷言驗證的符號模擬驗證問題轉(zhuǎn)化為符號計算理論適用的代數(shù)問題方法,并且初步建立代數(shù)化的模擬驗證的基本理論框架。首先將待驗證的布爾斷言表達(dá)式和系統(tǒng)符號執(zhí)行的結(jié)構(gòu)轉(zhuǎn)換為適當(dāng)?shù)姆蔷�性代數(shù)方程組的形式,本文采用基于數(shù)據(jù)流的多項式代數(shù)表達(dá)方法。根據(jù)符號代數(shù)的特點,將PSL中邏輯規(guī)范中關(guān)于布爾邏輯的定義進(jìn)行了修改,定義了信號邏輯與斷言邏輯以適應(yīng)斷言驗證的要求。PSL布爾層斷言雖然簡單,但卻是本文驗證方法的起始點和基礎(chǔ),在布爾斷言與組合電路模型分別代數(shù)化的基礎(chǔ)上,給出相應(yīng)的Groebner基方法和吳方法的驗證算法,并通過實例驗證。 (2)PSL時序?qū)拥拇鷶?shù)化符號模擬斷言驗證 提出了將基于PSL時序?qū)訑嘌则炞C的符號模擬驗證問題轉(zhuǎn)化為符號計算理論適用的代數(shù)問題方法,并且初步建立時序電路代數(shù)化模擬驗證的基本理論框架。針對符號模擬的特點以及通過Symbolic Trajectory Evaluation (STE)技術(shù)對比,重點研究符號斷言的刻畫和驗證問題。由于布爾值的真與假與電路信號的高與低在當(dāng)前PSL規(guī)范中未加以區(qū)分,從而導(dǎo)致符號代數(shù)驗證方法無法實施,所以首先定義了SERE的簡單約束子集以及對每種時序操作符代數(shù)化,在此基礎(chǔ)上,給出時序電路在時幀展開基礎(chǔ)上參數(shù)化多項式集合的建模方法。最后借鑒SymbolicTrajectory Evaluation (STE)技術(shù)的斷言圖方法來解決PSL中時序?qū)訑嘌缘目坍嫼万炞C問題。 (3) SystemVerilog斷言的代數(shù)化符號模擬斷言驗證 提出了將基于SystemVerilog斷言驗證的符號模擬驗證問題轉(zhuǎn)化為符號計算理論適用的代數(shù)問題方法,首先定義了SystemVerilog斷言的約束子集,并給出了每個序列以及屬性的操作符代數(shù)化步驟。然后在布爾斷言以及時序電路斷言驗證的基礎(chǔ)上,給出基于多項式理論的電路模型與SystemVerilog斷言模型建模方法,將基于模擬的驗證問題轉(zhuǎn)換為符號代數(shù)計算問題。最后給出相應(yīng)的Groebner基方法和吳方法的驗證算法,并通過實例驗證。 綜上所述,本文基于斷言驗證方法學(xué),將符號模擬技術(shù)代數(shù)化,提出一種集成電路代數(shù)化符號模擬的斷言驗證方法。該方法在代數(shù)符號計算與形式化驗證方法以及模擬技術(shù)之間搭建起一座橋梁,將傳統(tǒng)模擬驗證技術(shù)、形式化方法、代數(shù)符號計算相融合,有效避免純形式化方法與傳統(tǒng)電路驗證技術(shù)之間的割裂,并為集成電路驗證理論提供了一種新的解決思路。
【關(guān)鍵詞】：符號模擬 斷言驗證 代數(shù)符號計算 屬性描述語言 數(shù)字系統(tǒng)驗證
【學(xué)位授予單位】：北京交通大學(xué)
【學(xué)位級別】：博士
【學(xué)位授予年份】：2015
【分類號】：O151
【目錄】：

• 致謝5-6
• 摘要6-8
• ABSTRACT8-14
• 1 緒論14-28
• 1.1 研究背景及意義14-18
• 1.2 相關(guān)研究18-24
• 1.2.1 驗證技術(shù)18-20
• 1.2.2 斷言驗證方法學(xué)20-23
• 1.2.3 代數(shù)化驗證理論23-24
• 1.3 論文的研究內(nèi)容24-26
• 1.4 論文的結(jié)構(gòu)安排26-28
• 2 相關(guān)知識28-46
• 2.1 符號計算28-33
• 2.1.1 Groebner基方法28-31
• 2.1.2 吳方法31-33
• 2.2 符號模擬驗證方法33-40
• 2.2.1 基本思想35-38
• 2.2.2 基于STE的符號模擬38-40
• 2.3 形式化驗證方法40-45
• 2.3.1 定理證明方法41-42
• 2.3.2 等價性檢驗42-43
• 2.3.3 模型檢驗43-45
• 2.4 本章小結(jié)45-46
• 3 基于代數(shù)化符號模擬的布爾層PSL性質(zhì)驗證46-60
• 3.1 引言46-47
• 3.2 PSL布爾層及其代數(shù)表示47-49
• 3.3 布爾層組合電路建模49-50
• 3.4 基于Groebner基驗證算法及實例50-54
• 3.4.1 基于Groebner基的驗證算法50-52
• 3.4.2 基于Groebner基的驗證實例52-54
• 3.5 基于吳方法驗證算法及實例54-59
• 3.5.1 基于吳方法的驗證算法框架54-57
• 3.5.2 基于吳方法的驗證實例57-59
• 3.6 本章小結(jié)59-60
• 4 基于代數(shù)化符號模擬的SERE時序斷言驗證60-82
• 4.1 引言60-61
• 4.2 基于周期的符號模擬61-62
• 4.3 系統(tǒng)多項式表示模型62-67
• 4.3.1 算術(shù)、邏輯以及分支單元建模62-63
• 4.3.2 時序單元建模及展開63-65
• 4.3.3 時序操作符建模65-67
• 4.4 SERE轉(zhuǎn)換方法67-70
• 4.4.1 代數(shù)化過程67-68
• 4.4.2 布爾層建模68-70
• 4.5 基于Groebner基算法框架70-74
• 4.5.1 基于定理證明的驗證理論70-71
• 4.5.2 驗證算法71-74
• 4.6 基于Groebner基驗證實例分析74-77
• 4.6.1 電路及PSL建模74-76
• 4.6.2 使用Maple進(jìn)行斷言驗證76-77
• 4.7 基于吳方法的SERE時序斷言驗證77-81
• 4.7.1 基于吳方法驗證的算法框架77-79
• 4.7.2 基于吳方法驗證的實例研究79-81
• 4.8 本章小結(jié)81-82
• 5 基于代數(shù)化符號模擬的SystemVerilog的并發(fā)斷言驗證82-116
• 5.1 引言82-83
• 5.2 SystemVerilog基礎(chǔ)83-85
• 5.3 同步數(shù)字系統(tǒng)以及多項式表示85-87
• 5.3.1 組合邏輯模型85
• 5.3.2 時序單元建模85-86
• 5.3.3 符號模擬系統(tǒng)模型86-87
• 5.4 多項式集合表示SVA表達(dá)式87-96
• 5.4.1 多項式概念以及代數(shù)化87-88
• 5.4.2 時間區(qū)間及其展開模型88-89
• 5.4.3 時序的深度計算89-91
• 5.4.4 時序操作符建模91-93
• 5.4.5 局部變量表示及屬性操作符建模93-95
• 5.4.6 SystemVerilog斷言的約束子集95-96
• 5.5 基于Groebner基的SVA驗證理論及算法96-98
• 5.5.1 基于Groebner基斷言驗證原理96-97
• 5.5.2 驗證算法框架97-98
• 5.6 基于Groebner基斷言驗證實例98-103
• 5.6.1 電路及斷言建模98-101
• 5.6.2 使用Maple進(jìn)行計算101-103
• 5.7 基于吳方法的SVA驗證理論及算法103-104
• 5.7.1 基于吳方法的SVA驗證原理103-104
• 5.7.2 基于吳方法的SVA驗證算法104
• 5.8 基于吳方法的SVA實例驗證及實驗104-113
• 5.8.1 電路及斷言建模105-106
• 5.8.2 使用MMP驗證斷言106-107
• 5.8.3 經(jīng)典仲裁器電路的實驗107-112
• 5.8.4 實驗討論112-113
• 5.9 本章小結(jié)113-116
• 6 總結(jié)與展望116-120
• 6.1 研究工作總結(jié)116-118
• 6.2 未來工作展望118-120
• 參考文獻(xiàn)120-126
• 作者簡歷及攻讀博士學(xué)位期間取得的研究成果126-132
• 學(xué)位論文數(shù)據(jù)集132

【參考文獻(xiàn)】

中國期刊全文數(shù)據(jù)庫 前10條

1 吳文俊;ON THE DECISION PROBLEM AND THE MECHANIZATION OF THEOREM-PROVING IN ELEMENTARY GEOMETRY[J];Science in China,Ser.A;1978年02期

2 楊志;馬光勝;張曙;;基于多項式符號代數(shù)方法的高層次數(shù)據(jù)通路的等價驗證[J];計算機研究與發(fā)展;2009年03期

3 袁智德,宣國良;我國集成電路設(shè)計業(yè)發(fā)展的戰(zhàn)略選擇[J];經(jīng)濟理論與經(jīng)濟管理;2001年05期

4 馬博;韓俊剛;;采用PSL的基于斷言的驗證[J];計算機工程;2007年02期

5 閆煒;吳盡昭;高新巖;;符號模擬[J];計算機工程;2007年20期

6 鄭偉偉;吳為民;邊計年;;基于線性規(guī)劃的RTL可滿足性求解和性質(zhì)檢驗[J];計算機輔助設(shè)計與圖形學(xué)學(xué)報;2006年04期

7 楊志;馬光勝;馮剛;邵晶波;;應(yīng)用吳方法進(jìn)行高層次定界模型檢驗[J];計算機輔助設(shè)計與圖形學(xué)學(xué)報;2008年02期

8 虞蕾;趙宗濤;;PSL邏輯及驗證技術(shù)研究進(jìn)展與展望[J];計算機應(yīng)用研究;2010年07期

9 徐善鋒,初秀琴,李玉山,來新泉;21世紀(jì)微電子芯片設(shè)計技術(shù)發(fā)展方向[J];微電子學(xué);2001年05期

10 ;A CHARACTERISTIC SET METHOD FOR SOLVING BOOLEAN EQUATIONS AND APPLICATIONS IN CRYPTANALYSIS OF STREAM CIPHERS[J];Journal of Systems Science and Complexity;2008年02期

，

本文編號：595963