diff options
author | Yann Herklotz <git@yannherklotz.com> | 2021-04-16 17:10:19 +0100 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2021-04-16 17:11:02 +0100 |
commit | efa1e45a13c073ab6bec67eec9f195a4dc8c7039 (patch) | |
tree | 71051a866e6799d0de98a9863fc1c907a007e42a /introduction.tex | |
parent | 8746f4b67cc269a116a2497935edeec243a0bb7a (diff) | |
download | oopsla21_fvhls-efa1e45a13c073ab6bec67eec9f195a4dc8c7039.tar.gz oopsla21_fvhls-efa1e45a13c073ab6bec67eec9f195a4dc8c7039.zip |
Add some fixes
Diffstat (limited to 'introduction.tex')
-rw-r--r-- | introduction.tex | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/introduction.tex b/introduction.tex index b532112..146b33c 100644 --- a/introduction.tex +++ b/introduction.tex @@ -40,8 +40,8 @@ We have designed a new HLS tool in the Coq theorem prover and proved that any ou The contributions of this paper are as follows: \begin{itemize} - \item We present \vericert{}, the first mechanically verified HLS tool that compiles C to Verilog. In Section~\ref{sec:design}, we describe the design of \vericert{}, \JW{including a few optimisations related to memory accesses and division.} - \item We state the correctness theorem of \vericert{} with respect to an existing semantics for Verilog due to \citet{loow19_proof_trans_veril_devel_hol}. In Section~\ref{sec:verilog}, we describe how we lightly \JW{Maybe remove `lightly' now -- the changes feel a bit more than just `light' nowadays!} extended this semantics to make it suitable as an HLS target. + \item We present \vericert{}, the first mechanically verified HLS tool that compiles C to Verilog. In Section~\ref{sec:design}, we describe the design of \vericert{}, including a few optimisations related to memory accesses and division. + \item We state the correctness theorem of \vericert{} with respect to an existing semantics for Verilog due to \citet{loow19_proof_trans_veril_devel_hol}. In Section~\ref{sec:verilog}, we describe how we extended this semantics to make it suitable as an HLS target. \item In Section~\ref{sec:proof}, we describe how we proved the correctness theorem. The proof follows standard \compcert{} techniques -- forward simulations, intermediate specifications, and determinism results -- but we encountered several challenges peculiar to our hardware-oriented setting. These include handling discrepancies between byte- and word-addressable memories, different handling of unsigned comparisons between C and Verilog, correctly mapping CompCert's memory model onto a finite Verilog array and finally correctly rearranging memory reads and writes so that these behave properly as a RAM in hardware. \item In Section~\ref{sec:evaluation}, we evaluate \vericert{} on the \polybench{} benchmark suite~\cite{polybench}, and compare the performance of our generated hardware against an existing, unverified HLS tool called \legup{}~\cite{canis11_legup}. We show that \vericert{} generates hardware that is \slowdownOrig$\times$ slower (\slowdownDiv$\times$ slower in the absence of division) and \areaIncr$\times$ larger than that generated by \legup{}. We intend to bridge this performance gap in the future by introducing (and verifying) HLS optimisations of our own, such as scheduling and memory analysis. \end{itemize} |