PI: John Wickerson, PhD Student: Yann Herklotz, Imperial College London

  • High-level synthesis (HLS) is the process of automatically translating a software program  into an equivalent hardware design.
  • Existing HLS tools are not as reliable as previously thought.
  • In response, we are developing a new HLS tool whose correctness is formally proven in Coq.

The aim of this project was to make high-level synthesis (HLS) tools more reliable. Using fuzz-testing in the style of Csmith, we have demonstrated that existing HLS tools are not as reliable as previously thought [1]. In response, we are developing a new HLS tool whose correctness is formally proven in Coq.

High-level synthesis (HLS) is the process of automatically translating a software program (written in, e.g., C or C++) into an equivalent hardware design (written in, e.g., Verilog) that can be implemented on a programmable chip (e.g. an FPGA). HLS is attractive because it promises to let software engineers reap the huge performance and energy-efficiency improvements that a custom hardware implementation can bring.

This, together with the increasing power and availability of FPGAs (e.g. in AWS clouds) explains why HLS is rapidly growing in popularity. Conventional compilers have recently made great improvements in reliability thanks to rigorous testing (e.g. with Csmith and other fuzz-testers) and formal verification using a proof assistant (e.g. CompCert).

Yet HLS has not received this attention. The aim of this project is to address that. We will build automatic fuzz-testers that will assess and improve the reliability of existing HLS tools, and we will design and implement a new, formally verified HLS tool that is bug-free by construction, thus setting a new standard for reliability in HLS.

On the testing front, we have fuzz-tested existing HLS tools such as Xilinx Vivado HLS and the Intel HLS Compiler using randomly generated C programs from Csmith, suitably restricted to the language fragment supported by those tools. This effort, led by MSc student Zewei Du and PhD student Yann Herklotz, showed that out of 6700 randomly generated test-cases, 1178 of them failed in at least one of the four tools that we tested. After reducing the test-cases to find their minimal forms, we discovered at least 8 unique bugs, 5 of which have been confirmed by the vendors, and 1 of which has now been fixed. This work emphasises the reliability shortcomings of current HLS tools, and thus motivates the second part of the project.

On the verification front, Herklotz has built a prototype HLS tool called Vericert, fully verified in Coq. It is implemented by extending CompCert with a new hard-ware-oriented intermediate language and a new Verilog backend [2].

Initial benchmarking suggests that Vericert generates hardware designs that are within an order of magnitude, in terms of performance and area-efficiency, of those generated by an existing state-of-the-art HLS tool called LegUp. We are working to close this gap by implementing (and verifying) various optimisations in Vericert. For instance, MEng student Michalis Pardalos has added resource-sharing [3], and Herklotz is adding operator scheduling and pipelined arithmetic

PUBLICATIONS. [1] Y. Herklotz, Z. Du, N. Ramanathan, and J. Wickerson. “An empirical study of the reliability of high-level synthesis tools”. IEEE FCCM 2021. [2] Y. Herklotz, J.D. Pollard, N. Ramanathan, and J. Wickerson. “Formal verification of high-level synthesis”. OOPSLA 2021. [3] M. Pardalos, Y. Herklotz, and J. Wickerson. “Resource sharing for verified high-level synthesis”. In IEEE FCCM 2022.

IMPACT. “Dr Wickerson’s interests mesh with […] Xilinx’s view that robust HLS tools are a technology critical to our future success. The proposal […] to add support for Verilog as a CompCert target would be a significant contribution to the research community. Its principal value lies in the definition of the formal chain of correctness transformations unique to high-level synthesis compilers targeting hardware. Success in defining these transformations and proofs for even a small subset of C would provide a locus for research activity.”
– Dr Samuel Bayliss, Principal Engineer, Xilinx Research Labs, San Jose. –