Data-Flow Driven Equivalence Checking for Verification of Code Motion Techniques

Code motion techniques are extensively used in the pre-synthesis optimization and the scheduling phases of high-level synthesis (HLS) of digital circuits for control intensive behaviours. A formal verification method for checking correctness of code motion techniques is presented in this paper. Finite state machine with datapath (FSMD) models have been used to represent the input and the output behaviours of each synthesis step. The method consists in introducing cut points in one FSMD, visualizing its computations as concatenation of paths from cutpoints to cutpoints, and identifying equivalent finite path segments in the other FSMD, the process is then repeated with the FSMDs interchanged. It has been underlined in this work that for non-uniform code motions, identifying equivalent path segment involves model checking of specific data-flow driven properties. Unlike many other reported techniques, the method is capable of verifying both uniform and non-uniform code motion techniques. The method is tested on the synthesis results of a high-level synthesis tool called SPARK for several HLS benchmarks. Experimental results demonstrate the effectiveness of the method.