Verification using Satisfiability Checking, Predicate Abstraction, and Craig Interpolation
Abstract
Automatic verification of hardware and software implementations is crucial for computer systems. This thesis develops new techniques for building efficient decision procedures and adds new capabilities to existing decision procedures. Most SAT solvers require the input formula to be in Conjunctive Normal Form (CNF). However, typical formulas that arise in practice are not in CNF. Converting a general formula to CNF introduces overhead in the form of new variables and may destroy the structure of the initial formula. We present two non-clausal SAT algorithms that operate on the Negation Normal Form (NNF) of the given formula. The first algorithm is based on the idea of General Matings. The second algorithm applies the DPLL algorithm to NNF formulas. We devise new algorithms for performing Boolean Constraint Propagation (BCP). Most hardware verification tools convert a high level design into a low level representation called a netlist for verification. However, algorithms that operate at the netlist level are unable to exploit the structure of the higher abstraction levels, and thus, are less scalable. This thesis proposes the use of predicate abstraction for verifying register transfer level (RTL) Verilog. There are two challenges when applying predicate abstraction to circuits: (i) The computation of the abstract model in the presence of a large number of predicates, and (ii) discovery of suitable word-level predicates for abstraction refinement. We address the first problem using a technique called predicate clustering. We address the second problem by computing weakest pre-conditions of Verilog statements in order to obtain new word-level predicates during abstraction refinement. We focus on subsets of integer linear arithmetic. Our main results are polynomial time algorithms for obtaining proofs of unsatisfiability and interpolants for conjunctions of linear diophantine equations, linear modular equations (linear congruences), and linear diophantine disequations.
Document Details
- Document Type
- Technical Report
- Publication Date
- Sep 01, 2008
- Accession Number
- ADA493221
Entities
People
- Himanshu Jain
Organizations
- Carnegie Mellon University