Formal verification of high-level synthesis

Abstract

Latency, throughput, and energy efficiency are becoming increasingly important, leading to custom hardware accelerators being designed for numerous applications instead of using less efficient general processors. Alas, designing these accelerators can be an error-prone process, especially when using hardware description languages (HDLs) such as Verilog, which operate at the register transfer level.

An attractive alternative is high-level synthesis (HLS), where hardware designs are automatically compiled from software written in a high-level language like C. This way, hardware designers can benefit from mature software development tools. HLS tools promise designs with comparable performance and energy-efficiency to those hand-written in HDLs, reducing the time needed to design new accelerators. Reasoning about behaviour at a higher level should also make the process less error-prone. Unfortunately, HLS tools are unreliable; Vivado HLS produces incorrect designs in 1.2% of randomly generated C programs, undermining testing performed at the higher level of abstraction.

In an attempt to improve this situation, I propose a formally verified HLS tool called Vericert, providing a computer-checked proof that ensures it only generates hardware designs that behave like the input software program. Vericert extends CompCert, an established formally verified C Compiler, with a hardware back-end.

One expects a verified tool to produce significantly worse hardware than existing optimising HLS tools, as each transformation has to be simple enough to be proven correct. Indeed, an initial version of Vericert was up to 8x slower than a state-of-the-art HLS tool called Bambu. However, by verifying hyperblock scheduling in Vericert, a transformation which parallelises instructions in regions of code without loops, hardware produced by Vericert becomes only 1.6x slower than Bambu without optimisations and 3.6x slower than optimised Bambu. This is encouraging, showing that a verified HLS tool is comparable with an existing HLS tool, while being guaranteed to generate correct hardware designs.