diff options
| -rw-r--r-- | algorithm.tex | 2 | ||||
| -rw-r--r-- | introduction.tex | 4 | ||||
| -rw-r--r-- | main.tex | 7 |
3 files changed, 9 insertions, 4 deletions
diff --git a/algorithm.tex b/algorithm.tex index 4d8b1da..b9012ce 100644 --- a/algorithm.tex +++ b/algorithm.tex @@ -25,7 +25,7 @@ \draw[->] (rtl) -- (dfgstmd); \draw[->] (dfgstmd) -- (verilog); \end{tikzpicture}} - \caption{Verilog backend branching off at the RTL stage. \JW{It's a real nightmare that `RTL' is so ambiguous, meaning both software and hardware. I think we have to do something about it. One possibility: according to the CompCert webpages, software RTL is `also known as 3-address code', so we could replace (software) `RTL' with `3AC' (and give a footnote to explain why). Is it also possible to replace (hardware) `RTL' with just `Verilog'? I know Verilog could mean RTL or netlist, but since this paper doesn't talk much about RTL-to-netlist synthesis, perhaps that doesn't matter? Or perhaps RTL could be replaced with FSMD? Or even just `hardware design'?}}% + \caption{Verilog backend branching off at the RTL stage. \JW{It's a real nightmare that `RTL' is so ambiguous, meaning both software and hardware. I think we have to do something about it. One possibility: according to the CompCert webpages, software RTL is `also known as 3-address code', so we could replace (software) `RTL' with `3AC' (and give a footnote to explain why). Is it also possible to replace (hardware) `RTL' with just `Verilog'? I know Verilog could mean RTL or netlist, but since this paper doesn't talk much about RTL-to-netlist synthesis, perhaps that doesn't matter? Or perhaps RTL could be replaced with FSMD? Or even just `hardware design'?}\YH{I like that suggestion, I will actually replace RTL by 3AC then, and at least in this figure I did purposefully replace RTL by Verilog, and wanted to do it throughout the paper.}}% \label{fig:rtlbranch} \end{figure} diff --git a/introduction.tex b/introduction.tex index cb1ed1e..290d6a4 100644 --- a/introduction.tex +++ b/introduction.tex @@ -2,7 +2,9 @@ %% Motivation for why HLS might be needed -The current approach \JW{Maybe `the' is too strong -- could say `One current approach'.} to writing energy-efficient and high-throughput applications is to use application-specific hardware, instead of relying on a general-purpose CPU.\@ However, custom hardware designs come at the cost of having to design and produce them, which can be a tedious and error-prone process using hardware description languages (HDL) such as Verilog. Especially with the size of hardware designs growing over the years, it can become difficult to verify that the hardware design behaves in the expected way, as simulation of HDLs can be quite inefficient. Furthermore, the algorithms that are being accelerated in hardware often already have a software implementation, meaning they have to be reimplemented efficiently in a hardware description language which can be time-consuming. +% \JW{Maybe `the' is too strong -- could say `One current approach'.} + +One current approach to writing energy-efficient and high-throughput applications is to use application-specific hardware, instead of relying on a general-purpose CPU.\@ However, custom hardware designs come at the cost of having to design and produce them, which can be a tedious and error-prone process using hardware description languages (HDL) such as Verilog. Especially with the size of hardware designs growing over the years, it can become difficult to verify that the hardware design behaves in the expected way, as simulation of HDLs can be quite inefficient. Furthermore, the algorithms that are being accelerated in hardware often already have a software implementation, meaning they have to be reimplemented efficiently in a hardware description language which can be time-consuming. %% Definition and benefits of HLS One possible alternative to the tedious design process of custom hardware is to use high-level synthesis (HLS), which is the process of generating custom hardware, represented in an HDL, based on a behavioural description, often in a subset of C. This elevates the level of abstraction, because the description of the algorithm in C is inherently untimed, meaning actions don't have to be scheduled into clock cycles manually. The higher level of abstraction makes it easier to reason about the algorithms and therefore also facilitates maintaining them. As a result the time to design the hardware is reduced significantly, especially if a software description of the algorithm already exists, because there is no need to redesign at a lower level and directly in hardware. In addition, using HLS to design the hardware has the benefit of making the functional verification of the design much more efficient and simple than at the HDL stage, since the entire software ecosystem can be mobilised for this @@ -125,9 +125,12 @@ \email{j.wickerson@imperial.ac.uk} \begin{abstract} - High-level synthesis (HLS) refers to automatically compiling software into hardware. In a world increasingly reliant on application-specific hardware accelerators, HLS provides a higher-level of abstraction for hardware designers, while also benefitting from \JW{This sentence is slightly confused because it's not really `HLS' that benefits, it's the HLS user who benefits.} the rich software ecosystem to verify the functionality of their designs. However, adoption of HLS in safety-critical applications is still limited, because current tools cannot verify \JW{`cannot verify' is a dubious claim -- I guess something like SLEC can technically verify that the hardware is correct, but it's a big faff to use it} that the hardware implements the same behaviour as the software it was generated from, eliminating the benefits that software verification may provide. There is even evidence that HLS tools tend to be quite unreliable instead, either generating wrong hardware or sometimes not generating any hardware at all. \JW{`Not generating hardware' isn't too bad, and indeed VeriCert is guilty of that too, when presented with C programs that contain features that it can't yet handle. The real problem is the HLS tool crashing unceremoniously.} + % \JW{This sentence is slightly confused because it’s not really ‘HLS’ that benefits, it’s the HLS user who benefits.} + % \JW{‘cannot verify’ is a dubious claim – I guess something like SLEC can technically verify that the hardware is correct, but it’s a big faff to use it} + % \JW{‘Not generating hardware’ isn’t too bad, and indeed VeriCert is guilty of that too, when presented with C programs that contain features that it can’t yet handle. The real problem is the HLS tool crashing unceremoniously.} + High-level synthesis (HLS) refers to automatically compiling software into hardware. In a world increasingly reliant on application-specific hardware accelerators, HLS provides a higher-level of abstraction for hardware designers, while also allowing the designers to benefit from the rich software ecosystem to verify the functionality of their designs. However, adoption of HLS in safety-critical applications is still limited, because it may be infeasible to verify that the hardware implements the same behaviour as the software it was generated from, eliminating the benefits that software verification may provide. There is also evidence that HLS tools tend to be quite unreliable instead, either generating wrong hardware or sometimes crashing in unexpected ways for supported inputs. - We present the first mechanically verified HLS tool that preserves the behaviour of the software according to our semantics. Our tool, called VeriCert, extends the CompCert verified C compiler and consists of a new hardware specific \JW{hardware-specific} intermediate language and a Verilog back end, which has been proven correct in Coq. VeriCert supports all C constructs except for function pointers, recursive function calls, non-integer types and global variables. It has been evaluated on all suitable PolyBench benchmarks, which indicates that it generates hardware with area and cycle count around a magnitude larger than an existing, unverified HLS tool. \JW{Hopefully in due course we can nuance this a bit by adding in some figures relating to the unverified Vericert extensions.} + We present the first mechanically verified HLS tool that preserves the behaviour of the software according to our semantics. Our tool, called VeriCert, extends the CompCert verified C compiler and consists of a new hardware-specific intermediate language and a Verilog back end, which has been proven correct in Coq. VeriCert supports all C constructs except for function pointers, recursive function calls, non-integer types and global variables. It has been evaluated on all suitable PolyBench benchmarks, which indicates that it generates hardware with area and cycle count around a magnitude larger than an existing, unverified HLS tool. \JW{Hopefully in due course we can nuance this a bit by adding in some figures relating to the unverified Vericert extensions.}\YH{This might be the case, but maybe we want to keep that for a completely new paper as discussed.} \end{abstract} %% 2012 ACM Computing Classification System (CSS) concepts |