TG-PRO: A new model for SAT-based ATPG

Automatic Test Pattern Generation (ATPG) represents one of the first practical applications of Boolean Satisfiability (SAT). Even though ATPG can in general be considered easy for current state of the art SAT solvers, it is also the case that specific faults can be difficult to detect or prove undetectable, namely for large industrial circuits. Recent work on SAT-based ATPG has been motivated by industrial designs with ever increasing size, for which more efficient ATPG tools are essential. Moreover, ATPG models and algorithms find application in a number of other settings, that further motivate the development of more efficient SAT-based ATPG solutions. Interestingly, despite the potential interest of more efficient ATPG approaches, the core SAT-based ATPG model has remained essentially unchanged since it was first proposed in the late 80s. This paper proposes a new model for SAT-based ATPG. The proposed model is fundamentally different from previous SAT-based ATPG models in that the number of used variables is significantly reduced. Experimental results, obtained on a wide range of publicly available benchmarks, demonstrate that the new model allows significant performance improvements over other well-established models.