Sciweavers

Share
DAC
2008
ACM

Bi-decomposing large Boolean functions via interpolation and satisfiability solving

9 years 3 months ago
Bi-decomposing large Boolean functions via interpolation and satisfiability solving
Boolean function bi-decomposition is a fundamental operation in logic synthesis. A function f(X) is bi-decomposable under a variable partition XA, XB, XC on X if it can be written as h(fA(XA, XC ), fB(XB, XC )) for some functions h, fA, and fB. The quality of a bi-decomposition is mainly determined by its variable partition. A preferred decomposition is disjoint, i.e. XC = , and balanced, i.e. |XA| |XB|. Finding such a good decomposition reduces communication and circuit complexity, and yields simple physical design solutions. Prior BDD-based methods may not be scalable to decompose large functions due to the memory explosion problem. Also as decomposability is checked under a fixed variable partition, searching a good or feasible partition may run through costly enumeration that requires separate and independent decomposability checkings. This paper proposes a solution to these difficulties using interpolation and incremental SAT solving. Preliminary experimental results show that t...
Ruei-Rung Lee, Jie-Hong Roland Jiang, Wei-Lun Hung
Added 12 Nov 2009
Updated 12 Nov 2009
Type Conference
Year 2008
Where DAC
Authors Ruei-Rung Lee, Jie-Hong Roland Jiang, Wei-Lun Hung
Comments (0)
books