next up previous contents
Next: Rewind Up: Reference - Preprocessing Previous: Clustering + Existential Quantification   Contents

Dependent variable clustering

Equations such as the following:

x = and(a, b, c, d, ...)
x = or(a, b, c, d, ...)

appear often in many applications, particularly those related to circuits. In such a case, the BDD corresponding to the equation is conjoined with all other BDDs containing variable $x$, the variable appearing on the left side of equals, and then $x$ is existentially quantified out of the expression entirely. For example, the equations

x = and(a, b, c, d)
y = and(x, e, f, g)

are replaced by

y = and(a, b, c, d, e, f, g)

and $x$ is eliminated.

As it currently exists in the tool, this operation is limited to cases where the BDDs involved all depend on 8 or fewer variables unless the BDDs are special functions and can be conjoined to a SMURF which is reasonably small in size.

John Franco 2011-09-15