Bi-Decomposing Large Boolean Functions via Interpolation and Satisfiability Solving
Date Issued
2009
Date
2009
Author(s)
Lee, Ruei-Rung
Abstract
Boolean function bi-decomposition is a fundamental operation in logic synthesis. Roughly speaking, bi-decomposition is a special kind of decomposition which decomposes a function into a two-input function composed with two other input functions. Precisely speaking, 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 good variable partition makes the decomposition disjoint, i.e. XC = ∅, and balanced, i.e. |XA| ≈ |XB|. Such a good decomposition reduces communication and circuit complexity, and yields simple physical design solutions. Prior BDD-based methods may not be scalable to the decomposition due to the memory explosion problem. Also as decomposability is checked under a fixed variable partition, searching a feasible or good partition may run through costly enumeration that requires separate and independent decomposability checkings. We propose a solution to check whether a function is bi-decomposable using incremental SAT solving. Then, we derive subfunctions by Craig interpolation ifecomposable. Most importantly, we integrate the variable partition into SAT solving. In other words, we do not need to specify the variable partition before checking bi-decomposability. If the given function is bi-decomposable, the SAT solver will generate a feasible and non-trivial variable partition. When n functions are bi-decomposed separately, we have 2n subfunctions. If some subfunctions are complementary or identical to each other, then these subfunctionsan be replaced with each other. By doing so, we can bi-decompose n functions to fewer than 2n subfunctions and reduce circuit size further. Accordingly,t motivates us to bi-decompose multiple functions simultaneously such that some subfunctions can be shared. In this thesis, we consider both single-output and Noutputi-decomposition. Therefore, we use the term ”bi-decomposition” to denote single-output bi-decomposition. Besides, we focus on N-output or-decomposition. Experimental results show that the capacity of bi-decomposition can be scaled up substantially to handle large designs. Also it shows that 2-output or-decomposition can be used to reduce circuit size.
Subjects
bi-decomposition
variable partition
Craig interpolation.
Type
thesis
File(s)![Thumbnail Image]()
Loading...
Name
ntu-98-R96943065-1.pdf
Size
23.32 KB
Format
Adobe PDF
Checksum
(MD5):8f20f95dca6505a82f47699083c500a1