diff options
author | John Wickerson <j.wickerson@imperial.ac.uk> | 2021-04-13 19:06:05 +0000 |
---|---|---|
committer | overleaf <overleaf@localhost> | 2021-04-13 19:10:16 +0000 |
commit | 618f9118d899fa8411f88766127df6b147ec0ee5 (patch) | |
tree | 42ce6bd512be66ef581bfaa22a6f251c9e20fda7 /introduction.tex | |
parent | 2b05f33c7dc3588a476bed11c06b488730183846 (diff) | |
download | oopsla21_fvhls-618f9118d899fa8411f88766127df6b147ec0ee5.tar.gz oopsla21_fvhls-618f9118d899fa8411f88766127df6b147ec0ee5.zip |
Update on Overleaf.
Diffstat (limited to 'introduction.tex')
-rw-r--r-- | introduction.tex | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/introduction.tex b/introduction.tex index 56c271e..ab13d6c 100644 --- a/introduction.tex +++ b/introduction.tex @@ -43,7 +43,7 @@ The contributions of this paper are as follows: \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{}. \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 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. \JW{This sentence seems pretty good to me; is it up-to-date with the latest `challenges' you've faced?} These include handling discrepancies between byte- and word-addressable memories, different handling of unsigned comparisons between C and Verilog, and correctly mapping CompCert's memory model onto a finite Verilog array. - \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 \JW{Foll} \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. + \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 \JW{Following needs updating with new figures.} \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} \vericert{} is fully open source and available online. |