HANNIBAL: An efficient tool for logic verification based on recursive learning
- 30 December 2002
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
Abstract
This paper introduces a new approach to logic verification of combinational circuits, which is based on recursive learning. In particular, the described method efficiently extracts equivalencies between internal nodes of the two circuits to be verified. We present a tool, HANNIBAL, which is very efficient for many practical verification problems where such internal equivalencies exist. The presented method can also be used to drastically accelerate other verification tools. Experimental results clearly show the efficiency of HANNIBAL. For example, HANNIBAL verifies the multiplier c6288 against the redundancy-free version c6288nr in only 48 s on a Sparc Workstation ELC.Keywords
This publication has 14 references indexed in Scilit:
- Functional comparison of logic designs for VLSI circuitsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2003
- Logic verification using binary decision diagrams in a logic synthesis environmentPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2003
- Quantifying design quality: a model and design experimentsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2003
- Simulation of non-classical faults on the gate level - The fault simulator COMSIMPublished 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
- Indexed BDDs: algorithmic advances in techniques to represent and verify Boolean functionsIEEE Transactions on Computers, 1997
- Probabilistic verification of Boolean functionsFormal Methods in System Design, 1992
- SOCRATES: a highly efficient automatic test pattern generation systemIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 1988
- Graph-Based Algorithms for Boolean Function ManipulationIEEE Transactions on Computers, 1986
- Binary Decision DiagramsIEEE Transactions on Computers, 1978