|
|||||
|
|
Application of BDDs in Boolean matching techniques for formal logic combinational verification |
|
| Authors: | Janett Mohnke Paul Molitor Sharad Malik |
| Affiliation: | (1) DResearch Digital Media Systems, Otto-Schmirgal-Strasse 3, 10319 Berlin, Germany; E-mail: mohnke@dresearch.de, DE;(2) Institute for Computer Science, Martin-Luther-University, 06009 Halle an der Saale, Germany; E-Mail: molitor@informatik.uni-halle.de, DE;(3) Department of Electrical Engineering, Princeton University, Princeton, NJ 08544, USA; E-mail: malik@ee.princeton.edu, US |
| Abstract: | Verifying that an implementation of a combinational circuit meets its golden specification is an important step in the design process. As inputs and outputs can be swapped by synthesis tools or by interaction of the designer, the correspondence between the inputs and the outputs of the synthesized circuit and the inputs and the outputs of the golden specification has to be restored before checking equivalence. In this paper, we review the main approaches to this isomorphism problem and show how to apply OBDDs in order to obtain efficient methods. Published online: 15 May 2001 |
| Keywords: | : Formal verification – Permutation independent comparison of Boolean functions – Signature of Boolean variables |
| 本文献已被 SpringerLink 等数据库收录！ | |