VERILAT: verification using logic augmentation and transformations

This paper presents a new framework for formal logic verification. What is depicted here is fundamentally different from previous approaches. In earlier approaches, the circuit is either not changed during the verification process, as in ordered binary decision diagram (OBDD) or implication-based methods, 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 requires addition of gates to the reference circuit and/or the circuit to be verified. In the process, we reduce the dissimilarity between the two circuits, which makes it easier to verify the circuits. In this paper, we first introduce a method to identify pacts of the two circuits which are dissimilar. We use the number of implications that exist between the nodes of one circuit and the nodes of the other circuit as a metric of similarity. As demonstrated, this can be a very useful metric. We formulate transformations that can reduce the dissimilarity. These are performed on those parts of the circuits which are found to be dissimilar. These admissible transformations are functionality-preserving and based on certain Boolean difference formulations. The dissimilarity reduction transformations introduce new logical relationships between the two circuits that did not previously exist. These logical relationships are extracted as new implications, which are then used to reduce the complexity of the verification problem. These two steps are repeated in succession until the verification process is complete