An anytime symmetry detection algorithm for ROBDDs

ABSTRACT

Detecting symmetries is crucial to logic synthesis, technology mapping, detecting function equivalence under unknown input correspondence, and ROBDD minimization. State-of-the-art is represented by Mishchenko's algorithm. In this paper we present an efficient anytime algorithm for detecting symmetries in Boolean functions represented as ROBDDs, that output pairs of symmetric variables until a prescribed time bound is exceeded. The algorithm is complete in that given sufficient time it is guaranteed to find all symmetric pairs. The complexity of this algorithm is in O(n⁴ + n|G| + |G|³) where n is the number of variables and |G| the number of nodes in the ROBDD, and it is thus competitive with Mishchenko's O (|G|³) algorithm in the worst-case since n ≪ |G|. However, our algorithm performs significantly better because the anytime approach only requires lightweight data structure support and it offers unique opportunities for optimization.

REFERENCES

• 1: C. E. Shannon, "A Symbolic Analysis of Relay and Switching Circuits," AIEE Trans., vol. 57, pp. 713--723, 1938.
• 2: B. G. Kim and D. L. Dietmeyer, "Multilevel Logic Synthesis of Symmetric Switching Functions," IEEE Trans. Computer-Aided Design, vol. 10, no. 4, pp. 436--446, 1991.
• 3: C. R. Edward and S. L. Hurst, "A Digital Synthesis Procedure Under Function Symmetries and Mapping Methods," IEEE Trans. Comput., vol. C-27, no. 11, pp. 985--997, 1978.
• 4: Frédéric Mailhot , Giovanni De Micheli, Technology mapping using boolean matching and don't care sets, Proceedings of the conference on European design automation, March 12-15, 1990, Glasgow, Scotland
• 5: Yung-Te Lai , Sarma Sastry , Massoud Pedram, Boolean Matching Using Binary Decision Diagrams with Applications to Logic Synthesis and Verification, Proceedings of the 1991 IEEE International Conference on Computer Design on VLSI in Computer & Processors, p.452-458, October 11-14, 1992
• 6: Shipra Panda , Fabio Somenzi , Bernard F. Plessier, Symmetry detection and dynamic variable ordering of decision diagrams, Proceedings of the 1994 IEEE/ACM international conference on Computer-aided design, p.628-631, November 06-10, 1994, San Jose, California, United States
• 7: C. Scholl, D. Möller, P. Molitor, and R. Drechsler, "BDD Minimization Using Symmetries," IEEE Trans. Computer-Aided Design, vol. 18, no. 2, pp. 81--100, 1999.
• 8: Janett Mohnke , Sharad Malik, Permutation and phase independent Boolean comparison, Integration, the VLSI Journal, v.16 n.2, p.109-129, Dec. 1993 [doi>10.1016/0167-9260(93)90041-A]
• 9: D. I. Cheng and M. Marek Sadowska, "Verifying Equivalence of Functions with Unknown Input Correspondence," in European Design Automation Conference, 1993, pp. 272--277.
• 10: Victor N. Kravets , Karem A. Sakallah, Generalized symmetries in boolean functions, Proceedings of the 2000 IEEE/ACM international conference on Computer-aided design, November 05-09, 2000, San Jose, California
• 11: Gary D. Hachtel , Fabio Somenzi, Logic Synthesis and Verification Algorithms, Kluwer Academic Publishers, Norwell, MA, 2000
• 12: Dirk Möller , Janett Mohnke , Michael Weber, Detection of symmetry of Boolean functions represented by ROBDDs, Proceedings of the 1993 IEEE/ACM international conference on Computer-aided design, p.680-684, November 07-11, 1993, Santa Clara, California, United States
• 13: 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]
• 14: A. Mishchenko, "Fast Computation of Symmetries in Boolean Functions," IEEE Trans. Computer-Aided Design, vol. 22, no. 11, pp. 1588--1593, 2003.
• 15: 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
• 16: D. Bochmann and B. Steinbach, Logikenwurf mit XBOOLE: Algorithmen und Programme. Berlin: Verlag Technik GmBH, 1996.
• 17: Chien-Chung Tsai , Malgorzata Marek-Sadowska, Generalized Reed-Muller Forms as a Tool to Detect Symmetries, IEEE Transactions on Computers, v.45 n.1, p.33-40, January 1996 [doi>10.1109/12.481484]
• 18: Robert W. Floyd, Algorithm 97: Shortest path, Communications of the ACM, v.5 n.6, p.345, June 1962 [doi>10.1145/367766.368168]
• 19: Stephen Warshall, A Theorem on Boolean Matrices, Journal of the ACM (JACM), v.9 n.1, p.11-12, Jan. 1962 [doi>10.1145/321105.321107]
• 20: F. Somenzi, "CUDD Package, Release 2.4.0." {Online}. Available: http://vlsi.colorado.edu/~fabio/CUDD/cuddIntro.html
• 21: A. Mishchenko, "Extra Library of DD Procedures." {Online}. Available: http://www.ee.pdx.edu/~alanmi/research/extra.htm
• 22: "Lgsynth93 Benchmark Set." {Online}. Available: http://www.bddportal.org/benchmarks/
• 23: 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]

INDEX TERMS

Primary Classification:
  B. Hardware
  B.6 LOGIC DESIGN
      B.6.3 Design Aids
          Subjects: Automatic synthesis

Additional Classification:
  B. Hardware
  B.6 LOGIC DESIGN
      B.6.1 Design Styles
  B.8 Performance and Reliability
      B.8.2 Performance Analysis and Design Aids
  B.m MISCELLANEOUS
      Subjects: Design management

General Terms:
Design, Performance