Symmetry detection for large Boolean functions using circuit representation, simulation, and satisfiability

ABSTRACT

Classical two-variable symmetries play an important role in many EDA applications, ranging from logic synthesis to formal verification. This paper proposes a complete circuit-based method that makes uses of structural analysis, integrated simulation and Boolean satisfiability for fast and scalable detection of classical symmetries of completely-specified Boolean functions. This is in contrast to previous incomplete circuit-based methods and complete BDD-based methods. Experimental results demonstrate that the proposed method works for large Boolean functions, for which BDDs cannot be constructed.

REFERENCES

• 1: F. Aloul, A. Ramani, I. Markov, and K. Sakallah, "Solving difficult instances of Boolean satisfiability in the presence of symmetry", IEEE Trans. CAD, Vol. 22(9), Sep. 2003, pp. 1117--1137.
• 2: Fadi A. Aloul , Arathi Ramani , Igor L. Markov , Karem A. Sakallah, ShatterPB: symmetry-breaking for pseudo-Boolean formulas, Proceedings of the 2004 conference on Asia South Pacific design automation: electronic design and solution fair, p.883-886, January 27-30, 2004, Yokohama, Japan
• 3: Berkeley Logic Synthesis and Verification Group. ABC: A system for sequential synthesis and verification, Release 60303. http://www.eecs.berkeley.edu/~alanmi/abc/
• 4: F. Brglez, D. Bryan, and K. Kozminski, "Combinational profiles of sequential benchmark circuits," Proc. ISCAS '89, pp. 1929--1934.
• 5: Chih-Wei Chang , Chung-Kuan Cheng , Peter Suaris , Malgorzata Marek-Sadowska, Fast post-placement rewiring using easily detectable functional symmetries, Proceedings of the 37th conference on Design automation, p.286-289, June 05-09, 2000, Los Angeles, California, United States [doi>10.1145/337292.337420]
• 6: Chen-Ling Chou , Chun-Yao Wang , Geeng-Wei Lee , Jing-Yang Jou, Graph Automorphism-Based Algorithm for Determining Symmetric Inputs, Proceedings of the IEEE International Conference on Computer Design (ICCD'04), p.417-419, October 11-13, 2004
• 7: D. L. Dietmeyer and P. R. Schneider. "Identification of symmetry, redundancy, and equivalence of Boolean functions". IEEE Trans. Elec. Computers, Vol. 16(6), Dec. 1967, pp. 804--817.
• 8: C. R. Edward and S. L. Hurst. "A digital synthesis procedure under function symmetries and mapping methods". IEEE Trans. Computers, Vol. C-27(11), Nov. 1978, pp. 985--997.
• 9: N. Eén and N. Sörensson, "An extensible SAT-solver", Proc. SAT '03, pp. 502--518, http://www.cs.chalmers.se/Cs/Research/FormalMethods/ MiniSat/Main.html
• 10: E. Allen Emerson , A. Prasad Sistla, Symmetry and model checking, Formal Methods in System Design, v.9 n.1-2, p.105-131, Aug. 1996 [doi>10.1007/BF00625970]
• 11: Feng Lu , Li-C. Wang , Kwang-Ting Cheng , Ric C-Y Huang, A Circuit SAT Solver With Signal Correlation Guided Learning, Proceedings of the conference on Design, Automation and Test in Europe, p.10892, March 03-07, 2003
• 12: Feng Lu , Li-C. Wang , K.-T. (Tim) Cheng , John Moondanos , Ziyad Hanna, A signal correlation guided ATPG solver and its applications for solving difficult industrial cases, Proceedings of the 40th conference on Design automation, June 02-06, 2003, Anaheim, CA, USA [doi>10.1145/775832.775947]
• 13: C. N. Ip and D. L. Dill, "Better verification through symmetry", Proc. Formal Methods in System Design '96, pp. 41--75.
• 14: ITC '99 Benchmarks. http://www.cad.polito.it/tools/itc99.html
• 15: B.-G. Kim and D. L. Dietmeyer. "Multilevel logic synthesis of symmetric switching functions". IEEE Trans. CAD, Vol. 10(4), April 1991, pp. 436--44
• 16: 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
• 17: Victor Nikolayevich Kravets , Karem A. Sakallah, Constructive multi-level synthesis by way of functional properties, 2001
• 18: A. Kuehlmann, V. Paruthi, F. Krohm, and M. K. Ganai, "Robust Boolean reasoning for equivalence checking and functional property verification", IEEE Trans. CAD, Vol. 21(12), Dec. 2002, pp. 1377--1394.
• 19: João P. Marques-Silva , Karem A. Sakallah, GRASP: A Search Algorithm for Propositional Satisfiability, IEEE Transactions on Computers, v.48 n.5, p.506-521, May 1999 [doi>10.1109/12.769433]
• 20: A. Mishchenko, "Fast computation of symmetries in Boolean functions". IEEE Trans. CAD, Vol. 22(11), Nov. 2003, pp. 1588--1593.
• 21: A. Mishchenko, S. Chatterjee, R. Brayton, and N. Eén, "Improvements to combinational equivalence checking", Proc. IWLS '06. http://www. eecs.berkeley.edu/~alanmi/publications/2006/iwls06_cec.pdf
• 22: A. Mishchenko and R. Brayton, "Scalable logic synthesis using a simple circuit structure", Proc. IWLS '06. http://www.eecs. berkeley.edu/~alanmi/publications/2006/iwls06_sls.pdf
• 23: Alan Mishchenko , Satrajit Chatterjee , Robert Brayton, DAG-aware AIG rewriting a fresh look at combinational logic synthesis, Proceedings of the 43rd annual conference on Design automation, July 24-28, 2006, San Francisco, CA, USA [doi>10.1145/1146909.1147048]
• 24: A. Mishchenko, J. S. Zhang, S. Sinha, J. R. Burch, R. Brayton, and M. Chrzanowska-Jeske, "Using simulation and satisfiability to compute flexibilities in Boolean networks", IEEE Trans. CAD, Vol. 25(5), May 2006, pp. 743--755.
• 25: Janett Mohnke , Paul Molitor , Sharad Malik, Limits of Using Signatures for Permutation Independent Boolean Comparison, Formal Methods in System Design, v.21 n.2, p.167-191, September 2002 [doi>10.1023/A:1016091418702]
• 26: 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
• 27: Matthew W. Moskewicz , Conor F. Madigan , Ying Zhao , Lintao Zhang , Sharad Malik, Chaff: engineering an efficient SAT solver, Proceedings of the 38th conference on Design automation, p.530-535, June 2001, Las Vegas, Nevada, United States [doi>10.1145/378239.379017]
• 28: A. Mukhopadhyay. "Detection of total or partial symmetry of a switching function with the use of decomposition charts". IEEE Trans. Elec. Computers. Vol. 16(10), Oct. 1963, pp. 553--557.
• 29: 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
• 30: M. Pandey and R.E. Bryant, "Exploiting symmetry when verifying transistor-level circuits by symbolic trajectory evaluation," IEEE Trans. CAD, Vol. 18(7), July 1999, pp. 918--935.
• 31: I. Pomeranz and S.M. Reddy, "On determining symmetries in inputs of logic circuits", IEEE Trans. CAD, Vol. 13(11), Nov. 1994, pp. 1428--1434.
• 32: S. Rahardja and B. L. Falkowski. "Symmetry conditions of Boolean functions in complex Hadamard transform", Electronic letters, vol. 34, Aug. 1998, pp. 1634--1635.
• 33: Ch. Scholl, D. Möller, P. Molitor, and R. Drechsler. "BDD minimization using symmetries". IEEE Trans. CAD, Vol. 18(2), Feb. 1999, pp. 81--100.
• 34: SUN Microelectronics. PicoJava Microprocessor Cores. http://www.sun.com/microelectronics/picoJava/
• 35: 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]
• 36: Miroslav N. Velev, Efficient translation of boolean formulas to CNF in formal verification of microprocessors, Proceedings of the 2004 conference on Asia South Pacific design automation: electronic design and solution fair, p.310-315, January 27-30, 2004, Yokohama, Japan
• 37: Guoqiang Wang , Andreas Kuehlmann , Alberto Sangiovanni-Vincentelli, Structural Detection of Symmetries in Boolean Functions, Proceedings of the 21st International Conference on Computer Design, p.498, October 13-15, 2003
• 38: Kuo-Hua Wang , Jia-Hung Chen, K-disjointness paradigm with application to symmetry detection for incompletely specified functions, Proceedings of the 2005 conference on Asia South Pacific design automation, January 18-21, 2005, Shanghai, China [doi>10.1145/1120725.1120775]
• 39: S. Yang. Logic synthesis and optimization benchmarks. Version 3.0. Tech. Report. Microelectronics Center of North Carolina, 1991.
• 40: J. S. Zhang, M. Chrzanowska-Jeske, A. Mishchenko, and J. R. Burch, "Linear cofactor relationships in Boolean functions", IEEE Trans. CAD. To appear in June 2006 issue.

INDEX TERMS

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

General Terms:
Algorithms, Experimentation, Performance, Theory

Keywords:
and-inverter graphs, boolean functions, boolean satisfiability, classical symmetries, simulation