Update on Overleaf.

2 files changed, 210 insertions, 89 deletions

diff --git a/references.bib b/references.bib
index 770cc59..7810109 100644
--- a/references.bib
+++ b/references.bib
@@ -303,4 +303,22 @@
   timestamp = {Tue, 16 May 2017 14:24:38 +0200},
   biburl    = {https://dblp.org/rec/series/txtcs/BertotC04.bib},
   bibsource = {dblp computer science bibliography, https://dblp.org}
+}
+
+@article{six+20,
+  author    = {Cyril Six and
+               Sylvain Boulm{\'{e}} and
+               David Monniaux},
+  title     = {Certified and efficient instruction scheduling: application to interlocked
+               {VLIW} processors},
+  journal   = {Proc. {ACM} Program. Lang.},
+  volume    = {4},
+  number    = {{OOPSLA}},
+  pages     = {129:1--129:29},
+  year      = {2020},
+  url       = {https://doi.org/10.1145/3428197},
+  doi       = {10.1145/3428197},
+  timestamp = {Thu, 14 Oct 2021 08:48:52 +0200},
+  biburl    = {https://dblp.org/rec/journals/pacmpl/SixBM20.bib},
+  bibsource = {dblp computer science bibliography, https://dblp.org}
 }
\ No newline at end of file
diff --git a/verified_resource_sharing.tex b/verified_resource_sharing.tex
index f28fc2e..e1f8f0d 100644
--- a/verified_resource_sharing.tex
+++ b/verified_resource_sharing.tex
@@ -6,23 +6,27 @@
 
 \usepackage{listings}
 \lstset{
-basicstyle=\tt,
-escapeinside=@@,
+basicstyle=\tt\footnotesize,
+columns=fixed, basewidth=0.5em, %tip from https://tex.stackexchange.com/a/179072
+escapeinside=||,
 }
 \setlength{\fboxsep}{1.5pt} % to reduce \colorbox padding when highlighting
 
 %\usepackage{minted}
 %\setminted{
 %fontsize=\small,
-%escapeinside=@@,
+%escapeinside=||,
 %}
 %\usemintedstyle{manni}
 
+\definecolor{highlight0}{HTML}{ffffff}
 \definecolor{highlight1}{HTML}{b4d6d0} % 8dd3c7
 \definecolor{highlight2}{HTML}{fcfcdc} % ffffb3
 \definecolor{highlight3}{HTML}{c9c7d6} % bebada
 \definecolor{highlight4}{HTML}{fcc1bb} % fb8072
 
+\newcommand\HL[2]{\colorbox{highlight#1}{\vphantom{A}\smash{#2}}}
+
 % Leave review comments using
 % \jwcomment{...} (for John) or \yhcomment{...} (for Yann)
 % Using either directly leaves a margin note, using it as,
@@ -71,151 +75,250 @@ escapeinside=@@,
 
 The drive for faster, more energy-efficient computation has led to a surge in demand for custom hardware accelerators. These devices are traditionally designed using hardware description languages such as Verilog or VHDL, but the complexities of designing in such a language, as well as the abundance of engineers trained in software rather than hardware development, has meant that \emph{high-level synthesis} (HLS) tools have become an enticing option. 
 
-These tools, while incredibly useful, are also known to be unreliable. Previous work by \citet{Herklotz2021_empiricalstudy} has found numerous \emph{miscompilation} bugs in commercial HLS tools including Xilinx Vivado HLS~\cite{xilinx_vitis}, Intel i++~\cite{intel_hls}, and LegUp~\cite{legup_CanisAndrew2011}. This instability can be a significant hindrance in the development process, especially given the longer iteration times of hardware design compared to software. It also undermines the usefulness of HLS in safety- or security-critical settings. It is therefore essential to ensure that high-level synthesis tools are as reliable as possible.
+These tools are useful, but doubts have been raised about their reliability. For instance, \citet{Herklotz2021_empiricalstudy} found numerous miscompilation bugs in commercial HLS tools including Xilinx Vivado HLS~\cite{xilinx_vitis}, Intel i++~\cite{intel_hls}, and LegUp~\cite{legup_CanisAndrew2011}. This unreliability can be a significant hindrance in the development process, especially given the longer iteration times of hardware design compared to software. It also undermines the usefulness of HLS in safety- or security-critical settings. It is therefore essential to ensure that HLS tools are as reliable as possible.
 
-Vericert~\cite{Herklotz2020} is an HLS tool that aims to address this issue. Its correctness has been checked to the highest possible standard: machine-checked proof. It achieves that by providing a proof, checked using the Coq proof assistant, that every step of its translation from C to Verilog preserves the semantics of (i.e.\ behaves the same way as) its input program. This proof means that we can always trust any Verilog design produced by Vericert to behave the same way as the C program given to it as input. %It is based on the CompCert~\cite{compcert_Leroy2009} verified C compiler.
+Vericert~\cite{Herklotz2020} is an HLS tool that aims to address this issue. Its correctness has been checked to the highest possible standard: machine-checked proof. It achieves that by providing a proof, checked using the Coq proof assistant~\cite{coq}, that every step of its translation from C to Verilog preserves the semantics of (i.e.\ behaves the same way as) its input program. This proof means that we can always trust any Verilog design produced by Vericert to behave the same way as the C program given to it as input. %It is based on the CompCert~\cite{compcert_Leroy2009} verified C compiler.
 
-Clearly, however, it is not enough for an HLS tool simply to be \emph{correct}. The generated hardware must also meet several other desiderata, including high throughput, low latency, and \emph{area efficiency}. A common optimisation used by HLS tools to improve area efficiency is \emph{resource sharing}; that is, re-using hardware for more than one purpose. Accordingly, our work adds resource sharing to Vericert. Keeping with the aims of the Vericert project, we also extend the correctness proof.
+Clearly, however, it is not enough for an HLS tool simply to be \emph{correct}. The generated hardware must also meet several other desiderata, including high throughput, low latency, and good \emph{area efficiency}. A common optimisation used by HLS tools to improve area efficiency is \emph{resource sharing}; that is, re-using hardware for more than one purpose. Accordingly, our work adds resource sharing to Vericert. Keeping with the aims of the Vericert project, we also extend the correctness proof.
 
 \section{Background}
 
 \paragraph{The Coq proof assistant} Vericert is implemented using the Coq proof assistant~\cite{coq}. This means that it consists of a collection of functions that define the compilation process, together with the proof of a theorem stating that those definitions constitute a correct HLS tool. Coq mechanically checks this proof using a formal mathematical calculus, and then automatically translates the function definitions into OCaml code that can be compiled and executed. 
 
-Engineering a software system within a proof assistant like Coq is widely held to be the gold standard for correctness. Recent years have shown that it is feasible to design substantial pieces of software in this way, such as database management system~\cite{malecha+10}, web servers~\cite{chlipala15}, and operating system kernels~\cite{gu+16}. Coq has also been successfully deployed in the hardware design process, both in academia~\cite{braibant+13, bourgeat+20} and in industry~\cite{silveroak}. It has even been applied specifically to the HLS process: Faissole et al.~\cite{faissole+19} have used it to verify that HLS optimisations respect dependencies present in the source code.
+Engineering a software system within a proof assistant like Coq is widely held to be the gold standard for correctness. Recent years have shown that it is feasible to design substantial pieces of software in this way, such as database management systems~\cite{malecha+10}, web servers~\cite{chlipala15}, and operating system kernels~\cite{gu+16}. Coq has also been successfully deployed in the hardware design process, both in academia~\cite{braibant+13, bourgeat+20} and in industry~\cite{silveroak}. It has even been applied specifically to the HLS process: Faissole et al.~\cite{faissole+19} used it to verify that HLS optimisations respect dependencies present in the source code.
 
-\paragraph{The CompCert verified C compiler} Among the most celebrated applications of Coq is the CompCert project~\cite{compcert}. CompCert is a lightly optimising C compiler, with backend support for the Arm, x86, PowerPC, and Kalray VLIW architectures, that has been implemented and proven correct using Coq. CompCert handles most of the C99 language, and generally generates code of comparable performance to that generated by GCC at optimisation level \texttt{-O1}.
+\paragraph{The CompCert verified C compiler} Among the most celebrated applications of Coq is the CompCert project~\cite{compcert}. CompCert is a lightly optimising C compiler, with backend support for the Arm, x86, PowerPC, and Kalray VLIW architectures~\cite{six+20}, that has been implemented and proven correct using Coq. CompCert accepts most of the C99 language, and generally produces code of comparable performance to that produced by GCC at optimisation level \texttt{-O1}.
 
-CompCert transforms its input through a series of ten intermediate languages before generating the final output. This design ensures that each individual pass remains simple and well-scoped, and hence feasible to prove correct. The correctness proof of the entire compiler is formed by composing the correctness proofs of each of its internal passes.
+CompCert transforms its input through a series of ten intermediate languages before generating the final output. This design ensures that each individual pass remains relatively simple and hence feasible to prove correct. The correctness proof of the entire compiler is formed by composing the correctness proofs of each of its passes.
 
 \paragraph{The Vericert verified HLS tool}
 
-Introduced by \citet{Herklotz2020}, Vericert is a verified C-to-Verilog HLS tool. It is an extension of CompCert, essentially augmenting the existing verified C compiler with a new hardware-oriented intermediate language (called HTL) and a Verilog backend. In its current form, Vericert performs no significant optimisations, beyond those it inherits from CompCert's frontend. This results in performance generally about one order of magnitude slower than the designs generated by comparable, unverified HLS tools such as LegUp~\cite{legup_CanisAndrew2011}.
-
-Vericert branches off from CompCert at the intermediate language called register-transfer language (RTL). Since `RTL' is better known in the hardware community as `register-transfer level', and the two concepts are completely distinct, we shall henceforth refer to the CompCert intermediate language as `3AC' (for `three-address code').
+Introduced by \citet{Herklotz2020}, Vericert is a verified C-to-Verilog HLS tool. It is an extension of CompCert, essentially augmenting the existing verified C compiler with a new hardware-oriented intermediate language (called HTL) and a Verilog backend. In its current form, Vericert performs no significant optimisations, beyond those it inherits from CompCert's frontend. This results in performance generally about one order of magnitude slower than that achieved by comparable, unverified HLS tools such as LegUp~\cite{legup_CanisAndrew2011}.
 
-In the 3AC language, each function in the program is represented as a numbered list of instructions with gotos -- essentially, a control-flow graph (CFG). The essence of Vericert's compilation strategy is to treat this CFG as a finite-state machine (FSM), with each instruction in the CFG becoming an FSM state, and each edge in the CFG becoming an FSM transition. Moreover, program variables that do not have their address taken are mapped to hardware registers; other variables (including arrays and structs) are allocated in a block of RAM that represents the stack. More specifically, Vericert builds a finite-state machine with datapath (FSMD)~\cite{HwangVahid1999}. An FSMD comprises two maps, both of which take the current FSM state as their input: a \emph{control map} for determining the next FSM state, and a \emph{datapath} for updating the RAM and registers. FSMDs are captured in Vericert's new intermediate language, HTL. When Vericert compiles from HTL to the final Verilog output, these maps are converted from proper `mathematical' functions into syntactic Verilog case-statements, and each is placed inside an always-block.
+Vericert branches off from CompCert at the intermediate language called \emph{register-transfer language} (RTL). Since that abbreviation is usually used in the hardware community for `register-transfer level', we shall henceforth avoid possible confusion by referring to the CompCert intermediate language as `3AC' (for `three-address code').
 
-\JW{Worked example around here.}
+In the 3AC language, each function in the program is represented as a numbered list of instructions with gotos -- essentially, a control-flow graph (CFG). The essence of Vericert's compilation strategy is to treat this CFG as a finite-state machine (FSM), with each instruction in the CFG becoming an FSM state, and each edge in the CFG becoming an FSM transition. Moreover, program variables that do not have their address taken are mapped to hardware registers; other variables (including arrays and structs) are allocated in a block of RAM that represents the stack. More precisely, Vericert builds a finite-state machine with datapath (FSMD)~\cite{HwangVahid1999}. An FSMD comprises two maps, both of which take the current FSM state as their input: the \emph{control logic} map for determining the next FSM state, and a \emph{datapath} map for updating the RAM and registers. FSMDs are captured in Vericert's new intermediate language, HTL. When Vericert compiles from HTL to the final Verilog output, these maps are converted from proper `mathematical' functions into syntactic Verilog case-statements, and each is placed inside an always-block.
 
-\section{Rough notes}
+\section{Implementation of Vericert-Fun}
 
-Figure~\ref{fig:example_C} shows an example C file.
+Figure~\ref{fig:example_C} shows a simple C file that we shall employ as a worked example.
 
 \begin{figure}
 \begin{lstlisting}
 int add(int a, int b) {
-  @return a + b;@
+  |\HL0{return a + b;}|
 }
 
 int main() {
-  @\colorbox{highlight1}{int v = 0;}@
-  @\colorbox{highlight2}{v = add(v, 1);}@
-  @\colorbox{highlight3}{v = add(v, 2);}@
-  @\colorbox{highlight4}{return v;}@
+  |\HL1{int v = 0;}|
+  |\HL2{v = add(v, 1);}|
+  |\HL3{v = add(v, 2);}|
+  |\HL4{return v;}|
 }
 \end{lstlisting}
 \caption{Example C file}
 \label{fig:example_C}
 \end{figure}
 
-Figure~\ref{fig:example_3AC} shows the 3AC that the CompCert frontend compiles it to. \JW{In the HTL, the parameters to add are called a and b, but in the 3AC they're called x2 and x1. Presumably the HTL should use x2 and x1 too, right?}
+Figure~\ref{fig:example_3AC} shows the 3AC that the CompCert frontend obtains from the C program in Fig.~\ref{fig:example_C}. Highlighting is used to show the correspondence between C instructions and 3AC instructions. \JW{In the HTL, the parameters to add are called a and b, but in the 3AC they're called x2 and x1. Presumably the HTL should use x2 and x1 too, right?}
 
 \begin{figure}
 \begin{lstlisting}
 add (x2, x1) {
-  @2: x3 = x2 + x1 + 0 (int)@
-  @1: return x3@
+  |\HL0{2: x3 = x2 + x1 + 0 (int)}|
+  |\HL0{1: return x3}|
 }
 main () {
-  @\colorbox{highlight1}{9: x3 = 0}@
-  @\colorbox{highlight2}{8: x6 = 1}@
-  @\colorbox{highlight2}{7: x1 = "add"(x3, x6)}@
-  @\colorbox{highlight2}{6: x3 = x1}@
-  @\colorbox{highlight3}{5: x5 = 2}@
-  @\colorbox{highlight3}{4: x2 = "add"(x3, x5)}@
-  @\colorbox{highlight3}{3: x3 = x2}@
-  @\colorbox{highlight4}{2: x4 = x3}@
-  @\colorbox{highlight4}{1: return x4}@
+  |\HL1{9: x3 = 0}|
+  |\HL2{8: x6 = 1}|
+  |\HL2{7: x1 = "add"(x3, x6)}|
+  |\HL2{6: x3 = x1}|
+  |\HL3{5: x5 = 2}|
+  |\HL3{4: x2 = "add"(x3, x5)}|
+  |\HL3{3: x3 = x2}|
+  |\HL4{2: x4 = x3}|
+  |\HL4{1: return x4}|
 }
 \end{lstlisting}
 \caption{Example 3AC code}
 \label{fig:example_3AC}
 \end{figure}
 
+%add (clk, rst, start, a, b, ret, fin) {
+%  input clk, rst, start;
+%  input [31:0] a, b;
+%  output reg [31:0] ret;
+%  output reg fin;
+%  
+%  reg [31:0] reg_4;
+%  reg [31:0] reg_3;
 \begin{figure}
-\begin{lstlisting}[basicstyle=\tt\footnotesize]
-add (a, b) {
-  externctrl {
-    clk -> main.clk
-  }
+\begin{lstlisting}
+add (x2, x1) {
+  externctrl { clk -> main.clk }
   controllogic {
-    2: reg_4 <= 1;
-    1: reg_4 <= 3;
+    2: state <= 1;
+    1: state <= 3;
     3: ;
   }
   datapath {
-    2: reg_3 <= {{a + b} + 0};
-    1: finish = 1;
-       return = reg_3;
-    3: finish <= 0;
+    2: reg_3 <= {{x2 + x1} + 0};
+    1: fin = 1;
+       ret = reg_3;
+    3: fin <= 0;
   }
 }
-
+\end{lstlisting}
+\caption{Example HTL code (part 1)}
+\label{fig:example_HTL1}
+\end{figure}
+\begin{figure}
+%main (clk, rst, start, ret, fin) {
+%  input clk, rst, start;
+%  output reg [31:0] ret;
+%  output reg fin;
+%  
+%  reg[31:0] reg_1, reg_2, reg_3, reg_4, reg_5, reg_6, reg_7,
+%    add_0_rst, add_0_a, add_0_b, add_0_ret, add_0_fin,
+%    add_1_rst, add_1_a, add_1_b, add_1_ret, add_1_fin;
+\begin{lstlisting}
 main () {
   externctrl {
-    add_1_a -> add.param_0;
-    add_1_b -> add.param_1;
-    add_1_finish -> add.finish;
-    add_1_rst -> add.rst;
-    add_1_return -> add.return;
-    add_0_a -> add.param_0;
-    add_0_b -> add.param_1;
-    add_0_finish -> add.finish;
-    add_0_rst -> add.rst;
-    add_0_return -> add.return;
-    clk -> main.clk;
+    |\HL2{add\_0\_x2 -> add.param\_0;}|
+    |\HL2{add\_0\_x1 -> add.param\_1;}|
+    |\HL2{add\_0\_fin -> add.fin;}|
+    |\HL2{add\_0\_rst -> add.rst;}|
+    |\HL2{add\_0\_ret -> add.ret;}|
+    |\HL3{add\_1\_x2 -> add.param\_0;}|
+    |\HL3{add\_1\_x1 -> add.param\_1;}|
+    |\HL3{add\_1\_fin -> add.fin;}|
+    |\HL3{add\_1\_rst -> add.rst;}|
+    |\HL3{add\_1\_ret -> add.ret;}|
+    |\HL0{clk -> main.clk;}|
   }
   controllogic {
-    9: reg_7 <= 8;
-    8: reg_7 <= 7;
-    7: reg_7 <= 12;
-   12: if ({add_0_finish == 1}) reg_7 <= 6;
-    6: reg_7 <= 5;
-    5: reg_7 <= 4;
-    4: reg_7 <= 10;
-   10: if ({add_1_finish == 1}) reg_7 <= 3;
-    3: reg_7 <= 2;
-    2: reg_7 <= 1;
-    1: reg_7 <= 11;
-   11: ;
+    |\HL1{9: state <= 8;}|
+    |\HL2{8: state <= 7;}|
+    |\HL2{7: state <= 12;}|
+   |\HL2{12: if ({add\_0\_fin == 1}) state <= 6;}|
+    |\HL2{6: state <= 5;}|
+    |\HL3{5: state <= 4;}|
+    |\HL3{4: state <= 10;}|
+   |\HL3{10: if ({add\_1\_fin == 1}) state <= 3;}|
+    |\HL3{3: state <= 2;}|
+    |\HL4{2: state <= 1;}|
+    |\HL4{1: state <= 11;}|
+   |\HL0{11: ;}|
   }
   datapath {
-    9: reg_3 <= 0;
-    8: reg_6 <= 1;
-    7: add_0_rst <= 1;
-       add_0_a <= reg_3;
-       add_0_b <= reg_6;
-   12: add_0_rst <= 0;
-       reg_1 <= add_0_return;
-    6: reg_3 <= reg_1;
-    5: reg_5 <= 2;
-    4: add_1_rst <= 1;
-       add_1_a <= reg_3;
-       add_1_b <= reg_5;
-   10: add_1_rst <= 0;
-       reg_2 <= add_1_return;
-    3: reg_3 <= reg_2;
-    2: reg_4 <= reg_3;
-    1: finish = 1;
-       return = reg_4;
-   11: finish <= 0;
+    |\HL1{9: reg\_3 <= 0;}|
+    |\HL2{8: reg\_6 <= 1;}|
+    |\HL2{7: add\_0\_rst <= 1;}|
+       |\HL2{add\_0\_a <= reg\_3;}|
+       |\HL2{add\_0\_b <= reg\_6;}|
+   |\HL2{12: add\_0\_rst <= 0;}|
+       |\HL2{reg\_1 <= add\_0\_ret;}|
+    |\HL2{6: reg\_3 <= reg\_1;}|
+    |\HL3{5: reg\_5 <= 2;}|
+    |\HL3{4: add\_1\_rst <= 1;}|
+       |\HL3{add\_1\_a <= reg\_3;}|
+       |\HL3{add\_1\_b <= reg\_5;}|
+   |\HL3{10: add\_1\_rst <= 0;}|
+       |\HL3{reg\_2 <= add\_1\_ret;}|
+    |\HL3{3: reg\_3 <= reg\_2;}|
+    |\HL4{2: reg\_4 <= reg\_3;}|
+    |\HL4{1: fin = 1;}|
+       |\HL4{ret = reg\_4;}|
+   |\HL0{11: fin <= 0;}|
   }
 }
 \end{lstlisting}
-\caption{Example HTL code}
-\label{fig:example_HTL}
+\caption{Example HTL code (part 2)}
+\label{fig:example_HTL2}
 \end{figure}
 
+\begin{figure}
+% NB: reg_3 renamed to reg_7
+\begin{lstlisting}
+module main (clk, rst, ret, fin) {
+  reg add_rst, add_fin;
+  reg[31:0] add_ret, add_x2, add_x1, reg_7, add_state;
+  
+  always @(posedge clk) // control logic for "add"
+    if ({add_rst == 1}) begin 
+      add_state <= 2; 
+      add_fin <= 0; 
+    end else begin 
+      case (add_state)
+        2: add_state <= 1;
+        1: add_state <= 3;
+        3: ;
+        default: ;
+      endcase
+    end   
+    
+  always @(posedge clk) // datapath for "add"    
+    case (add_state)
+      2: reg_7 <= {{add_x2 + add_x1} + 0};
+      1: add_fin = 1;
+         add_ret = reg_7;
+      3: add_fin <= 0;
+    endcase
+    
+  input clk, rst, start;
+  output reg [31:0] ret;
+  output reg fin;
+  reg[31:0] state; 
+  reg[31:0] reg_1, reg_2, reg_3, reg_4, reg_5, reg_6;
+  
+  always @(posedge clk) // control logic for "main"
+    if ({rst == 1}) begin 
+      state <= 9; 
+      fin <= 0; 
+    end else begin
+      case (state)
+        |\HL1{9: state <= 8;}|
+        |\HL2{8: state <= 7;}|
+        |\HL2{7: state <= 12;}|
+       |\HL2{12: if ({add\_fin == 1}) state <= 6;}|
+        |\HL2{6: state <= 5;}|
+        |\HL3{5: state <= 4;}|
+        |\HL3{4: state <= 10;}|
+       |\HL3{10: if ({add\_fin == 1}) state <= 3;}|
+        |\HL3{3: state <= 2;}|
+        |\HL4{2: state <= 1;}|
+        |\HL4{1: state <= 11;}|
+       |\HL0{11: ;}|
+      endcase
+    end
+
+  always @(posedge clk) // datapath for "main"
+    case (state)
+      |\HL1{9: reg\_3 <= 0;}|
+      |\HL2{8: reg\_6 <= 1;}|
+      |\HL2{7: add\_rst <= 1;}|
+         |\HL2{add\_x2 <= reg\_3;}|
+         |\HL2{add\_x1 <= reg\_6;}|
+     |\HL2{12: add\_rst <= 0;}|
+         |\HL2{reg\_1 <= add\_ret;}|
+      |\HL2{6: reg\_3 <= reg\_1;}|
+      |\HL3{5: reg\_5 <= 2;}|
+      |\HL3{4: add\_rst <= 1;}|
+         |\HL3{add\_x2 <= reg\_3;}|
+         |\HL3{add\_x1 <= reg\_5;}|
+     |\HL3{10: add\_rst <= 0;}|
+         |\HL3{reg\_2 <= add\_ret;}|
+      |\HL3{3: reg\_3 <= reg\_2;}|
+      |\HL4{2: reg\_4 <= reg\_3;}|
+      |\HL4{1: fin = 1;}|
+         |\HL4{ret = reg\_4;}|
+     |\HL0{11: fin <= 0;}|
+    endcase
+endmodule
+\end{lstlisting}
+\caption{Example Verilog code}
+\label{fig:example_Verilog}
+\end{figure}
 
 \begin{figure}
 \begin{tikzpicture}[yscale=-1]