Article

Free access

Symmetry detection and dynamic variable ordering of decision diagrams

Authors:

Bernard F. PlessierAuthors Info & Claims

ICCAD '94: Proceedings of the 1994 IEEE/ACM international conference on Computer-aided design

Pages 628 - 631

Published: 06 November 1994 Publication History

Abstract

Knowing that some variables are symmetric in a function has numerous applications; in particular, it can help produce better variable orders for Binary Decision Diagrams (BDDs) and related data structures (e.g., Algebraic Decision Diagrams). It has been conjectured that there always exists an optimum order for a BBD wherein symmetric variables are contiguous. We propose a new algorithm for the detection of symmetries, based on dynamic reordering, and we study its interaction with the reordering algorithm itself. We show that combining sifting with an efficient symmetry check for contiguous variables results in the fastest symmetry detection algorithm reported to date and produces better variable orders for many BDDs. The overhead on the sifting algorithm is negligible.

References

[1]

R. I. Bahar, E. A. Frohm, C. M. Gaona, G. D. Hachtel, E. Macii, A. Pardo, and F. Somenzi. Algebraic decision diagrams and their applications. In Proceedings of the International Conference on Computer-Aided Design, pages 188-191, Santa Clara, CA, November 1993.

Digital Library

[2]

K. S. Brace) R. L. Rudell) and R. E. Bryant. Efficient implementation of a BDD package. In Proceedings of the 27th Design Automation Conference, pages 40-45, Orlando, FL, June 1990.

Digital Library

[3]

N. Cala~,.ans, Q. Zhang, R. Jacobi, B. Yernaux, and A.-M. Trullemans. Advanced ordering and manipulation techniques for binary decision diagrams. In Proceedings of the European Conference on Design Automation, pages 452-457, Brussels, Belgium, March 1992.

[4]

D. I. Cheng and M. Marek-Sadowska. Verifying equivalence of functions with unknown input correspondence. In Proceedings of the European Conference on Design Automation, pages 81-85, Paris, France, February 1993.

[5]

E. Felt) G. York, R. K. Brayton) and A. Sangiovanni- Vincentelli. Dynamic variable reordering for BDD minimiT.ation. In Proceedings of the European Design Automation Conference) pages 130-135, Hamburg, Germany, September 1993.

[6]

M. Fujita) Y. Matsunaga) and T. Kakuda. On variable ordering of binary decision diagrams for the application of multi-level logic synthesis. In Proceedings of the European Conference on Design Automation) pages 50-54) Amsterdam) February 1991.

Digital Library

[7]

N. Ishiura, H. Sawada, and S. Yajima. Minimization of binary decision diagrams based on exchanges of variables. In Proceeding8 of the International Conference on Computer-Aided Design, pages 472-475, Santa Clara, CA, November 1991.

[8]

S.-W. Jeong) T.-S. Kim) and F. Somenzi. An efficient method for optimal BDD ordering computation. In International Conference on VLSI and CAD (ICVC'93), Waejon, Korea, November 1993.

[9]

Y.-T. Lai and S. Sastry. Edge-valued binary decision diagrams for multi-level hierarchical verification. In Proceeding8 of the Design Automation Conference, pages 608-613, Anaheim, CA) June 1992.

[10]

S. Malik, A. Wang, R. Brayton, and A. Sangiovanni- Vincentelli. Logic verification using binary decision diagrams in a logic synthesis environment. In Proceedings of the IEEE International Conference on Computer Aided Design, pages 6-9) Santa Clara) CA) November 1988.

[11]

S.-I. Minato. Zero-suppressed BDDs for set manipulation in combinatorial problems. In Proceedings of the Design Automation Conference) pages 272-277, Dallas, TX, June 1993.

Digital Library

[12]

D. MSller, J. Mohnke, and M. Weber. Detection of symmetry of boolean functions represented by ROBDDs. In Proceeding8 of the International Conference on Computer-Aided Design, pages 680-684, Santa Clara, CA, November 1993.

Digital Library

[13]

B. F. Plessier. A General Framework, for Verification of Sequential Circuits. PhD thesis) University of Colorado at Boulder, Dept. of Electrical and Computer Engineering) 1993.

[14]

R. Rudell. Dynamic variable ordering for ordered binary decision diagrams. In Proceedings of the International Conference on Computer-Aided Design) pages 42-47, Santa Clara, CA, November 1993.

Digital Library

[15]

C. E. Shannon. A symbolic analysis of relay and switching circuits. AIEE Trans., 57:713-723, 1938.

Digital Library

[16]

C. C. Tsai and M. Marek-Sadowska. Detecting symmetric variables in boolean functions using generalized Reed-Muller forms. In Proceedings of the International Symposium on Circuits and Systems, London, Britain, May 1994.

Cited By

Scholl CKonrad ALi Z(2020)Symbolic computer algebra and SAT based information forwarding for fully automatic divider verificationProceedings of the 57th ACM/EDAC/IEEE Design Automation Conference10.5555/3437539.3437552(1-6)Online publication date: 20-Jul-2020
https://dl.acm.org/doi/10.5555/3437539.3437552
Mishchenko AEen NBrayton RCase MChauhan PSharma NMacii E(2013)A semi-canonical form for sequential AIGsProceedings of the Conference on Design, Automation and Test in Europe10.5555/2485288.2485481(797-802)Online publication date: 18-Mar-2013
https://dl.acm.org/doi/10.5555/2485288.2485481
Stergiou SStok LDutt NHassoun S(2011)Implicit permutation enumeration networks and binary decision diagrams reorderingProceedings of the 48th Design Automation Conference10.1145/2024724.2024866(615-620)Online publication date: 5-Jun-2011
https://dl.acm.org/doi/10.1145/2024724.2024866
Show More Cited By

Index Terms

Symmetry detection and dynamic variable ordering of decision diagrams
1. Hardware
  1. Integrated circuits
    1. Digital switches
      1. Logic families

Recommendations

Symmetry and asymmetry of solutions in discrete variable structural optimization

In this paper symmetry and asymmetry of optimal solutions in symmetric structural optimization problems is investigated, based on the choice of variables. A group theory approach is used to define the symmetry of the structural problems in a general ...
Multiple-Valued Decision Diagrams with Symmetric Variable Nodes
ISMVL '96: Proceedings of the 26th International Symposium on Multiple-Valued Logic

Symmetry is an important property of logic functions. In this paper, we introduce symmetric variable nodes, and investigate how they can be used to advantage in decision diagrams. We consider totally-symmetric and partially-symmetric functions as well ...
The multiple variable order problem for binary decision diagrams: theory and practical application
ASP-DAC '01: Proceedings of the 2001 Asia and South Pacific Design Automation Conference

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 ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

ICCAD '94: Proceedings of the 1994 IEEE/ACM international conference on Computer-aided design

November 1994

771 pages

ISBN:0897916905

Chairmen:
Jochen A. G. Jess
Eindhoven Univ. of Technology, Eindhoven, The Netherlands
,
Richard Rudell
Synopsys, Inc., Mountain View, CA

Sponsors

SIGDA: ACM Special Interest Group on Design Automation
IEEE-CS: Computer Society

Publisher

IEEE Computer Society Press

Washington, DC, United States

Publication History

Published: 06 November 1994

Check for updates

Qualifiers

Article

Conference

ICCAD '94

Sponsor:

SIGDA
IEEE-CS

ICCAD '94: International Conference on Computer Aided Design

November 6 - 10, 1994

California, San Jose, USA

Acceptance Rates

Overall Acceptance Rate 457 of 1,762 submissions, 26%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

29
Total Citations
View Citations
389
Total Downloads

Downloads (Last 12 months)13
Downloads (Last 6 weeks)1

Reflects downloads up to 19 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Scholl CKonrad ALi Z(2020)Symbolic computer algebra and SAT based information forwarding for fully automatic divider verificationProceedings of the 57th ACM/EDAC/IEEE Design Automation Conference10.5555/3437539.3437552(1-6)Online publication date: 20-Jul-2020
https://dl.acm.org/doi/10.5555/3437539.3437552
Mishchenko AEen NBrayton RCase MChauhan PSharma NMacii E(2013)A semi-canonical form for sequential AIGsProceedings of the Conference on Design, Automation and Test in Europe10.5555/2485288.2485481(797-802)Online publication date: 18-Mar-2013
https://dl.acm.org/doi/10.5555/2485288.2485481
Stergiou SStok LDutt NHassoun S(2011)Implicit permutation enumeration networks and binary decision diagrams reorderingProceedings of the 48th Design Automation Conference10.1145/2024724.2024866(615-620)Online publication date: 5-Jun-2011
https://dl.acm.org/doi/10.1145/2024724.2024866
Tang YNorman TParsons S(2010)Computing argumentation in polynomial number of BDD operationsProceedings of the 7th international conference on Argumentation in Multi-Agent Systems10.1007/978-3-642-21940-5_16(268-285)Online publication date: 10-May-2010
https://dl.acm.org/doi/10.1007/978-3-642-21940-5_16
Chang KMarkov IBertacco V(2008)Postplacement rewiring by exhaustive search for functional symmetriesACM Transactions on Design Automation of Electronic Systems10.1145/1255456.125546912:3(1-21)Online publication date: 22-May-2008
https://dl.acm.org/doi/10.1145/1255456.1255469
Gherman VWunderlich HMascarenhas RSchloeffel JGarbers MZhou HMacii EYan ZMassoud Y(2007)Synthesis of irregular combinational functions with large don't care setsProceedings of the 17th ACM Great Lakes symposium on VLSI10.1145/1228784.1228856(287-292)Online publication date: 11-Mar-2007
https://dl.acm.org/doi/10.1145/1228784.1228856
Zhang JMishchenko ABrayton RChrzanowska-Jeske MSentovich E(2006)Symmetry detection for large Boolean functions using circuit representation, simulation, and satisfiabilityProceedings of the 43rd annual Design Automation Conference10.1145/1146909.1147044(510-515)Online publication date: 24-Jul-2006
https://dl.acm.org/doi/10.1145/1146909.1147044
Kettle NKing AHirose F(2006)An anytime symmetry detection algorithm for ROBDDsProceedings of the 2006 Asia and South Pacific Design Automation Conference10.1145/1118299.1118364(243-248)Online publication date: 24-Jan-2006
https://dl.acm.org/doi/10.1145/1118299.1118364
Chang KMarkov IBertacco V(2005)Post-placement rewiring and rebuffering by exhaustive search for functional symmetriesProceedings of the 2005 IEEE/ACM International conference on Computer-aided design10.5555/1129601.1129612(56-63)Online publication date: 31-May-2005
https://dl.acm.org/doi/10.5555/1129601.1129612
Li BHsiao MSheng S(2004)A Novel SAT All-Solutions Solver for Efficient Preimage ComputationProceedings of the conference on Design, automation and test in Europe - Volume 110.5555/968878.969034Online publication date: 16-Feb-2004
https://dl.acm.org/doi/10.5555/968878.969034
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents