diff options
Diffstat (limited to 'main.tex')
| -rw-r--r-- | main.tex | 2 |
1 files changed, 1 insertions, 1 deletions
@@ -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} |