Combining ATPG and SAT for Preimage Computation in Unbounded Model Checking

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 ISCAS 89and ITC 99 benchmark demonstrate the effectiveness of our proposed approach.