Improvements to satisfiability-based boolean function bi-decomposition
- 1 October 2011
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- p. 142-147
Abstract
Boolean function decomposition is ubiquitous in logic synthesis. Existing solutions are based on BDDs and, more recently, on Boolean Satisfiability (SAT). A widely studied special case is function bi-decomposition, where a function is decomposed into two other functions connected with a simple gate. Recent work exploited the identification of Minimally Unsatisfiable Subformulas (MUSes) for computing the sets of variables to use in Boolean function bi-decomposition. This paper develops new techniques for improving the use of MUSes in function bi-decomposition. The first technique exploits structural properties of the function being decomposed, whereas the second technique exploits group-oriented MUSes. Experimental results obtained on representative benchmarks demonstrate significant improvements in performance and in the quality of decompositions.Keywords
This publication has 13 references indexed in Scilit:
- To SAT or Not to SAT: Scalable Exploration of Functional DependencyIEEE Transactions on Computers, 2010
- A compositional theory for post-reboot observational equivalence checking of hardware2009
- Sequential logic synthesis using symbolic bi-decomposition2009
- DDBDD: Delay-Driven BDD Synthesis for FPGAsIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 2008
- Bi-decomposing large Boolean functions via interpolation and satisfiability solving2008
- Algorithms for Computing Minimal Unsatisfiable Subsets of ConstraintsJournal of Automated Reasoning, 2007
- Timing-driven logic bi-decompositionIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 2003
- Technology mapping for TLU FPGAs based on decomposition of binary decision diagramsIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 1996
- A General Approach to Boolean FunctionDecomposition and its Application in FPGABasedSynthesisVLSI Design, 1995
- BDD based decomposition of logic functions with application to FPGA synthesis1993