保序模块的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、验证环境搭建、验证模型编写、JasperGolddebug的流程来展开介绍。
本文详细内容请下载：http://www.chinaaet.com/resource/share/2000004647。
作者信息：
赵亚雪，植 玉，梁其锋，石义军
(深圳市中兴微电子技术有限公司，广东 深圳518054)
此内容为AET网站原创，未经授权禁止转载。