Disjunctive partitioning and partial iterative squaring: an effective approach for symbolic traversal of large circuits

ABSTRACT

Extending the applicability of reachability analysis to large andreal circuits is a key issue.In fact they are still limited forthe following reasons: peak BDD size during image computation,BDD explosion for representing state sets and very highsequential depth.Following the promising trend of partitioning and problem decomposition,we present a new approach based on a disjunctivepartitioned transition relation and on an improved iterativesquaring.In this approach a Finite State Machine is decomposedand traversed one "functioning-mode" at a time bymeans of the "disjunctive" partitioned approach.The overall algorithm aims at lowering the intermediate peakBDD size pushing further reachability analysis.Experimentson a few industrial circuits containing counters and on somelarge benchmarks show the feasibility of the approach.

REFERENCES

• 1: Kavita Ravi , Fabio Somenzi, High-density reachability analysis, Proceedings of the 1995 IEEE/ACM international conference on Computer-aided design, p.154-158, November 05-09, 1995, San Jose, California, United States
• 2: Gianpiero Cabodi , Paolo Camurati , Stefano Quer, Improved reachability analysis of large finite state machines, Proceedings of the 1996 IEEE/ACM international conference on Computer-aided design, p.354-360, November 10-14, 1996, San Jose, California, United States
• 3: J.R. Butch, E.M. Clarke, D.E. Long, K.L. McMillan, D.L. Dill: "Symbolic Model Checking for Sequential Circuit Verification," lEEE-Trar~saction on CAD, pp. 401-424, Volume 13, Number 4, April 1994
• 4: J. R. Burch , E. M. Clarke , D. E. Long, Representing circuits more efficiently in symbolic model checking, Proceedings of the 28th conference on ACM/IEEE design automation, p.403-407, June 17-22, 1991, San Francisco, California, United States [doi>10.1145/127601.127702]
• 5: Ramin Hojati , Sriram C. Krishnan , Robert K. Brayton, Early Quantification and Partitioned Transition Relations, Proceedings of the 1996 International Conference on Computer Design, VLSI in Computers and Processors, p.12-19, October 07-09, 1996
• 6: H. Cho, G.D. I-Iachtel, E. Macii, M. Poncino, K. Ravi, F. Somenzi, "Approximate Finite State Machine Traversal: Extensions and New Results," in Proc. IWLS'95, May 1995
• 7: M68HCll Reference Manual, Motorola inc., 1991
• 8: G. Cabodi , P. Camurati , L. Lavagno , S. Quer, Verification and Synthesis of Counters Based on Symbolic Techniques, Proceedings of the 1997 European conference on Design and Test, p.176, March 17-20, 1997

INDEX TERMS

Primary Classification:
  B. Hardware
  B.7 INTEGRATED CIRCUITS

Additional Classification:
  B. Hardware

  C. Computer Systems Organization

  F. Theory of Computation
  F.1 COMPUTATION BY ABSTRACT DEVICES
      F.1.1 Models of Computation
          Subjects: Automata (e.g., finite, push-down, resource-bounded)

  K. Computing Milieux
  K.6 MANAGEMENT OF COMPUTING AND INFORMATION SYSTEMS
      K.6.2 Installation Management
          Subjects: Benchmarks

General Terms:
Design, Experimentation, Measurement, Performance, Standardization, Theory