From 9e7a5c8ea24d7abba7f08da9066ea96da7248c37 Mon Sep 17 00:00:00 2001 From: Yann Herklotz 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