diff options
| -rw-r--r-- | verified_resource_sharing.tex | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/verified_resource_sharing.tex b/verified_resource_sharing.tex index 9933ae8..8239a55 100644 --- a/verified_resource_sharing.tex +++ b/verified_resource_sharing.tex @@ -124,7 +124,7 @@ It transforms its input through a series of ten intermediate languages before ge %This design ensures that each individual pass remains relatively simple and hence feasible to prove correct. The correctness proof of the entire compiler is formed by composing the correctness proofs of each of those passes. \YHchanged{That the Csmith compiler testing tool}~\cite{csmith} has found hundreds of bugs in GCC and LLVM but none in (the verified parts of) CompCert is a testament to the reliability of this development approach. -\YHchanged{However, we} cannot guarantee \vericertfun{} designs will never go wrong, because of fallible components not covered by the theorem, such as the synthesis toolchain~\cite{verismith} and the FPGA itself. +\YHchanged{In \vericertfun{} designs, however, we cannot guarantee that they will never go wrong, because of fallible components not covered by the theorem, such as the synthesis toolchain~\cite{verismith} and the FPGA itself.} \paragraph{The \vericert{} verified HLS tool} |