Verification of scheduling in high-level synthesis

This paper describes a formal method for checking the equivalence between two descriptions of the target system, one before and the other after scheduling. The descriptions are represented as finite state machines with data paths (FSMD). The basic principle is to show that any computation of one FSMD is covered by a computation on the other, a computation being characterized by a concatenation of paths in the FSMD. These notions are formalized in the paper. The method is strong enough to accommodate merging of the segments in the original behaviour by the typical scheduler such as DLS, a feature common in scheduling. The method also works for limited arithmetic transformations. Although the proposed method is found to have a non-polynomial worst case complexity, many non-trivial examples encounter a low polynomial order of complexity. The technique is illustrated with an example.