A Two-Variable Model for SAT-Based ATPG

Automatic test pattern generation (ATPG) is one of the first applications that motivated the development of modern Boolean satisfiability (SAT). It is now widely accepted that ATPG is easy for current state-of-the-art SAT solvers. Nevertheless, as with any NP-hard problem, for large complex industrial circuits, some faults may be difficult to detect or prove undetectable. Recent work on SAT-based ATPG has been motivated by industrial designs with ever increasing size, for which more efficient ATPG models are essential. Moreover, ATPG models and algorithms find applications in a number of other settings, which further motivate the development of more efficient SAT-based ATPG solutions. Interestingly, despite the interest in more efficient ATPG approaches, the core SAT-based ATPG model has remained essentially unchanged since it was first proposed in the 1980s. This paper describes an alternative 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. This paper proposes extensions and optimizations to the basic model, and integrates known techniques for further improving performance. This paper extends the new model, proposes optimizations to it, and integrates known techniques for further improving performance. To achieve an unbiased evaluation, this paper also reimplements previous models and comprehensively compares them with the proposed models. Experimental results, obtained on a wide range of publicly available benchmarks for ATPG, demonstrate that the basic model and extended models allow significant performance improvements over other well-established models.