From e6483607fcb8498a79be996063d6ba809f0d6902 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
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 

