diff options
Diffstat (limited to 'main.tex')
| -rw-r--r-- | main.tex | 2 |
1 files changed, 1 insertions, 1 deletions
@@ -209,7 +209,7 @@ There are many optimisations that need to be added to \vericert{} to turn it int \paragraph{Response:} It is true that a verified tool is still allowed to fail at compile time, meaning none of the correctness proofs need to hold if no output is produced. However, this is mostly a matter of putting more engineering work into the tool to make it more complete. Bugs are easier to identify as they will induce tool failures at compile time. -In addition to that, specifically for an HLS tool taking C as input, undefined behaviour in the input code 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, because if it is not free of undefined behaviour, then none of the proofs will hold. Extra steps therefore need to be performed to ensure that the input is free of any undefined behaviour. +In addition to that, specifically for an HLS tool taking C as input, undefined behaviour in the input code 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, because if it is not free of undefined behaviour, then none of the proofs will hold. Extra steps therefore need to be performed to ensure that the input is free of any undefined behaviour, by using a tool like VST~\cite{appel11_verif_softw_toolc} for example. Finally, the input and output language semantics also need to be trusted, as the proofs only hold as long as the semantics are a faithful representation of the languages. In \vericert{} this comes down to trusting the C semantics developed by \compcert{}~\cite{blazy09_mechan_seman_cligh_subset_c_languag} and the Verilog semantics, which we adapted from \citet{loow19_proof_trans_veril_devel_hol}. |