Add more

2 files changed, 7 insertions, 7 deletions

diff --git a/main.tex b/main.tex
index 8094667..afc2bfc 100644
--- a/main.tex
+++ b/main.tex
@@ -121,9 +121,9 @@ In what follows, we will argue our position by presenting several possible \emph
 
 \objection{People should not be designing hardware in C to begin with}
 
-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 formalising circuit design in Coq itself to ease design verification~\cite{choi17_kami,singh_silver_oak}.
+Formally verifying HLS of C is the wrong approach.  C should not be used to design hardware, let alone hardware where reliability is crucial.  First of all, HLS tools are not unreliable in terms of correctness, but more so in terms the quality of the hardware which can be quite unpredictable~\cite{nigam20_predic_accel_desig_time_sensit_affin_types}.  For example, writing C for an HLS tool, small changes in the input could result in large differences in area and performance for the resulting hardware, leading to a kind of flakiness in the output.  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 formalising circuit design in Coq itself to ease design verification~\cite{choi17_kami,singh_silver_oak}.
 
-\textbf{\textit{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 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.
+\textbf{\textit{Response:}} Verifying HLS is also important.  First, 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 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.  Finally, even though unpredictability of the output of HLS tools might seem like the largest issue, working on a functionally correct HLS tool provides a good baseline to work on improving the predictability of the output as well.  Reasoning about correctness could maybe be extended with proofs about the variability of the generated output hardware, thereby also improving the quality of the output.  \compcert{}~\cite{leroy09_formal_verif_realis_compil}, an existing formally verified C compiler, has recently been extended with a proof of preservation of constant-time~\cite{barthe20_formal_c}, and a similar approach could be taken to improve to prove properties about the preservation of the hardware area or performance.
 
 \objection{HLS tools are already commonly used in industry, so they are clearly already reliable enough}
 
@@ -151,14 +151,10 @@ Another concern is that a verified HLS tool might not be performant enough to be
 
 \textbf{\textit{Response:}} We think that even a verified HLS tool can be comparable in performance to a state-of-the-art unverified HLS tool.  Taking \vericert{} as an example, which does not currently include many optimisations, we found that performing comparisons between the fully verified bits of \vericert{} and \legup{}~\cite{canis11_legup}, we found that the speed and area was comparable ($1\times$ - $1.5\times$) to that of \legup{} without LLVM optimisations and without operation chaining.  With those optimisations fully turned on, \vericert{} is around $4.5\times$ slower than \legup{}, with half the speed up being due to LLVM.\@
 
-There are many optimisations that need to be added to \vericert{} to turn it into a viable and competitive HLS tool.  First of all, a good scheduling implementation that supports operation chaining and pipelined operators is critical.  Our main focus is implementing scheduling based on systems of difference constraints~\cite{cong06_sdc}, which is the same algorithm \legup{} uses.  With this optimisation turned on, \vericert{} is only $~2\times$ to $~3\times$ slower than fully optimised \legup{}, with a slightly larger area.  The scheduling step is implemented using verified translation validation, meaning the scheduling algorithm can be tweaked and optimised without ever having to touch the correctness proof.
-
-\vspace{2mm}
+There are many optimisations that need to be added to \vericert{} to turn it into a viable and competitive HLS tool.  First of all, a good scheduling implementation that supports operation chaining and pipelined operators is critical.  Our main focus is implementing scheduling based on systems of difference constraints~\cite{cong06_sdc}, which is the same algorithm \legup{} uses.  With this optimisation turned on, \vericert{} is only $~2\times$ to $~3\times$ slower than fully optimised \legup{}, with a slightly larger area.  The scheduling step is implemented using verified translation validation, meaning the scheduling algorithm can be tweaked and optimised without ever having to touch the correctness proof.\\
 
 \objection{Even a formally verified HLS tool can't give absolute guarantees about the hardware it produces}~
 
-\vspace{-3mm}
-
 \textbf{\textit{Response:}} It is true that a verified tool is still allowed to fail at compile time, meaning none of the correctness proofs need to hold if no output is produced.  However, this is mostly a matter of putting more engineering work into the tool to make it more complete.  Bugs are easier to identify as they will induce tool failures at compile time.
 
 In addition to that, specifically for an HLS tool taking C as input, undefined behaviour in the input code will allow the HLS tool to behave any way it wishes.  This becomes even more important when passing the C to a verified HLS tool, because if it is not free of undefined behaviour, then none of the proofs will hold.  Extra steps therefore need to be performed to ensure that the input is free of any undefined behaviour, by using a tool like VST~\cite{appel11_verif_softw_toolc} for example.
diff --git a/reviews.md b/reviews.md
index 5546faf..9377ae2 100644
--- a/reviews.md
+++ b/reviews.md
@@ -83,3 +83,7 @@ It would be helpful to get some clue about why the problems [1] face seems to ha
 Their response are also standard "why proofs  of compiler are useful".
 
 This is neither a problem nor a weakness, but I believe it could have been more explicitly pointed out that many of those concern have little to do with hardware (or if they do, or their answer do, I would have missed that).
+
+[1] Rapid Cycle-Accurate Simulator for High-Level Synthesis,  Chi&al. (available at http://cadlab.cs.ucla.edu/~jaywang/papers/fpga19-sim.pdf)
+
+[2] Predictable Accelerator Design with Time-Sensitive Affine Types, Nigam& al. (available at https://rachitnigam.com/files/pubs/dahlia.pdf)