VERILAT: verification using logic augmentation and transformations
- 24 December 2002
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
Abstract
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 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.Keywords
This publication has 11 references indexed in Scilit:
- Logic verification using binary decision diagrams in a logic synthesis environmentPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2003
- HANNIBAL: An efficient tool for logic verification based on recursive learningPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Functional learning: a new approach to learning in digital circuitsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- LOT: Logic optimization with testability - new transformations using recursive learningPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- An efficient equivalence checker for combinational circuitsPublished by Association for Computing Machinery (ACM) ,1996
- A novel framework for logic verification in a synthesis environmentIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 1996
- Combinational and sequential logic optimization by redundancy addition and removalIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 1995
- Verification of arithmetic circuits with binary moment diagramsPublished by Association for Computing Machinery (ACM) ,1995
- Recursive learning: a new implication technique for efficient solutions to CAD problems-test, verification, and optimizationIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 1994
- Graph-Based Algorithms for Boolean Function ManipulationIEEE Transactions on Computers, 1986