diff options
author | John Wickerson <j.wickerson@imperial.ac.uk> | 2020-11-18 16:45:04 +0000 |
---|---|---|
committer | overleaf <overleaf@localhost> | 2020-11-18 16:45:24 +0000 |
commit | 7a269041d29e22d6a16c582a0a3758e5efb70c37 (patch) | |
tree | 9129d4888c6b70d866c421d0700f40ecf08c225e /introduction.tex | |
parent | 11b2a38aec9323ad4bc69ff7505e7f24f6833b39 (diff) | |
download | oopsla21_fvhls-7a269041d29e22d6a16c582a0a3758e5efb70c37.tar.gz oopsla21_fvhls-7a269041d29e22d6a16c582a0a3758e5efb70c37.zip |
Update on Overleaf.
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 b2d25b0..0f0c789 100644 --- a/introduction.tex +++ b/introduction.tex @@ -34,7 +34,7 @@ For example, the translation validation for Catapult C~\cite{mentor20_catap_high Our position is that none of the above workarounds are necessary if the HLS tool can simply be trusted to work correctly. \subsection{Our solution} -We have written a new HLS tool in the Coq theorem prover~\cite{bertot04_inter_theor_provin_progr_devel} and proven that it any output it produces always has the same behaviour as its input. Our tool, which is called \vericert{}, is automatically extracted to an OCaml program from Coq, which ensures that the object of the proof is the same as the implementation of the tool. \vericert{} is built by extending the \compcert{} verified C compiler~\cite{leroy09_formal_verif_realis_compil} with a new hardware-specific intermediate language and a Verilog back end. It supports all C constructs except for function pointers, recursive function calls, non-integer types and global variables. +We have written a new HLS tool in the Coq theorem prover~\cite{bertot04_inter_theor_provin_progr_devel} and proven that it any output it produces always has the same behaviour as its input. Our tool, which is called \vericert{},\ifANONYMOUS\footnote{Tool name has been changed for blind review.}\fi{} is automatically extracted to an OCaml program from Coq, which ensures that the object of the proof is the same as the implementation of the tool. \vericert{} is built by extending the \compcert{} verified C compiler~\cite{leroy09_formal_verif_realis_compil} with a new hardware-specific intermediate language and a Verilog back end. It supports all C constructs except for function pointers, recursive function calls, non-integer types and global variables. \subsection{Contributions and Outline} @@ -42,7 +42,7 @@ 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. The design of \vericert{} is described in Section~\ref{sec:design}. - \item We prove \vericert{} correct w.r.t. an existing semantics for Verilog due to \citet{loow19_formalise}. We describe in Section~\ref{sec:verilog} how we lightly extended this semantics to make it suitable as an HLS target. Section~\ref{sec:proof} describes the proof itself. + \item We prove \vericert{} correct w.r.t. an existing semantics for Verilog due to \citet{loow19_proof_trans_veril_devel_hol}. We describe in Section~\ref{sec:verilog} how we lightly extended this semantics to make it suitable as an HLS target. Section~\ref{sec:proof} describes the proof itself. \item We have conducted a performance comparison between \vericert{} and a widely-used (unverified) HLS tool called \legup{}~\cite{canis11_legup} using the PolyBench benchmarks. As described in Section~\ref{sec:evaluation}, \vericert{} generates hardware that is about 9x slower and 21x less area-efficient than that generated by \legup{}. We expect that these numbers will improve once we have extended \vericert{} with such optimisations as loop pipelining and scheduling. \end{itemize} |