VLSI CADhas greatly bene?ted from the use of reduced ordered Binary Decision Diagrams (BDDs) and the clausal representation as a problem of Boolean Satis?ability (SAT), e.g. in logic synthesis, ver- c
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 conside
