High-level synthesis (HLS), which refers to the automatic compilation of software into hardware, is
rapidly gaining popularity. In a world increasingly reliant on application-specific hardware
accelerators, HLS promises hardware designs of comparable performance and energy efficiency to those
coded by hand in a hardware description language such as Verilog, while maintaining the convenience
and the rich ecosystem of software development. However, current HLS tools cannot always guarantee
that the hardware designs they produce are equivalent to the software they were given, thus
undermining any reasoning conducted at the software level. Furthermore, there is mounting evidence
that existing HLS tools are quite unreliable, sometimes generating wrong hardware or crashing when
given valid inputs.

To address this problem, we present the first HLS tool that is mechanically verified to preserve the
behaviour of its input software. Our tool, called Vericert, extends the CompCert verified C
compiler with a new hardware-oriented intermediate language and a Verilog back end, and has been
proven correct in Coq. Vericert supports most C constructs, including all integer operations,
function calls, local arrays, structs, unions, and general control-flow statements. An evaluation
on the PolyBench/C benchmark suite indicates that Vericert generates hardware that is around an
order of magnitude slower (only around 2$\times$ slower in the absence of division) and about the
same size as hardware generated by an existing, optimising (but unverified) HLS tool.