Combined Formal Post- and Presynthesis Verification in High Level Synthesis.

We propose a formal framework based on higher order logic theorem proving as a support for high level synthesis. We suppose that the design process starts from a behavioural or functional specification in terms of a VHDL description. It produces a structural description at the register transfer level. We propose a method for proving the correctness of synthesis results combining the advantages of presynthesis and postsynthesis verification. To perform the postsynthesis task automatically and efficiently correctness-implying properties of an intermediate synthesis result are checked.