detecting equivalent output signals to improve the speed of synthesis, and the size of the AIG
If the initial specification contains constraints like G(i <-> o)
or G(i xor o)
we can actually replace o
by i
or !i
everywhere in the formula, solve the problem, and only add o
back on the result. Of course we only remove controllable APs.
Such an output signal can be added to AIG without requiring any additional gate.