欢迎您！东篱公司
退出
-
申报数据库
-
立项数据库
-
成果数据库
-
项目获奖数据库
中文摘要：
提出一种无界模型检验的前像计算方法，该方法有效地结合ATPG和SAT引擎，充分利用引擎各自的优点．SAT用来判断是否已经穷尽所有解；每次SAT枚举出一个前像解后，采用一个专门的ATPG过程减少状态变量上的赋值，从而减少前像解的总个数，加快后面的不动点迭代处理．最后通过在ISCAS89和ITC99电路上的实验证明了文中方法的有效性．
英文摘要：
This paper presents a preimage computation approach used in unbounded model checking. The approach combines ATPG and SAT engines effectively and makes full use of their respective advantages. First, a SAT solver is used to determine whether the preimage solution has been exhausted. When a preimage solution is generated by the SAT solver, a specific ATPG process is adopted to minimize the sets of assignments to state variables. This in turn reduces the number of all the preimage solutions and accelerates the fixed point iteration process. Experimental results on ISCAS89 and ITC99 benchmark demonstrate the effectiveness of our proposed approach.
位置：
同期刊论文项目
