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 , the variable
appearing on the left side of equals, and then is existentially
quantified out of the expression entirely. For example, the
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 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.