Introduction

To make a long story short, finding tests to detect failures in complex circuits (Automatic Test Pattern Generation, ATPG) is a hard computational problem. Due to exponentially increasing circuit sizes, traditional ATPG algorithms reach their limits. Solvers for Boolean Satisfiability (SAT) recently showed their potential on real world ATPG problems. Thus, SAT-based ATPG is a promising alternative solution for this threatening bottleneck in circuit design when facing this rapid growth. Why do we need to test? Why do current algorithms reach their limits? What is SAT? How may SAT-based ATPG help? The following longer story gives some answers.