diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2020-06-30 15:03:47 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2020-06-30 15:03:47 +0100 |
| commit | 7ccf35966e15de7daa30351ddde04663cab38e3c (patch) | |
| tree | 74d510d667b1eaaa5c958cae731388c0df304c55 /introduction.tex | |
| parent | 0cef8950a05b85547ce491b34c12b5e285449e28 (diff) | |
| download | oopsla21_fvhls-7ccf35966e15de7daa30351ddde04663cab38e3c.tar.gz oopsla21_fvhls-7ccf35966e15de7daa30351ddde04663cab38e3c.zip | |
Add examples
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 1476d33..c72f788 100644 --- a/introduction.tex +++ b/introduction.tex @@ -26,7 +26,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 high-level synthesis \JW{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 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: \begin{itemize} \item First mechanised and formally verified HLS flow from C to Verilog. |