Verifying clock schedules

Timing verification and optimization have been formulated as mathematical programming problems. The computational aspects of using such a formulation for verifying clock schedules are considered. The formulation can have multiple solutions, and these extraneous solutions can cause previously published algorithms to produce incorrect or misleading results. The conditions under which multiple solutions exist are characterized, and it is shown that even when the solution is unique, the running times of these previous algorithms can be unbounded. By contrast, a simple polynomial time algorithm for clock schedule verification is exhibited. The algorithm was implemented and used to check the timing of all the circuits in the ISCAS-89 benchmark suite. Observed running times are linear in circuit size and quite practical.<>