位置:成果数据库 > 期刊 > 期刊详情页
浮点乘加部件的自动化形式验证
  • ISSN号:1000-1239
  • 期刊名称:《计算机研究与发展》
  • 时间:0
  • 分类:TP3[自动化与计算机技术—计算机科学与技术]
  • 作者机构:中国科学院计算技术研究所, 中国科学院研究生院
  • 相关基金:国家“九七三”重点基础研究发展计划基金项目(2005CB321600);国家“八六三”高技术研究发展计划基金项目(2008AA110901);国家自然科学基金项目(60803029,60736012,60921002);北京市自然科学基金项目(4072024);国家“核高基”科技重大专项课题基金项目(2009ZX01029-001-003,2009ZX01028-002-003)
中文摘要:

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

英文摘要:

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

同期刊论文项目
期刊论文 118 会议论文 65
期刊论文 143 会议论文 81 获奖 3 专利 9 著作 4
同项目期刊论文
期刊信息
  • 《计算机研究与发展》
  • 中国科技核心期刊
  • 主管单位:中国科学院
  • 主办单位:中国科学院计算技术研究所
  • 主编:徐志伟
  • 地址:北京市科学院南路6号中科院计算所
  • 邮编:100190
  • 邮箱:crad@ict.ac.cn
  • 电话:010-62620696 62600350
  • 国际标准刊号:ISSN:1000-1239
  • 国内统一刊号:ISSN:11-1777/TP
  • 邮发代号:2-654
  • 获奖情况:
  • 2001-2007百种中国杰出学术期刊,2008中国精品科...,中国期刊方阵“双效”期刊
  • 国内外数据库收录:
  • 俄罗斯文摘杂志,荷兰文摘与引文数据库,美国工程索引,日本日本科学技术振兴机构数据库,中国中国科技核心期刊,中国北大核心期刊(2004版),中国北大核心期刊(2008版),中国北大核心期刊(2011版),中国北大核心期刊(2014版),中国北大核心期刊(2000版)
  • 被引量:40349