Equivalence Checking By Logic Relaxation

TL;DR

This paper presents a novel framework called Logic Relaxation for equivalence checking of Boolean circuits, which simplifies the process by relaxing formulas and analyzing the resulting behaviors to verify properties efficiently.

Contribution

It introduces Logic Relaxation as a new technique for equivalence checking, enabling powerful inductive proofs and simplified analysis through partial quantifier elimination.

Findings

Supports equivalence checking with experimental evidence

Facilitates generation of inductive proofs

Simplifies analysis by checking behaviors in relaxed formulas

Abstract

We introduce a new framework for Equivalence Checking (EC) of Boolean circuits based on a general technique called Logic Relaxation (LoR). The essence of LoR is to relax the formula to be solved and compute a superset S of the set of new behaviors. Namely, S contains all new satisfying assignments that appeared due to relaxation and does not contain assignments satisfying the original formula. Set S is generated by a procedure called partial quantifier elimination. If all possible bad behaviors are in S, the original formula cannot have them and so the property described by this formula holds. The appeal of EC by LoR is twofold. First, it facilitates generation of powerful inductive proofs. Second, proving inequivalence comes down to checking the presence of some bad behaviors in the relaxed formula i.e. in a simpler version of the original formula. We give some experimental evidence that supports our approach.