An ATPG Engine for Formal Verification

ATPG can generate patterns for testing integrated circuit chips, it is also an important engine for design verification In this paper, an algebraic algorithm for combinational circuits test generation is presented, it can also be an ATPG engine for combinational verification This algorithm makes full use of the advantages of binary decision diagram （BDD） and Boolean satisfiability （SAT） Through interleaving SAT based algorithm with BDD based algorithm with some heuristics, it avoids potential memory explosion caused by constructing BDDs Moreover, this algorithm uses incremental satisfiability, which improves the algorithm’s efficiency The experimental results demonstrate the effectiveness and feasibility of this algorithm