文獻(xiàn)識(shí)別碼: A
DOI:10.16157/j.issn.0258-7998.229801
中文引用格式: 趙亞雪,,植玉,梁其鋒,,等. 保序模塊的formal fpv驗(yàn)證[J].電子技術(shù)應(yīng)用,,2022,48(8):38-41,,45.
英文引用格式: Zhao Yaxue,,Zhi Yu,,Liang Qifeng,,et al. Formal FPV verification of sequence preserving module[J]. Application of Electronic Technique,2022,,48(8):38-41,,45.
0 引言
芯片驗(yàn)證方向經(jīng)過多年的探索和積累已經(jīng)有一套較為完備的驗(yàn)證體系[1]。其中,,simulation驗(yàn)證和formal驗(yàn)證是兩大常用的驗(yàn)證方法,。從對(duì)測(cè)試點(diǎn)的覆蓋程度上來說,兩者的區(qū)別在于simulation著眼于測(cè)試空間中的單個(gè)點(diǎn),,而formal驗(yàn)證可以完全覆蓋輸入空間,,從而能在約束條件下有效證明設(shè)計(jì)的準(zhǔn)確度[2],formal驗(yàn)證方法能在短時(shí)間內(nèi)遍歷所有可能的激勵(lì),,從而大大提高驗(yàn)證效率[3],,因此近年來formal驗(yàn)證方法得到了越來越多的關(guān)注。
formal驗(yàn)證工具大體可以分為兩類[4],,一類是MFV(Mainstream Formal Verification),,其具有成熟的功能,,能實(shí)現(xiàn)高度自動(dòng)化驗(yàn)證。另一類是FPV(Formal Property Verification),,需要手動(dòng)開發(fā)驗(yàn)證環(huán)境,,編寫property[5]。對(duì)于邏輯較為復(fù)雜,、難以調(diào)用工具自帶模型的模塊更傾向于選擇FPV工具來進(jìn)行驗(yàn)證,。
保序模塊用于確保處理器內(nèi)部讀、寫訪問嚴(yán)格按照既定的順序處理,,其與時(shí)序控制以及流水線控制密切相關(guān),,設(shè)計(jì)規(guī)模較大,邏輯復(fù)雜度較高,,采用formal fpv工具,,本文按照驗(yàn)證對(duì)象介紹、Design Review,、驗(yàn)證環(huán)境搭建,、驗(yàn)證模型編寫、JasperGold debug的流程來展開介紹,。
本文詳細(xì)內(nèi)容請(qǐng)下載:http://forexkbc.com/resource/share/2000004647,。
作者信息:
趙亞雪,植 玉,,梁其鋒,,石義軍
(深圳市中興微電子技術(shù)有限公司,廣東 深圳518054)