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

摘要：

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

关键词： 浮点运算部件 形式化方法 自动化形式验证

作者: 陈博文 郭琦 沈海华

作者单位: 中国科学院计算技术研究所,北京 100190

会议类型: 国内会议

会议名称: 第六届中国测试学术会议

会议地点: 合肥

会议语种:中文

页码: 569-574

在线出版日期: 2010-07-24（万方平台首次上网日期，不代表论文的发表时间）