Automated formal verification of scheduling process using finite state machines with datapath (FSMD)
Young Sik Kim, S. Kopuri, Najme Mansouri · 2004
This paper presents a methodology for the formal veri-fication 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 specifi-cation and the scheduled Control-Data Flow Graph (CDFG)- that is the result of scheduling- is established using their FSMD models. The equivalence conditions are mathemati-cally modeled and implemented in the higher-order specifi-cation 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. 1