浮点乘加部件的自动化形式验证  

Automatic Formal Verification of Floating-Point Fused Multiply-Add Unit

作　　者：陈博文[1,2] 郭琦[1] 沈海华[1] 

机构地区：[1]中国科学院计算技术研究所,北京100190 [2]中国科学院研究生院,北京100049

出　　处：《计算机研究与发展》2010年第S1期262-267,共6页Journal of Computer Research and Development

基　　金：国家"九七三"重点基础研究发展计划基金项目(2005CB321600);国家"八六三"高技术研究发展计划基金项目(2008AA110901);国家自然科学基金项目(60803029;60736012;60921002);北京市自然科学基金项目(4072024);国家"核高基"科技重大专项课题基金项目(2009ZX01029-001-003;2009ZX01028-002-003)

摘　　要：浮点运算部件的功能验证是处理器设计验证中重要的一环.相对于传统的模拟仿真方法,形式化方法具有验证完备且时间短的优点.给出了一种浮点乘加部件的形式化验证方法.该方法基于BDD和*PHDD,将设计分为3部分多种情况分别验证.其优点在于自动化程度高、划分粒度粗、可广泛适用于工业级设计.该方法已应用于龙芯3A浮点乘加部件的验证,验证结果显示出该方法具有良好的时空复杂度.浮点运算部件的功能验证是处理器设计验证中重要的一环.相对于传统的模拟仿真方法,形式化方法具有验证完备且时间短的优点.给出了一种浮点乘加部件的形式化验证方法.该方法基于BDD和*PHDD,将设计分为3部分多种情况分别验证.其优点在于自动化程度高、划分粒度粗、可广泛适用于工业级设计.该方法已应用于龙芯3A浮点乘加部件的验证,验证结果显示出该方法具有良好的时空复杂度.

关 键 词：形式化验证 运算电路 乘加部件 BDD *PHDD 

分 类 号：TP3[自动化与计算机技术—计算机科学与技术]