Approximation and decomposition of binary decision diagrams

ABSTRACT

Efficient techniques for the manipulation of Binary Decision Diagrams (BDDs) are key to the success of formal verification tools. Recent advances in reachability analysis and model checking algorithms have emphasized the need for efficient algorithms for the approximation and decomposition of BDDs. In this paper we present a new algorithm for approximation and analyze its performance in comparison with existing techniques. We also introduce a new decomposition algorithm that produces balanced partitions. The effectiveness of our contributions is demonstrated by improved results in reachability analysis for some hard problem instances.

REFERENCES

• 1: 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
• 2: 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]
• 3: 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]
• 4: J.R. Butch, E.M. Clarke, K. L. McMillan, D. L. Dill. and L. J. Hwang. Symbolic model checking: 1020 states and beyond. In Proceedings of the FiJ'~h Annual Symposium on Logic in Computer Science, June 1990.
• 5: 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]
• 6: 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
• 7: H. Cho, G. D. Hachtel, E. Macii, B. Plessier, and F. Somenzi. Algorithms for approximate FSM traversal based on state space decomposition. IEEE Transactions on Computer-Aided Design, 15( 12): 1465-1478, December 1996.
• 8: 0. Coudert, C, Berthet, and J. C. Madre. Verification of sequential machines using boolean functional vectors. In L. Claesen, editor, Proceedings IFIP International Workshop on Applied Formul Method.~' fiJr Correct VLSI Design, pages 111-128, Leuven, Belgium, November 1989.
• 9: 0. Coudert and J. C. Madre. A unified framework for the formal verification of sequential circuits. In Proceedings of the IEEE Internutionul Conference on Computer Aided Design, pages 126-129, November 1990.
• 10: 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
• 11: Youpyo Hong , Peter A. Beerel , Jerry R. Burch , Kenneth L. McMillan, Safe BDD minimization using don't cares, Proceedings of the 34th annual conference on Design automation, p.208-213, June 09-13, 1997, Anaheim, California, United States [doi>10.1145/266021.266068]
• 12: S.-W. Jeong, B. Plessier, G. D. Hachtel, and F. Somenzi. Variable ordering and selection for FSM traversal. In Proceedings ~' the IEEE Internutionul Conference on Computer Aided Design, pages 476-479, Santa Clara, CA, November 1991.
• 13: Robert P. Kurshan, Computer-aided verification of coordinating processes: the automata-theoretic approach, Princeton University Press, Princeton, NJ, 1994
• 14: R. P. Kurshan, Formal verification in a commercial setting, Proceedings of the 34th annual conference on Design automation, p.258-262, June 09-13, 1997, Anaheim, California, United States [doi>10.1145/266021.266089]
• 15: Woohyuk Lee , Abelardo Pardo , Jae-Young Jang , Gary Hachtel , Fabio Somenzi, Tearing based automatic abstraction for CTL model checking, Proceedings of the 1996 IEEE/ACM international conference on Computer-aided design, p.76-81, November 10-14, 1996, San Jose, California, United States
• 16: David Esley Long, Model checking, abstraction, and compositional verification, Carnegie Mellon University, Pittsburgh, PA, 1993
• 17: K. L. McMi!lan. Symbolic Model Checking. Kluwer Academic Publishers, Boston, MA, 1994.
• 18: 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
• 19: Amit Narayan , Adrian J. Isles , Jawahar Jain , Robert K. Brayton , Alberto L. Sangiovanni-Vincentelli, Reachability analysis using partitioned-ROBDDs, Proceedings of the 1997 IEEE/ACM international conference on Computer-aided design, p.388-393, November 09-13, 1997, San Jose, California, United States
• 20: 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
• 21: Abelardo Pardo , Gary D. Hachtel, Automatic Abstraction Techniques for Propositional µ-calculus Model Checking, Proceedings of the 9th International Conference on Computer Aided Verification, p.12-23, June 22-25, 1997
• 22: R.K. Ranjan, A. Aziz, R. K. Brayton, B. F. Plessier, and C. Pixley. Efficient BDD algorithms for FSM synthesis and verification. Presented at IWLS95, Lake Tahoe, CA., May 1995.
• 23: 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
• 24: Richard Rudell, Dynamic variable ordering for ordered binary decision diagrams, Proceedings of the 1993 IEEE/ACM international conference on Computer-aided design, p.42-47, November 07-11, 1993, Santa Clara, California, United States
• 25: Thomas Robert Shiple , Alberto Sangiovanni-Vincentelli, Formal analysis of synchronous circuits, 1996
• 26: T.R. Shiple, R. K. Ranjan, A. L. Sangiovanni-Vincentelli, and R. K. Brayton. Deciding state teachability for large FSMs. Technical Report UCB/ERL M97/73, University of California at Berkeley, August 1996.
• 27: F. Somenzi. CUDD: CUD e c i s i o n Diagram Package. ftp://vlsi.colorado.edu/pub/.
• 28: H. Touati, H. Savoj, B. Lin, R. K. Brayton, and A. Sangiovanni-Vincentelli. Implicit enumeration of finite state machines using BDD's. In Proceedings of the IEEE International ConJerence on Computer Aided Design, pages 130-133, November 1990.

INDEX TERMS

Primary Classification:
  G. Mathematics of Computing
  G.2 DISCRETE MATHEMATICS

Additional Classification:
  B. Hardware
  B.7 INTEGRATED CIRCUITS
  B.8 Performance and Reliability

  C. Computer Systems Organization

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

  J. Computer Applications

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

Keywords:
ISM frequency band, RF CMOS, digital radio, spread spectrum communication, transceiver