SAT and ATPG: Boolean engines for formal hardware verification

In this survey, we outline basic SAT- and ATPGprocedures as well as their applications in formal hardware verification. We attempt to give the reader a trace trough literature and provide a basic orientation concerning the problem formulations and known approaches in this active field of research. 1 Background Checking satisfiability (SAT) of propositional formulae in conjunctive normal form (CNF) is the classical NPcomplete problem. A formula is in CNF if it is a product of sums of literals. Many hard problems can be translated into a SAT problem. This has been the main motivation to work on good heuristics and algorithms. The idea is that once implemented in a generic SAT-solver good heuristics could be used and shared across multiple application Additionally, the abstract framework often allows to find general heuristics more easily than it would be possible with a narrow application point of view. The research around SAT-procedures started in the context of automated theorem provi...

• Type: Conference
• Year: 2002
• Where: ICCAD
• Authors: Armin Biere, Wolfgang Kunz
• Keywords: Fault Location, Fault Model, Hardware, ICCAD 2002, Large Sat Problems