PLDI: G: Formal Verification of High-Level Synthesis

As latency, throughput and energy efficiency become increasingly important, custom hardware accelerators are being designed for numerous applications. Alas, designing these accelerators can be a tedious and error-prone process using a hardware description language (HDL) such as Verilog. An attractive alternative is high-level synthesis (HLS), in which hardware designs are automatically compiled from software written in a high-level language like C. Modern HLS tools such as LegUp [1], Vivado HLS [2], Intel i++ [3], and Bambu HLS [4] promise designs with comparable performance and energy-efficiency to those hand-written in an HDL [5], while offering the convenient abstractions and rich ecosystems of software development. But existing HLS tools cannot always guarantee that the hardware designs they produce are equivalent to the software they were given, and this undermines any reasoning conducted at the software level. Indeed, there are reasons to doubt that HLS tools actually do always preserve equivalence. For instance, Vivado HLS has been shown to apply pipelining optimisations incorrectly1 or to silently generate wrong code should the programmer stray outside the fragment of C that it supports.2 Meanwhile, Lidbury et al. [6] had to abandon their attempt to fuzz-test Altera’s (now Intel’s) OpenCL compiler since it “either crashed or emitted an internal compiler error” on so many of their test inputs. More recently, Herklotz et al. [7] fuzz-tested three commercial HLS tools using Csmith [8], and despite restricting the generated programs to the C fragment explicitly supported by all the tools, they still found that on average 2.5% of test cases generated a design that did not match the behaviour of the input.