A novel framework for logic verification in a synthesis environment
- 1 January 1996
- journal article
- Published by Institute of Electrical and Electronics Engineers (IEEE) in IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems
- Vol. 15 (1) , 20-32
- https://doi.org/10.1109/43.486269
Abstract
A new methodology for formal logic verification of combinational circuits is presented. Specifically, a structural (logic network) approach is used, based on indirect implications derived by recursive learning. It is shown that implications can be used to capture similarity between designs. This is extended to formulate a hybrid approach, this structural (logic network) information is used to reduce the complexity of a subsequent functional method based on OBDDs. We demonstrate that OBDD-based verification can take great advantage of structural preprocessing in a synthesis environment where many small operations are performed that modify the circuit. The experimental results show that an effective combination can be achieved between memory efficient structural methods and powerful functional methodsKeywords
This publication has 22 references indexed in Scilit:
- Multi-level Logic Optimization By Implication AnalysisPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2005
- ON THE ACCELERATION OF TEST GENERATION ALGORlTHMSPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2005
- Methods for automatic design error correction in sequential circuitsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- On diagnosis and correction of design errorsPublished 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
- Advanced Verification Techniques Based on LearningProceedings of the 39th conference on Design automation - DAC '02, 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
- Efficient representation and manipulation of switching functions based on ordered Kronecker functional decision diagramsPublished by Association for Computing Machinery (ACM) ,1994
- The transduction method-design of logic networks based on permissible functionsIEEE Transactions on Computers, 1989
- SOCRATES: a highly efficient automatic test pattern generation systemIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 1988