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

发布时间：2018-01-31 06:58

本文关键词： 浮点运算单元形式化验证 JasperGold FPV SEC　出处：《电子技术应用》2017年02期 　论文类型：期刊论文

【摘要】：随着芯片复杂度的急剧增加,模拟仿真验证不能保证测试向量的完备性,尤其是一些边界情况。形式验证方法因其完整的状态空间遍历性和良好的完备性,被业界应用于设计规模不大的模块和子单元中。针对处理器浮点运算单元,采用Cadence公司JasperGold工具对一些关键模块进行了形式化验证,对流水控制中的纠错码(Error Correcting Code,ECC)、软件结构寄存器(Software Architected Register,SAR)和计算单元中的公共模块分别采用了基于FPV(Formal Property Veri fication)的性质检验和基于SEC(Sequential Equivalence Checking)的等价性检验。结果表明,形式化验证在保证设计正确性的基础上极大地缩短了验证周期。
[Abstract]:With the rapid increase of chip complexity, simulation verification can not guarantee the completeness of test vectors, especially in some boundary cases. Formal verification method is due to its complete state space ergodicity and good completeness. It is applied to the module and sub-unit of small design scale in the industry, aiming at the floating-point operation unit of the processor. Some key modules are formally validated by JasperGold tools of Cadence Company. Error Correcting code in income control. Software Architected Register. SAR) and the common modules in the unit are based on FPV(Formal Property Veri validation and SEC-based, respectively. The equivalence test of Sequential Equivalence checking. Formal verification greatly shortens the verification cycle on the basis of ensuring the correctness of the design.
【作者单位】：苏州大学;
【分类号】：TP332
【正文快照】： 0 引言随着集成电路设计规模和复杂度增加,系统设计的功能验证面临着严峻挑战。据统计,验证的时间和人力投入已占到整个设计的50%以上,用于测试和错误诊断的代价超过了产品实现成本的50%。因此,推出一种新的验证方法成为验证界的热点和难点。传统的模拟验证方法,基于软件

【参考文献】