Reachability analysis of large circuits using disjunctive partitioning and partial 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 state space explosion problem, it is currently limited to medium-small circuits, and extending its applicability is still a key issue. Among the factors that limit reachability analysis, let us list: the peak binary decision diagrams (BDD) size during image computation, the BDD size to represent state sets, and very high sequential depth. Following the promising trend of partitioning, 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 functionality, 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 intermediate peak BDD size, and dealing with high-depth subcomponents. Experiments on a few industrial circuits and on some large benchmarks show the feasibility of the approach.