Proving Wire-Wise Correctness for Handel-C Hardware Compilation in HOL

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 the authors first introduce a variation of the existing semantic model for Handel-C compilation that is amenable for mechanical proofs and detailed enough to analyse properties about the generated hardware. They then use this model to prove the correctness of the wiring schema used to interconnect the different components at the hardware level and propagate control signals among them. Finally, they present the most interesting aspects of the mechanisation of the model and the correctness proofs in the HOL theorem prover.