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

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

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

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

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