System and method for checking equivalence between descriptions

摘要

A behavior synthesis apparatus performs a behavior synthesis while optimizing an intermediate point pair, which is equivalent to each other only under a condition to be referenced. When an equivalence condition is provided for an intermediate cone, an equivalence-condition setting unit provides the intermediate cone with the condition for the equivalence. A logic-cone comparison unit determines whether or not the intermediate cone is equivalent under the provided equivalence condition. An intermediate-point-result reflection unit simplifies the intermediate cone with respect to the intermediate point pair determined to be equivalent in the logic cones to be verified. The logic-cone comparison unit checks the equivalence using the simplified logic cone.