Formal verification of high-level synthesis
Formal verification of high-level synthesis
复制标题
高级综合的形式化验证
DOI：
--
复制
发表时间：
2021
期刊：
影响因子：
--
通讯作者：
John Wickerson
中科院分区：
文献类型：
--
作者：
Yann Herklotz;James D. Pollard;Nadesh Ramanathan;John Wickerson
高级综合（High-level synthesis， HLS）是指将软件自动编译成硬件的技术，目前正迅速普及。在一个越来越依赖于特定应用硬件加速器的世界里，HLS承诺硬件设计的性能和能效与那些用硬件描述语言（如Verilog）手工编码的硬件设计相当，同时保持了软件开发的便利性和丰富的生态系统。然而，当前的HLS工具不能总是保证它们产生的硬件设计与给出的软件相同，从而破坏了在软件级别进行的任何推理。此外，越来越多的证据表明，现有的HLS工具非常不可靠，有时会生成错误的硬件或在给定有效输入时崩溃。为了解决这个问题，我们提出了第一个经过机械验证以保持其输入软件行为的HLS工具。我们的工具名为Vericert，它使用一种新的面向硬件的中间语言和Verilog后端扩展了经过CompCert验证的C编译器，并且在Coq中被证明是正确的。Vericert支持大多数C语言结构，包括所有整数操作、函数调用、局部数组、结构体、联合和通用控制流语句。对PolyBench/C基准套件的评估表明，Vericert生成的硬件大约慢一个数量级（在没有除法的情况下仅慢2倍左右），并且与现有的优化（但未经验证）HLS工具生成的硬件大小相同。
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 hardware-oriented 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.
影响因子：
--
作者：
Yuting Wang;Xiangzhe Xu;Pierre Wilke;Zhong Shao
通讯作者：
Yuting Wang;Xiangzhe Xu;Pierre Wilke;Zhong Shao