Model checking techniques applied to large industrial circuits suffer from the state space explosion problem. A major technique to address this problem is abstraction. While predicate abstraction has been applied successfully to large software programs, it is hardly used for hardware. This paper adopts software model checking techniques for the verification of word-level models of circuits. Furthermore, the performance of predicate abstraction of circuits is improved as follows: 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 faster. We identify lazy abstraction as a special case of the predicate partitioning. 2) We use weakest preconditions of circuit transitions in order to obtain new predicates during abstraction refinement. These techniques have not been applied to circuits before. We provide experimental results on publicly available benchmarks from the Texas97 suite to demonstrate the advantages of the new approach.
Submitted for publication, a copy is available upon request, 2004, 6 pages.
© 2004 Natasha Sharygina.