Algebraic Decompositions of Cofactors in BDD Representations of a Systems of Incompletely Defined Boolean Functions
In design systems for digital VLSI (Very Large Integrated Circuits), the BDD (Binary Decision Diagrams) is used for VLSI verification, as well as for technologically independent optimization, performed as the first stage in the synthesis of logic circuits in various technological bases. BDD is an acyclic graph defining a Boolean function or a system of Boolean functions. Each vertex of this graph corresponds to the complete or reduced Shannon expansion formula. Having constructed BDD representation for systems of Boolean functions, it is possible to perform additional logical optimization based on the proposed method of searching for algebraic representations of cofactors (subfunctions) of the same BDD level in the form of a disjunction, conjunction of cofactors of the same level of BDD. A directed BDD graph for a system of functions is constructed based on the Shannon expansion of all component functions of the system by the same permutation of variables. The method allows to reduce the number of literals by replacing the Shannon expansion formulas with simpler formulas that are disjunctions or conjunctions of cofactors, and to reduce the number of literals in specifying a system of Boolean functions. The number of literals in algebraic multilevel representations of systems of fully defined Boolean functions is the main optimization criterion in the synthesis of combinational circuits from library logic gates.