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

摘要：

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

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

所属期刊栏目：20

分类号：TP391.7(计算技术、计算机技术)

资助基金：国家自然科学基金60273081

在线出版日期：2008-05-14（万方平台首次上网日期，不代表论文的发表时间）

页数：共7页

页码：137-143