Probabilistic manipulation of Boolean functions using free Boolean diagrams

We propose a data structure for Boolean functions termed “the free Boolean diagram.” A free Boolean diagram allows decision vertices as in the conventional binary decision diagram, but also allows function vertices corresponding to the AND and XOR functions. It has been shown previously that the equivalence of two free Boolean diagrams can be decided probabilistically in polynomial time. Based on the equivalence checking method, we develop a set of algorithms for the probabilistic construction of free Boolean diagrams from multilevel combinational logic circuits, and for their manipulation. These algorithms are modified versions of reduced, ordered binary decision diagram manipulation methods. We provide the implementation details of a free Boolean diagram package. We show that functions difficult to verify using reduced, ordered binary decision diagrams can be verified using the free Boolean diagrams package using substantially less memory