HANNIBAL: An efficient tool for logic verification based on recursive learning. 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 for this software
References in zbMATH (referenced in 8 articles )
Showing results 1 to 8 of 8.
- Drechsler, R.; Eggersglüß, S.; Fey, G.; Tille, D.: Test pattern generation using Boolean proof engines (2009)
- Fey, Görschwin; Drechsler, Rolf: Robustness and usability in modern design flows (2008)
- Drechsler, Rolf; Fey, Görschwin: Automatic test pattern generation (2006)
- Mukherjee, Rajarshi; Jain, Jawahar; Takayama, Koichiro; Abraham, Jacob A.; Fussell, Donald S.: Efficient combinational verification using overlapping local BDDs and a hash table (2002)
- Williams, Poul Frederick: Formal verification based on Boolean expression diagrams. (2001)
- Huang, Shi-Yu; Cheng, Kwang-Ting: Formal equivalence checking and design debugging (1998)
- Nijssen, R.X.T.; van Eijk, C.A.J.: GreyHound: A methodology for utilizing datapath regularity in standard design flows (1998)
- van Eijk, C.A.J.: A BDD-based verification method for large synthesized circuits (1997)