Equivalence checking by logic relaxation
Eugene Goldberg · 2016
We introduce a new framework for Equivalence Checking (EC) of Boolean circuits based on a general technique called Logic Relaxation (LoR). LoR is meant for checking if a propositional formula G has only “good” satisfying assignments specified by a design property. The essence of LoR is to relax G into a formula Grlxand compute a set S that contains all assignments that satisfy Grlxbut do not satisfy G. If all bad satisfying assignments are in S, formula G can have only good ones and the design property in question holds. Set S is built by a procedure called partial quantifier elimination. The appeal of EC by LoR is twofold. First, it facilitates generation of powerful inductive proofs. Second, proving inequiv-alence comes down to checking the existence of some assignments satisfying Grlxi.e. a simpler version of the original formula. We give experimental evidence that supports our approach.