From 9e7a5c8ea24d7abba7f08da9066ea96da7248c37 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Thu, 25 Feb 2021 18:45:30 +0000
Subject: Some more fixes

---
 main.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'main.tex')

diff --git a/main.tex b/main.tex
index 611b951..c1b688b 100644
--- a/main.tex
+++ b/main.tex
@@ -175,7 +175,7 @@ In what follows, we will argue our position by presenting several possible \emph
 
 Formally verifying HLS of C is the wrong approach. C should not be used to design hardware, let alone hardware where reliability is crucial. Instead, there have been many efforts to formally verify the translation of high-level hardware description languages like Bluespec with K\^{o}i\-ka~\cite{bourgeat20_essen_blues}, formalising the synthesis of Verilog into technology-mapped net-lists with Lutsig~\cite{loow21_lutsig}, or work on formalising circuit design in Coq itself to ease design verification~\cite{choi17_kami,singh_silver_oak}.
 
-\paragraph{Response:} However, verifying HLS is also important.  Not only is HLS becoming more popular, as it requires much less design effort to produce new hardware~\cite{lahti19_are_we_there_yet}, but much of that convenience comes from the easy behavioural testing that HLS allows to ensure correct functionality of the design.  This assumes that HLS tools are correct.
+\paragraph{Response:} Verifying HLS is also important.  Firstly, C is often the starting point for hardware designs, as initial models are written in those languages to get a quick prototype~\cite{gajski10_what_hls}, so it is only natural to continue using C when designing the hardware.  Not only is HLS from C becoming more popular, but much of that convenience also comes from the easy behavioural testing that HLS allows to ensure correct functionality of the design~\cite{lahti19_are_we_there_yet}.  This assumes that HLS tools are correct.
 
 \objection{Current HLS tools are already reliable enough}
 
-- 
cgit 

