Disjunctive Partitioning And Partial Iterative Squaring: An Effective Approach For Symbolic Traversal Of Large Circuits
Gianpiero Cabodi, P. Camurati, L. Lavagno, Stefano Quer · 2005
Extending the applicability of reachability analysis to large and real circuits is a key issue. In fact they are still limited for the following reasons: peak BDD size during image computation, BDD explosion for representing state sets and very high sequential depth. Following the promising trend of partitioning and problem decomposition, we present a new approach based on a disjunctive partitionedtransition relation and on an improved iterative squaring. In this approach a Finite State Machine is decomposed and traversed one "functioning--mode" at a time by means of the "disjunctive" partitioned approach. The overall algorithm aims at lowering the intermediate peak BDD size pushing further reachability analysis. Experiments on a few industrial circuits containing counters and on some large benchmarks show the feasibility of the approach. 1 Introduction State-of-the-art approaches for state space exploration of Finite State Machines (FSMs) exploit symbolic techniques based on Binar...