diff options
| -rw-r--r-- | conference.bib | 10 | ||||
| -rw-r--r-- | intro.tex | 14 |
2 files changed, 7 insertions, 17 deletions
diff --git a/conference.bib b/conference.bib index 92bd22c..178b5ec 100644 --- a/conference.bib +++ b/conference.bib @@ -163,12 +163,4 @@ with {LegUp} High-Level Synthesis}, url = {https://doi.org/10.1109/ICVD.2003.1183177}, ISSN = {1063-9667}, month = {Jan}, -} - -@misc{mentor20_catap_high_level_synth, - author = {Mentor}, - title = {Catapult High-Level Synthesis}, - url = {https://www.mentor.com/hls-lp/catapult-high-level-synthesis/c-systemc-hls}, - urldate = {2020-06-06}, - year = 2020, -} +}
\ No newline at end of file @@ -6,11 +6,6 @@ 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. - - -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{framed}{An example of a fuzzed buggy program} \begin{figure} \centering \begin{minted}{c} @@ -27,7 +22,10 @@ int main() { \caption{Miscompilation bug found in Vivado 2018.3 and 2019.2 which returns \code{0x006535FF} instead of \code{0x046535FF} which is the correct result.}\label{fig:vivado_bug1} \end{figure} -\paragraph{} + +\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. @@ -42,10 +40,10 @@ Finally, the value of \code{b} is an oracle that could not be changed without ma 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} - +% \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} +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. \paragraph{Our contribution} \begin{itemize} |