并發(fā)的廣義符號(hào)軌跡賦值的研究.pdf

1、隨著數(shù)字邏輯設(shè)計(jì)的規(guī)模越來(lái)越大,復(fù)雜度越來(lái)越高,功能驗(yàn)證已成為設(shè)計(jì)過(guò)程中的首要瓶頸。在過(guò)去幾十年中,人們對(duì)于數(shù)字電路順序行為的驗(yàn)證進(jìn)行了深入而廣泛的研究并提出了許多行之有效的驗(yàn)證方法,主要分為基于模擬的和基于形式方法的驗(yàn)證技術(shù)[1]。然而,數(shù)字集成電路是典型的并發(fā)系統(tǒng),如何實(shí)現(xiàn)對(duì)并發(fā)行為的有效驗(yàn)證就成為保證數(shù)字電路功能正確性的關(guān)鍵因素。
　　 本文在了解國(guó)內(nèi)外形式驗(yàn)證技術(shù)研究成果的基礎(chǔ)上,對(duì)當(dāng)前主流形式化驗(yàn)證方法中的廣義符號(hào)軌跡

2、賦值(generalized symbolic trajectory evaluation,GSTE)[2-3]驗(yàn)證方法進(jìn)行了深入的研究和拓展,修改斷言圖及其驗(yàn)證算法使之能更簡(jiǎn)潔的描述和驗(yàn)證數(shù)字電路的并發(fā)性質(zhì)。
　　 本文在研究方法上,首先深入學(xué)習(xí)和研究了廣義符號(hào)軌跡賦值相關(guān)的理論包括電路模型、電路模擬方法,符號(hào)軌跡賦值[4-5]和廣義符號(hào)軌跡賦值的核心算法。并通過(guò)實(shí)例展示了斷言圖描述電路并發(fā)性質(zhì)時(shí)的不足。
　　 其次,

3、學(xué)習(xí)和研究了進(jìn)程代數(shù)[6-8]的表示方法后,本文提出了一個(gè)基于廣義符號(hào)軌跡賦值的組合方法來(lái)克服斷言圖不能簡(jiǎn)潔描述電路并發(fā)性質(zhì)的限制。(1)提出了一個(gè)規(guī)范語(yǔ)言,它能用組合的方式簡(jiǎn)潔的描述系統(tǒng)的并發(fā)行為。這種組合是邏輯的,不依賴于對(duì)系統(tǒng)實(shí)現(xiàn)細(xì)節(jié)的深入理解。這個(gè)語(yǔ)言是對(duì)廣義符號(hào)軌跡賦值規(guī)范語(yǔ)言的拓展,它引入了一個(gè)新的meet運(yùn)算符,用類似于進(jìn)程代數(shù)的方式表達(dá)。(2)針對(duì)新的斷言圖規(guī)范,本文對(duì)經(jīng)典的廣義符號(hào)軌跡賦值的算法進(jìn)行了修改,該算法能直接

4、深入規(guī)范的語(yǔ)法結(jié)構(gòu)并建立從規(guī)范的語(yǔ)言元素到電路狀態(tài)集合的模擬關(guān)系。本文設(shè)計(jì)了一個(gè)高效而實(shí)用的方法來(lái)直接驗(yàn)證并發(fā)規(guī)范。
　　 第三,在平臺(tái)Forte平臺(tái)環(huán)境[9]下利用FL語(yǔ)言對(duì)改進(jìn)后的并發(fā)驗(yàn)證算法進(jìn)行編碼實(shí)現(xiàn)和測(cè)試。實(shí)驗(yàn)結(jié)果表明修改后的斷言圖和算法是有效的,在驗(yàn)證并發(fā)性質(zhì)時(shí)確實(shí)能夠減小斷言圖的復(fù)雜度。
　　 最后,對(duì)全文進(jìn)行系統(tǒng)、全面的總結(jié),指出了下一步研究和改善的方向。并展望了形式化驗(yàn)證算法在電路設(shè)計(jì)領(lǐng)域的良好應(yīng)用前景