A Value Propagation Based Equivalence Checking Method for Verification of Code Motion Techniques

A novel value propagation based equivalence checking method of finite state machines with datapath (FSMDs) is presented here for validation of code motion transformations commonly applied during scheduling phase of high-level synthesis. Unlike many other reported techniques, our method is able to handle code motions across loop bodies. This is accomplished by repeated propagation of the mismatched values to subsequent paths until the values match or the final path segments are traversed without finding a match. Checking loop invariance of the values being propagated beyond the loops has been underlined to play an important role. The proposed method is capable of handling control structure modification as well. The method has been implemented and satisfactorily tested for some benchmark examples.