summaryrefslogtreecommitdiffstats
path: root/intro.tex
diff options
context:
space:
mode:
authorYann Herklotz <git@yannherklotz.com>2020-09-11 12:39:48 +0100
committerYann Herklotz <git@yannherklotz.com>2020-09-11 12:39:48 +0100
commitb23936ccae70f420f3708e247a6af47f4e524f50 (patch)
treecaf09ab33feeb526d89c77f0d86755d18bb008bd /intro.tex
parent501c0ff9576ee63962b5f83fc6df09cd3c41e410 (diff)
downloadfccm21_esrhls-b23936ccae70f420f3708e247a6af47f4e524f50.tar.gz
fccm21_esrhls-b23936ccae70f420f3708e247a6af47f4e524f50.zip
Add more bugs to the introduction
Diffstat (limited to 'intro.tex')
-rw-r--r--intro.tex24
1 files changed, 23 insertions, 1 deletions
diff --git a/intro.tex b/intro.tex
index d662977..33e963d 100644
--- a/intro.tex
+++ b/intro.tex
@@ -6,6 +6,28 @@ It is even being used in high-assurance settings, such as financial services~\ci
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}
+ \centering
+\begin{minted}{c}
+unsigned int b = 0x1194D7FF;
+int a[6] = {1, 1, 1, 1, 1, 1};
+
+int result() {
+ int c;
+ for (c = 0; c < 2; c++)
+ b = b >> a[c];
+ return b;
+}
+\end{minted}
+ \caption{Miscompilation bug found in Vivado 2018.3 and 2019.2 which returns \texttt{6535FF} instead of \texttt{46535FF} which is the correct result.}\label{fig:vivado_bug1}
+\end{figure}
+
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.
-We hope that our work serves to stimulate efforts to improve the quality of HLS tools. \ No newline at end of file
+We hope that our work serves to stimulate efforts to improve the quality of HLS tools.
+
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "main"
+%%% End: