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

【摘要】：隨著芯片復(fù)雜度的急劇增加,模擬仿真驗證不能保證測試向量的完備性,尤其是一些邊界情況。形式驗證方法因其完整的狀態(tài)空間遍歷性和良好的完備性,被業(yè)界應(yīng)用于設(shè)計規(guī)模不大的模塊和子單元中。針對處理器浮點運(yùn)算單元,采用Cadence公司JasperGold工具對一些關(guān)鍵模塊進(jìn)行了形式化驗證,對流水控制中的糾錯碼(Error Correcting Code,ECC)、軟件結(jié)構(gòu)寄存器(Software Architected Register,SAR)和計算單元中的公共模塊分別采用了基于FPV(Formal Property Veri fication)的性質(zhì)檢驗和基于SEC(Sequential Equivalence Checking)的等價性檢驗。結(jié)果表明,形式化驗證在保證設(shè)計正確性的基礎(chǔ)上極大地縮短了驗證周期。
[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è)計規(guī)模和復(fù)雜度增加,系統(tǒng)設(shè)計的功能驗證面臨著嚴(yán)峻挑戰(zhàn)。據(jù)統(tǒng)計,驗證的時間和人力投入已占到整個設(shè)計的50%以上,用于測試和錯誤診斷的代價超過了產(chǎn)品實現(xiàn)成本的50%。因此,推出一種新的驗證方法成為驗證界的熱點和難點。 傳統(tǒng)的模擬驗證方法,基于軟件

【參考文獻(xiàn)】

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

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

【共引文獻(xiàn)】

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

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

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

【相似文獻(xiàn)】

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

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

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

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

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

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

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

本文編號：1478521