To SAT or not to SAT: Ashenhurst decomposition in a large scale

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 singleand 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 nondisjoint decomposition. Experimental results show that the proposed method can effectively decompose functions with up to 300 input variables.

• Type: Conference
• Year: 2008
• Where: ICCAD
• Authors: Hsuan-Po Lin, Jie-Hong Roland Jiang, Ruei-Rung Lee
• Keywords: Decomposition Process, Functional Decomposition Suffer, Hardware, ICCAD 2008, Preferable Functional Decomposition