Update on Overleaf.

1 files changed, 7 insertions, 2 deletions

diff --git a/introduction.tex b/introduction.tex
index b312fe0..166d092 100644
--- a/introduction.tex
+++ b/introduction.tex
@@ -43,12 +43,17 @@ The contributions of this paper are as follows:
 \begin{itemize}
   \item We present \vericert{}, the first mechanically verified HLS tool that compiles C to Verilog. The design of \vericert{} is described in Section~\ref{sec:design}.
   \item We prove \vericert{} correct w.r.t. an existing semantics for Verilog due to \citet{loow19_formalise}. We describe in Section~\ref{sec:verilog} how we lightly extended this semantics to make it suitable as an HLS target. Section~\ref{sec:proof} describes the proof itself.
-  \item We have conducted a performance comparison between \vericert{} and a widely-used (unverified) HLS tool called \legup{}~\cite{canis11_legup} using the PolyBench benchmarks. As described in Section~\ref{sec:evaluation}, \vericert{} generates hardware that is about 9x slower and 21x less area-efficient than that generated by \legup{}. We expect that these numbers will improve when we extend \vericert{} with such optimisations as loop pipelining and scheduling.
+  \item We have conducted a performance comparison between \vericert{} and a widely-used (unverified) HLS tool called \legup{}~\cite{canis11_legup} using the PolyBench benchmarks. As described in Section~\ref{sec:evaluation}, \vericert{} generates hardware that is about 9x slower and 21x less area-efficient than that generated by \legup{}. We expect that these numbers will improve once we have extended \vericert{} with such optimisations as loop pipelining and scheduling.
 \end{itemize}
 
-\vericert{} is fully open source and available online. \JW{We'll have to blind this (and maybe even the name of the tool itself) for submission.}
+\vericert{} is fully open source and available online.
+
 \begin{center}
+\ifANONYMOUS
 \url{https://github.com/ymherklotz/vericert}
+\else 
+
+\fi
 \end{center}