Boolean Manipulation with Free BDDs: An Application in Combinational Logic Verification.
Jordan Gergov, Christoph Meinel · 1994
INTRODUCTION By means of hardware description languages, circuits can be described at a very high level of abstraction which allows the designer to specify the behavior of a circuit beforehand realizing it. In order to validate these specifications and to verify a designed circuit, against its specification, formal methods were developed which lead to problem descriptions in terms of Boolean functions. Then the verification problem is solved by analyzing and manipulating these functions. Here we consider the problem of determining whether a combinational logic circuit C correctly implements a given specification S, i.e. to test whether fC = f S , if fC and f S are the functions realized by C and S, respectively. A common way for doing this [e.g. Eve91] is to construct representations for fC and