基于GSTE理論的抽象與細(xì)化問題的研究.pdf

1、近年來,由于電路規(guī)模不斷增大和集成度不斷提高,使得超大規(guī)模集成電路(VLSI)變得越來越復(fù)雜,而設(shè)計(jì)過程又難以保證邏輯設(shè)計(jì)的正確性。同時(shí)集成電路設(shè)計(jì)時(shí)的差錯(cuò)所帶來的損失巨大,當(dāng)前沒有修復(fù)芯片的技術(shù)不可能對(duì)VLSI中的錯(cuò)誤部分進(jìn)行修正。因此,設(shè)計(jì)和建立高可靠性的集成電路系統(tǒng)成為一個(gè)關(guān)鍵問題。驗(yàn)證作為一個(gè)的保證設(shè)計(jì)正確的重要環(huán)節(jié),正發(fā)揮著越來越重要的作用,并引起人們?cè)絹碓蕉嗟年P(guān)注和興趣。本課題在GSTE理論的基礎(chǔ)上,研究抽象以及細(xì)化處理在該

2、理論上的應(yīng)用,希望解決由抽象所帶來的效率以及驗(yàn)證精確性的統(tǒng)一問題。通過變量劃分技術(shù),對(duì)變量集有區(qū)別的進(jìn)行抽象以有效表示狀態(tài)空間；為有效地表示相關(guān)變量的狀態(tài)集,使用參數(shù)化表示將狀態(tài)空間進(jìn)行壓縮化處理,并利用BDD技術(shù)實(shí)現(xiàn)GSTE理論驗(yàn)證算法。
　　 由于當(dāng)前形式化驗(yàn)證方法基于狀態(tài)搜索的處理方法,因此存在處理能力有限的問題,而不能驗(yàn)證大規(guī)模的電路系統(tǒng)。當(dāng)前大部分形式化驗(yàn)證工具都引入了抽象與細(xì)化處理,來解決狀態(tài)爆炸的問題。在研究方法上

3、,首先,本文講述了為解決狀態(tài)爆炸問題而產(chǎn)生的形式化驗(yàn)證方法,簡(jiǎn)要分析了它們的驗(yàn)證思想以及存在的問題。其次,講了形式化驗(yàn)證方法如何對(duì)驗(yàn)證電路進(jìn)行建模,并重點(diǎn)介紹當(dāng)前主要的形式化驗(yàn)證方法:STE和GSTE,并且對(duì)電路模型的定義,驗(yàn)證規(guī)范的描述以及驗(yàn)證算法進(jìn)行分析,同時(shí)針對(duì)它們驗(yàn)證模擬的原理和方法,分析其優(yōu)缺點(diǎn),并對(duì)它們進(jìn)行對(duì)比分析。進(jìn)一步了解了抽象處理的方法以及對(duì)電路的符號(hào)化處理技術(shù),同時(shí)分析了GSTE的抽象處理以及細(xì)化處理的過程。在以上理