A formal method for checking equivalence between the behavioural specification prior to scheduling and the one produced by the scheduler is described. FSMD (finite state machine with data path) models have been used to represent both the behaviours. The method is strong enough to accommodate merging of path segments in the original behaviour, a feature very common in scheduling but not captured by many works reported in the literature. It is also capable of verifying some arithmetic transformations and many code motion techniques employed during scheduling. Correctness and complexity of the method have been dealt with. Experimental results for several high-level synthesis benchmarks demonstrate the effectiveness of the method.