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 parts of the two circuits which are dissimilar. We use the number of ...

• Type: Conference
• Year: 1996
• Where: ICCAD
• Authors: Dhiraj K. Pradhan, Debjyoti Paul, Mitrajit Chatterjee
• Keywords: Formal Logic Verification, Hardware, ICCAD 1996, Reference Circuit, Verification Process