Abstract
This paper presents a methodology for the formal verification of scheduling during High-Level Synthesis(HLS). A notion of functional equivalence between two Finite State Machines with Datapath (FSMDs) is de.ned, on the basis of which we propose a methodology to verify scheduling. The functional equivalence between the behavioral specification and the scheduled Control-Data Flow Graph (CDFG) - that is the result of scheduling - is established using their FSMD models. The equivalence conditions are mathematically modeled and implemented in the higher-order specification language of theorem proving environment PVS [11], integrated with a HLS tool. The proof of correctness of the design is subsequently verified by the PVS proof checker.