diff options
Diffstat (limited to 'introduction.tex')
| -rw-r--r-- | introduction.tex | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/introduction.tex b/introduction.tex index 290d6a4..bcaf52f 100644 --- a/introduction.tex +++ b/introduction.tex @@ -29,7 +29,7 @@ CompCert~\cite{leroy06_formal_certif_compil_back_end} is a C compiler that has b %% Contributions of paper -In this paper we describe a fully verified HLS tool called CoqUp, 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. @@ -41,12 +41,12 @@ In this paper we describe a fully verified HLS tool called CoqUp, which adds a V 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. -CoqUp is open source and is hosted on GitHub\footnote{\url{https://github.com/ymherklotz/coqup}}. +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 CoqUp?}\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 |