Instance Generation for SAT-based ATPG

Recently, there is a renewed interest in Automatic Test Pattern Generation (ATPG) based on Boolean Satisfiability (SAT). This results from the availability of very powerful SAT solvers that have been developed in the last few years. Studies have shown that SAT-based ATPG tools can clearly outperform classical approaches for hard-to-test faults. While the ATPG problem has to be solved on a circuit, SAT solvers work on Conjunctive Normal Forms (CNFs). In this paper the problem to efficiently generate a SAT instance from a circuit is studied. Experimental results on large industrial circuits show the efficiency of the approach.