Reachability analysis of large circuits using disjunctive partitioning andpartial iterative squaring

Reachability analysis is an orthogonal, state-of-the-art technique for the verification and validation of finite state machines (FSMs). Due to the sta te space explosion problem, it is currently limited to medium-small circuit s, and extending its applicability is still a key issue. Among the factors that limit reachability analysis, let us list: the peak binary decision dia grams (BDD) size during image computation, the BDD size to represent state sets, and very high sequential depth. Following the promising trend of part itioning, we decompose a finite state machine into "functioning-modes''. We operate on a disjunctive partitioned transition relation. Decomposition is obtained heuristically based on complexity, i.e., BDD size, or functionali ty, i.e., dividing memory elements into "active" and "idle" ones. We use an improved iterative squaring algorithm to traverse high-depth subcomponents . The resulting methodology attacks the above problems, lowering intermedia te peak BDD size, and dealing with high-depth subcomponents. Experiments on a few industrial circuits and on some large benchmarks show the feasibilit y of the approach. (C) 2001 Elsevier Science B.V. All rights reserved.