Verification of Data-path and Controller Generation Phase of High-level Synthesis

The paper describes a verification method of data-path and controller generation phase of high-level synthesis (HLS) process. The goal is achieved in two steps. In step 1, the generated RTL description is analyzed to obtain the register transfer (RT) operations executed in the data-path for a given control assertion pattern in each control step and in step 2, an equivalence checking method is proposed to verify the correctness of the controller. The method is implemented and integrated with an existing HLS tool, called SAST. The experimental results on several HLS benchmarks prove the effectiveness of the proposed method.