保序模塊的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.xxav2194.com/resource/share/2000004647。
作者信息：
趙亞雪，植 玉，梁其鋒，石義軍
(深圳市中興微電子技術有限公司，廣東 深圳518054)
此內容為AET網站原創，未經授權禁止轉載。