diff options
Diffstat (limited to 'main.tex')
-rw-r--r-- | main.tex | 9 |
1 files changed, 8 insertions, 1 deletions
@@ -187,7 +187,14 @@ CompCert~\cite{leroy06_formal_certif_compil_back_end} is a C compiler that has b %% Contributions of paper -Using CompCert, we can therefore build a fully verified high-level synthesis tool written in Coq +In this paper we describe a fully verified high-level synthesis tool called CoqUp, which adds a Verilog backend to CompCert and proves that the behaviour of the C code does not change according to existing Verilog semantics. The main contributions of the paper are the following: + +\begin{itemize} + \item Proof by simulation mechanised in Coq between CompCert's intermediate language and Verilog. + \item Description of the Verilog semantics used to integrate it into CompCert's model. +\end{itemize} + +CoqUp is open source and is hosted on Github\footnote{https://github.com/ymherklotz/coqup}. \section{Background} |