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