數(shù)字系統(tǒng)形式設(shè)計的理論與方法研究.pdf

1、為了提高數(shù)字硬件的設(shè)計層次,保證數(shù)字系統(tǒng)設(shè)計的正確性,采用"形式化方法"(Formal Methods)設(shè)計數(shù)字硬件或者集成電路系統(tǒng)是一種比較好的途徑.所謂形式化方法,就是利用嚴(yán)格的數(shù)學(xué)方法,從給出系統(tǒng)設(shè)計的規(guī)范(Specifications)開始并逐步地推導(dǎo)或者驗證系統(tǒng)的方法.該文將試圖研究數(shù)字系統(tǒng)形式設(shè)計所涉及的主要理論、方法和技術(shù);探討在系統(tǒng)級的層次應(yīng)用形式設(shè)計的可行性,并提出一種新的數(shù)字硬件形式化設(shè)計方法.該論文的研究和創(chuàng)新工作

2、主要包括以下內(nèi)容:(1)對形式設(shè)計方法所取得的成果作了詳細(xì)的回顧,并討論了形式設(shè)計過程中所用到的理論和方法.詳細(xì)論述了形式規(guī)范、程序的精化演算的作用、類型、適用范圍.在此基礎(chǔ)上,分析了幾個用形式方法設(shè)計的硬件系統(tǒng).(2)提出了以Agent組成的硬件設(shè)計的形式計算模型FCMHD(Formal Computa-tional Model for Hardware Design).這是一個基于兩層的形式設(shè)計模型.該模型將簡化形式設(shè)計的過程并有效

3、降低設(shè)計過程的復(fù)雜性.給出了FCMHD的區(qū)間時態(tài)邏輯(Interval Temporal Logic,ITL)語義.作者以時段演算(Duration Calculus,DC)為工具對VHDL的子集進(jìn)行了形式語義分析;通過分析VHDL和Verilog HDL部分語句的形式語義,為硬件描述語言的分析、設(shè)計、編譯提供了一個嚴(yán)格的理論基礎(chǔ)和新的途徑.同時也對該文后半部分提出新的硬件描述語言CHDL作好準(zhǔn)備.(3)提出了一個新的硬件描述語言一"基

4、本硬件描述語言"CHDL(Core Hardware Description Language).該語言的抽象程度要稍高于目前常見的硬件描述語言,但又很容易將其轉(zhuǎn)換為常見的硬件描述語言.并給出了CHDL的形式語義及常用的硬件的語義;提出了把CHDL轉(zhuǎn)換為VHDL或VerilogHDL的方法.(4)論述了FCMHD的精化演算并給出了具體的精化規(guī)則;論述了ITL的復(fù)合驗證.(5)運(yùn)用前面討論的理論和方法,研究了一個比較大的實例.從給出高層設(shè)