Test Pattern Generation using Boolean Proof Engines
For further information on the book and an overview of the contents the
preface is also online available at Springer in
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.
Rolf Drechsler received his diploma and Dr. phil. nat. degree in computer science from the J.W.
Goethe-University in Frankfurt am Main, Germany, in 1992 and 1995, respectively. He was with the
Institute of Computer Science at the Albert-Ludwigs-University of Freiburg im Breisgau, Germany
from 1995 to 2000. He joined the Corporate Technology Department of Siemens AG, Munich in 2000,
where he worked as a Senior Engineer in the formal verification group. Since October 2001 he has
been with the University of Bremen, Germany, where he is now a full professor for computer
architecture. His research interests include data structures logic synthesis, test, and
Stephan Eggersglüß received his diploma in Computer Science from the
University of Bremen, Bremen, Germany in 2006. In this year, he also was
with the Design-for-Test group of Philips Semiconductors, Hamburg,
Germany. Since then he has been with the computer architecture group at
the University of Bremen, Bremen, Germany working towards his doctor
degree. His research interests include the satisfiability problem, test
in general, and delay test generation in particular.
Görschwin Fey received his Diploma in Computer Science from the Martin-Luther Universität,
Halle-Wittenberg, Germany in 2001. Since then he has been with the research group of computer
architecture at the University of Bremen, where he received the Dr. degree in 2006.
He is also with the VLSI Design & Education Center (VDEC) at the University of Tokyo during 2007
and 2008 as a visiting professor. His research interests are in testing and formal verification
of circuits and systems.
Daniel Tille received his diploma in Computer Science from the
Martin-Luther-University Halle-Wittenberg, Germany in 2006. Since then
he has been with the computer architecture group at the University of
Bremen, Germany. His research interests include the satisfiability
problem, test, and formal methods.