Analysis of composition complexity and how to obtain smaller canonical graphs

ABSTRACT

We discuss an open problem in construction of Reduced Ordered Binary Decision Diagrams (ROBDDs) using composition, and prove that the worst case complexity of the construction is truly cubic. With this insight we show that the process of composition naturally leads to the construction of (even exponentially) compact partitioned-OBDDs (POBDDs) [12]. Our algorithm which incorporates dynamic partitioning, leads to the most general (and compact) form of POBDDs - graphs with multiple root variables. To show that our algorithm is robust and practical, we have analyzed some well known problems in Boolean function representation, verification and finite state machine analysis where our approach generates graphs which are even orders of magnitude smaller.

REFERENCES

• 1: J. R. Burch , E. M. Clarke , K. L. McMillan , David L. Dill, Sequential circuit verification using symbolic model checking, Proceedings of the 27th ACM/IEEE conference on Design automation, p.46-51, June 24-27, 1990, Orlando, Florida, United States [doi>10.1145/123186.123223]
• 2: 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 ]
• 3: B. Bollig and I. Wegener. "Partitioned BDDs vs. Other BDD Models" Proc. IWLS, 1997.
• 4: 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]
• 5: 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]
• 6: Gianpiero Cabodi , Paolo Camurati , Stefano Quer, Efficient State Space Pruning in Symbolic Backward Traversal, Proceedings of the1994 IEEE International Conference on Computer Design: VLSI in Computer & Processors, p.230-235, October 10-12, 1994
• 7: G. Cabodi , S. Quer , P. Camurati, Extending equivalence class computation to large FSMs, Proceedings of the 1995 International Conference on Computer Design: VLSI in Computers and Processors, p.258, October 02-04, 1995
• 8: O. Coudert, C. Berthet, and J. Madre. "Verification of Sequential Machines Using Boolean Functional Vectors". Formal VLSI Correctness Verification. Elsevier Sc., pages 179-196, 1990.
• 9: 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]
• 10: Y.V. Hoskote. "Formal Techniques for Verification of Synchronous Sequential Circuits". Ph.D Dissertation, Dept. of Electrical and Computer Engineering, The University of Texas at Austin, 1995.
• 11: Shi-Yu Huang , Kwang-Ting Cheng , Kuang-Chien Chen , Uwe Gläser, An ATPG-Based Framework for Verifying Sequential Equivalence, Proceedings of the IEEE International Test Conference on Test and Design Validity, p.865-874, October 20-25, 1996
• 12: J. Jain, J. Bitner, D. S. Fussell, and J. A. Abraham. "Functional partitioning for verification and related problems". Brown/MIT VLSI Conference, March 1992.
• 13: Jawahar Jain, On analysis of Boolean functions, University of Texas at Austin, Austin, TX, 1993
• 14: 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
• 15: Zvi Kohavi , Richard W. Hamming , Edward A. Feigenbaum, Switching and Finite Automata Theory: Computer Science Series, McGraw-Hill Higher Education, 1990
• 16: A. Narayan , S. P. Khatri , J. Jain , M. Fujita , R. K. Brayton , A. Sangiovanni-Vincentelli, A study of composition schemes for mixed apply/compose based construction of ROBDDs, Proceedings of the 9th International Conference on VLSI Design: VLSI in Mobile Communication, p.249, January 03-06, 1996
• 17: 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
• 18: 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
• 19: C. Pixley. "A Theory and Implementation of Sequential Hardware Equivalence". IEEE Trans. on CAD, pages 1469-1494, 1992.
• 20: Carl Pixley , Vigyan Singhal , Adnan Aziz , Robert K. Brayton, Multi-level synthesis for safe replaceability, Proceedings of the 1994 IEEE/ACM international conference on Computer-aided design, p.442-449, November 06-10, 1994, San Jose, California, United States
• 21: R. Mukherjee, J. Jain, K. Takayama, M. Fujita, J. Abraham, and D. Fussell. "An Efficient Filter-based Approach for Combinational Verification". IEEE Transactions on Computer-Aided Design, Vol-18, Pages 1542-1557, November 1999.
• 22: D. Sieling and I. Wegener "NC-Algorithms for Operations on Binary Decision Diagrams". Parallel Processing Letters, 3:3-12, 1993.

INDEX TERMS

Primary Classification:
  J. Computer Applications

Additional Classification:
  B. Hardware
  B.7 INTEGRATED CIRCUITS

  G. Mathematics of Computing
  G.2 DISCRETE MATHEMATICS

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