W. Kunz et al., A NOVEL FRAMEWORK FOR LOGIC VERIFICATION IN A SYNTHESIS ENVIRONMENT, IEEE transactions on computer-aided design of integrated circuits and systems, 15(1), 1996, pp. 20-32
A new methodology for formal logic verification of combinational circu
its is presented. Specifically, a structural (logic network) approach
is used, based on indirect implications derived by recursive learning,
It is shown that implications can be used to capture similarity betwe
en designs, This is extended to formulate a hybrid approach, this stru
ctural (logic network) information is used to reduce the complexity of
a subsequent functional method based on OBDD's. We demonstrate that O
BDD-based verification can take great advantage of structural preproce
ssing in a synthesis environment where many small operations are perfo
rmed that modify the circuit. The experimental results show that an ef
fective combination can be achieved between memory efficient structura
l methods and powerful functional methods.