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 the capacity of bi-decomposition can be scaled up substantially to handle large designs.

Functional decomposition is a fundamental operation in logic synthesis. Prior BDD-based approaches to functional decomposition suffer from the memory explosion problem and do not scale well to large Boolean functions. Variable partitioning has to be specified a priori and often restricted to a few bound-set variables. Moreover, non-disjoint decomposition requires substantial sophistication. This paper shows that, when Ashenhurst decomposition (the simplest and preferable functional decomposition) is considered, both single-and multiple-output decomposition can be formulated with satisfiability solving, Craig interpolation, and functional dependency. Variable partitioning can be automated and integrated into the decomposition process without the bound-set size restriction. The computation naturally extends to non-disjoint decomposition. Experimental results show that the proposed method can effectively decompose functions with up to 300 input variables.