本文關(guān)鍵詞： 浮點(diǎn)運(yùn)算單元 形式化驗(yàn)證 JasperGold FPV SEC　出處：《電子技術(shù)應(yīng)用》2017年02期 　論文類型：期刊論文

【摘要】：隨著芯片復(fù)雜度的急劇增加,模擬仿真驗(yàn)證不能保證測試向量的完備性,尤其是一些邊界情況。形式驗(yàn)證方法因其完整的狀態(tài)空間遍歷性和良好的完備性,被業(yè)界應(yīng)用于設(shè)計(jì)規(guī)模不大的模塊和子單元中。針對處理器浮點(diǎn)運(yùn)算單元,采用Cadence公司JasperGold工具對一些關(guān)鍵模塊進(jìn)行了形式化驗(yàn)證,對流水控制中的糾錯碼(Error Correcting Code,ECC)、軟件結(jié)構(gòu)寄存器(Software Architected Register,SAR)和計(jì)算單元中的公共模塊分別采用了基于FPV(Formal Property Veri fication)的性質(zhì)檢驗(yàn)和基于SEC(Sequential Equivalence Checking)的等價性檢驗(yàn)。結(jié)果表明,形式化驗(yàn)證在保證設(shè)計(jì)正確性的基礎(chǔ)上極大地縮短了驗(yàn)證周期。
[Abstract]:With the rapid increase of chip complexity, simulation verification can not guarantee the completeness of test vectors, especially in some boundary cases. Formal verification method is due to its complete state space ergodicity and good completeness. It is applied to the module and sub-unit of small design scale in the industry, aiming at the floating-point operation unit of the processor. Some key modules are formally validated by JasperGold tools of Cadence Company. Error Correcting code in income control. Software Architected Register. SAR) and the common modules in the unit are based on FPV(Formal Property Veri validation and SEC-based, respectively. The equivalence test of Sequential Equivalence checking. Formal verification greatly shortens the verification cycle on the basis of ensuring the correctness of the design.
【作者單位】： 蘇州大學(xué);
【分類號】：TP332
【正文快照】： 0 引言 隨著集成電路設(shè)計(jì)規(guī)模和復(fù)雜度增加,系統(tǒng)設(shè)計(jì)的功能驗(yàn)證面臨著嚴(yán)峻挑戰(zhàn)。據(jù)統(tǒng)計(jì),驗(yàn)證的時間和人力投入已占到整個設(shè)計(jì)的50%以上,用于測試和錯誤診斷的代價超過了產(chǎn)品實(shí)現(xiàn)成本的50%。因此,推出一種新的驗(yàn)證方法成為驗(yàn)證界的熱點(diǎn)和難點(diǎn)。 傳統(tǒng)的模擬驗(yàn)證方法,基于軟件

【參考文獻(xiàn)】

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

1 陳云霽;馬麟;沈海華;胡偉武;;龍芯2號微處理器浮點(diǎn)除法功能部件的形式驗(yàn)證[J];計(jì)算機(jī)研究與發(fā)展;2006年10期

【共引文獻(xiàn)】

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

1 朱峰;魯征浩;朱青;;形式化驗(yàn)證在處理器浮點(diǎn)運(yùn)算單元中的應(yīng)用[J];電子技術(shù)應(yīng)用;2017年02期

2 吳曉非;;TURBO51嵌入式微處理器功能驗(yàn)證[J];微處理機(jī);2010年02期

【相似文獻(xiàn)】

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

1 王朋朋;;具有硬件矢量浮點(diǎn)運(yùn)算單元的微控制器在醫(yī)療電子中的應(yīng)用[J];電子技術(shù)應(yīng)用;2009年03期

2 張小妍;邵杰;;高速浮點(diǎn)運(yùn)算單元的FPGA實(shí)現(xiàn)[J];信息化研究;2009年11期

3 ;Cyrix新一代芯片內(nèi)核Jalapeno[J];電腦采購周刊;2000年S1期

4 許秋華;劉偉;;基于FPGA的浮點(diǎn)運(yùn)算單元的設(shè)計(jì)方法[J];大眾科技;2009年10期

5 張素萍;李紅剛;張慧堅(jiān);董定超;;單精度浮點(diǎn)運(yùn)算單元的FPGA設(shè)計(jì)與實(shí)現(xiàn)[J];計(jì)算機(jī)測量與控制;2011年05期

6 應(yīng)麗婭;張s，

本文編號：1478521