From 59cd6bc28260b9a7d3b203444cf4dbd92b970e6a Mon Sep 17 00:00:00 2001 From: John Wickerson Date: Wed, 12 Jan 2022 10:00:21 +0000 Subject: minor --- verified_resource_sharing.tex | 7 +++++++ 1 file changed, 7 insertions(+) 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: -- cgit