Update on Overleaf.

1 files changed, 4 insertions, 4 deletions

diff --git a/related.tex b/related.tex
index 2296f33..466040b 100644
--- a/related.tex
+++ b/related.tex
@@ -1,10 +1,10 @@
-\section{Background}
+\section{Related Work}
 
-Lidbury et al. \cite{lidbury15_many_core_compil_fuzzin} fuzz-tested several OpenCL compilers, including an HLS compiler from Altera (now Intel). They were only able to subject that compiler to superficial testing because so many of the test cases they generated led to it crashing. In comparison to our work: where Lidbury et al. generated target-independent OpenCL programs that could be used to test HLS tools and conventional compilers alike, we specifically generate programs that are tailored for HLS (e.g. with HLS-specific pragmas) with the aim of testing the HLS tools more deeply. Another difference is that where we test using sequential C programs, they test using highly concurrent OpenCL programs, and thus have to go to great lengths to ensure that any discrepancies observed between compilers cannot be attributed to the nondeterminism of concurrency.
+The only other work of which we are aware on fuzzing HLS tools is that by Lidbury et al. \cite{lidbury15_many_core_compil_fuzzin}, who tested several OpenCL compilers, including an HLS compiler from Altera (now Intel). They were only able to subject that compiler to superficial testing because so many of the test cases they generated led to it crashing. In comparison to our work: where Lidbury et al. generated target-independent OpenCL programs that could be used to test HLS tools and conventional compilers alike, we specifically generate programs that are tailored for HLS (e.g. with HLS-specific pragmas) with the aim of testing the HLS tools more deeply. Another difference is that where we test using sequential C programs, they test using highly concurrent OpenCL programs, and thus have to go to great lengths to ensure that any discrepancies observed between compilers cannot be attributed to the inherent nondeterminism of concurrency.
 
-Herklotz et al.~\cite{verismith} fuzz-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.
+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 fare better under testing campaigns like ours.  One such example might be a Handel-C compiler which has been partially formally proven in a theorem prover called HOL~\cite{perna12_mechan_wire_wise_verif_handel_c_synth}.  However, Handel-C requires the manual parallelisation of hardware and would require many more checks to avoid data races.  In addition to that, a HLS tool called SPARK~\cite{gupta03_spark} also contains passes that are validated during compilation time~\cite{chouksey20_verif_sched_condit_behav_high_level_synth}, such as the scheduling algorithm.  Unfortunately the tools are not readily available yet to properly test, or do not support C as input directly.  Finally Catapult C~\cite{mentor20_catap_high_level_synth} is also a high-level synthesis tool that proves that the netlist is equivalent to the input, and should therefore not produce any bugs and only fail if the output cannot be proven.
+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 a Handel-C compiler which has been mechanically proven correct, at least in part, using the HOL theorem prover~\cite{perna12_mechan_wire_wise_verif_handel_c_synth}. However, Handel-C 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. Another example is an HLS tool called SPARK~\cite{gupta03_spark}, which contains passes that are mechanically validated during compilation~\cite{chouksey20_verif_sched_condit_behav_high_level_synth}, such as the scheduling algorithm.  Unfortunately the tools are not readily available yet to test properly, or do not support C as input directly. Finally, the HLS tool Catapult C~\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. \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?}
 
 %%% Local Variables:
 %%% mode: latex