This paper presents a new framework for formal logic verification. What is
depicted here is fundamentally different from previous approaches. In earli
er approaches, the circuit is either not changed during the verification pr
ocess, as in ordered binary decision diagram (OBDD) or implication based me
thods, or the circuit is progressively reduced during verification. Whereas
, in our approach, we actually enlarge the circuits by adding gates during
the verification process. specifically, introduced here is a new technique
that transforms the reference circuit as well as the circuit to be verified
, so that the similarity between the two is progressively enhanced. This re
quires addition of gates to the reference circuit and/or the circuit to be
verified. In the process, we reduce the dissimilarity between the two circu
its, which makes it easier to verify the circuits.
In this paper, we first introduce a method to identify parts of the two cir
cuits which are dissimilar. We use the number of implications that exist be
tween the nodes of one circuit and the nodes of the other circuit as a metr
ic of similarity. As demonstrated, this can be a very useful metric. We for
mulate transformations that can reduce the dissimilarity. These are perform
ed on those parts of the circuits which are found to be dissimilar. These a
dmissible transformations are functionality-preserving and based on certain
Boolean difference formulations. The dissimilarity reduction transformatio
ns introduce new logical relationships between the two circuits that did no
t previously exist. These logical relationships are extracted as new implic
ations, which are then used to reduce the complexity of the verification pr
oblem. These two steps are repeated in succession until the verification pr
ocess is complete. A complete procedure is presented which demonstrates the
power of our logic verification technique. The concept presented in this p
aper can be useful in accelerating verification frameworks which rely on st
ructural methods.