Reachability analysis using partitioned-ROBDDs

ABSTRACT

In this paper, we address the problem of finite state machine (FSM) traversal, a key step in most sequential verification and synthesis algorithms. We propose the use of partitioned-ROBDDs to reduce the memory explosion problem associated with symbolic state space exploration techniques. In our technique, the reachable state set is represented as a partitioned-ROBDD Different partitions of the Boolean space are allowed to have different variable orderings and only one partition needs to be in memory at any given time. We show the effectiveness of our approach on a set of ISCAS89 benchmark circuits. Our techniques result in a significant reduction in total memory utilization. For a given memory limit, partitioned-ROBDD based method can complete traversal for many circuits for which monolithic ROBDDs fail. For circuits where both partitioned-ROBDDs as well as monolithic-ROBDDs cannot complete traversal, partitioned-ROBDDs can reach a significantly larger set of states.

REFERENCES

• 1: Jochen Bern , Christoph Meinel , Anna Slobodová, Efficient OBDD-based boolean manipulation in CAD beyond current limits, Proceedings of the 32nd ACM/IEEE conference on Design automation, p.408-413, June 12-16, 1995, San Francisco, California, United States [doi>10.1145/217474.217563]
• 2: Beate Bollig , Martin Sauerhoff , Detlef Sieling , Ingo Wegener, Hierarchy theorems for kOBDDs and kIBDDs, Theoretical Computer Science, v.205 n.1-2, p.45-60, Sept. 28, 1998 [doi>10.1016/S0304-3975(97)00034-0]
• 3: B. Bollig and I. Wegener. Partitioned-BDDs vs. Other BDD Models. In To be published in IWLS 97, Tahoe City, CA, May 1997.
• 4: B. Bollig and Ingo Wegener. manuscript, Personal communication, 1997.
• 5: Randal E. Bryant, Graph-based algorithms for Boolean function manipulation, IEEE Transactions on Computers, v.35 n.8, p.677-691, Aug. 1986 [doi>10.1109/TC.1986.1676819]
• 6: 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]
• 7: J. R. Burch , E. M. Clarke , K. L. McMillan , D. L. Dill , L. J. Hwang, Symbolic model checking: 1020 states and beyond, Information and Computation, v.98 n.2, p.142-170, June 1992 [doi>10.1016/0890-5401(92)90017-A]
• 8: G. Cabodi and E Camurati. Symbolic FSM Traversals Based on the Transition Relation. Manuscript Submitted to Transaction on Computer- Aided Design, 1994.
• 9: Gianpiero Cabodi , Paolo Camurati , Stefano Quer, Auxiliary variables for extending symbolic traversal techniques to data paths, Proceedings of the 31st annual conference on Design automation, p.289-293, June 06-10, 1994, San Diego, California, United States [doi>10.1145/196244.196380]
• 10: 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
• 11: Gianpiero Cabodi , Paolo Camurati , Luciano Lavagno , Stefano Quer, Disjunctive partitioning and partial iterative squaring: an effective approach for symbolic traversal of large circuits, Proceedings of the 34th annual conference on Design automation, p.728-733, June 09-13, 1997, Anaheim, California, United States [doi>10.1145/266021.266355]
• 12: O. Coudert , C. Berthet , J. C. Madre, Verification of synchronous sequential machines based on symbolic execution, Proceedings of the international workshop on Automatic verification methods for finite state systems, p.365-373, February 1990, Grenoble, France
• 13: R. Drechsler , A. Sarabi , M. Theobald , B. Becker , M. A. Perkowski, Efficient representation and manipulation of switching functions based on ordered Kronecker functional decision diagrams, Proceedings of the 31st annual conference on Design automation, p.415-419, June 06-10, 1994, San Diego, California, United States [doi>10.1145/196244.196444]
• 14: J. Gergov , C. Meinel, Efficient Boolean Manipulation with OBDD's Can be Extended to FBDD's, IEEE Transactions on Computers, v.43 n.10, p.1197-1209, October 1994 [doi>10.1109/12.324545]
• 15: E. Goldberg, Y. Kukimoto, and R. K. Brayton. Canonical TBDD's - A New Data Structure for Boolean Functions. In Proc. of the Intl. Workshop on Logic Synthesis, May 1997.
• 16: Robert K. Brayton , Gary D. Hachtel , Alberto L. Sangiovanni-Vincentelli , Fabio Somenzi , Adnan Aziz , Szu-Tsung Cheng , Stephen A. Edwards , Sunil P. Khatri , Yuji Kukimoto , Abelardo Pardo , Shaz Qadeer , Rajeev K. Ranjan , Shaker Sarwary , Thomas R. Shiple , Gitanjali Swamy , Tiziano Villa, VIS: A System for Verification and Synthesis, Proceedings of the 8th International Conference on Computer Aided Verification, p.428-432, August 03, 1996
• 17: Ramin Hojati , Sriram Krishnan , Robert K. Brayton, Heuristic Algorithms for Early Quantification and Partial, University of California at Berkeley, Berkeley, CA, 1994
• 18: Jawahar Jain, On analysis of Boolean functions, University of Texas at Austin, Austin, TX, 1993
• 19: Jawahar Jain , James Bitner , Magdy S. Abadir , Jacob A. Abraham , Donald S. Fussell, Indexed BDDs: Algorithmic Advances in Techniques to Represent and Verify Boolean Functions, IEEE Transactions on Computers, v.46 n.11, p.1230-1245, November 1997 [doi>10.1109/12.644298]
• 20: J. Jain, J. Bitner, D. S. Fussell, and J. A. Abraham. Functional partitioning for verification and related problems. Brown/MIT VLSI Conference, March 1992.
• 21: Jawahar Jain , Amit Narayan , C. Coelho , Sunil P. Khatri , Alberto L. Sangiovanni-Vincentelli , Robert K. Brayton , Masahiro Fujita, Decomposition Techniques for Efficient ROBDD Construction, Proceedings of the First International Conference on Formal Methods in Computer-Aided Design, p.419-434, November 06-08, 1996
• 22: U. Kebschull et. al. Multilevel logic synthesis based on Functional Decision Diagrams. European DAC, pages 43-47, 1992.
• 23: Kenneth L. McMillan, Symbolic Model Checking, Kluwer Academic Publishers, Norwell, MA, 1993
• 24: Kenneth L. McMillan, A Conjunctively Decomposed Boolean Representation for Symbolic Model Checking, Proceedings of the 8th International Conference on Computer Aided Verification, p.13-25, August 03, 1996
• 25: Shin-ichi Minato, Zero-suppressed BDDs for set manipulation in combinatorial problems, Proceedings of the 30th international conference on Design automation, p.272-277, June 14-18, 1993, Dallas, Texas, United States [doi>10.1145/157485.164890]
• 26: Amit Narayan , Jawahar Jain , M. Fujita , A. Sangiovanni-Vincentelli, Partitioned ROBDDs—a compact, canonical and efficiently manipulable representation for Boolean functions, Proceedings of the 1996 IEEE/ACM international conference on Computer-aided design, p.547-554, November 10-14, 1996, San Jose, California, United States
• 27: Carl Pixley, Introduction to a Computational Theory and Implementation of Sequential Hardware Equivalence, Proceedings of the 2nd International Workshop on Computer Aided Verification, p.54-64, June 18-21, 1990
• 28: R.K. Ranjan, A. Aziz, R. K. Brayton, B. Plessier, and C. Pixley. Efficient BDD Algorithms for FSM Synthesis and Verification. In Proc. of the Intl. Workshop on Logic Synthesis, Tahoe City, NV, May 1995.
• 29: 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
• 30: Detlef Sieling , Ingo Wegener, Graph driven BDDs—a new data structure for Boolean functions, Theoretical Computer Science, v.141 n.1-2, p.283-310, April 17, 1995 [doi>10.1016/0304-3975(94)00078-W]
• 31: E Somenzi. CUDD: CU Decision Diagram Package, Release 2.1.1. Department of Electrical and Computer Engineering, University of Colorado at Boulder, February 1997.
• 32: H. J. Touati, H. Savoj, B. Lin, R. K. Brayton, and A. L. Sangiovanni- Vincentelli. Implicit State Enumeration of Finite State Machines using BDD's. In ICCAD, pages 130-133, November 1990.
• 33: Stephan Waack, On the Descriptive and Algorithmic Power of Parity Ordered Binary Decision Diagrams, Proceedings of the 14th Annual Symposium on Theoretical Aspects of Computer Science, p.201-212, February 27-March 01, 1997

INDEX TERMS

Primary Classification:
  J. Computer Applications

Additional Classification:
  B. Hardware
  B.7 INTEGRATED CIRCUITS
      B.7.1 Types and Design Styles
          Subjects: Algorithms implemented in hardware; VLSI (very large scale integration)

  G. Mathematics of Computing
  G.4 MATHEMATICAL SOFTWARE
      Subjects: Algorithm design and analysis

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

Keywords:
ROBDD, Partitioning, Reachability, FSM, Verification, Sequential, Traversal, Symbolic