This paper describes a formal verification methodology of high-level synthesis (HLS) process. The abstraction level of the input to HLS is so high compared to thatof the output that the verification has to proceed hand-in-hand with the synthesis process. The HLS verificationis performed in three phases in this work. The verification method is based on equivalence checking of two finite state machines with data-paths(FSMDs). Unlike most reported works that targets the individual phases independently, the proposed method applies to all these three phases. The method is strong enoughto accommodate control structure modification of the original behaviour, application of several code motion techniques during scheduling and register optimization during register allocation. It can also verify the correctness of the controller. A hand-in-hand synthesis and verification tool SAST has been developed and tested for effectiveness on several HLS benchmark circuits.