Novel Verification Framework Combining Structural and OBDD Methods in a Synthesis Environment
- 1 December 1995
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE) in Proceedings of the 39th conference on Design automation - DAC '02
- No. 0738100X,p. 414-419
- https://doi.org/10.1109/dac.1995.249983
Abstract
This paper presents a new methodology for formal logic verification for combinational circuits. Specifically, a structural approach is used, based on indirect implications derived by using Recursive Learning. This is extended to formulate a hybrid approach where this structural method is used to reduce the complexity of a subsequent functional method based on OBDDs. It is demonstrated how OBDD-based verification can take great advantage of structural preprocessing in a synthesis environment. The experimental results show the effective compromise achieved between memory-efficient structural methods and functional methods. One more advantage of these methods lies in the fact that resources that go into logic synthesis can effectively be reused for verification purposes.Keywords
This publication has 15 references indexed in Scilit:
- ON THE ACCELERATION OF TEST GENERATION ALGORlTHMSPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2005
- Logic verification using binary decision diagrams in a logic synthesis environmentPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2003
- Functional approaches to generating orderings for efficient symbolic representationsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2003
- Probabilistic construction and manipulation of Free Boolean DiagramsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Verification of large synthesized designsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- HANNIBAL: An efficient tool for logic verification based on recursive learningPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Dynamic variable ordering for ordered binary decision diagramsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Logic synthesis of 100-percent testable logic networksPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Efficient implementation of a BDD packagePublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- 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