A NOVEL FRAMEWORK FOR LOGIC VERIFICATION IN A SYNTHESIS ENVIRONMENT

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.