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

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

• Type: Conference
• Year: 2006
• Where: DAC
• Authors: Jin S. Zhang, Alan Mishchenko, Robert K. Brayton, Malgorzata Chrzanowska-Jeske
• Keywords: Boolean Satisfiability, Completely-specified Boolean Functions, DAC 2006, Design Automation, Large Boolean Functions