A formal verification method of datapath and controller generation phase of a high-level synthesis (HLS) process is described in this paper. The goal is achieved in two steps. In step 1, the datapath interconnection and the controller FSM description generated by a high-level synthesis process are analyzed to obtain the register transfer (RT) operations executed in the datapath for a given control assertion pattern in each control step. In step 2, an equivalence checking method is deployed establishing equivalence between the input and the output behaviours of this phase. A rewriting method is proposed for step 1. Unlike many other reported techniques, our method is capable of validating pipelined and multicyle operations, if any, spanning over several states. The correctness and complexity of the proposed method have been treated formally. The method is implemented and integrated with an existing HLS tool, called SAST. The experimental results on several HLS benchmarks indicate the effectiveness of the proposed method.