应用吴方法进行高层次定界模型检验  

High-Level Bounded Model Checking Using Wu's Method

作　　者：杨志[1] 马光胜[1] 冯刚[1] 邵晶波 

机构地区：[1]哈尔滨工程大学计算机科学与技术学院,哈尔滨150001

出　　处：《计算机辅助设计与图形学学报》2008年第2期137-143,共7页Journal of Computer-Aided Design & Computer Graphics

基　　金：国家自然科学基金(60273081)

摘　　要：以吴方法为理论基础,提出一种针对高层次设计验证的定界模型检验方法·通过使用多项式等式建模高层次设计和待验证性质,将定界模型检验问题转化为定理证明问题,并用吴方法有效地解决该定理证明问题·实验结果表明,与基于布尔SAT、基于LP的RTLSAT以及基于非线性求解器的性质检验方法相比,该方法在时间消耗上具有相当大的优势·A bounded model checking method for the high-level design verification using Wu＇s method is proposed. By modeling high-level designs and targeting properties as polynomial equations, bounded model checking is reduced to the task of theorem proving, which can be solved by Wu＇ s method efficiently. Experimental results demonstrated the superiority in time consumption of the proposed approach compared with the property checking methods based on Boolean SAT, LP-based RTL SAT and non-linear solver.

关 键 词：高层次设计 定界模型检验 吴方法 形式验证 

分 类 号：TP391.7[自动化与计算机技术—计算机应用技术]