【摘要】：運(yùn)算電路模塊是當(dāng)代微處理器的關(guān)鍵組件。微處理器電路設(shè)計(jì)的驗(yàn)證工作必須確保運(yùn)算電路模塊設(shè)計(jì)的正確性。當(dāng)電路復(fù)雜度達(dá)到一定規(guī)模后，傳統(tǒng)的仿真驗(yàn)證方法已無(wú)法覆蓋整個(gè)狀態(tài)空間，從而無(wú)法保證像微處理器運(yùn)算電路這類復(fù)雜設(shè)計(jì)的正確性。因此，基于形式化方法的運(yùn)算電路驗(yàn)證方法，特別是完全自動(dòng)化的模型檢驗(yàn)方法，已經(jīng)成為當(dāng)前國(guó)內(nèi)外科研機(jī)構(gòu)以及EDA廠商所關(guān)注的熱點(diǎn)問(wèn)題。 本文結(jié)合龍芯I號(hào)微處理器運(yùn)算部件的設(shè)計(jì)和驗(yàn)證工作，系統(tǒng)地研究了運(yùn)算電路的規(guī)范語(yǔ)言、基于決策圖的模型檢驗(yàn)方法以及基于可滿足性判定的模型檢驗(yàn)方法。以下是本文的主要貢獻(xiàn)與創(chuàng)新點(diǎn)： (1)定義了運(yùn)算電路CTL公式的語(yǔ)法和語(yǔ)義，給出了運(yùn)算電路CTL公式的模型檢驗(yàn)方法以及基于~*PHDD的實(shí)現(xiàn)方法。 (2)提出了基于~*PHDD實(shí)現(xiàn)運(yùn)算操作算法的一般優(yōu)化原則。特別地，針對(duì)運(yùn)算電路驗(yàn)證中經(jīng)常出現(xiàn)的基為2的整數(shù)次冪的整除和取模運(yùn)算，推出了四條定理，并且基于這四條定理對(duì)運(yùn)算過(guò)程進(jìn)行了簡(jiǎn)化。這些措施有效提高了~*PHDD運(yùn)算操作算法的效率。 (3)提出了更接近于實(shí)際取值范圍的~*PHDD上下界計(jì)算算法。在整除、取模以及比較運(yùn)算中，上下界可用于簡(jiǎn)化運(yùn)算操作。當(dāng)函數(shù)上下界越接近~*PHDD實(shí)際取值范圍時(shí)，滿足簡(jiǎn)化條件的可能性越大，簡(jiǎn)化算法越有效。 (4)提出了基于條件預(yù)處理的條件約束算法，降低了條件約束算法的運(yùn)行時(shí)間；同時(shí)又提出了多級(jí)約束機(jī)制和約束過(guò)濾機(jī)制，降低了約束條件的規(guī)模，并消除了大量非必要的約束函數(shù)調(diào)用。 (5)提出了基于可滿足性判定算法的運(yùn)算電路驗(yàn)證方法，突破了現(xiàn)有可滿足性判定算法在應(yīng)用上的局限性。實(shí)驗(yàn)結(jié)果表明，該驗(yàn)證方法對(duì)于存在設(shè)計(jì)錯(cuò)誤的運(yùn)算電路或者約束嚴(yán)格的正確運(yùn)算電路非常有效，是決策圖方法的一個(gè)有效補(bǔ)充。 (6)基于上述研究結(jié)果，，實(shí)現(xiàn)了一個(gè)字級(jí)模型檢驗(yàn)系統(tǒng)ArithSMV，并使用該系統(tǒng)驗(yàn)證了龍芯I號(hào)微處理器的浮點(diǎn)加法部件。實(shí)驗(yàn)證明該系統(tǒng)具有實(shí)用高效的特點(diǎn)。
【圖文】：

當(dāng)前摩爾定律的定義。按照摩爾定律，2010年微處理器包含的晶體管數(shù)將達(dá)到18億個(gè)。工藝水平的提高使單個(gè)芯片中可集成的功能部件逐漸增多，隨著芯片設(shè)計(jì)越來(lái)越復(fù)雜，驗(yàn)證工作在整個(gè)芯片設(shè)計(jì)中所占的比重也越來(lái)越大。如圖1.1所示，2003年，在100萬(wàn)邏輯門的SOC設(shè)計(jì)中，仿真驗(yàn)證工作在整個(gè)設(shè)計(jì)工作量中的比重達(dá)到50一80%D[503]，即項(xiàng)目中有超過(guò)一半的設(shè)計(jì)資源包括計(jì)算機(jī)和人力資源都在致力于設(shè)計(jì)驗(yàn)證工作。因此，隨著集成電路復(fù)雜度的增加，功能驗(yàn)證已經(jīng)成為集成電路開(kāi)發(fā)過(guò)程中的瓶頸，對(duì)驗(yàn)證方法進(jìn)行深入研究將有助于縮短集成電路的開(kāi)發(fā)周期，降低開(kāi)發(fā)成本，幫助制造商實(shí)現(xiàn)收入最大化。
【學(xué)位授予單位】：中國(guó)科學(xué)院研究生院（計(jì)算技術(shù)研究所）
【學(xué)位級(jí)別】：博士
【學(xué)位授予年份】：2004
【分類號(hào)】：TP332.2

【引證文獻(xiàn)】

相關(guān)期刊論文 前3條

1 鄧承諾;吳丹;黃威;戴葵;鄒雪城;;高效能ESCA協(xié)處理器驗(yàn)證技術(shù)研究[J];計(jì)算機(jī)工程與科學(xué);2014年01期

2 陳博文;郭琦;沈海華;;浮點(diǎn)乘加部件的自動(dòng)化形式驗(yàn)證[J];計(jì)算機(jī)研究與發(fā)展;2010年S1期

3 陳云霽;張健;沈海華;胡偉武;;一種基于SAT的運(yùn)算電路查錯(cuò)方法[J];計(jì)算機(jī)學(xué)報(bào);2007年12期

相關(guān)會(huì)議論文 前1條

1 陳博文;郭琦;沈海華;;浮點(diǎn)乘加部件的自動(dòng)化形式驗(yàn)證[A];第六屆中國(guó)測(cè)試學(xué)術(shù)會(huì)議論文集[C];2010年

相關(guān)碩士學(xué)位論文 前4條

1 鄒科;基于Alloy的群論定理的機(jī)器驗(yàn)證[D];遼寧師范大學(xué);2018年

2 李婉;群論問(wèn)題的形式化及驗(yàn)證研究[D];西南交通大學(xué);2017年

3 李黎明;代數(shù)系統(tǒng)和復(fù)數(shù)理論的形式化及DS編碼器的驗(yàn)證應(yīng)用[D];首都師范大學(xué);2012年

4 劉超;基于模型檢驗(yàn)的飛機(jī)系統(tǒng)安全性分析方法研究[D];南京航空航天大學(xué);2012年

本文編號(hào)：2690385