Equivalence Checking on System Level Using a Priori Knowledge

Equivalence checking is applied when a system description is refined iteratively to reduce the manual effort required to check the consistency before and after modifications. We present a novel functional equivalence checking algorithm which is especially designed to verify equivalence of two hardware descriptions on the system level. Our algorithm uses a stepwise induction proof guided by counterexamples and incorporates a priori knowledge provided by a designer to speed up reasoning. The a priori knowledge is given symbolically in form of a hypothesis, i.e., A logical formula, which approximates the set of all possible equivalence states of the two designs. The algorithm step wisely refines the hypothesis until either a counterexample has been found disproving equivalence or the hypothesis over approximating all equivalence states. Preliminary experiments for two case studies, a scalable parallel counter and a processor model, show the applicability of our approach in practice.