Update on Overleaf.

1 files changed, 2 insertions, 2 deletions

diff --git a/verified_resource_sharing.tex b/verified_resource_sharing.tex
index 7b01737..ea45cff 100644
--- a/verified_resource_sharing.tex
+++ b/verified_resource_sharing.tex
@@ -102,9 +102,9 @@ However, doubts have been raised about the reliability of the current crop of HL
 
 Aiming to address this issue is \vericert{}~\cite{vericert}, a new HLS tool whose correctness has been checked to the highest possible standard: machine-checked proof. It provides a proof, checked using the Coq proof assistant~\cite{coq}, that every step of its translation from C to Verilog preserves the semantics of its input program. This means that we can always trust any Verilog design produced by \vericert{} to behave the same way as the C program given as input. %It is based on the CompCert~\cite{compcert_Leroy2009} verified C compiler.
 
-Clearly, however, it is not enough for an HLS tool simply to be \emph{correct}; the generated hardware must also enjoy high throughput, low latency, and good \emph{area efficiency} -- the last of which is the topic of this paper. A common optimisation employed by HLS tools to improve area efficiency is \emph{resource sharing}; that is, re-using hardware for more than one purpose. Accordingly, our work adds resource sharing to \vericert{}. We christen the new prototype HLS tool ` Keeping with the aims of the \vericert{} project, work is ongoing to extend the correctness proof.
+Clearly, however, it is not enough for an HLS tool simply to be \emph{correct}; the generated hardware must also enjoy high throughput, low latency, and good \emph{area efficiency} -- the last of which is the topic of this paper. A common optimisation employed by HLS tools to improve area efficiency is \emph{resource sharing}; that is, re-using hardware for more than one purpose. Accordingly, our work adds function-level resource sharing to \vericert{}, yielding a new prototype HLS tool called `\vericertfun'. In keeping with the aims of the \vericert{} project, work is ongoing to extend the correctness proof.
 
-The entire \vericertfun{} development is fully open-source~\cite{vericertfun-github}. Further details about the implementation and proofs are available in a technical report~\cite{pardalos_thesis}.
+The entire \vericertfun{} development is fully open-source~\cite{vericertfun-github}, and more details about the implementation and proofs are available in a technical report~\cite{pardalos_thesis}.
 
 \section{Background}