Equivalence checking of HWMCC 2012 Circuits

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.