Formal Verification of High-Level Synthesis

Add to your list(s) Download to your calendar using vCal

• Yann Herklotz Grave ( Imperial College)
• Monday 07 December 2020, 16:00-17:00
• Teams.

If you have a question about this talk, please contact George A Constantinides.

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 like 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. Worse, there is mounting evidence that existing HLS tools are actually 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-specific intermediate language and a Verilog back end, and has been proven correct in Coq.  Vericert supports all C constructs except for function pointers, recursive function calls, non-integer types and global variables.  An evaluation on all suitable PolyBench benchmarks indicates that it generates hardware with area and cycle counts around a magnitude larger than an existing, unverified HLS tool.

This talk is part of the CAS Talks series.

This talk is included in these lists:

• Andrea Picciau's list
• CAS Talks
• Circuits and Systems Group: Internal Seminars
• Teams

Note that ex-directory lists are not shown.