《電子技術(shù)應(yīng)用》
您所在的位置：首頁 > 其他 > 設(shè)計應(yīng)用 > 保序模塊的formal fpv驗證
保序模塊的formal fpv驗證
2022年電子技術(shù)應(yīng)用第8期
趙亞雪,，植 玉,，梁其鋒，石義軍
深圳市中興微電子技術(shù)有限公司,，廣東 深圳518054
摘要： 與simulation驗證相比,，formal驗證方法可以在短時間內(nèi)遍歷所有可能的激勵，大大提高驗證的效率,。保序模塊與時序控制以及流水線控制密切相關(guān),，設(shè)計規(guī)模較大，邏輯復雜度較高,。介紹了使用formal fpv驗證保序模塊的流程,，并對JasperGold debug結(jié)果進行了分析，采用formal fpv驗證能提高驗證效率,，加快驗證收斂速度,。
關(guān)鍵詞： formal FPV 保序模塊 JasperGold
中圖分類號： TN402
文獻識別碼： 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.
Formal FPV verification of sequence preserving module
Zhao Yaxue，Zhi Yu,，Liang Qifeng，Shi Yijun
Shenzhen Sanechips Technology Co.,，Ltd.,，Shenzhen 518054，China
Abstract： Compared with simulation verification, the formal verification method can traverse all possible incentives in a short time, which greatly improves the efficiency of verification. The sequence preserving module is closely related to timing control and pipeline control, with large design scale and high logic complexity. This paper introduces the process of verifying the sequence preserving module using formal FPV, and analyzes the JasperGold debug results. Formal FPV verification can improve the verification efficiency and accelerate the verification convergence speed.
Key words : formal,；FPV,；sequence preserving module；JasperGold

0 引言

    芯片驗證方向經(jīng)過多年的探索和積累已經(jīng)有一套較為完備的驗證體系[1],。其中,，simulation驗證和formal驗證是兩大常用的驗證方法。從對測試點的覆蓋程度上來說,，兩者的區(qū)別在于simulation著眼于測試空間中的單個點,，而formal驗證可以完全覆蓋輸入空間,，從而能在約束條件下有效證明設(shè)計的準確度[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],。對于邏輯較為復雜,、難以調(diào)用工具自帶模型的模塊更傾向于選擇FPV工具來進行驗證。

    保序模塊用于確保處理器內(nèi)部讀,、寫訪問嚴格按照既定的順序處理,，其與時序控制以及流水線控制密切相關(guān)，設(shè)計規(guī)模較大,，邏輯復雜度較高,，采用formal fpv工具，本文按照驗證對象介紹,、Design Review,、驗證環(huán)境搭建、驗證模型編寫,、JasperGold debug的流程來展開介紹,。




本文詳細內(nèi)容請下載：http://wldgj.com/resource/share/2000004647。




作者信息：

趙亞雪,，植  玉,，梁其鋒，石義軍

(深圳市中興微電子技術(shù)有限公司,，廣東 深圳518054)




wd.jpg

此內(nèi)容為AET網(wǎng)站原創(chuàng),，未經(jīng)授權(quán)禁止轉(zhuǎn)載。