diff options
| author | John Wickerson <j.wickerson@imperial.ac.uk> | 2022-01-12 10:00:21 +0000 |
|---|---|---|
| committer | John Wickerson <j.wickerson@imperial.ac.uk> | 2022-01-12 10:00:21 +0000 |
| commit | 59cd6bc28260b9a7d3b203444cf4dbd92b970e6a (patch) | |
| tree | 13dfc5cf2adbf8286d4eaf34e650c7d53f34a6e7 | |
| parent | a16a2e25e3a7ab29d8476d0f3165c9871b2f8622 (diff) | |
| download | fccm22_rsvhls-59cd6bc28260b9a7d3b203444cf4dbd92b970e6a.tar.gz fccm22_rsvhls-59cd6bc28260b9a7d3b203444cf4dbd92b970e6a.zip | |
minor
| -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: |