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 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.