diff options
| -rw-r--r-- | algorithm.tex | 4 | ||||
| -rw-r--r-- | introduction.tex | 8 | ||||
| -rw-r--r-- | main.tex | 10 | ||||
| -rw-r--r-- | verilog.tex | 1 |
4 files changed, 12 insertions, 11 deletions
diff --git a/algorithm.tex b/algorithm.tex index 944c1b3..deafece 100644 --- a/algorithm.tex +++ b/algorithm.tex @@ -9,8 +9,8 @@ The availability of \compcert{}~\cite{leroy09_formal_verif_realis_compil} also p %Since a lot of existing code for HLS is written in C, supporting C as an input language, rather than a custom domain-specific language, means that \vericert{} is more practical. %An alternative was to support LLVM IR as an input language, however, to get a full work flow from a higher level language to hardware, a front end for that language to LLVM IR would also have to be verified. \JW{Maybe save LLVM for the `Choice of implementation language'?} We considered Bluespec~\cite{nikhil04_blues_system_veril}, but decided that although it ``can be classed as a high-level language''~\cite{greaves_note}, it is too hardware-oriented to be suitable for traditional HLS. -We also considered using a language with built-in parallel constructs that map well to parallel hardware, such as occam~\cite{page91_compil_occam}, Spatial~\cite{spatial} or Scala~\cite{chisel}, \JWcouldcut{but found these languages too niche.} -% However, this would not qualify as being HLS due to the manual parallelism that would have to be performed. \JW{I don't think the presence of parallelism stops it being proper HLS.} +We also considered using a language with built-in parallel constructs that map well to parallel hardware, such as occam~\cite{page91_compil_occam}, Spatial~\cite{spatial} or Scala~\cite{chisel}. +% However, this would not qualify as being HLS due to the manual parallelism that would have to be performed. \JW{I don't think the presence of parallelism stops it being proper HLS.} %\JP{I think I agree with Yann here, but it could be worded better. At any rate not many people have experience writing what is essentially syntactic sugar over a process calculus.} %\JW{I mean: there are plenty of software languages that involve parallel constructs. Anyway, perhaps we can just dismiss occam for being too obscure.} diff --git a/introduction.tex b/introduction.tex index ab13d6c..30ad118 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. \paragraph{Our solution} -We have designed a new HLS tool in the Coq theorem prover \JW{I think Coq is so standard that it doesn't need a citation (like you don't cite the C programming language, for instance).}~\cite{bertot04_inter_theor_provin_progr_devel} and proved that any output it produces always has the same behaviour as its input. Our tool, 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 case statements, function pointers, recursive function calls, integers larger than 32 bits, floats, and global variables. +We have designed a new HLS tool in the Coq theorem prover and proved that any output it produces always has the same behaviour as its input. Our tool, 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 case statements, function pointers, recursive function calls, integers larger than 32 bits, floats, and global variables. \paragraph{Contributions and Outline} The contributions of this paper are as follows: @@ -42,10 +42,10 @@ 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{}. \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{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. + \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} - +%\JW{This sentence seems pretty good to me; is it up-to-date with the latest `challenges' you've faced?} \vericert{} is fully open source and available online. \begin{center} @@ -58,7 +58,7 @@ \ANONYMOUSfalse \newif\ifCOMMENTS -\COMMENTSfalse +\COMMENTStrue \newcommand{\Comment}[3]{\ifCOMMENTS\textcolor{#1}{{\bf [\![#2:} #3{\bf ]\!]}}\fi} \newcommand\JW[1]{\Comment{red!75!black}{JW}{#1}} \newcommand\YH[1]{\Comment{green!50!blue}{YH}{#1}} @@ -90,9 +90,9 @@ \newcommand{\compcert}{Comp\-Cert} \newcommand{\legup}{Leg\-Up} -\newcommand{\slowdownOrig}{56} -\newcommand{\slowdownDiv}{10} -\newcommand{\areaIncr}{21} +\newcommand{\slowdownOrig}{30} +\newcommand{\slowdownDiv}{2} +\newcommand{\areaIncr}{1.1} \def\polybench{Polybench/C} @@ -140,7 +140,7 @@ \begin{abstract} 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 like 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. Worse, 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. \JW{Could maybe drop the following sentence from the abstract?} \vericert{} supports all C constructs except for case statements, function pointers, recursive function calls, integers larger than 32 bits, floats, and global variables. \JW{Following sentence needs updating with new figures.} An evaluation on the PolyBench/C benchmark suite indicates that \vericert{} generates hardware that is around an order of magnitude slower and larger than hardware generated by an existing, optimising (but unverified) HLS tool. + 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. \JW{Could maybe drop the following sentence from the abstract?}\YH{Hmm, I don't know actually, I feel like as we don't support all of the C features one might want to know what features are supported.} \vericert{} supports all C constructs except for case statements, function pointers, recursive function calls, integers larger than 32 bits, floats, and global variables. An evaluation on the PolyBench/C benchmark suite indicates that \vericert{} generates hardware that is around an order of magnitude slower but about the same size as hardware generated by an existing, optimising (but unverified) HLS tool.\YH{Technically this is right, but we might want to add the division values.} \end{abstract} %% 2012 ACM Computing Classification System (CSS) concepts diff --git a/verilog.tex b/verilog.tex index c2a8add..ad9af9f 100644 --- a/verilog.tex +++ b/verilog.tex @@ -22,6 +22,7 @@ An example of a rule for executing an \alwaysblock{} that is triggered at the po Two types of assignments are supported in \alwaysblock{}s: nonblocking and blocking assignment. Nonblocking assignments all take effect simultaneously at the end of the clock cycle, %and atomically. while blocking assignments happen instantly so that later assignments in the clock cycle can pick them up. To model both of these assignments, the state $\Sigma$ has to be split into two maps: $\Gamma$, which contains the current values of all variables and arrays, and $\Delta$, which contains the values that will be assigned at the end of the clock cycle. %, we can therefore say that $\Sigma = (\Gamma, \Delta)$. +$\Gamma$ and $\Delta$ each contain Nonblocking assignment can therefore be expressed as follows: \begin{equation*} \inferrule[Nonblocking Reg]{\yhkeyword{name}\ d = \yhkeyword{OK}\ n \\ (\Gamma, e) \downarrow_{\text{expr}} v}{((\Gamma, \Delta), d\ \yhkeyword{ <= } e) \downarrow_{\text{stmnt}} (\Gamma, \Delta [n \mapsto v])}\\ |