Add information about flakiness

1 files changed, 3 insertions, 1 deletions

diff --git a/main.tex b/main.tex
index fb757a4..4fee192 100644
--- a/main.tex
+++ b/main.tex
@@ -216,7 +216,9 @@ However, \citet{du21_fuzzin_high_level_synth_tools}, for example, show that on a
 
 \subsection{A Verified tool can still be flaky and fail}
 
-It is true that a verified tool is still allowed to fail at compilation time, meaning none of the correctness proofs need to hold, as no output was produced.  However, this is only a matter of putting more engineering work into the tool to make it reliable and get it to output
+It is true that a verified tool is still allowed to fail at compilation time, meaning none of the correctness proofs need to hold, as no output was produced.  However, this is only a matter of putting more engineering work into the tool to make it reliable.  If a test bench is available, it is also quite simple to check this property, as it just has to be randomly tested without even having to execute the output.
+
+In addition to that, specifically for an HLS tool taking C as input, undefined behaviour will allow the HLS tool to behave any way it wishes.  This becomes even more important when passing the C to a verified HLS tool, as if it is not free of undefined behaviour, then none of the proofs will hold.
 
 \section{Guarantees of trusted code}