TG-Pro: A SAT-based ATPG System

Automatic Test Pattern Generation (ATPG) is arguably one of the practical applications that motivated the development of modern Boolean Satisfiability (SAT) solvers in the mid 90s. Despite the interest of using SAT in ATPG, the original model remained mostly unchanged for nearly two decades, even in the presence of renewed interest in applying modern SAT technology to large-scale hardware designs. This paper describes the SAT-based ATPG system TG-Pro. In contrast to all SAT-based ATPG work over the last two decades, TG-Pro is based on a new fundamentally different SAT-based ATPG model. Experimental results, obtained on well-known and publicly available benchmarks, demonstrate that TG-Pro achieves major performance improvements over other well-established SAT-based ATPG models.