基于AI加速的可复用FPV平台库

形式验证FPV可将DUT抽象为状态空间进行遍历,针对动态仿真难以随机到的边界场景、异常场景和复杂组合场景可提高收敛速度,增强验证质量。但高质量Property开发对验证人员能力有较高的要求。面对该挑战,基于Cadence公司Jaspergold ABVIP提出了一种可复用FPV平台库解决方案,可在不同模块之间重用,降低FPV验证平台搭建时间,提升Property质量,同时借助其AI工具Proof Master生成加速Proven效率的database。FPV平台库+AI Database已在中兴微电子某车规项目落地并复用,发现动态仿真遗漏的4个故障。Proof Master可应用于项目全周期内,回归效率平均提升80.17%,FPV平台库+AI database可提升FPV初次Proven效率44.96%。与此同时对生成式大模型提升Property编写效率做了一定探讨。

保序模块的formal fpv验证

与simulation验证相比,formal验证方法可以在短时间内遍历所有可能的激励,大大提高验证的效率。保序模块与时序控制以及流水线控制密切相关,设计规模较大,逻辑复杂度较高。介绍了使用formal fpv验证保序模块的流程,并对JasperGold debug结果进行了分析,采用formal fpv验证能提高验证效率,加快验证收敛速度。

形式化验证在处理器浮点运算单元中的应用

随着芯片复杂度的急剧增加,模拟仿真验证不能保证测试向量的完备性,尤其是一些边界情况。形式验证方法因其完整的状态空间遍历性和良好的完备性,被业界应用于设计规模不大的模块和子单元中。针对处理器浮点运算单元,采用Cadence公司JasperGold工具对一些关键模块进行了形式化验证,对流水控制中的纠错码(Error Correcting Code,ECC)、软件结构寄存器(Software Architected Register,SAR)和计算单元中的公共模块分别采用了基于FPV(Formal Property Veri fication)的性质检验和基于SEC(Sequential Equivalence Checking)的等价性检验。结果表明,形式化验证在保证设计正确性的基础上极大地缩短了验证周期。