diff options
Diffstat (limited to 'introduction.tex')
| -rw-r--r-- | introduction.tex | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/introduction.tex b/introduction.tex index bcaf52f..8411ebe 100644 --- a/introduction.tex +++ b/introduction.tex @@ -25,28 +25,28 @@ However, the fact that the behaviour is preserved after HLS cannot be guaranteed %%\NR{Having said that, keep the text for related work section.}\YH{Added into related works.} To mitigate the problems about the unreliability of synthesis tool, it is often required to check the generated hardware for functional correctness. This is commonly done by simulating the design with a large test-bench, however, the guarantees are only as good as the test-bench, meaning if all the inputs were not covered, there is a risk that bugs remain in the untested code. To ensure that the hardware does indeed behave in the same way as the C code, it may therefore be necessary to prove that they are equivalent. Translation validation~\cite{pnueli98_trans} is the main method which is used to prove that the HLS translation was successful, and has been successfully applied to many HLS optimisations~\cite{kim04_autom_fsmd,karfa06_formal_verif_method_sched_high_synth,chouksey20_verif_sched_condit_behav_high_level_synth,banerjee14_verif_code_motion_techn_using_value_propag,chouksey19_trans_valid_code_motion_trans_invol_loops}. However, the main problem is that the validator itself has often not been mechanically proven correct, meaning that the implementation is quite separate from the proof. In addition to that, with large designs it may not be feasible to perform translation validation, as the state space would grow exponentially. \JW{Does this link back to Mentor's Catapult-C, which you mentioned earlier? Does Catapult-C attempt to do translation validation as part of its HLS process? And if so, can you make the point that this effort is largely ineffective because once the design is a reasonable size, the translation validation usually fails anyway?}\YH{TODO: Currently I only have a whitepaper which goes over the translation validation in a very high level, but they do actually mention some flakiness and state that the user would have to manually change the code to fix that. So I think I can actually make that point. I just realised they have a pretty funny diagram of verification $\rightarrow$ differences $\rightarrow$ adjustments $\rightarrow$ ... until it is finally verified.} A mechanically verified HLS tool would remove the need to perform simulation after the synthesis process if one has proven desirable properties about the C code. In addition to that, it would allow for the implementation of optimisation passes which are also proven correct mechanically by translation validation, thereby greatly improving the reliability of these passes. -CompCert~\cite{leroy06_formal_certif_compil_back_end} is a C compiler that has been written and formally verified in the Coq theorem prover~\cite{bertot04_inter_theor_provin_progr_devel}. First of all, most of the compiler passes in CompCert have been proven correct, meaning that once the compiler is built, the proofs can be erased as the algorithm has been shown to be correct independent of the input. However, some optimisation passes such as software pipelining require translation validation~\cite{tristan08_formal_verif_trans_valid}, in which case the correctness of the compiler pass needs to be checked at runtime. However, even in this case the verifier itself is proven to only verify code correct that does indeed behave in the same way. +\compcert{}~\cite{leroy06_formal_certif_compil_back_end} is a C compiler that has been written and formally verified in the Coq theorem prover~\cite{bertot04_inter_theor_provin_progr_devel}. First of all, most of the compiler passes in \compcert{} have been proven correct, meaning that once the compiler is built, the proofs can be erased as the algorithm has been shown to be correct independent of the input. However, some optimisation passes such as software pipelining require translation validation~\cite{tristan08_formal_verif_trans_valid}, in which case the correctness of the compiler pass needs to be checked at runtime. However, even in this case the verifier itself is proven to only verify code correct that does indeed behave in the same way. %% Contributions of paper -In this paper we describe a fully verified HLS tool called Vericert, which adds a Verilog back end to CompCert and proves that the behaviour of the C code is preserved with respect to an existing Verilog semantics. The main contributions of the paper are the following: +In this paper we describe a fully verified HLS tool called \vericert{}, which adds a Verilog back end to \compcert{} and proves that the behaviour of the C code is preserved with respect to an existing Verilog semantics. The main contributions of the paper are the following: \begin{itemize} \item First mechanised and formally verified HLS flow from C to Verilog. - \item Proof by simulation mechanised in Coq between CompCert's intermediate language and Verilog. - \item Description of the Verilog semantics integrated into CompCert and how this interacts with CompCert's intermediate language. + \item Proof by simulation mechanised in Coq between \compcert{}'s intermediate language and Verilog. + \item Description of the Verilog semantics integrated into \compcert{} and how this interacts with \compcert{}'s intermediate language. \item Correct by construction Verilog code for four programs that are part of the CHStone benchmark suite, which is a well-known HLS benchmark. -%% \item \NR{We implement our Verilog semantics in CompCert and we are able to generate correct-by-construction Verilog for all programs in the CHStone benchmark suite, which is a well-known HLS benchmark.} +%% \item \NR{We implement our Verilog semantics in \compcert{} and we are able to generate correct-by-construction Verilog for all programs in the CHStone benchmark suite, which is a well-known HLS benchmark.} \end{itemize} -The first section will describe the Verilog semantics that were used and extended to fit into CompCert's model. The second section will then describe the HLS algorithm, together with its proof. +The first section will describe the Verilog semantics that were used and extended to fit into \compcert{}'s model. The second section will then describe the HLS algorithm, together with its proof. -Vericert is open source and is hosted on GitHub\footnote{\url{https://github.com/ymherklotz/vericert}}. +\vericert{} is open source and is hosted on GitHub\footnote{\url{https://github.com/ymherklotz/vericert}}. \NR{Other comments:} \NR{Is both the translator and verifier written in Coq?}\YH{Currently there is no verifier, the algorithms themselves are proven directly in Coq.} %%\NR{A tool-flow diagram here will be useful. I thought you had one previously?} -\NR{Do you think we have a very simple example of a program where wrong Verilog is generated in VHLS or LegUp, but not in Vericert?}\YH{The LegUp example actually with the shift might be a good one.} +\NR{Do you think we have a very simple example of a program where wrong Verilog is generated in VHLS or LegUp, but not in \vericert{}?}\YH{The LegUp example actually with the shift might be a good one.} %%% Local Variables: %%% mode: latex |