A BDD-based Verification Engine for Combinational Equivalence Checking

In this paper we discuss the development of a BDD-based verification engine for combinational equivalence checking. We focus on the techniques used to obtain efficient processing of practical problem instances. These techniques include the detection and utilization of functionally equivalent signals and of isomorphic sub-circuits. Experimental results on well-known benchmarks as well as industrial designs are presented to evaluate these techniques. Keywords---formal verification; logic design and verification; combinational verification; binary decision diagrams I. Introduction With the increasing complexity and tight time-tomarket schedules of today's digital circuits, it is becoming increasingly difficult to design correct circuits. Therefore it is necessary to check throughout the design process that no errors are made. Formal verification methods are clearly gaining acceptance in industry to address this issue. The key characteristic of these methods is that they use formal techn..