Pankaj P. Chauhan

Verification of Large Industrial Circuits Using SAT Based Reparameterization and Automated Abstraction-Refinement Degree Type: Ph.D. in Computer Science
Advisor(s): Edmund Clarke
Graduated: May 2007

Abstract:

Automatic formal verification of large industrial circuits with thousands of latches is still a major challenge today due to the state space explosion problem. Moreover, BDD based algorithms are very sensitive to the variable ordering. Satisfiability (SAT) procedures have become much more powerful over the last few years, and hence they have been used in formal verification of large circuits with techniques like automated abstraction refinement and ATPG.

This thesis addresses the capacity challenge at multiple levels. First, at the core, I provide new algorithms for both BDD based and SAT based image computation. Image computation involves efficient quantification of variables from Boolean functions. I propose BDD based algorithms that use various combinatorial optimization techniques to obtain better quantification schedules, and in the later part, consider novel non-linear quantification schedules. The SAT based image computation uses algorithms for efficiently enumerating satisfying assignments to a Boolean formula, and for storing the enumerated assignments. Building upon this enumeration algorithm, I propose a novel SAT based reparameterization algorithm that increases the capacity of symbolic simulation by large extent. The reparameterization algorithm recomputes a much smaller representation for the set of states, whenever the size of the representation of state set becomes too large in symbolic simulation. These improvements help in bounded model checking of large systems, by allowing for much deeper depths. I demonstrate a 3x improvement in the runtime and space requirement over existing BMC algorithm and BDD based symbolic simulator on large industrial circuits. Finally, the reparameterization algorithm is incorporated in a SAT based automated abstraction-refinement framework. The reparamaterization algorithm can simulate much longer abstract counterexamples than previously possible. I then extract the refinement information from the simulation, completing the abstraction refinement loop. Thus, contributions beginning at the core problem of image computation, through state space travesals and continuing all the way up to the abstraction-refinement are addressed in this thesis.

Thesis Committee:
Edmund M. Clarke (Chair)
Randal E. Bryant
James Hoe
Jin Yang (Intel)

Jeannette Wing, Head, Computer Science Department
Randy Bryant, Dean, School of Computer Science

Keywords:
Model checking, image computation, quantification scheduling, SAT, bounded model checking, parametric representation, abstraction-refinement