Application of BDDs in Boolean matching techniques for formal logic combinational verification

摘要

Verifying that an implementation of a com- bubatuibal circuit its golden specification is an im- oirtabt step in the design process. As inputs and out- puts can be designer, the correspondence between the inputs and the outputs of the synthesized circuit and the in- puts and the outputs of the golden specification has to be restored before checking equivalence.