Update on Overleaf.

1 files changed, 4 insertions, 15 deletions

diff --git a/intro.tex b/intro.tex
index 26555c2..2928014 100644
--- a/intro.tex
+++ b/intro.tex
@@ -4,9 +4,7 @@ High-level synthesis (HLS), which refers to the automatic translation of softwar
 It promises to increase the productivity of hardware engineers by raising the abstraction level of their designs, and it promises software engineers the ability to produce application-specific hardware accelerators without having to understand Verilog.
 It is even being used in high-assurance settings, such as financial services~\cite{hls_fintech}, control systems~\cite{hls_controller}, and real-time object detection~\cite{hls_objdetect}. As such, HLS tools are increasingly relied upon. In this paper, we investigate whether they are trustworthy.
 
-Our method is brought over from the compiler testing literature. We use a tool called Csmith~\cite{yang11_findin_under_bugs_c_compil} to generate well-formed C programs from the subset of the C language that is supported by all the HLS tools we test, and then augment each program with randomly chosen HLS-specific directives. We synthesise each C program to RTL, and use a Verilog simulator to calculate its return value. If synthesis crashes, or if this return value differs from the return value obtained by executing a binary compiled from the C program by gcc, then we have found a candidate bug. We then use trial-and-error to reduce the C program to a minimal version that still triggers a bug.
-
-\begin{figure}
+\begin{figure}[t]
   \centering
 \begin{minted}{c}
 unsigned int b = 0x1194D7FF;
@@ -23,39 +21,30 @@ int main() {
 \end{figure}
 
 
-\begin{framed}
-\vspace{-3pt}
 \paragraph{An example of a fuzzed buggy program}
 Figure~\ref{fig:vivado_bug1} shows a minimal example that produces the wrong result during RTL simulation in all three versions of VivadoHLS, compared to GCC execution. 
 In this example, we right shift a large integer value \code{b} by values of array elements, in array \code{a}, within iterations of a \code{for}-loop.
 VivadoHLS returns \code{0x006535FF} instead of \code{0x046535FF} as in GCC. 
-The circumstances in which we found this right shift bug shows the challenge of testing current HLS tools.
+The circumstances in which we found this bug shows the challenge of testing HLS tools.
 
 For instance, the for-loop was also necessary to ensure that a bug was detected.
 Also, the shift value needs to be accessed from an array.
 Replacing the array accesses within the loop with constants result in the bug not surfacing.
 Additionally, the array \code{a} needed to be at least six elements in size although the for-loop only has two iterations. 
-Any array smaller than that did not surface this bug.
+% Any array smaller than that did not surface this bug.
 Finally, the value of \code{b} is an oracle that could not be changed without masking the bug. 
 Producing such circumstances within C code for HLS testing is both arduous and counter-intuitive to human testers. 
 In contrast, producing non-intuitive, complex but valid C programs is the cornerstone of fuzzing tools. 
 Thus, it was natural to adopt program fuzzing for our HLS testing campaign. 
 % \NR{Yann, please double check my claims about the bug. I hope I accurately described what we discussed. }\YH{Yes I agree with all that, I think that is a good description of it}
-\end{framed}
 
 \paragraph{Our contribution}
+Our method is brought over from the compiler testing literature. We use a tool called Csmith~\cite{yang11_findin_under_bugs_c_compil} to generate well-formed C programs from the subset of the C language that is supported by all the HLS tools we test, and then augment each program with randomly chosen HLS-specific directives. We synthesise each C program to RTL, and use a Verilog simulator to calculate its return value. If synthesis crashes, or if this return value differs from the return value obtained by executing a binary compiled from the C program by gcc, then we have found a candidate bug. We then use trial-and-error to reduce the C program to a minimal version that still triggers a bug.
 
 We have tested three widely used HLS tools: LegUp~\cite{canis13_legup}, Xilinx Vivado HLS~\cite{xilinx20_vivad_high_synth}, and the Intel HLS Compiler~\cite{?}. For all three tools, we were able to find valid C programs that cause crashes while compiling and valid C programs that cause wrong RTL to be generated. We have submitted a total of \ref{?} bug reports to the developers, \ref{?} of which have been confirmed and \ref{?} of which have now been fixed at the time of writing. 
 
-
-\begin{itemize}
-    \item Fuzzing flow 
-    \item Tested against three tools 
-\end{itemize}
-
 We hope that our work serves to stimulate efforts to improve the quality of HLS tools.
 
-
 %%% Local Variables:
 %%% mode: latex
 %%% TeX-master: "main"