Automated formal verification of scheduling process using finite state machines with datapath (FSMD)

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 defined, 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, integrated with a HLS tool. The proof of correctness of the design is subsequently verified by the PVS proof checker.