diff options
Diffstat (limited to 'verified_resource_sharing.tex')
-rw-r--r-- | verified_resource_sharing.tex | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/verified_resource_sharing.tex b/verified_resource_sharing.tex index c041988..5d41c6c 100644 --- a/verified_resource_sharing.tex +++ b/verified_resource_sharing.tex @@ -399,11 +399,18 @@ The y-axis shows the impact of resource sharing on the area usage of the hardwar \section{Proving Vericert-Fun correct} +The CompCert correctness theorem~\cite{compcert} expresses that every behaviour that can be exhibited by the compiled program is also a behaviour of the source program. Vericert~\cite{Herklotz2020} adapted this theorem for HLS by replacing `compiled program' with `generated Verilog design'. In both cases ... + +The behaviours of a Verilog design are determined by appealing to a formal semantics of the Verilog language, which \citeauthor{Herklotz2020} mechanised in Coq. + +In order to extend the Vericert correctness theorem to Vericert-Fun, we need to extend the Verilog semantics to handle ... + \JW{Todo: \begin{itemize} \item What is needed for the correctness proof? (Semantics for C, semantics for Verilog, ...) \end{itemize}} + \section{Rough notes} A few points that we might want to address at some point: |