Implicit verification of structurally dissimilar arithmetic circuits

In this paper we present a method for verifying structurally dissimilar arithmetic circuits which does not depend on knowledge of the circuit´s intended behavior. Rather than trying to prove that two outputs are equivalent, the method tries to find an implication of the form A→C where the consequent C states that the outputs are equivalent. If we then prove that the antecedent, A, of the implication is true, then our original outputs must be equivalent. Since the truth of A implies the truth of C, we call this method implicit verification. Unlike previously reported implication techniques, we allow the antecedent A to be the conjunction of many conditions rather than a single condition. In addition to allowing more general antecedents, we give a method for choosing them in a useful manner. Using this implicit verification technique, we have been able to verify a 32×32 array multiplier versus a 32×32 Wallace tree multiplier