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

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

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

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

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