Update on Overleaf.

1 files changed, 12 insertions, 2 deletions

diff --git a/related.tex b/related.tex
index cbff444..a9d2f58 100644
--- a/related.tex
+++ b/related.tex
@@ -4,10 +4,20 @@ The only other work of which we are aware on fuzzing HLS tools is that by Lidbur
 
 Other stages of the FPGA toolchain have been subjected to fuzzing. Herklotz et al.~\cite{verismith} tested several FPGA synthesis tools using randomly generated Verilog programs. Where they concentrated on the RTL-to-netlist stage of hardware design, we focus our attention on the earlier C-to-RTL stage.
 
-Several authors have taken steps toward more rigorously engineered HLS tools that may be more resilient to testing campaigns such as ours. One such example might be the Handel-C compiler by Perna and Woodcock~\cite{perna12_mechan_wire_wise_verif_handel_c_synth} which has been mechanically proven correct, at least in part, using the HOL theorem prover. 
+Several authors have taken steps toward more rigorously engineered HLS tools that may be more resilient to testing campaigns such as ours. 
+\begin{itemize}
+    
+\item The Handel-C compiler by Perna and Woodcock~\cite{perna12_mechan_wire_wise_verif_handel_c_synth} has been mechanically proven correct, at least in part, using the HOL theorem prover. 
 %However, the Handel-C language relies upon the user to perform the parallelisation that is necessary for good hardware performance, and would require many more checks to avoid data races. 
 However, the tool does not support C as input directly, so is not amenable to fuzzing.
-Another example is the SPARK HLS tool~\cite{gupta03_spark}, in which some compiler passes, such as scheduling, are mechanically validated during compilation~\cite{chouksey20_verif_sched_condit_behav_high_level_synth}. Unfortunately, this tool is not yet readily available to test properly. Finally, the Catapult C HLS tool~\cite{mentor20_catap_high_level_synth} is designed only to produce an output netlist if it can mechanically prove it equivalent to the input program. It should therefore never produce wrong RTL. In future work, we intend to test Catapult C alongside Vivado HLS, LegUp, and Intel HLS 
+
+\item Ramanathan et al.~\cite{ramanathan+17} proved their implementation of C atomic operations in LegUp correct up to a bound using model checking. However, our testing campaign is not applicable to their implementation because we do not generate concurrent C programs.
+
+\item In the SPARK HLS tool~\cite{gupta03_spark}, some compiler passes, such as scheduling, are mechanically validated during compilation~\cite{chouksey20_verif_sched_condit_behav_high_level_synth}. Unfortunately, this tool is not yet readily available to test properly.
+
+\item Finally, the Catapult C HLS tool~\cite{mentor20_catap_high_level_synth} is designed only to produce an output netlist if it can mechanically prove it equivalent to the input program. It should therefore never produce wrong RTL. In future work, we intend to test Catapult C alongside Vivado HLS, LegUp, and the Intel HLS Compiler.
+
+\end{itemize}  
 %more prevalent these were prioritised.
 % JW: We're not really sure that LegUp is more prevalent than Catapult HLS. Indeed, it probably isn't!
 %\JW{Obvious reader question at this point: why not test that claim by giving our Csmith test cases to Catapult C too? Can we address that here? No worries if not; but shall we try and do that after the deadline anyway?}\YH{Yes, definitely, it would be great to get an idea of how Catapult C performs, and I currently have it installed already.  I have added a small sentence for that now, but let me know if I should mention this in the conclusion instead though. }