Armin Biere, Marijn Heule, Matti Järvisalo, Norbert Manthey,
"Equivalence checking of HWMCC 2012 Circuits"
, in A. Balint, A. Belov, M. Heule, M. Järvisalo: In Proceedings of SAT Competition 2013, Vol. B-2013-1, Department of Computer Science, University of Helsinki, Seite(n) 104, 2013
Original Titel:
Equivalence checking of HWMCC 2012 Circuits
Sprache des Titels:
Englisch
Original Buchtitel:
In Proceedings of SAT Competition 2013
Original Kurzfassung:
A miter encodes an equivalence check of two Boolean
circuits. This is encoded as a combinatorial problem searching
for an input for these circuits such that their output is different.
Fig 1 shows an illustration of a miter: Two circuits have the
same inputs and there is an exclusive-OR (XOR) for each
output of the circuits. If the output of one of these XORs
can be assigned to true, a certificate is found that shows that
the circuits are not equivalent. Miters are generally used as
follows: one of the two circuits is an optimized variant of
the other one. If the miter has no solution (unsatisfiable), it
means that the circuits are equivalent and that the optimization
is valid.
Forschungs-