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

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

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

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

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