The multiple variable order problem for binary decision diagrams: theory and practical application

ABSTRACT

Reduced Ordered Binary Decision Diagrams (ROBDDs) gained widespread use in logic design verification, test generation, fault simulation, and logic synthesis [17, 7]. Since the size of an ROBDD heavily depends on the variable order used, there is a strong need to find variable orders that minimize the number of nodes in an ROBDD. In certain applications we have to cope with ROBDDs with different variable orders, whereas further manipulations of these ROBDDs require common variable orders. In this paper we give a theoretical background for this "Multiple Variable Order problem". Moreover, we solve the problem to transform ROBDDs with different variable orders into a good common variable order using dynamic variable ordering techniques.

REFERENCES

• 1: S.B. Akers. Binary decision diagrams. IEEE Trans. on Comp., 27:509-516, 1978.
• 2: Pranav Ashar , Sharad Malik, Fast functional simulation using branching programs, Proceedings of the 1995 IEEE/ACM international conference on Computer-aided design, p.408-412, November 05-09, 1995, San Jose, California, United States
• 3: B. Bollig, M. L obbing, and I. Wegener. Simulated annealing to improve variable orderings for OBDDs. In Int'l Workshop on Logic Synth., pages 5b:5.1-5.10, 1995.
• 4: Beate Bollig , Ingo Wegener, Improving the Variable Ordering of OBDDs Is NP-Complete, IEEE Transactions on Computers, v.45 n.9, p.993-1002, September 1996 [doi>10.1109/12.537122]
• 5: Karl S. Brace , Richard L. Rudell , Randal E. Bryant, Efficient implementation of a BDD package, Proceedings of the 27th ACM/IEEE conference on Design automation, p.40-45, June 24-27, 1990, Orlando, Florida, United States [doi>10.1145/123186.123222]
• 6: 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]
• 7: Randal E. Bryant, Symbolic Boolean manipulation with ordered binary-decision diagrams, ACM Computing Surveys (CSUR), v.24 n.3, p.293-318, Sept. 1992 [doi>10.1145/136035.136043]
• 8: 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
• 9: G. Cabodi, S. Quer, C. Meinel, Harald Sack, A. Slobodova, and C. Stangier. Binary decision diagrams and the multiple variable order problem. In Int'l Workshop on Logic Synth., pages 346-352, 1998.
• 10: R. Drechsler, B. Becker, and N. Gockel. A genetic algorithm for variable ordering of OBDDs. In Int'l Workshop on Logic Synth., pages 5c:5.55-5.64, 1995.
• 11: E. Felt, G York, R. Brayton, and A. Sangiovanni-Vincentelli. Dynamic Variable Reordering for BDD Minimization. In European Design Automation Conf., pages 130-135, 1993.
• 12: Hiroshige Fujii , Goichi Ootomo , Chikahiro Hori, Interleaving based variable ordering methods for ordered binary decision diagrams, Proceedings of the 1993 IEEE/ACM international conference on Computer-aided design, p.38-41, November 07-11, 1993, Santa Clara, California, United States
• 13: M. Fujita, H. Fujisawa, and N. Kawato. Evaluation and improvements of Boolean comparison method based on binary decision diagrams. In Int'l Conf. on CAD, pages 2-5, 1988.
• 14: Masahiro Fujita , Yusuke Matsunaga , Taeko Kakuda, On variable ordering of binary decision diagrams for the application of multi-level logic synthesis, Proceedings of the conference on European design automation, February 25-28, 1991, Amsterdam, The Netherlands
• 15: N. Ishiura, H. Sawada, and S. Yajima. Minimization of binary decision diagrams based on exchange of variables. In Int'l Conf. on CAD, pages 472-475, 1991.
• 16: C.Y. Lee. Representation of switching circuits by binary decision diagrams. Bell System Technical Jour., 38:985-999, 1959.
• 17: S. Malik, A.R. Wang, R.K. Brayton, and A.L. Sangiovanni- Vincentelli. Logic verification using binary decision diagrams in a logic synthesis environment. In Int'l Conf. on CAD, pages 6-9, 1988.
• 18: Patrick C. McGeer , Kenneth L. McMillan , Alexander Saldanha , Alberto L. Sangiovanni-Vincentelli , Patrick Scaglia, Fast discrete function evaluation using decision diagrams, Proceedings of the 1995 IEEE/ACM international conference on Computer-aided design, p.402-407, November 05-09, 1995, San Jose, California, United States
• 19: Bernard M. E. Moret, Decision Trees and Diagrams, ACM Computing Surveys (CSUR), v.14 n.4, p.593-623, Dec. 1982 [doi>10.1145/356893.356898]
• 20: 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
• 21: 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
• 22: C. Scholl , B. Becker , A. Brogle, Solving the Multiple Variable Order Problem for Binary Decision Diagrams by Use of Dynamic Reordering Techniques, Albert-Ludwigs University at Freiburg, 1999
• 23: Christoph Scholl , Rolf Drechsler , Bernd Becker, Functional simulation using binary decision diagrams, Proceedings of the 1997 IEEE/ACM international conference on Computer-aided design, p.8-12, November 09-13, 1997, San Jose, California, United States
• 24: F. Somenzi. CUDD: CU Decision Diagram Package Release 2.3.0. University of Colorado at Boulder, 1998.
• 25: Seiichiro Tani , Kiyoharu Hamaguchi , Shuzo Yajima, The Complexity of the Optimal Variable Ordering Problems of Shared Binary Decision Diagrams, Proceedings of the 4th International Symposium on Algorithms and Computation, p.389-398, December 15-17, 1993

INDEX TERMS

Primary Classification:
  B. Hardware

Additional Classification:
  B. Hardware
  B.6 LOGIC DESIGN
      B.6.3 Design Aids
          Subjects: Verification
  B.8 Performance and Reliability

  C. Computer Systems Organization

  J. Computer Applications
  J.2 PHYSICAL SCIENCES AND ENGINEERING
      Subjects: Electronics

General Terms:
Design, Performance, Theory, Verification