保序模块的formal fpv验证
2022年电子技术应用第8期
赵亚雪，植 玉，梁其锋，石义军
深圳市中兴微电子技术有限公司，广东 深圳518054
摘要： 与simulation验证相比，formal验证方法可以在短时间内遍历所有可能的激励，大大提高验证的效率。保序模块与时序控制以及流水线控制密切相关，设计规模较大，逻辑复杂度较高。介绍了使用formal fpv验证保序模块的流程，并对JasperGold debug结果进行了分析，采用formal fpv验证能提高验证效率，加快验证收敛速度。
中圖分類號： TN402
文獻識別碼： A
DOI：10.16157/j.issn.0258-7998.229801
中文引用格式： 趙亞雪，植玉，梁其鋒，等. 保序模塊的formal fpv驗證[J].電子技術應用，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.
文獻識別碼： A
DOI：10.16157/j.issn.0258-7998.229801
中文引用格式： 趙亞雪，植玉，梁其鋒，等. 保序模塊的formal fpv驗證[J].電子技術應用，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 引言
芯片驗證方向經過多年的探索和積累已經有一套較為完備的驗證體系[1]。其中，simulation驗證和formal驗證是兩大常用的驗證方法。從對測試點的覆蓋程度上來說，兩者的區別在于simulation著眼于測試空間中的單個點，而formal驗證可以完全覆蓋輸入空間，從而能在約束條件下有效證明設計的準確度[2]，formal驗證方法能在短時間內遍歷所有可能的激勵，從而大大提高驗證效率[3]，因此近年來formal驗證方法得到了越來越多的關注。
formal驗證工具大體可以分為兩類[4]，一類是MFV(Mainstream Formal Verification)，其具有成熟的功能，能實現高度自動化驗證。另一類是FPV(Formal Property Verification)，需要手動開發驗證環境，編寫property[5]。對于邏輯較為復雜、難以調用工具自帶模型的模塊更傾向于選擇FPV工具來進行驗證。
保序模塊用于確保處理器內部讀、寫訪問嚴格按照既定的順序處理，其與時序控制以及流水線控制密切相關，設計規模較大，邏輯復雜度較高，采用formal fpv工具，本文按照驗證對象介紹、Design Review、驗證環境搭建、驗證模型編寫、JasperGold debug的流程來展開介紹。
本文詳細內容請下載：http://www.tom3567.com/resource/share/2000004647。
作者信息：
趙亞雪，植 玉，梁其鋒，石義軍
(深圳市中興微電子技術有限公司，廣東 深圳518054)
此內容為AET網站原創，未經授權禁止轉載。