From e6483607fcb8498a79be996063d6ba809f0d6902 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Tue, 9 Jun 2020 13:15:42 +0100 Subject: Mostly finished first draft of intro --- main.tex | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) (limited to 'main.tex') diff --git a/main.tex b/main.tex index b3c9846..8bbcf5a 100644 --- a/main.tex +++ b/main.tex @@ -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} -- cgit