Improved reachability analysis of large finite state machines

ABSTRACT

BDD-based symbolic traversals are the state-of-the-art technique for reachability analysis of Finite State Machines. They are currently limited to medium-small circuits for two reasons: peak BDD size during image computation and BDD explosion for representing state sets. Starting from these limits, this paper presents an optimized traversal technique particularly oriented to the exact exploration of the state space of large machines. This is possible thanks to: 1) temporary simplification of a Finite State Machine by removing some of its state elements, 2) a "divide-and-conquer" approach based on state set decomposition. An effective use of secondary memory allows us to store relevant portions of BDDs and to regularize access to memory, resulting in less page faults. Experimental results show that this approach is particularly effective on the larger ISCAS'89 and ISCAS'89-addendum'93 circuits.

REFERENCES

• 1: H. Touati, H. Savoj, B. Lin, R.K. Brayton, A. Sangiovanni-Vincentelli, ~qmplicit enumeration of finite state machines using BDDs," in Proc. {EEE {C- CAD'90, November 1990, pp. 130-133
• 2: H. Cho, G. Hachtel, S.W. Jeong, B. Plessier, E. Schwarz, F. Somenzi, ~ATPG Aspects of FSM Verification," in Proc. {EEE {CCAD'90, November 1990, pp. 134-137
• 3: O. Coudert, J.C. Madre, ~A Unified Framework for the Formal Verification of Sequential Circuits" in Proc. {EEE {CCAD'90, November 1990, pp. 126-129
• 4: 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
• 5: F. Somenzi, ~CUDD: CU Decision Diagram Package- Release 1.0.4," Technical Report, Dept. of Electrical and Computer Engineering, University of Colorado, Boulder, November 1995
• 6: H. Cho, G.D. Hatchel, E. Macii, M. Poncino, K. Ravi, F. Somenzi, ~Approximate Finite State Machine Traversal: Extensions and New Results," IWLS'95: IEEE International Workshop on Logic Synthesis, Lake Tahoe, CA, USA, May 1995
• 7: Daniel Geist , Ilan Beer, Efficient Model Checking by Automated Ordering of Transition Relation Partitions, Proceedings of the 6th International Conference on Computer Aided Verification, p.299-310, June 21-23, 1994
• 8: R.K. Ranjan, A. Aziz, R.K. Brayton, B. Plessier, C. Pixley, ~Efficient BDD Algorithms for FSM Synthesis and Verification," IWLS'95: IEEE International Workshop on Logic Synthesis, Lake Tahoe, CA, USA, May 1995, poster presentation
• 9: Gianpiero Cabodi , Luciano Lavagno , Enrico Macii , Massimo Poncino , Stefano Quer , Paolo Camurati , Ellen Sentovicha, Enhancing FSM Traversal by Temporary Re-Encoding, Proceedings of the 1996 International Conference on Computer Design, VLSI in Computers and Processors, p.6-11, October 07-09, 1996

INDEX TERMS

Primary Classification:
  B. Hardware
  B.7 INTEGRATED CIRCUITS

Additional Classification:
  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)
  F.2 ANALYSIS OF ALGORITHMS AND PROBLEM COMPLEXITY
      F.2.2 Nonnumerical Algorithms and Problems
          Subjects: Computations on discrete structures

  G. Mathematics of Computing
  G.2 DISCRETE MATHEMATICS
      G.2.2 Graph Theory
          Subjects: Path and circuit problems

General Terms:
Experimentation, Performance, Verification

Keywords:
Sequential Logic Synthesis and Verification