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

作     者：朱峰 鲁征浩 朱青 Zhu Feng;Lu Zhenghao;Zhu Qing

作者机构：苏州大学江苏苏州215006 

出 版 物：《电子技术应用》 (Application of Electronic Technique)

年 卷 期：2017年第43卷第2期

页      码：29-32页

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

主 题 词：浮点运算单元 形式化验证 Jasper Gold FPV SEC 

学科分类：080903[080903] 0809[工学-计算机类] 08[工学] 081202[081202] 0812[工学-测绘类] 

D　O　I：10.16157/j.issn.0258-7998.2017.02.005

馆 藏 号：203215682...