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

Formal Verification of Godson-2 Microprocessor Floating-Point Division Unit

作　　者：陈云霁[1] 马麟[1] 沈海华[1] 胡伟武[1] 

机构地区：[1]中国科学院计算技术研究所微处理器研究中心,北京100080

出　　处：《计算机研究与发展》2006年第10期1835-1841,共7页Journal of Computer Research and Development

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

摘　　要：基于决策图的字级模型检验方法虽然能完全验证运算电路,但它从有缺陷的设计中发现系统规范的反例所需时间较长.而基于SAT的有界模型检验方法虽然能较快地发现反例,但它不支持包含数学公式的系统规范,因而难以用于验证运算电路.提出了基于SAT的字级模型检验方法,该方法将CNF扩展为能混合布尔公式和数学公式的E-CNF用以表示设计和系统规范,并对有界模型检验工具和SAT求解器进行字级的扩展,使它们能分别生成和处理E-CNF.龙芯2号微处理器浮点除法功能部件验证同时采用了基于PHDD和基于SAT的字级模型检验方法.数据表明,基于SAT的字级模型检验方法能快速地发现运算电路中的设计缺陷.两种方法互为补充,在能完全验证设计的同时显著缩短了设计周期.Word level model checking based on decision diagrams can verify arithmetic circuits completely, but its bug finding is time-consuming. SAT-based bounded model checking is powerful in bug finding, but it does not support specification with mathematic formula. In this paper, the SAT-based word level model checking method is presented. This method extends CNF to E-CNF which can represent both Boolean formula and mathematic formula, and extends bounded model checking and SAT solver to word level to cooperate with E-CNF. Experiments show that SAT-based model checking is powerful in bug finding for arithmetic circuit. The verification of floating-point division unit of Godson-2 microprocessor adopts both ~PHDD-based and SAT-based model checking methods. These two methods are excellently complementary to each other, giving the ability to completely verify design as well as shorten design＇ cycle.

关 键 词：形式验证 PHDD 字级模型检验 SAT CNF 有界模型检验 

分 类 号：TP301[自动化与计算机技术—计算机系统结构]