《電子技術(shù)應(yīng)用》
您所在的位置：首頁(yè) > 其他 > 設(shè)計(jì)應(yīng)用 > 保序模塊的formal fpv驗(yàn)證
保序模塊的formal fpv驗(yàn)證
2022年電子技術(shù)應(yīng)用第8期
趙亞雪，植 玉，梁其鋒，石義軍
深圳市中興微電子技術(shù)有限公司，廣東 深圳518054
摘要： 與simulation驗(yàn)證相比，formal驗(yàn)證方法可以在短時(shí)間內(nèi)遍歷所有可能的激勵(lì)，大大提高驗(yàn)證的效率。保序模塊與時(shí)序控制以及流水線控制密切相關(guān)，設(shè)計(jì)規(guī)模較大，邏輯復(fù)雜度較高。介紹了使用formal fpv驗(yàn)證保序模塊的流程，并對(duì)JasperGold debug結(jié)果進(jìn)行了分析，采用formal fpv驗(yàn)證能提高驗(yàn)證效率，加快驗(yàn)證收斂速度。
關(guān)鍵詞： formal FPV 保序模塊 JasperGold
中圖分類號(hào)： TN402
文獻(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.
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 引言

    芯片驗(yàn)證方向經(jīng)過(guò)多年的探索和積累已經(jīng)有一套較為完備的驗(yàn)證體系[1]。其中，simulation驗(yàn)證和formal驗(yàn)證是兩大常用的驗(yàn)證方法。從對(duì)測(cè)試點(diǎn)的覆蓋程度上來(lái)說(shuō)，兩者的區(qū)別在于simulation著眼于測(cè)試空間中的單個(gè)點(diǎn)，而formal驗(yàn)證可以完全覆蓋輸入空間，從而能在約束條件下有效證明設(shè)計(jì)的準(zhǔn)確度[2]，formal驗(yàn)證方法能在短時(shí)間內(nèi)遍歷所有可能的激勵(lì)，從而大大提高驗(yàn)證效率[3]，因此近年來(lái)formal驗(yàn)證方法得到了越來(lái)越多的關(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工具來(lái)進(jìn)行驗(yàn)證。

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




本文詳細(xì)內(nèi)容請(qǐng)下載：http://ihrv.cn/resource/share/2000004647。




作者信息：

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

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




wd.jpg

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