SAT based Abstraction Refinement for Hardware Verification

opinions, findings and conclusions or recommendations expressed in this material are those of the authors and do not necessarily reflect the views of GSRC, NSF, or the United States Government. Model checking is a widely used automatic formal verification technique. Despite the recent advances in model checking technology, its application is still limited by the state explosion problem. For model checking large real world systems, abstraction is essential. This thesis investigates abstraction techniques for the efficient verification of hardware designs with thousands of registers. A technique, called SAT conflict dependency analysis, is developed and used to derive several efficient abstraction algorithms. If a CNF formula is unsatisfiable, this technique can extract a proof of unsatisfiability by analyzing conflict clauses and conflict graphs generated by the SAT procedure. In this thesis, we propose two new algorithms to improve the efficienc