diff options
| -rw-r--r-- | main.tex | 8 |
1 files changed, 6 insertions, 2 deletions
@@ -155,9 +155,9 @@ There are many optimisations that need to be added to \vericert{} to turn it int \objection{Even a formally verified HLS tool can't give absolute guarantees about the hardware it produces}{} -\response{} It is true that a verified tool is still allowed to fail at compile time, which means that no output is produced despite the input being valid. 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. +\response{} It is true that a verified tool is still allowed to fail at compile time, which means that no output is produced despite the valid input. 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, by using a tool like VST~\cite{appel11_verif_softw_toolc} for example. +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, 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 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 that we adapted from \citet{loow19_proof_trans_veril_devel_hol}. @@ -165,6 +165,10 @@ Finally, the input and output language semantics need to be trusted, as the proo In conclusion, we have argued that HLS tools should be formally verified, and through our Vericert prototype, we have demonstrated that doing so is feasible. Even though the performance does not yet match state-of-the-art HLS tools, as more and more optimisations are implemented and formally verified, similar performance should be achievable. We believe that Vericert has the potential to raise the standard of reliability across the HLS field. It also has the potential to bring HLS to a new domain: designers of security- or safety-critical hardware, who are currently forced to design at very low levels of abstraction in order to minimise their trusted computing base. +\begin{acks} + We acknowledge financial support from the Research Institute on Verified Trustworthy Software Systems (VeTSS), which is funded by the UK National Cyber Security Centre (NCSC). +\end{acks} + %In addition to that, a formally verified HLS tool, written in a theorem prover, would provide a good base to mechanically verify other HLS-specific optimisations and help develop more reliable HLS tools in the future. %% Acknowledgments |