Mechanised wire-wise verification of Handel-C synthesis

The compilation of Handel-C programs into net-list descriptions of hardware components has been extensively used in commercial tools but never formally verified. In this paper, we first introduce an extension of the compilation schema that allows the synthesis of the prioritised choice construct. Then we present a variation of the existing semantic model for Handel-C compilation that is amenable to mechanical proof and detailed enough for analysing properties of the hardware generated. We use this model to prove the correctness of the wiring schema used to interconnect the components at the hardware level and propagate control signals among them. Finally, we present the most interesting aspects of the mechanisation of the model and the correctness proofs in the HOL theorem prover.