Formal verification of high-level synthesis
File(s)
Published version
Author(s)
Herklotz Grave, Yann
Pollard, JAMES
Ramanathan, nADESH
Wickerson, John
Type
Journal Article
Abstract
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 such as 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.
Furthermore, there is mounting evidence that existing HLS tools are 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 hardwareoriented intermediate language and a Verilog back end, and has been proven correct in Coq. Vericert supports
most C constructs, including all integer operations, function calls, local arrays, structs, unions, and general
control-flow statements. An evaluation on the PolyBench/C benchmark suite indicates that Vericert generates
hardware that is around an order of magnitude slower (only around 2× slower in the absence of division) and
about the same size as hardware generated by an existing, optimising (but unverified) HLS tool.
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 such as 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.
Furthermore, there is mounting evidence that existing HLS tools are 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 hardwareoriented intermediate language and a Verilog back end, and has been proven correct in Coq. Vericert supports
most C constructs, including all integer operations, function calls, local arrays, structs, unions, and general
control-flow statements. An evaluation on the PolyBench/C benchmark suite indicates that Vericert generates
hardware that is around an order of magnitude slower (only around 2× slower in the absence of division) and
about the same size as hardware generated by an existing, optimising (but unverified) HLS tool.
Date Issued
2021-10-18
Date Acceptance
2021-08-31
Citation
Proceedings of the ACM on Programming Languages, 2021, 5 (OOPSLA), pp.1-30
ISSN
2475-1421
Publisher
Association for Computing Machinery (ACM)
Start Page
1
End Page
30
Journal / Book Title
Proceedings of the ACM on Programming Languages
Volume
5
Issue
OOPSLA
Copyright Statement
© 2021 Copyright held by the owner/author(s). This work is licensed under a Creative Commons Attribution 4.0 International License.
License URL
Sponsor
Engineering & Physical Science Research Council (E
National Cybersecurity Centre
The National Cyber Security Centre (NCSC)
Identifier
https://dl.acm.org/doi/10.1145/3485494
Grant Number
Ref: 542716
4214174 / RFA 20601
Publication Status
Published
Article Number
117
Date Publish Online
2021-10-15