This post is about a paper by Yann Herklotz, James Pollard, Nadesh Ramanathan, and myself that will be presented shortly at OOPSLA 2021.
High-level synthesis (HLS) is an increasingly popular way to design hardware. It appeals to software developers because it allows them to exploit the performance and energy-efficiency of custom hardware without having to learn Verilog, and it appeals to hardware engineers because it offers them the convenient abstractions of high-level software languages like C.
However, there are concerns about its reliability. For instance, Andrew Canis, co-founder of LegUp Computing, has described the HLS process as “inherently prone to introducing bugs or regressions in the final circuit functionality”. Indeed, our own recent work gave credence to those concerns by uncovering several instances where mainstream HLS tools really do compile C programs into incorrect Verilog designs. This lack of reliability undermines the usefulness of HLS in safety-critical contexts.
To address this problem, we have built a new open-source HLS tool, called Vericert, that is mechanically proven correct. This means that whenever Vericert compiles a C program into a Verilog design, the Verilog design is guaranteed to behave in exactly the same way as the C program. To achieve this, we extended an existing verified C compiler called CompCert with a new hardware-specific intermediate language and a new Verilog backend. To phrase Vericert’s correctness theorem, we rely on a Verilog semantics developed by Lööw and Myreen, which we lightly extended to handle a few more language features that we needed. Vericert currently supports most C constructs, including integer operations, function calls (all inlined), local arrays, structs, unions, and general control-flow statements, but currently excludes support for case statements, function pointers, recursive function calls, non-32-bit integers, floats, and global variables.
We used the PolyBench/C benchmark suite to evaluate the performance of Vericert in comparison to an existing open-source HLS tool called LegUp. Area-wise: Vericert fares quite well, generating designs that are only around 10% larger than those generated by LegUp. Speed-wise: we initially found Vericert’s designs to run about 27x slower (!) than LegUp’s. This can mostly be blamed on Vericert’s naive strategy of cramming each operation into a single clock cycle, because whenever complicated operations like divisions are present, the clock has to run really slowly to give them time to complete. After replacing all the divisions in PolyBench/C with iterated shifts, we found Vericert’s designs to be about 2x slower than LegUp’s, which is much less objectionable. The remaining gap can be largely attributed to Vericert’s current lack of support for performing operations in parallel, and that’s a feature we’re working to add at the moment.
Of course, the main selling point of Vericert is its watertight guarantee of correctness, and this is something that we have evaluated empirically too. We used Csmith to generate thousands of random C programs and fed each one into Vericert. When we did this with other HLS tools, they tended to miscompile a few percent of the test programs, but we found that Vericert never produced an incorrect output (once we fixed a little bug in our pretty-printer, which is unverified). To be clear: Vericert quite frequently failed to produce any output at all, due to its lack of support for a few C language features that appeared in the test programs, but it never produced incorrect output.
Vericert is fully open-source and available on Github.