Accession Number:

ADA493221

Title:

Verification using Satisfiability Checking, Predicate Abstraction, and Craig Interpolation

Descriptive Note:

Doctoral thesis

Corporate Author:

CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE

Personal Author(s):

Report Date:

2008-09-01

Pagination or Media Count:

297.0

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.

Subject Categories:

  • Computer Programming and Software
  • Computer Hardware

Distribution Statement:

APPROVED FOR PUBLIC RELEASE