文獻(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ì)測試點(diǎn)的覆蓋程度上來說，兩者的區(qū)別在于simulation著眼于測試空間中的單個(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://m.ihrv.cn/resource/share/2000004647。
作者信息：
趙亞雪，植 玉，梁其鋒，石義軍
(深圳市中興微電子技術(shù)有限公司，廣東 深圳518054)
