基于GSTE理論的反例研究.pdf

1、在過(guò)去幾十年,人們對(duì)信息技術(shù)大量需求,微電子技術(shù)高速發(fā)展,使得集成電路的規(guī)模和復(fù)雜度越來(lái)越高,這些對(duì)集成電路的設(shè)計(jì)和制造提出了更高的要求。在億萬(wàn)級(jí)的晶體管電路中,完全不出現(xiàn)錯(cuò)誤是非常難的,1994年Intel公司的芯片中的浮點(diǎn)錯(cuò)誤就是一個(gè)例子,因此設(shè)計(jì)驗(yàn)證已經(jīng)越來(lái)越受重視。STE是基于四值符號(hào)模擬的模型驗(yàn)證技術(shù),在大規(guī)模硬件設(shè)計(jì)中發(fā)揮了很大的作用。盡管STE驗(yàn)證很高效,但是STE的固有缺陷是它驗(yàn)證的屬性種類(lèi)有限,對(duì)于無(wú)限時(shí)間屬性無(wú)能為力

2、,另外STE只能進(jìn)行前向模擬,而不能進(jìn)行后向模擬,所以也無(wú)法查找反例。在最近的一些年,GSTE(廣義符號(hào)軌跡賦值,Generalized symbolic trajectoryevaluation)是對(duì)STE擴(kuò)展最成功的一個(gè)理論,GSTE可以驗(yàn)證無(wú)限時(shí)間性質(zhì),同時(shí)還可以進(jìn)行后向模擬,由于GSTE具有可以后向模擬的特點(diǎn),所以可以應(yīng)用GSTE的這個(gè)特點(diǎn)進(jìn)行本課題的研究,即研究GSTE理論的反例生成。
　　 因?yàn)镚STE一般進(jìn)行的是性

3、質(zhì)相關(guān)的驗(yàn)證,性質(zhì)一旦失敗,就需要為其生成一個(gè)反例,提供給設(shè)計(jì)者來(lái)調(diào)試失敗的錯(cuò)誤,通過(guò)反例來(lái)確定失敗的原因。設(shè)計(jì)者通過(guò)對(duì)于反例的調(diào)試,可以確定這個(gè)錯(cuò)誤是由于無(wú)效的輸入引起的,還是由于設(shè)計(jì)錯(cuò)誤導(dǎo)致的。在前一種情況下,需要加入約束來(lái)消除無(wú)效性,后一種則需要系統(tǒng)設(shè)計(jì)返工。由于GSTE理論比較新穎,目前并沒(méi)有學(xué)者對(duì)于GSTE的反例查找進(jìn)行系統(tǒng)的研究,所以本課題進(jìn)行反例查找技術(shù)的研究,對(duì)于GSTE理論的完善來(lái)說(shuō)至關(guān)重要。
　　 本文首先對(duì)

4、驗(yàn)證的發(fā)展進(jìn)行了介紹,并重點(diǎn)介紹了STE驗(yàn)證理論和GSTE驗(yàn)證理論,并對(duì)它們的優(yōu)缺點(diǎn)進(jìn)行了分析。然后介紹了查找反例技術(shù)的發(fā)展,并重點(diǎn)介紹了其在GSTE理論中的的作用,基于以上原因,重點(diǎn)設(shè)計(jì)了兩個(gè)查找反例的算法,通過(guò)這兩個(gè)算法補(bǔ)充了GSTE理論在反例查找方面的欠缺。當(dāng)應(yīng)用GSTE進(jìn)行驗(yàn)證時(shí),如果出現(xiàn)斷言錯(cuò)誤時(shí),可以使用第一個(gè)算法找出系統(tǒng)的一個(gè)反例。緊接著對(duì)第一個(gè)算法進(jìn)行擴(kuò)展,當(dāng)出現(xiàn)斷言錯(cuò)誤時(shí),可以使用擴(kuò)展算法將與此錯(cuò)誤相關(guān)的所有反例全部列