1. A computer-implemented method of determining if first and second circuits, each with a set of corresponding common primary inputs and corresponding common primary outputs, are equivalent, comprising: representing the first circuit as a first Boolean function; representing the second circuit as a second Boolean function; representing a Boolean space by exclusive ORing the corresponding primary outputs of the first and second Boolean functions; building a decomposed first Binary Decision Diagram for the Boolean space; partitioning the Boolean space into first and second partitions during composition of a decomposition point when the Binary Decision Diagram resulting from composition exceeds a predetermined constraint on computer memory usage; and determining if the first and second partitions are zero.