CMU-CS-04-139
Computer Science Department
School of Computer Science, Carnegie Mellon University



CMU-CS-04-139

Predicate Abstraction and Refinement Techniques for
Verifying Verilog

Edmund Clarke, Himanshu Jain, Daniel Kroening

June 2004

CMU-CS-04-139.ps
CMU-CS-04-139.pdf


Keywords: Predicate abstraction, Verilog, SAT


Model checking techniques applied to large industrial circuits suffer from the state explosion problem. A major technique to address this problem is abstraction. Predicate abstraction has been applied successfully to large software programs. Applying this technique to hardware designs poses additional challenges. This paper evaluates three techniques to improve the performance of SAT-based predicate abstraction of circuits: 1) We partition the abstraction problem by forming subsets of the predicates. The resulting abstractions are more coarse, but the computation of the abstract transition relation becomes easier. 2) We evaluate the performance effect of lazy abstraction, i.e., the abstraction is only performed if required by a spurious counterexample. 3) We use weakest preconditions of circuit transitions in order to obtain new predicates during refinement. We provide experimental results on publicly available benchmarks from the Texas97 benchmark suite.

26 pages


Return to: SCS Technical Report Collection
School of Computer Science homepage

This page maintained by reports@cs.cmu.edu