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

以吴方法为理论基础,提出一种针对高层次设计验证的定界模型检验方法.通过使用多项式等式建模高层次设计和待验证性质,将定界模型检验问题转化为定理证明问题,并用吴方法有效地解决该定理证明问题.实验结果表明,与基于布尔SAT、基于LP的RTL SAT以及基于非线性求解器的性质检验方法相比,该方法在时间消耗上具有相当大的优势.

High-Level Bounded Model Checking Using Wu's Method

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.