Formal verification of high-level synthesis with global code motions.

摘要

Verification has become the bottleneck of any design process. In automated synthesis procedures, there is the additional difficulty to fully or partially automate verification task as well. Consequently, several methods have recently been proposed to automate verification of the synthesized designs or the synthesis processes employed in generation of the design. However, the subset of synthesized designs that can be verified using these methods is limited. One of the open problems is a verification of synthesized designs with global code motion for improving the quality of results for synthesis.; This dissertation presents a methodology for the formal verification of High-Level Synthesis (HLS) with global code motion. We defined a notion of weak equivalence between two Finite State Machines with Datapath (FSMDs). On this basis, we propose a methodology to verify the equivalence between two designs modeled as FSMDs. This methodology is then used to verify the scheduling phase in HLS by establishing functional equivalence between the behavioral specification and the scheduled Control-Data Flow Graph (CDFG)---that is the result of scheduling---using their FSMD models. For scheduling with global code motion, we propose the concept of Recomposed FSMD such that it maintains the functionality of original FSMD, but consists of altered state sequence and/or operations of each state. We generate recomposed FSMDs from FSMD models of scheduling input/output, and verify the scheduling with code motion by establishing the functional equivalence between these recomposed FSMDs. The verification of binding phase is performed by conventional FSMD equivalence definition. The equivalence conditions are mathematically modeled and implemented in the higher-order specification language of theorem-proving environment PVS [30], integrated with a HLS tool. The proof of correctness of the design is subsequently verified by the PVS proof checker.; The goal of the proposed approach is to verify the synthesis results exhaustively by using theorem-proving as our paradigm of choice. It allows us to verify designs of relatively large size and complexity. This would not have been possible in a model-checking environment. A main contribution of this work is a formal verification methodology that can prove the correctness of the HLS processes which use sophisticated scheduling transformations like global code motion. This is realized by automating the functional equivalence checking of FSMDs using theorem-proving, through an induction-based approach.