| 摘要 |
PROBLEM TO BE SOLVED: To systematically verify equivalence between two logic circuit descriptions containing even the relation of the timing of the change of an output signal value with respect to the timing of the change of an input signal value. SOLUTION: A stationary finite state machine generation part generates a stationary finite state machine from the individual logic circuit descriptions by referring to auxiliary information. An equivalence verification part proves logic equivalence between the two stationary finite state machines which are thus generated, and it is outputted from an output part 17. The system of equivalence between the circuits shown by circuit description by the circuit description of a low abstraction degree such as a net list between general logic elements containing feedback and circuit description by a transistor net list is verified without constituting a synchronous machine. Thus, the error of the circuit owing to the timing of the change of the input signal, which a designer does not intend, can be removed. |
