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

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

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

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