欢迎您！东篱公司
退出
-
申报数据库
-
立项数据库
-
成果数据库
-
项目获奖数据库
中文摘要：
基于决策图的字级模型检验方法虽然能完全验证运算电路，但它从有缺陷的设计中发现系统规范的反例所需时间较长．而基于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.
同期刊论文项目
同项目期刊论文
期刊信息
位置：