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

Effective formal applications in CPU floating point unit

作　　者：朱峰[1] 鲁征浩[1] 朱青[1] 

机构地区：[1]苏州大学,江苏苏州215006

出　　处：《电子技术应用》2017年第2期29-32,共4页Application of Electronic Technique

摘　　要：随着芯片复杂度的急剧增加,模拟仿真验证不能保证测试向量的完备性,尤其是一些边界情况。形式验证方法因其完整的状态空间遍历性和良好的完备性,被业界应用于设计规模不大的模块和子单元中。针对处理器浮点运算单元,采用Cadence公司JasperGold工具对一些关键模块进行了形式化验证,对流水控制中的纠错码(Error Correcting Code,ECC)、软件结构寄存器(Software Architected Register,SAR)和计算单元中的公共模块分别采用了基于FPV(Formal Property Veri fication)的性质检验和基于SEC(Sequential Equivalence Checking)的等价性检验。结果表明,形式化验证在保证设计正确性的基础上极大地缩短了验证周期。With the increasing complexity of chip design, it is almost impossible to ensure the completeness of test space, especially corner cases. Formal verification is applied to block and subunit level design in industry due to systematic and efficient way to explore exhaustively all reachable state space. This paper describes our practical experiences and results with applying formal verification to floating point unit using Cadence JasperGold. Specially, FPV（Formal Property Verification） and SEC（Sequential Equivalence Checking） are applied to ECC（Error Correcting Code） as well as SAR（Software Architecture Register） in pipeline control and shared arithmetic modules respectively. The implemented results show that JasperGold improves verification quality with exposing corner cas- es, locates potential bugs accurately and speeds up verification achievement.

关 键 词：浮点运算单元 形式化验证 JASPER GOLD FPV SEC 

分 类 号：TN401[电子电信—微电子学与固体电子学] TP301[自动化与计算机技术—计算机系统结构]