More work on sections

2 files changed, 25 insertions, 28 deletions

diff --git a/main.tex b/main.tex
index 57f2641..bb65570 100644
--- a/main.tex
+++ b/main.tex
@@ -204,49 +204,31 @@ However, verifying HLS also important.  Not only in HLS becoming more popular, a
 
 \paragraph{Existing approaches for testing or formally verifying hardware designs are sufficient for ensuring reliability.}
 
-The standard methods for checking the outputs of the HLS tools are the following.  First, the output could be checked by using a test bench and checking the outputs against the model.  However, this does not provide many guarantees, as many edge cases may never be tested.  Second, there has been research on checking that the generated hardware design has the same functionality as the input design, where the focus is on creating translation validators~\cite{pnueli98_trans} to prove the equivalence between the design and input code, while supporting various optimisations such as scheduling~\cite{kim04_autom_fsmd,karfa06_formal_verif_method_sched_high_synth,chouksey20_verif_sched_condit_behav_high_level_synth} or code motion~\cite{banerjee14_verif_code_motion_techn_using_value_propag,chouksey19_trans_valid_code_motion_trans_invol_loops}.  However, these aren't perfect solutions either, as there is no guarantee that these proofs really compose with each other.  This means that an equivalence checker normally needs to work for the all of the translations that the HLS tool might perform, increasing the chances that it cannot check for equivalence anymore.
+\citet{du21_fuzzin_high_level_synth_tools} showed that on average 2.5\% of randomly generated C, tailored to the specific HLS tool, end up with incorrect designs.  These bugs were reported and confirmed to be new bugs in the tools, demonstrating that existing internal tests did not catch these bugs.  In addition to that, existing verification techniques for checking the output of HLS tools may not be enough to catch these bugs reliably.  Checking the final design against the original model using a test bench may miss many edge cases that produce bugs.
 
-The radical solution to this problem is to formally verify the complete tool, writing the complete tool in Coq~\cite{coquand86}, an interactive theorem prover.  This has been proven to be successful, for example, \compcert{}~\cite{leroy09_formal_verif_realis_compil} is a formally verified C compiler written in Coq.  The reliability of formal verification in Coq was demonstrated by CSmith~\cite{yang11_findin_under_bugs_c_compil}, a random C, valid C generator, which found more than 300 bugs in GCC and Clang, whereas only 5 bugs were found in the unverified parts of \compcert{}, which prompted the verification of those parts as well.  In addition to that, recently Lutsig~\cite{loow21_lutsig}, a synthesis tool going from behavioural Verilog to a technology mapped netlist in Verilog, was also proven correct.
+There has been research on performing equivalence checks on the design and the behavioural input, focusing on creating translation validators~\cite{pnueli98_trans} to prove the equivalence between the design and input code, while supporting various optimisations such as scheduling~\cite{kim04_autom_fsmd,karfa06_formal_verif_method_sched_high_synth,chouksey20_verif_sched_condit_behav_high_level_synth} or code motion~\cite{banerjee14_verif_code_motion_techn_using_value_propag,chouksey19_trans_valid_code_motion_trans_invol_loops}.  However, these aren't perfect solutions either, as there is no guarantee that these proofs really compose with each other.  This means that an equivalence checkers are normally designed to check the translation from start to finish, which is computationally expensive, as well as possibly being unreliable due to a combination of optimisations producing an output that cannot be matched to the input, even though it is correct.
 
-Another argument against building a verified HLS tool is that current testing techniques for these tools are good enough.  There are many internal test benches that ensure the correctness of the HLS tool, as well as equivalence checkers to ensure that the final design behaves the same as the input.
-
-However, \citet{du21_fuzzin_high_level_synth_tools}, for example, show that on average 2.5\% of randomly generated C, tailored to the specific HLS tool, end up with incorrect designs.  This means that such test cases were not present in the internal test benches used to test the tools.  In addition to that, with the increasing complexity of HLS designs, it may sometimes not be possible to run an equivalence checker on the whole design, as the state space might be too big.
+The radical solution to this problem is to formally verify the complete tool.  This has been proven to be successful, in \compcert{}~\cite{leroy09_formal_verif_realis_compil}, for example, which is a formally verified C compiler written in Coq~\cite{coquand86}.  The reliability of formal verification in Coq was demonstrated by CSmith~\cite{yang11_findin_under_bugs_c_compil}, a random, valid C generator, which found more than 300 bugs in GCC and Clang, whereas only 5 bugs were found in the unverified parts of \compcert{}, which prompted the verification of those parts as well.
 
 \paragraph{HLS applications don't require the levels of reliability that a formally verified compiler affords.}
 
-One might argue that developing a formally verified tool in a theorem prover and proving correctness theorems about it might be too tedious and take too long.  However, we have already been developed our own verified HLS tool called \vericert{}~\cite{herklotz21_formal_verif_high_level_synth} based on \compcert{}, adding a Verilog back end to the compiler.  We currently have a completely verified translation from a large subset of C into Verilog, which fulfills the minimum requirements for an HLS tool.  We found that it normally takes $5\times$ or $10\times$ longer to prove a translation correct compared to writing the algorithm.
+One might argue that developing a formally verified tool in a theorem prover and proving correctness theorems about it might be too tedious and take too long, and that HLS tools specifically do not need that kind of reliability.  With our experience developing a verified HLS tool called \vericert{}~\cite{herklotz21_formal_verif_high_level_synth} based on \compcert{}, we found that it normally takes $5\times$ or $10\times$ longer to prove a translation correct compared to writing the algorithm.
 
-However, this could be seen as being beneficial, as proving the correctness of the HLS tool proves the absence of any bugs according to the language semantics, meaning much less time spent on fixing bugs.  In addition to that, even though simple testing would still be required to check the tool does indeed perform simple translations, and generates performant designs, these test benches would not have to cover every single edge case.  Finally, verification also forces the algorithm to deal with many different edge cases that may be hard to identify normally, and may even allow for more optimisations as one can be certain about assumptions one would usually have to make.
+However, this could be seen as being beneficial, as proving the correctness of the HLS tool proves the absence of any bugs according to the language semantics, meaning much less time has to be spent on fixing bugs.  In addition to that, verification also forces the algorithm to deal with many different edge cases that may be hard to identify normally, and may even allow for more optimisations as one can be certain about assumptions one would usually have to make.
 
 \paragraph{Any HLS tool that is simple enough for formal verification to be feasible won't produce sufficiently optimised designs to be useful.}
 
-Another concern might be that a verified HLS tool might not be performant enough to be usable in practice.  If that is the case, then the verification effort could be seen as useless, as it could not be used.
-
-First of all, performing comparisons between the fully verified bits of \vericert{} and \legup{}~\cite{canis11_legup}, we find that
-
-Finally, it is interesting to compare the performance of \vericert{} compared to existing HLS tools, to see how correctness guarantees affect the size and speed of the final hardware.  This was done on a common compiler benchmark called PolyBench/C~\cite{polybench}.
-
-There are many optimisations that need to be added to \vericert{} to turn it into a viable and competitive HLS tool.  First of all, the most important addition is a good scheduling implementation, which supports operation chaining and properly pipelining operators.  Our main focus is trying to implement scheduling based on system of difference constraint~\cite{cong06_sdc}, which is the same algorithm which \legup{} uses.  We have currently implemented the scheduling algorithm, as well as a simple verifier for the translation, but are missing the semantic preservation proofs that the verifier should produce.
+Another concern might be that a verified HLS tool might not be performant enough to be usable in practice.  If that is the case, then the verification effort could be seen as useless, as it could not be used.  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$) 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 of the speed-up being due to LLVM.\@
 
-The main idea used to prove the scheduling correct, is to split it up into multiple stages.  The first stage of the translation will turn basic blocks into a parallel basic block representation, whereas the second
+There are many optimisations that need to be added to \vericert{} to turn it into a viable and competitive HLS tool.  First of all, the most important addition is a good scheduling implementation, which supports operation chaining and properly pipelining operators.  Our main focus is trying to implement scheduling based on system of difference constraint~\cite{cong06_sdc}, which is the same algorithm which \legup{} uses.  We have currently implemented the scheduling algorithm, as well as a simple verifier for the translation, but are missing the semantic preservation proofs that the verifier should produce.  With this optimisation turned on, we are only around $2\times$ to $3\times$ slower than fully optimised \legup{}, with a slightly larger area.  As scheduling is implemented using translation validation, the scheduling algorithm can be tweaked and optimised without ever having to touch the correctness proof, with the downside of other translation validation approaches where the equivalence may sometimes not be provable, but errors will at least be caught at compilation time.
 
 \paragraph{Even a formally verified HLS tool can't give absolute guarantees about the hardware designs it produces.}
 
-It is true that a verified tool is still allowed to fail at compilation time, meaning none of the correctness proofs need to hold, as no output was produced.  However, this is only a matter of putting more engineering work into the tool to make it reliable.  If a test bench is available, it is also quite simple to check this property, as it just has to be randomly tested without even having to execute the output.
-
-In addition to that, specifically for an HLS tool taking C as input, undefined behaviour 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, as if it is not free of undefined behaviour, then none of the proofs will hold.
-
-There are a couple of theorems one can prove about the HLS tool once it is written in Coq.  The first, which is the most important one, is that transforming the C code into Verilog is semantics preserving, meaning the translated code will behave the same as the C code.  The following backward simulation, as initially presented in \compcert{}, shows the main property that we should want to show:
-
-\begin{equation*}
-  \forall C, V, B \in \texttt{Safe},\, \yhfunction{hls} (C) = \yhconstant{OK} (V) \land V \Downarrow B \implies C \Downarrow B.
-\end{equation*}
-
-\noindent Given a \textit{safe} behaviour $B$, meaning it does not contain undefined behaviour, we want to show that if the translation from C to Verilog succeeded, that executing the Verilog program with that behaviour implies that the C code will execute with the same behaviour.
+It is true that a verified tool is still allowed to fail at compilation 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 reliable.  If a test bench is available, it is also quite simple to check this property, as it just has to be randomly tested without even having to execute the output.
 
-However, there are also assumptions that have to be made about the tool.  In the case of \vericert{}, the only assumption that needs to be made is if the C semantics and Verilog semantics can be trusted.  This is much simpler than checking that the translation algorithm is implemented properly.  Using that assumption, the proofs ensure that the translation preserves the behaviour and doesn't need to be trusted.
+In addition to that, specifically for an HLS tool taking C as input, undefined behaviour 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, as 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.
 
-Trusting the Verilog semantics is not that easy, since it is not quite clear which semantics to take.  Verilog can either be simulated or synthesised into hardware, and has different semantics based on how it is used.  We therefore use existing Verilog semantics by \citet{loow19_proof_trans_veril_devel_hol}, which are designed to only model a small part of the semantics, while ensuring that the behaviour for synthesis and simulation stays the same.
+Finally, the input and output language semantics also need to be trusted, as the proofs only hold as long as the semantics hold are a true representation of the language.  In \vericert{} this comes down to trusting the C semantics developed by CompCert~\cite{blazy09_mechan_seman_cligh_subset_c_languag}. Trusting the Verilog semantics is not that easy, since it is not quite clear which semantics to take.  Verilog can either be simulated or synthesised into hardware, and has different semantics based on how it is used.  We therefore use existing Verilog semantics by \citet{loow19_proof_trans_veril_devel_hol}, which are designed to only model a small part of the semantics, while ensuring that the behaviour for synthesis and simulation stays the same.
 
 \section{Conclusion}
 
diff --git a/references.bib b/references.bib
index 9ece4da..86b7a4e 100644
--- a/references.bib
+++ b/references.bib
@@ -287,3 +287,18 @@ title = {{Silver Oak}},
 author = {Satnam Singh},
 url = {https://github.com/project-oak/silveroak},
 }
+
+@article{blazy09_mechan_seman_cligh_subset_c_languag,
+	author = "Blazy, Sandrine and Leroy, Xavier",
+	title = {Mechanized Semantics for the Clight Subset of the C Language},
+	journal = "Journal of Automated Reasoning",
+	volume = 43,
+	number = 3,
+	pages = "263--288",
+	year = 2009,
+	doi = "10.1007/s10817-009-9148-3",
+	url = {https://doi.org/10.1007/s10817-009-9148-3},
+	day = 01,
+	issn = "1573-0670",
+	month = "Oct"
+}