基于MDD和多值多位變量的GSTE算法實(shí)現(xiàn).pdf

1、電子電路設(shè)計(jì)隨著大規(guī)模集成電路的迅速發(fā)展而受到了廣泛的關(guān)注，并取得了一定的研究進(jìn)展，但是還是遠(yuǎn)遠(yuǎn)趕不上大規(guī)模集成電路的發(fā)展速度，成為了電子電路產(chǎn)業(yè)中發(fā)展的滯后點(diǎn)，傳統(tǒng)的電路驗(yàn)證已經(jīng)遠(yuǎn)遠(yuǎn)的不能滿足現(xiàn)在大規(guī)模集成電路的需求，需要更加快速和更大規(guī)模的驗(yàn)證算法及驗(yàn)證平臺(tái)，形式化方法應(yīng)運(yùn)而生。本文主要在廣義符號賦值算法的研究和實(shí)現(xiàn)上做出了一定的工作，主要實(shí)現(xiàn)了以廣義符號賦值算法為驗(yàn)證基礎(chǔ)的驗(yàn)證平臺(tái)?，F(xiàn)今已有的驗(yàn)證平臺(tái)中伯克利大學(xué)開發(fā)的VIS和公司

2、流行使用的Cospan等驗(yàn)證平臺(tái)都是基于CTL和LTL語言描述驗(yàn)證性質(zhì)的平臺(tái)，廣義符號賦值算法則是基于斷言圖描述驗(yàn)證性質(zhì)的平臺(tái)，彌補(bǔ)了這兩個(gè)平臺(tái)在一些驗(yàn)證問題上的缺陷。本文中設(shè)計(jì)出的平臺(tái)填補(bǔ)了在形式化驗(yàn)證領(lǐng)域中沒有基于廣義符號賦值算法驗(yàn)證平臺(tái)的空白，更加的完善了在形式化驗(yàn)證領(lǐng)域的驗(yàn)證平臺(tái)的種類，使得在解決不同問題時(shí)有了更多的選擇，可以通過對比時(shí)間和空間復(fù)雜度來選用一款比較適合解決這類問題的平臺(tái)
　　本文首先介紹廣義符號賦值算法的背

3、景以及發(fā)展歷史，接下來會(huì)介紹VIS驗(yàn)證平臺(tái)，并完成對我們自己設(shè)計(jì)的驗(yàn)證平臺(tái)的介紹，然后會(huì)介紹在平臺(tái)實(shí)現(xiàn)中對廣義符號賦值算法的重點(diǎn)難點(diǎn)問題的解決和實(shí)現(xiàn)，以及一些在研究和實(shí)現(xiàn)以廣義符號賦值算法為基礎(chǔ)的驗(yàn)證平臺(tái)時(shí)對算法的創(chuàng)新點(diǎn)。電路設(shè)計(jì)驗(yàn)證過程中最重要的一點(diǎn)是找到電路設(shè)計(jì)是否滿足設(shè)計(jì)者所設(shè)想的要求，在廣義符號賦值算法中是通過對模型和性質(zhì)的抽象，來驗(yàn)證模型是否滿足性質(zhì)的方法來驗(yàn)證電路設(shè)計(jì)的正確性。算法中的核心是找到不動(dòng)點(diǎn)或出錯(cuò)點(diǎn)，若算法找到不動(dòng)

4、點(diǎn)，則電路滿足設(shè)計(jì)者所提要求；若算法找到出錯(cuò)點(diǎn)，則根據(jù)設(shè)計(jì)的回溯算法找出錯(cuò)誤路徑，提示用戶沿著這條路徑，電路設(shè)計(jì)中會(huì)出現(xiàn)不滿足設(shè)計(jì)者要求的結(jié)果。最后在進(jìn)行研究的過程中，發(fā)現(xiàn)平臺(tái)依然存在一些問題，在求解一些大規(guī)模的電路過程中，會(huì)遇到一些時(shí)間上和空間上不足的問題，這些問題也是當(dāng)今流行的驗(yàn)證軟件同樣很難解決的問題，在平臺(tái)設(shè)計(jì)技術(shù)以及編碼技術(shù)上的改進(jìn)不能在根本上去解決這個(gè)問題，而解決這個(gè)問題的根本方法是在算法上的創(chuàng)新，如果算法上能夠把解決這類問