Method for circuit verification and multi-level circuit optimization based on structural implications

摘要

A method for verifies that two integrated circuits are functionally equivalent by extracting equivalencies between internal nodes of the two circuits. Values are assigned to internal nodes in the first circuit and the effects of the assignments are determined in the rest of the first circuit and the second circuit. These effects, or implications, are analyzed to find internal equivalents between the first and second circuit. These steps are repeated with different values assigned to different nodes in the first circuit. The set of stored implications is used to determine if the two circuits are functionally equivalent. A method is also disclosed for using the equivalencies, or indirect implications determined above to remove redundancies from the second circuit using a set of predetermined transformations. Based on an indirect implication a particular transform is selected and applied to the second circuit. This transformation is intended to create redundancies elsewhere in the circuit that can be removed thus optimizing the second circuit.