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

作     者：陈云霁 马麟 沈海华 胡伟武 Chen Yunji;Ma Lin;Shen Haihua;Hu Weiwu

作者机构：中国科学院计算技术研究所微处理器研究中心北京100080 

出 版 物：《计算机研究与发展》 (Journal of Computer Research and Development)

年 卷 期：2006年第43卷第10期

页      面：1835-1841页

核心收录：

学科分类：08[工学] 081202[工学-计算机软件与理论] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

基　　金：国家"九七三"重点基础研究发展规划基金项目(2005CB321600) 国家自然科学基金杰出青年基金项目(60325205) 国家"八六三"高技术研究发展计划重点基金项目(2002AA110010 2005AA110010 2005AA119020) 中国科学院计算技术研究所基础研究基金项目(20056020) 中国科学院计算技术研究所知识创新课题基金项目(20056240) 

主　　题：形式验证 PHDD 字级模型检验 SAT CNF 有界模型检验 

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