1. A method of checking correctness of scheduling of a circuit where a schedule for the circuit is obtained from a behavioral description, the method comprising: (a) extracting loop invariants to determine a sufficient set of acyclic threads when loops are present in the circuit; (b) performing symbolic simulation to extract the loop invariants; and (c) proving equivalence of the acyclic threads.