In Test Pattern Generation using Boolean Proof Engines, we give an
introduction to ATPG. The basic concept and classical ATPG algorithms
are reviewed. Then, the formulation as a SAT problem is considered. As
the underlying engine, modern SAT solvers and their use on circuit
related problems are comprehensively discussed. Advanced techniques for
SAT-based ATPG are introduced and evaluated in the context of an
industrial environment. The chapters of the book cover efficient
instance generation, encoding of multiple-valued logic, usage of various
fault models, and detailed experiments on multi-million gate designs.
The book describes the state of the art in the field, highlights
research aspects, and shows directions for future work.