龙芯2号微处理器浮点除法功能部件的形式验证

陈云霁; 马麟; 沈海华; 胡伟武

首页> 中文期刊> 《计算机研究与发展》 >龙芯2号微处理器浮点除法功能部件的形式验证

龙芯2号微处理器浮点除法功能部件的形式验证

开具论文收录证明 >>

期刊封面封底目录下载 >>

文献代查 >>

页面导航

摘要
著录项
相似文献
相关主题

摘要

基于决策图的字级模型检验方法虽然能完全验证运算电路,但它从有缺陷的设计中发现系统规范的反例所需时间较长.而基于SAT的有界模型检验方法虽然能较快地发现反例,但它不支持包含数学公式的系统规范,因而难以用于验证运算电路.提出了基于SAT的字级模型检验方法,该方法将CNF扩展为能混合布尔公式和数学公式的E-CNF用以表示设计和系统规范,并对有界模型检验工具和SAT求解器进行字级的扩展,使它们能分别生成和处理E-CNF.龙芯2号微处理器浮点除法功能部件验证同时采用了基于*PHDD和基于SAT的字级模型检验方法.数据表明,基于SAT的字级模型检验方法能快速地发现运算电路中的设计缺陷.两种方法互为补充,在能完全验证设计的同时显著缩短了设计周期.

著录项

来源
《计算机研究与发展》 |2006年第10期|1835-1841|共7页
作者
陈云霁; 马麟; 沈海华; 胡伟武;
展开▼
作者单位

中国科学院计算技术研究所微处理器研究中心;

北京;

100080;

中国科学院计算技术研究所微处理器研究中心;

北京;

100080;

中国科学院计算技术研究所微处理器研究中心;

北京;

100080;

中国科学院计算技术研究所微处理器研究中心;

北京;

100080;

展开▼
原文格式 PDF
正文语种 chi
中图分类计算技术、计算机技术;
关键词
形式验证; *PHDD; 字级模型检验; SATCNF; 有界模型检验;

相似文献

中文文献
外文文献
专利

1. 中国微处理器(秋季)论坛:微处理器巨擎云集,畅想明天——ARM、Intel、IBM、龙芯等讲演,院士、理事长助阵 [J] . 高威 ,王莹 . 电子产品世界 . 2006,第019期
2. 浮点乘加部件的自动化形式验证 [J] . 陈博文 ,郭琦 ,沈海华 . 计算机研究与发展 . 2010,第S1期
3. 龙芯2号处理器功能部件设计 [J] . 张戈 ,齐子初 ,胡伟武 . 计算机研究与发展 . 2006,第006期
4. 基于UVM的浮点功能部件验证 [J] . 吴升光 ,羊箭锋 ,冯春阳 . 微电子学与计算机 . 2017,第4期
5. 龙芯微处理器控制板在大学生设计竞赛中的应用 [J] . 牟峰 . 科教导刊-电子版（下旬） . 2020,第010期
6. 基于CORDIC算法实现浮点功能部件的关键技术研究 [C] . 岳虹 ,戴葵 ,王志英 . 第九届计算机工程与工艺全国学术年会 . 2005
7. 高性能浮点除法及基本函数功能部件的研究 [A] . 刘华平 . 2003

龙芯2号微处理器浮点除法功能部件的形式验证

摘要

著录项

相似文献

相关主题

期刊订阅