基于VHDL的模型檢查應(yīng)用與實(shí)現(xiàn).pdf

1、隨著計算機(jī)軟硬件系統(tǒng)規(guī)模的日益復(fù)雜化、重要化，如何保證計算機(jī)系統(tǒng)的正確性和可靠性，逐漸成為當(dāng)前理論界和產(chǎn)業(yè)界共同關(guān)心的重要問題。長期以來，常用的系統(tǒng)設(shè)計檢驗方法是以經(jīng)驗為基礎(chǔ)的測試方法。但是，測試方法只能證明錯誤的存在，但不能證明錯誤的不存在，所以，對于高可靠性系統(tǒng)來說，測試方法有明顯的局限性。 在過去二十多年間，各國研究人員為解決這個問題付出了巨大的努力，取得了重要的進(jìn)展。在為此提出的諸多理論和方法中，模型檢查(Model C

2、hecking)以其簡潔明了和自動化程度高而引人注目。 本文首先介紹了模型檢查技術(shù)的基本思想、研究方向和最新研究進(jìn)展以及相關(guān)背景工具和VHDL語言，然后介紹了模型檢查技術(shù)的理論基礎(chǔ)，并研究和設(shè)計了一個針對時序電路VHDL設(shè)計的模型檢查系統(tǒng)的解決方案。本文的主要工作有： 1.研究模型檢查相關(guān)理論和算法，包括Kripke結(jié)構(gòu)、時序邏輯CTL、不動點(diǎn)計算、反例路徑生成等。并在此基礎(chǔ)上實(shí)現(xiàn)了一個基于Kripke結(jié)構(gòu)、不動點(diǎn)計算和

3、OBDD動態(tài)排序的模型檢查器，可驗證VHDL設(shè)計的正確性。 2.提出了一個針對時序電路VHDL設(shè)計的模型檢查系統(tǒng)的解決方案。包括了實(shí)現(xiàn)方案選擇、系統(tǒng)主要內(nèi)容(包括VHDL建模，給出規(guī)格說明，進(jìn)行模型檢查)以及系統(tǒng)總體框架； 3.實(shí)現(xiàn)將VHDL設(shè)計轉(zhuǎn)換成有限狀態(tài)機(jī)，并使之能同時適用于異步時序電路和同步時序電路，這包括建模算法、子模型的建立，子模型的合并等；另外對上述建模算法進(jìn)行優(yōu)化，對于同步時序電路能有效化簡，減少系統(tǒng)狀態(tài)