结合ATPG和SAT的无界模型检验前像计算方法

摘要：

提出一种无界模型检验的前像计算方法,该方法有效地结合ATPG和SAT引擎,充分利用引擎各自的优点.SAT用来判断是否已经穷尽所有解;每次SAT枚举出一个前像解后,采用一个专门的ATPG过程减少状态变量上的赋值,从而减少前像解的总个数,加快后面的不动点迭代处理.最后通过在ISCAS89和ITC99电路上的实验证明了文中方法的有效性.

关键词：形式验证、无界模型检验、前像计算、自动化测试激励生成、布尔可满足性问题

所属期刊栏目：19

分类号：TP3(计算技术、计算机技术)

资助基金：国家重点基础研究发展计划973计划2005CB321605;国家自然科学基金60633060

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

页数：共5页

页码：376-380