SAT and ATPG: Boolean engines for formal hardware verification

13 years 11 months ago
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...
Armin Biere, Wolfgang Kunz
Added 16 Mar 2010
Updated 16 Mar 2010
Type Conference
Year 2002
Authors Armin Biere, Wolfgang Kunz
Comments (0)