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.chinaaet.com/resource/share/2000004647。
作者信息：
赵亚雪，植 玉，梁其锋，石义军
(深圳市中兴微电子技术有限公司，广东 深圳518054)
此内容为AET网站原创，未经授权禁止转载。
