SCHEDULING CORRECTNESS CHECKING METHOD AND SCHEDULE VERIFYING METHOD FOR CIRCUIT

摘要

PROBLEM TO BE SOLVED: To provide a method for checking the correctness of scheduling of a circuit and a method for verifying the schedule of the circuit corresponding to the behavior description of the circuit. SOLUTION: The schedule for the circuit is provided from the behavior description. Concerning the method for checking the correctness of scheduling of the circuit, a loop invariant term is extracted for determining the sufficient set of a non-cyclic thread while a loop is inside the circuit, a symbolic simulation is executed for extracting the loop invariant term, and the equivalency of the non-cyclic thread is proved. Concerning the method for verifying the schedule of the circuit corresponding to the behavior description of the circuit, the schedule thread of possible execution containing the loop is selected from the schedule, a correspondent behavior thread is identified out of the behavior description, the un-conditional equivalency of the schedule thread and the behavior thread is proved, and the operation is repeated concerning all the threads of execution.