path: root/chapters/hls.tex

\environment fonts_env
\environment lsr_env

\startcomponent hls

\def\slowdownOrig{27}
\def\slowdownDiv{2}
\def\areaIncr{1.1}

\chapter[sec:hls]{High-Level Synthesis}

\startsynopsis
  This chapter outlines the base implementation of a formally verified high-level synthesis tool
  called Vericert.  This chapter is based on a paper describing the initial implementation in
  detail~\citef{herklotz21_formal_verif_high_level_synth}.
\stopsynopsis

We have designed a new HLS tool in the Coq theorem prover and proved that any output design it
produces always has the same behaviour as its input program. Our tool, called Vericert, is
automatically extracted to an OCaml program from Coq, which ensures that the object of the proof is
the same as the implementation of the tool. Vericert is built by extending the
\index{CompCert}CompCert verified C compiler~\cite[leroy09_formal_verif_realis_compil] with a new
hardware-specific intermediate language and a Verilog back end. It supports most C constructs,
including integer operations, function calls (which are all inlined), local arrays, structs, unions,
and general control-flow statements, but currently excludes support for case statements, function
pointers, recursive function calls, non-32-bit integers, floats, and global variables.

\paragraph{Contributions and Outline.} The contributions of this paper are as follows:

\startitemize[]
\item We present Vericert, the first mechanically verified HLS tool that compiles C to Verilog. In
  \in{Section}[sec:hls:design], we describe the design of Vericert, including certain optimisations
  related to memory accesses and division.
\item We state the correctness theorem of Vericert with respect to an existing semantics for Verilog
  due to \cite[authoryear][loow19_proof_trans_veril_devel_hol]. In \in{Section}[sec:hls:verilog], we
  describe how we extended this semantics to make it suitable as an HLS target.  We also describe
  how the Verilog semantics is integrated into CompCert's language execution model and its framework
  for performing simulation proofs. A mapping of CompCert's infinite memory model onto a finite
  Verilog array is also described.
\item In \in{Section}[sec:hls:proof], we describe how we proved the correctness theorem. The proof
  follows standard CompCert techniques -- forward simulations, intermediate specifications, and
  determinism results -- but we encountered several challenges peculiar to our hardware-oriented
  setting.  These include handling discrepancies between the byte-addressed memory assumed by the
  input software and the word-addressed memory that we implement in the output hardware, different
  handling of unsigned comparisons between C and Verilog, and carefully implementing memory reads
  and writes so that these behave properly as a RAM in hardware.
%\item In \in{Section}[sec:hls:evaluation], we evaluate Vericert on the PolyBench/C benchmark
%  suite~\cite[pouchet13_polyh], and compare the performance of our generated hardware against an
%  existing, unverified HLS tool called LegUp~\cite[canis11_legup]. We show that Vericert generates
%  hardware that is \slowdownOrig$\times$ slower (\slowdownDiv$\times$ slower in the absence of
%  division) and \areaIncr$\times$ larger than that generated by LegUp. This performance gap can be
%  largely attributed to Vericert's current lack of support for instruction-level parallelism and the
%  absence of an efficient, pipelined division operator. We intend to close this gap in the future by
%  introducing (and verifying) HLS optimisations of our own, such as scheduling and memory analysis.
%  This section also reports on our campaign to fuzz-test Vericert using over a hundred thousand
%  random C programs generated by Csmith~\cite{yang11_findin_under_bugs_c_compil} in order to confirm
%  that its correctness theorem is watertight.
\stopitemize

\section[sec:hls:design]{Designing a Verified HLS Tool}

This section describes the main architecture of the HLS tool, and the way in which the Verilog back
end was added to CompCert.  This section also covers an example of converting a simple C program
into hardware, expressed in the Verilog language.

\subsection{Main Design Decisions}

\paragraph{Choice of source language.} C was chosen as the source language as it remains the most
common source language amongst production-quality HLS tools~\cite[canis11_legup,
  xilinx20_vivad_high_synth, intel20_high_synth_compil, pilato13_bambu]. This, in turn, may be
because it is \quotation{[t]he starting point for the vast majority of algorithms to be implemented
  in hardware}~\cite{gajski10_what_hls}, lending a degree of practicality.  The availability of
CompCert~\cite{leroy09_formal_verif_realis_compil} also provides a solid basis for formally verified
C compilation.  We considered Bluespec~\cite{nikhil04_blues_system_veril}, but decided that although
it \quotation{can be classed as a high-level language}~\cite{greaves19_resear_note}, it is too
hardware-oriented to be suitable for traditional HLS.  We also considered using a language with
built-in parallel constructs that map well to parallel hardware, such as
occam~\cite{page91_compil_occam}, Spatial~\cite{spatial} or Scala~\cite{bachrach12_chisel}.

\paragraph{Choice of target language.} Verilog~\cite{06_ieee_stand_veril_hardw_descr_languag} is an
HDL that can be synthesised into logic cells which can either be placed onto a field-programmable
gate array (FPGA) or turned into an application-specific integrated circuit (ASIC).  Verilog was
chosen as the output language for Vericert because it is one of the most popular HDLs and there
already exist a few formal semantics for it that could be used as a
target~\cite{loow19_verif_compil_verif_proces, meredith10_veril}.  Bluespec, previously ruled out as
a source language, is another possible target and there exists a formally verified translation to
circuits using Kôika~\cite{bourgeat20_essen_blues}.

\paragraph{Choice of implementation language.} We chose Coq as the implementation language because
of its mature support for code extraction; that is, its ability to generate OCaml programs directly
from the definitions used in the theorems.  We note that other authors have had some success
reasoning about the HLS process using other theorem provers such as Isabelle~\cite{ellis08_correc}.
CompCert~\cite{leroy09_formal_verif_realis_compil} was chosen as the front end because it has a well
established framework for simulation proofs about intermediate languages, and it already provides a
validated C parser~\cite{jourdan12_valid_lr_parser}.  The Vellvm
framework~\cite{zhao12_formal_llvm_inter_repres_verif_progr_trans} was also considered because
several existing HLS tools are already LLVM-based, but additional work would be required to support
a high-level language like C as input.  The .NET framework has been used as a basis for other HLS
tools, such as Kiwi~\cite{greaves08_kiwi}, and LLHD~\cite{schuiki20_llhd} has been recently proposed
as an intermediate language for hardware design, but neither are suitable for us because they lack
formal semantics.

\startplacefigure[reference={fig:rtlbranch},title={Vericert as a Verilog back end to CompCert.}]
  \hbox{\starttikzpicture [language/.style={fill=white,rounded corners=3pt,minimum height=7mm},
    continuation/.style={},
    linecount/.style={rounded corners=3pt,dashed}]
    \fill[compcert,rounded corners=3pt] (-1.2,-0.5) rectangle (10.2,2);
    \fill[formalhls,rounded corners=3pt] (-1.2,-1) rectangle (10.2,-2.4);
    %\draw[linecount] (-0.95,-0.45) rectangle (3.6,1);
    %\draw[linecount] (4,-0.45) rectangle (7.5,1);
    \node[language] at (-0.3,0) (clight) {Clight};
    \node[continuation] at (1,0) (conta) {$\cdots$};
    \node[language] at (2.7,0) (cminor) {CminorSel};
    \node[language] at (4.7,0) (rtl) {3AC};
    \node[language] at (6.2,0) (ltl) {LTL};
    \node[language,anchor=west] at (8.4,0) (aarch) {aarch64};
    \node[language,anchor=west] at (8.4,0.8) (x86) {x86};
    \node[continuation,anchor=west] at (8.4,1.4) (backs) {$\cdots$};
    \node[continuation] at (7.3,0) (contb) {$\cdots$};
    \node[language] at (4.7,-1.5) (htl) {HTL};
    \node[language] at (6.7,-1.5) (verilog) {Verilog};
    \node[anchor=west] at (-0.9,1.6) {\bold{CompCert}};
    \node[anchor=west] at (-0.9,-1.4) {\bold{Vericert}};
    %%\node[anchor=west] at (-0.9,0.7) {\small $\sim$ 27 kloc};
    %%\node[anchor=west] at (4.1,0.7) {\small $\sim$ 46 kloc};
    %%\node[anchor=west] at (2,-1.5) {\small $\sim$ 17 kloc};
    \node[align=center] at (3.2,-2) {RAM\\[-0.5ex]insertion};
    \draw[->,thick] (clight) -- (conta);
    \draw[->,thick] (conta) -- (cminor);
    \draw[->,thick] (cminor) -- (rtl);
    \draw[->,thick] (rtl) -- (ltl);
    \draw[->,thick] (ltl) -- (contb);
    \draw[->,thick] (contb) -- (aarch);
    \draw[->,thick] (contb) to [out=0,in=200] (x86.west);
    \draw[->,thick] (contb) to [out=0,in=190] (backs.west);
    \draw[->,thick] (rtl) -- (htl);
    \draw[->,thick] (htl) -- (verilog);
    \draw[->,thick] (htl.west) to [out=180,in=150] (4,-2.2) to [out=330,in=270] (htl.south);
  \stoptikzpicture}
\stopplacefigure

\paragraph{Architecture of Vericert.} The main work flow of Vericert is given in
\in{Figure}[fig:rtlbranch], which shows those parts of the translation that are performed in
CompCert, and those that have been added.  This includes translations to two new intermediate
languages added in Vericert, \lindex{HTL}HTL and \lindex{Verilog}Verilog, as well as an additional
optimisation pass labelled as \quotation{RAM insertion}.

\def\numcompcertlanguages{ten}

CompCert translates Clight\footnote{A deterministic subset of C with pure expressions.} input into
assembly output via a sequence of intermediate languages; we must decide which of these
\numcompcertlanguages{} languages is the most suitable starting point for the HLS-specific
translation stages.

We select CompCert's \lindex{RTL}three-address code (3AC)\footnote{This is known as register transfer
  language (RTL) in the CompCert literature. `3AC' is used in this paper instead to avoid confusion
  with register-transfer level (RTL), which is another name for the final hardware target of the HLS
  tool.} as the starting point. Branching off \emph{before} this point (at CminorSel or earlier)
denies CompCert the opportunity to perform optimisations such as constant propagation and dead-code
elimination, which, despite being designed for software compilers, have been found useful in HLS
tools as well~\cite{cong11_high_level_synth_fpgas}. And if we branch off \emph{after} this point (at
LTL or later) then CompCert has already performed register allocation to reduce the number of
registers and spill some variables to the stack; this transformation is not required in HLS because
there are many more registers available, and these should be used instead of RAM whenever possible.

3AC is also attractive because it is the closest intermediate language to LLVM IR, which is used by
several existing HLS compilers.  It has an unlimited number of pseudo-registers, and is represented
as a control flow graph (CFG) where each instruction is a node with links to the instructions that
can follow it. One difference between LLVM IR and 3AC is that 3AC includes operations that are
specific to the chosen target architecture; we chose to target the x86\_32 back end because it
generally produces relatively dense 3AC thanks to the availability of complex addressing modes.

\subsection{An Introduction to Verilog}

This section will introduce Verilog for readers who may not be familiar with the language,
concentrating on the features that are used in the output of Vericert.  Verilog is a hardware
description language (HDL) and is used to design hardware ranging from complete CPUs that are
eventually produced as integrated circuits, to small application-specific accelerators that are
placed on FPGAs.  Verilog is a popular language because it allows for fine-grained control over the
hardware, and also provides high-level constructs to simplify development.

Verilog behaves quite differently to standard software programming languages due to it having to
express the parallel nature of hardware.  The basic construct to achieve this is the always-block,
which is a collection of assignments that are executed every time some event occurs.  In the case of
Vericert, this event is either a positive (rising) or a negative (falling) clock edge.  All
always-blocks triggering on the same event are executed in parallel. Always-blocks can also express
control-flow using if-statements and case-statements.

\startplacemarginfigure[reference={fig:tutorial:state_machine},title={Example of a state machine
    implementation in Verilog and its corresponding state diagram.}]
  \startfloatcombination[nx=2, ny=1]
    \startplacesubfigure
      \startframedtext[width={0.6\textwidth},frame=off,offset=none,bodyfont=11pt]
      \starthlverilog
         module main(input rst, input y,
                     input clk, output reg z);
           reg tmp, state;
           always @(posedge clk)
             case (state)
               1'b0: tmp <= y;
               1'b1: begin tmp <= 1'b0;
                           z <= tmp; end
             endcase
           always @(posedge clk)
             if (rst) state <= 1'b0;
             else case (state)
               1'b0: if (y) state <= 1'b1;
                     else state <= 1'b0;
               1'b1: state <= 1'b0;
             endcase
         endmodule
      \stophlverilog
    \stopframedtext
    \stopplacesubfigure
    \startplacesubfigure
    \hbox{\starttikzpicture
      \node[draw,circle,inner sep=6pt] (s0) at (0,0) {$S_{\mathit{start}} / \text{\tt x}$};
      \node[draw,circle,inner sep=8pt] (s1) at (1.5,-3) {$S_{1} / \text{\tt 1}$};
      \node[draw,circle,inner sep=8pt] (s2) at (3,0) {$S_{0} / \text{\tt 1}$};
      \node (s2s) at ($(s2.west) + (-0.3,1)$) {\type{00}};
      \node (s2ss) at ($(s2.east) + (0.3,1)$) {\type{1x}};
      \draw[-{Latex[length=2mm,width=1.4mm]}] ($(s0.west) + (-0.3,1)$) to [out=0,in=120] (s0);
      \draw[-{Latex[length=2mm,width=1.4mm]}] (s0)
           to [out=-90,in=150] node[midway,left] {\type{01}} (s1);
      \draw[-{Latex[length=2mm,width=1.4mm]}] (s1)
      to [out=80,in=220] node[midway,left] {\type{xx}} (s2);
      \draw[-{Latex[length=2mm,width=1.4mm]}] (s2)
      to [out=260,in=50] node[midway,right] {\type{01}} (s1);
      \draw[-{Latex[length=2mm,width=1.4mm]}] (s2)
      to [out=120,in=40] ($(s2.west) + (-0.3,0.7)$) to [out=220,in=170] (s2);
      \draw[-{Latex[length=2mm,width=1.4mm]}] (s2)
      to [out=60,in=130] ($(s2.east) + (0.3,0.7)$) to [out=310,in=10] (s2);
      \stoptikzpicture}
    \stopplacesubfigure
  \stopfloatcombination
\stopplacemarginfigure

A simple state machine can be implemented as shown in \in{Figure}[fig:tutorial:state_machine].  At
every positive edge of the clock (\type{clk}), both of the always-blocks will trigger
simultaneously.  The first always-block controls the values in the register \type{x} and the output
\type{z}, while the second always-block controls the next state the state machine should go to.
When the \type{state} is 0, \type{tmp} will be assigned to the input \type{y} using nonblocking
assignment, denoted by \type{<=}.  Nonblocking assignment assigns registers in parallel at the end
of the clock cycle, rather than sequentially throughout the always-block. In the second
always-block, the input \type{y} will be checked, and if it is high it will move on to the next
state, otherwise it will stay in the current state.  When \type{state} is 1, the first always-block
will reset the value of \type{tmp} and then set \type{z} to the original value of \type{tmp}, since
nonblocking assignment does not change its value until the end of the clock cycle.  Finally, the
last always-block will set the state to 0 again.

\startplacemarginfigure[reference={fig:accumulator_c_rtl},title={Translating a simple
    program from C to Verilog.}]
  \startfloatcombination[nx=2,ny=1]
    \startplacefigure[number=no]
    \startfloatcombination[nx=1,ny=2]
    \startplacesubfigure[title={Example C code passed to Vericert.}]
      \startframedtext[width={0.4\textwidth},frame=off,offset=none,bodyfont=11pt]
        \starthlC
          int main() {
              int x[2] = {3, 6};
              int i = 1;
              return x[i];
          }
        \stophlC
      \stopframedtext
    \stopplacesubfigure
    \startplacesubfigure[title={3AC produced by the CompCert front-end without any optimisations.}]
      \startframedtext[width={0.4\textwidth},frame=off,offset=none,bodyfont=11pt]
      \starthlC
      main() {
        x5 = 3
        int32[stack(0)] = x5
        x4 = 6
        int32[stack(4)] = x4
        x1 = 1
        x3 = stack(0) (int)
        x2 = int32[x3 + x1
                   * 4 + 0]
        return x2
      }
      \stophlC
      \stopframedtext
    \stopplacesubfigure
    \stopfloatcombination
    \stopplacefigure
    \startplacesubfigure[title={Verilog produced by Vericert. It demonstrates the instantiation of
        the RAM (lines 9--15), the data-path (lines 16--32) and the control logic (lines 33--42).}]
      \startframedtext[width={\textwidth},frame=off,offset=none,bodyfont=10pt]
      \starthlverilog
module main(reset, clk, finish, return_val);
  input [0:0] reset, clk;
  output reg [0:0] finish = 0;
  output reg [31:0] return_val = 0;
  reg [31:0] reg_3 = 0, addr = 0, d_in = 0,
             reg_5 = 0, wr_en = 0;
  reg [0:0] en = 0, u_en = 0;
  reg [31:0] state = 0, reg_2 = 0, reg_4 = 0,
             d_out = 0, reg_1 = 0;
  reg [31:0] stack [1:0];
  // RAM interface
  always @(negedge clk)
    if ({u_en != en}) begin
      if (wr_en) stack[addr] <= d_in;
      else d_out <= stack[addr];
      en <= u_en;
    end
  // Data-path
  always @(posedge clk)
    case (state)
      32'd11: reg_2 <= d_out;
      32'd8: reg_5 <= 32'd3;
      32'd7: begin u_en <= ( ~ u_en); wr_en <= 32'd1;
                   d_in <= reg_5; addr <= 32'd0; end
      32'd6: reg_4 <= 32'd6;
      32'd5: begin u_en <= ( ~ u_en); wr_en <= 32'd1;
                   d_in <= reg_4; addr <= 32'd1; end
      32'd4: reg_1 <= 32'd1;
      32'd3: reg_3 <= 32'd0;
      32'd2: begin u_en <= ( ~ u_en); wr_en <= 32'd0;
                   addr <= {{{reg_3 + 32'd0}
                           + {reg_1 * 32'd4}}
                           / 32'd4};
             end
      32'd1: begin finish = 32'd1; return_val = reg_2; end
      default: ;
    endcase
  // Control logic
  always @(posedge clk)
    if ({reset == 32'd1}) state <= 32'd8;
    else case (state)
           32'd11: state <= 32'd1;      32'd4: state <= 32'd3;
           32'd8: state <= 32'd7;       32'd3: state <= 32'd2;
           32'd7: state <= 32'd6;       32'd2: state <= 32'd11;
           32'd6: state <= 32'd5;       32'd1: ;
           32'd5: state <= 32'd4;       default: ;
         endcase
endmodule
      \stophlverilog
      \stopframedtext
    \stopplacesubfigure
  \stopfloatcombination
\stopplacemarginfigure

\subsection{Translating C to Verilog by Example}
\in{Figure}[fig:accumulator_c_rtl] illustrates the translation of a simple program that stores and
retrieves values from an array.  In this section, we describe the stages of the Vericert
translation, referring to this program as an example.

\subsubsection{Translating C to 3AC}

The first stage of the translation uses unmodified CompCert to transform the C input, shown in
\in{Figure}{c}[fig:accumulator_c_rtl], into a 3AC intermediate representation, shown in
\in{Figure}{d}[fig:accumulator_c_rtl].  As part of this translation, function inlining is performed
on all functions, which allows us to support function calls without having to support the
\mono{Icall} 3AC instruction.  Although the duplication of the function bodies caused by inlining
can increase the area of the hardware, it can have a positive effect on latency and is therefore a
common HLS optimisation~\cite{noronha17_rapid_fpga}. Inlining precludes support for recursive
function calls, but this feature is not supported in most HLS tools
anyway~\cite{davidthomas_asap16}.

\subsubsection{Translating 3AC to HTL}

The next translation is from 3AC to a new \lindex{HTL}hardware translation language (HTL).  This
involves going from a CFG representation of the computation to a \index{FSMD}finite state machine
with data-path (FSMD) representation~\cite{hwang99_fsmd}. The core idea of the FSMD representation
is that it separates the control flow from the operations on the memory and registers.  Hence, an
HTL program consists of two maps from states to Verilog statements: the \emph{control logic} map,
which expresses state transitions, and the \emph{data-path} map, which expresses computations.
\in{Figure}[fig:accumulator_diagram] shows the resulting FSMD architecture. The right-hand block is
the control logic that computes the next state, while the left-hand block updates all the registers
and RAM based on the current program state.

The HTL language was mainly introduced to simplify the proof of translation from 3AC to Verilog, as
these languages have very different semantics.  It serves as an intermediate language with similar
semantics to 3AC at the top level, using maps to represents what to execute at every state, and
similar semantics to Verilog at the lower level by already using Verilog statements instead of more
abstract instructions.  Compared to plain Verilog, HTL is simpler to manipulate and analyse, thereby
making it easier to prove optimisations like proper RAM insertion.

\startplacemarginfigure[title={The FSMD for the example shown in \in{Figure}[fig:accumulator_c_rtl],
    split into a data-path and control logic for the next state calculation.  The Update block takes
    the current state, current values of all registers and at most one value stored in the RAM, and
    calculates a new value that can either be stored back in the RAM or in a
    register.},reference={fig:accumulator_diagram}]
  \definecolor[control][x=B3E2CD] \definecolor[data][x=FDCDAC]
\starttikzpicture
  \startscope[scale=1.15]
  \fill[control,fill opacity=1] (6.5,0) rectangle (12,5);
  \fill[data,fill opacity=1] (0,0) rectangle (5.5,5);
  \node at (1,4.7) {Data-path};
  \node at (7.5,4.7) {Control Logic};

  \fill[white,rounded corners=10pt] (7,0.5) rectangle (11.5,2.2);
  \node at (8,2) {\rmxx Next State FSM};
  \foreach \x in {8,...,2}
    {\pgfmathtruncatemacro{\y}{8-\x}%
      \node[draw,circle,inner sep=0,minimum size=10,scale=0.8] (s\x) at (7.5+\y/2,1.35) {\rmxx \x};}
  \node[draw,circle,inner sep=0,minimum size=10,scale=0.8] (s1c) at (11,1.35) {\rmxx 1};
  \node[draw,circle,inner sep=0,minimum size=13,scale=0.8] (s1) at (s1c) {};
  \foreach \x in {8,...,3}
    {\pgfmathtruncatemacro{\y}{\x-1}\draw[-{Latex[length=1mm,width=0.7mm]}] (s\x) -- (s\y);}
  \node[draw,circle,inner sep=0,minimum size=10,scale=0.8] (s11) at (10.5,0.9) {\rmxx 11};
  \draw[-{Latex[length=1mm,width=0.7mm]}] (s2) -- (s11);
  \draw[-{Latex[length=1mm,width=0.7mm]}] (s11) -- (s1);
  \draw[-{Latex[length=1mm,width=0.7mm]}] (7.2,1.7) to [out=0,in=100] (s8);

  \node[draw,fill=white] (nextstate) at (9.25,3) {\rmxx Current State};
  \draw[-{Latex[length=1mm,width=0.7mm]}] let \p1 = (nextstate) in
    (11.5,1.25) -| (11.75,\y1) -- (nextstate);
  \draw let \p1 = (nextstate) in (nextstate) -- (6,\y1) |- (6,1.5);
  \node[scale=0.5,rotate=60] at (7.5,0.75) {\mono{clk}};
  \node[scale=0.5,rotate=60] at (7.7,0.75) {\mono{rst}};
  \draw[-{Latex[length=1mm,width=0.7mm]}] (7.65,-0.5) -- (7.65,0.5);
  \draw[-{Latex[length=1mm,width=0.7mm]}] (7.45,-0.5) -- (7.45,0.5);

  \fill[white,rounded corners=10pt] (2,0.5) rectangle (5,3);
  \filldraw[fill=white] (0.25,0.5) rectangle (1.5,2.75);
  \node at (2.6,2.8) {\rmxx Update};
  \node[align=center] at (0.875,2.55) {\rmxx \mono{RAM}};
  \node[scale=0.5] at (4.7,1.5) {\mono{state}};
  \draw[-{Latex[length=1mm,width=0.7mm]}] (6,1.5) -- (5,1.5);
  \draw[-{Latex[length=1mm,width=0.7mm]}] (6,1.5) -- (7,1.5);
  \node[scale=0.5,rotate=60] at (4.1,0.9) {\mono{finished}};
  \node[scale=0.5,rotate=60] at (3.9,0.95) {\mono{return\_val}};
  \node[scale=0.5,rotate=60] at (2.5,0.75) {\mono{clk}};
  \node[scale=0.5,rotate=60] at (2.7,0.75) {\mono{rst}};

  \node[scale=0.5,right,inner sep=5pt] (ram1) at (2,2.1) {\mono{u\_en}};
  \node[scale=0.5,right,inner sep=5pt] (ram2) at (2,1.9) {\mono{wr\_en}};
  \node[scale=0.5,right,inner sep=5pt] (ram3) at (2,1.7) {\mono{addr}};
  \node[scale=0.5,right,inner sep=5pt] (ram4) at (2,1.5) {\mono{d\_in}};
  \node[scale=0.5,right,inner sep=5pt] (ram5) at (2,1.3) {\mono{d\_out}};

  \node[scale=0.5,left,inner sep=5pt] (r1) at (1.5,2.1) {\mono{u\_en}};
  \node[scale=0.5,left,inner sep=5pt] (r2) at (1.5,1.9) {\mono{wr\_en}};
  \node[scale=0.5,left,inner sep=5pt] (r3) at (1.5,1.7) {\mono{addr}};
  \node[scale=0.5,left,inner sep=5pt] (r4) at (1.5,1.5) {\mono{d\_in}};
  \node[scale=0.5,left,inner sep=5pt] (r5) at (1.5,1.3) {\mono{d\_out}};

  \draw[-{Latex[length=1mm,width=0.7mm]}] (ram1) -- (r1);
  \draw[-{Latex[length=1mm,width=0.7mm]}] (ram2) -- (r2);
  \draw[-{Latex[length=1mm,width=0.7mm]}] (ram3) -- (r3);
  \draw[-{Latex[length=1mm,width=0.7mm]}] (ram4) -- (r4);
  \draw[-{Latex[length=1mm,width=0.7mm]}] (r5) -- (ram5);

  \draw[-{Latex[length=1mm,width=0.7mm]}] (4,0.5) -- (4,-0.5);
  \draw[-{Latex[length=1mm,width=0.7mm]}] (3.75,0.5) -- (3.75,-0.5);
  \draw[-{Latex[length=1mm,width=0.7mm]}] (2.45,-0.5) -- (2.45,0.5);
  \draw[-{Latex[length=1mm,width=0.7mm]}] (2.65,-0.5) -- (2.65,0.5);

  \foreach \x in {0,...,1}
  {\draw (0.25,1-0.25*\x) -- (1.5,1-0.25*\x); \node at (0.875,0.88-0.25*\x) {\rmxx \x};}

  %\node[scale=0.5] at (1.2,2.2) {\mono{wr\_en}};
  %\node[scale=0.5] at (1.2,2) {\mono{wr\_addr}};
  %\node[scale=0.5] at (1.2,1.8) {\mono{wr\_data}};
  %\node[scale=0.5] at (1.2,1.4) {\mono{r\_addr}};
  %\node[scale=0.5] at (1.2,1.2) {\mono{r\_data}};
  %
  %\node[scale=0.5] at (2.3,2.2) {\mono{wr\_en}};
  %\node[scale=0.5] at (2.3,2) {\mono{wr\_addr}};
  %\node[scale=0.5] at (2.3,1.8) {\mono{wr\_data}};
  %\node[scale=0.5] at (2.3,1.4) {\mono{r\_addr}};
  %\node[scale=0.5] at (2.3,1.2) {\mono{r\_data}};
  %
  %\draw[-{Latex[length=1mm,width=0.7mm]}] (2,2.2) -- (1.5,2.2);
  %\draw[-{Latex[length=1mm,width=0.7mm]}] (2,2) -- (1.5,2);
  %\draw[-{Latex[length=1mm,width=0.7mm]}] (2,1.8) -- (1.5,1.8);
  %\draw[-{Latex[length=1mm,width=0.7mm]}] (2,1.4) -- (1.5,1.4);
  %\draw[-{Latex[length=1mm,width=0.7mm]}] (1.5,1.2) -- (2,1.2);

  \filldraw[fill=white] (2.8,3.25) rectangle (4.2,4.75);
  \node at (3.5,4.55) {\rmxx \mono{Registers}};
  \draw[-{Latex[length=1mm,width=0.7mm]}] (2,2.4) -| (1.75,4) -- (2.8,4);
  \draw[-{Latex[length=1mm,width=0.7mm]}] (4.2,4) -- (5.25,4) |- (5,2.4);
  \draw[-{Latex[length=1mm,width=0.7mm]}] (5.25,2.4) -- (6.2,2.4) |- (7,1.8);

  \node[scale=0.5] at (3.5,4.2) {\mono{reg\_1}};
  \node[scale=0.5] at (3.5,4) {\mono{reg\_2}};
  \node[scale=0.5] at (3.5,3.8) {\mono{reg\_3}};
  \node[scale=0.5] at (3.5,3.6) {\mono{reg\_4}};
  \node[scale=0.5] at (3.5,3.4) {\mono{reg\_5}};
\stopscope
\stoptikzpicture
\stopplacemarginfigure

\paragraph{Translating memory.} Typically, HLS-generated hardware consists of a sea of registers and
RAMs.  This memory view is very different from the C memory model, so we perform the following
translation from CompCert's abstract memory model to a concrete RAM.  Variables that do not have
their address taken are kept in registers, which correspond to the registers in 3AC.  All
address-taken variables, arrays, and structs are kept in RAM.  The stack of the main function
becomes an unpacked array of 32-bit integers representing the RAM block.  Any loads and stores are
temporarily translated to direct accesses to this array, where each address has its offset removed
and is divided by four.  In a separate HTL-to-HTL conversion, these direct accesses are then
translated to proper loads and stores that use a RAM interface to communicate with the RAM, shown on
lines 21, 24 and 28 of \in{Figure}{a}[fig:accumulator_c_rtl].  This pass inserts a RAM block with
the interface around the unpacked array.  Without this interface and without the RAM block, the
synthesis tool processing the Verilog hardware description would not identify the array as a RAM,
and would instead implement it using many registers.  This interface is shown on lines 9--15 in the
Verilog code in \in{Figure}{a}[fig:accumulator_c_rtl].  A high-level overview of the architecture
and of the RAM interface can be seen in \in{Figure}[fig:accumulator_diagram].

\paragraph{Translating instructions.} Most 3AC instructions correspond to hardware constructs.  For
example, line 2 in \in{Figure}{d}[fig:accumulator_c_rtl] shows a 32-bit register \type{x5} being
initialised to 3, after which the control flow moves execution to line 3. This initialisation is
also encoded in the Verilog generated from HTL at state 8 in both the control logic and data-path
always-blocks, shown at lines 33 and 16 respectively in \in{Figure}{a}[fig:accumulator_c_rtl].
Simple operator instructions are translated in a similar way.  For example, the add instruction is
just translated to the built-in add operator, similarly for the multiply operator.  All 32-bit
instructions can be translated in this way, but some special instructions require extra care. One
such instruction is the \type{Oshrximm} instruction, which is discussed further in
\in{Section}[sec:algorithm:optimisation:oshrximm].  Another is the \type{Oshldimm} instruction,
which is a left rotate instruction that has no Verilog equivalent and therefore has to be
implemented in terms of other operations and proven to be equivalent.  The only 32-bit instructions
that we do not translate are case-statements (\type{Ijumptable}) and those instructions related to
function calls (\type{Icall}, \type{Ibuiltin}, and \type{Itailcall}), because we enable
\oindex{inlining}inlining by default.

\subsubsection{Translating HTL to Verilog}

Finally, we have to translate the HTL code into proper Verilog.  The challenge here is to translate
our FSMD representation into a Verilog AST.  However, as all the instructions in HTL are already
expressed as Verilog statements, only the top-level data-path and control logic maps need to be
translated to valid Verilog case-statements.  We also require declarations for all the variables in
the program, as well as declarations of the inputs and outputs to the module, so that the module can
be used inside a larger hardware design.  In addition to translating the maps of Verilog statements,
an always-block that will behave like the RAM also has to be created, which is only modelled
abstractly at the HTL level.  \in{Figure}{a}[fig:accumulator_c_rtl] shows the final Verilog output
that is generated for our example.

Although this translation seems quite straight\-forward, proving that this translation is correct is
complex.  All the implicit assumptions that were made in HTL need to be translated explicitly to
Verilog statements and it needs to be shown that these explicit behaviours are equivalent to the
assumptions made in the HTL semantics.  One main example of this is proving that the specification
of the RAM in HTL does indeed behave in the same as its Verilog implementation.  We discuss these
proofs in upcoming sections.

\subsection{Optimisations}

Although we would not claim that Vericert is a proper \quote{optimising} HLS compiler yet, we have
nonetheless made several design choices that aim to improve the quality of the hardware designs it
produces.

\subsubsection{Byte- and Word-Addressable Memories}

One big difference between C and Verilog is how memory is represented.  Although Verilog arrays use
similar syntax to C arrays, they must be treated quite differently. To make loads and stores as
efficient as possible, the RAM needs to be word-addressable, which means that an entire integer can
be loaded or stored in one clock cycle.  However, the memory model that CompCert uses for its
intermediate languages is byte-addre\-ssa\-ble~\cite{blazy05_formal_verif_memor_model_c}.  If a
byte-addressable \index{memory model}memory was used in the target hardware, which is closer to
CompCert's memory model, then a load and store would instead take four clock cycles, because a RAM
can only perform one read and write per clock cycle.  It therefore has to be proven that the
byte-addressable memory behaves in the same way as the word-addressable memory in hardware.  Any
modifications of the bytes in the CompCert memory model also have to be shown to modify the
word-addressable memory in the same way.  Since only integer loads and stores are currently
supported in Vericert, it follows that the addresses given to the loads and stores will be multiples
of four.  Translating from byte-addressed memory to word-addressed memory can then be done by
dividing the address by four.

\subsubsection[sec:algorithm:optimisation:ram]{Implementation of RAM Interface}

The simplest way to implement loads and stores in Vericert would be to access the Verilog array
directly from within the data-path (i.e., inside the always-block on lines 16--32 of
\in{Figure}{a}[fig:accumulator_c_rtl]). This would be correct, but when a Verilog array is accessed
at several program points, the synthesis tool is unlikely to detect that it can be implemented as a
RAM block, and will resort to using lots of registers instead, ruining the circuit's area and
performance.  To avert this, we arrange that the data-path does not access memory directly, but
simply sets the address it wishes to access and then toggles the \type{u_en} flag. This activates
the RAM interface (lines 9--15 of \in{Figure}{a}[fig:accumulator_c_rtl]) on the next falling clock
edge, which performs the requested load or store. By factoring all the memory accesses out into a
separate interface, we ensure that the underlying array is only accessed from a single program point
in the Verilog code, and thus ensure that the synthesis tool will correctly infer a RAM
block.\footnote{Interestingly, the Verilog code shown for the RAM interface must not be modified,
  because the synthesis tool will only generate a RAM when the code matches a small set of specific
  patterns.}

Therefore, an extra compiler pass is added from HTL to HTL to extract all the direct accesses to the
Verilog array and replace them by signals that access the RAM interface in a separate
always-block. The translation is performed by going through all the instructions and replacing each
load and store expression in turn.  Stores can simply be replaced by the necessary wires
directly. Loads are a little more subtle: loads that use the RAM interface take two clock cycles
where a direct load from an array takes only one, so this pass inserts an extra state after each
load.

There are two interesting parts to the inserted RAM interface.  Firstly, the memory updates are
triggered on the negative (falling) edge of the clock, out of phase with the rest of the design
which is triggered on the positive (rising) edge of the clock.  The advantage of this is that
instead of loads and stores taking three clock cycles and two clock cycles respectively, they only
take two clock cycles and one clock cycle instead, greatly improving their performance.  Using the
negative edge of the clock is widely supported by synthesis tools, and does not affect the maximum
frequency of the final design.

Secondly, the logic in the enable signal of the RAM (\type{en != u_en}) is also atypical in
hardware designs.  Enable signals are normally manually controlled and inserted into the appropriate
states, by using a check like the following in the RAM: \type{en == 1}.  This means that the RAM
only turns on when the enable signal is set.  However, to make the proof simpler and avoid reasoning
about possible side effects introduced by the RAM being enabled but not used, a RAM which disables
itself after every use would be ideal.  One method for implementing this would be to insert an extra
state after each load or store that disables the RAM, but this extra state would eliminate the speed
advantage of the negative-edge-triggered RAM. Another method would be to determine the next state
after each load or store and disable the RAM in that state, but this could quickly become
complicated, especially in the case where the next state also contains a memory operation, and hence
the disable signal should not be added. The method we ultimately chose was to have the RAM become
enabled not when the enable signal is high, but when it \emph{toggles} its value.  This can be
arranged by keeping track of the old value of the enable signal in \type{en} and comparing it to the
current value \type{u_en} set by the data-path.  When the values are different, the RAM gets
enabled, and then \type{en} is set to the value of \type{u_en}. This ensures that the RAM will
always be disabled straight after it was used, without having to insert or modify any other states.

\startplacemarginfigure[reference={fig:ram_load_store},title={Timing diagrams showing the execution
    of loads and stores over multiple clock cycles.}]
  \startfloatcombination[nx=2]
    \startplacesubfigure[title={Timing diagram for loads. At time 1, the \type{u_en} signal is
        toggled to enable the RAM. At time 2, \type{d_out} is set to the value stored at the
        address in the RAM, which is finally assigned to the register \type{r} at time 3.}]
      \externalfigure[figures/timing-1.pdf]
    \stopplacesubfigure
  \startplacesubfigure[title={Timing diagram for stores. At time 1, the \type{u_en} signal is
      toggled to enable the RAM, and the address \type{addr} and the data to store \type{d_in} are
      set. On the negative edge at time 2, the data is stored into the RAM.}]
    \externalfigure[figures/timing-2.pdf]
  \stopplacesubfigure
  \stopfloatcombination
\stopplacemarginfigure

\in{Figure}[fig:ram_load_store] gives an example of how the RAM interface behaves when values are
loaded and stored.

\subsubsection[sec:algorithm:optimisation:oshrximm]{Implementing the \mono{Oshrximm}
  Instruction}

Many of the CompCert instructions map well to hardware, but \type{Oshrximm} (efficient signed
division by a power of two using a logical shift) is expensive if implemented na\"ively. The problem
is that in CompCert it is specified as a signed division: (where $x, y \in \mathbb{Z}$,
$0 \leq y < 31$, and $-2^{31} \leq x < 2^{31}$) and instantiating divider circuits in hardware is
well known to cripple performance. Moreover, since Vericert requires the result of a divide
operation to be ready within a single clock cycle, the divide circuit needs to be entirely
combinational. This is inefficient in terms of area, but also in terms of latency, because it means
that the maximum frequency of the hardware must be reduced dramatically so that the divide circuit
has enough time to finish.  It should therefore be implemented using a sequence of shifts.

CompCert eventually performs a translation from this representation into assembly code which uses
shifts to implement the division, however, the specification of the instruction in 3AC itself still
uses division instead of shifts, meaning this proof of the translation cannot be reused.  In
Vericert, the equivalence of the representation in terms of divisions and shifts is proven over the
integers and the specification, thereby making it simpler to prove the correctness of the Verilog
implementation in terms of shifts.

\section[title={A Formal Semantics for Verilog},reference={sec:hls:verilog}]

This section describes the Verilog semantics that was chosen for the target language, including the
changes that were made to the semantics to make it a suitable HLS target. The Verilog standard is
quite
large~\cite[06_ieee_stand_veril_hardw_descr_languag,05_ieee_stand_veril_regis_trans_level_synth],
but the syntax and semantics can be reduced to a small subset that Vericert needs to target. This
section also describes how CompCert's representation of memory differs from CompCert's memory model.

The Verilog semantics we use is ported to Coq from a semantics written in HOL4 by
\cite[authoryears][loow19_proof_trans_veril_devel_hol] and used to prove the translation from HOL4
to Verilog~\cite[loow19_verif_compil_verif_proces]. This semantics is quite practical as it is
restricted to a small subset of Verilog, which can nonetheless be used to model the hardware
constructs required for HLS. The main features that are excluded are continuous assignment and
combinational always-blocks; these are modelled in other semantics such as that
by~\cite[authoryears][meredith10_veril].

The semantics of Verilog differs from regular programming languages, as it is used to describe
hardware directly, which is inherently parallel, rather than an algorithm, which is usually
sequential. The main construct in Verilog is the always-block. A module can contain multiple
always-blocks, all of which run in parallel. These always-blocks further contain statements such as
if-statements or assignments to variables. We support only {\em synchronous} logic, which means that
the always-block is triggered on (and only on) the positive or negative edge of a clock signal.

The semantics combines the big-step and small-step styles. The overall execution of the hardware is
described using a small-step semantics, with one small step per clock cycle; this is appropriate
because hardware is routinely designed to run for an unlimited number of clock cycles and the
big-step style is ill-suited to describing infinite executions. Then, within each clock cycle, a
big-step semantics is used to execute all the statements. An example of a rule for executing an
always-block that is triggered at the positive edge of the clock is shown below, where $\Sigma$ is
the state of the registers in the module and $s$ is the statement inside the always-block:

\placeformula\startformula
  \text{\sc Always }\ \dfrac{(\Sigma, s)\downarrow_{\text{stmnt}} \Sigma'}{(\Sigma, \text{\tt always
        @(posedge clk)} s) \downarrow_{\text{always}^{+}} \Sigma'}
\stopformula

This rule says that assuming the statement $s$ in the always-block runs with state $\Sigma$ and
produces the new state $\Sigma'$, the always-block will result in the same final state.

Two types of assignments are supported in always-blocks: nonblocking and blocking
assignment. Nonblocking assignments all take effect simultaneously at the end of the clock cycle,
while blocking assignments happen instantly so that later assignments in the clock cycle can pick
them up. To model both of these assignments, the state $\Sigma$ has to be split into two maps:
$\Gamma$, which contains the current values of all variables and arrays, and $\Delta$, which
contains the values that will be assigned at the end of the clock cycle. $\Sigma$ can therefore be
defined as follows: $\Sigma = (\Gamma, \Delta)$. Nonblocking assignment can therefore be expressed
as follows:

\placeformula\startformula \text{\sc Nonblocking Reg }\ \frac{\text{\tt name}\ d = \text{\tt OK}\ n \\ (\Gamma, e) \downarrow_{\text{expr}} v}{((\Gamma, \Delta), d\ \text{\tt <= } e) \downarrow_{\text{stmnt}} (\Gamma, \Delta [n \mapsto v])}\\ \stopformula

where assuming that $\downarrow_{\text{expr}}$ evaluates an expression $e$ to a value $v$, the
nonblocking assignment $d\ \text{\tt <= } e$ updates the future state of the variable $d$ with value
$v$.

Finally, the following rule dictates how the whole module runs in one clock cycle:

\placeformula\startformula \text{\sc Module }\ \frac{(\Gamma, \epsilon, \vec{m})\
  \downarrow_{\text{module}} (\Gamma', \Delta')}{\left(\Gamma,
    \startmatrix[align={1:left}]
      \NC\text{\tt module}\ \text{\tt main} \text{\tt (...);}\NR
      \NC\quad\vec{m}\NR
      \NC\text{\tt endmodule}\NR
    \stopmatrix\right) \downarrow_{\text{program}} (\Gamma'\ //\
  \Delta')} \stopformula

where $\Gamma$ is the initial state of all the variables, $\epsilon$ is the empty map because the
$\Delta$ map is assumed to be empty at the start of the clock cycle, and $\vec{m}$ is a list of
variable declarations and always-blocks that $\downarrow_{\text{module}}$ evaluates sequentially to
obtain $(\Gamma', \Delta')$. The final state is obtained by merging these maps using the $//$
operator, which gives priority to the right-hand operand in a conflict. This rule ensures that the
nonblocking assignments overwrite at the end of the clock cycle any blocking assignments made during
the cycle.

\subsection[changes-to-the-semantics]{Changes to the Semantics}

Five changes were made to the semantics proposed by
\cite[authoryears][loow19_proof_trans_veril_devel_hol] to make it suitable as an HLS target.

\subsubsection[adding-array-support]{Adding array support}

The main change is the addition of support for arrays, which are needed to model RAM in Verilog. RAM
is needed to model the stack in C efficiently, without having to declare a variable for each
possible stack location. Consider the following Verilog code:

\blank[big]
\starthlverilog
reg [31:0] x[1:0];
always @(posedge clk) begin x[0] = 1; x[1] <= 1; end
\stophlverilog
\blank[big]

which modifies one array element using blocking assignment and then a second using nonblocking
assignment. If the existing semantics were used to update the array, then during the merge, the
entire array \type{x} from the nonblocking association map would replace the entire array from the
blocking association map. This would replace \type{x[0]} with its original value and therefore
behave incorrectly. Accordingly, we modified the maps so they record updates on a per-element
basis. Our state $\Gamma$ is therefore further split up into $\Gamma_{r}$ for instantaneous updates
to variables, and $\Gamma_{a}$ for instantaneous updates to arrays
($\Gamma = (\Gamma_{r}, \Gamma_{a})$); $\Delta$ is split similarly
($\Delta = (\Delta_{r}, \Delta_{a})$). The merge function then ensures that only the modified
indices get updated when $\Gamma_{a}$ is merged with the nonblocking map equivalent $\Delta_{a}$.

\subsubsection[adding-negative-edge-support]{Adding negative edge support}

To reason about circuits that execute on the negative edge of the clock (such as our RAM interface
described in \in{Section}[sec:algorithm:optimisation:ram]), support for negative-edge-triggered
always-blocks was added to the semantics. This is shown in the modifications of the {\sc Module}
rule shown below:

\placeformula\startformula \text{\sc Module }\ \frac{
\startmatrix
(\NC \Gamma, \epsilon, \vec{m})\
  \downarrow_{\text{module}^{+}} (\Gamma', \Delta') \NR\NC (\Gamma'\ //\ \Delta', \epsilon, \vec{m})
  \downarrow_{\text{module}^{-}} (\Gamma'', \Delta'')\NR\stopmatrix}{\left(\Gamma,
    \startmatrix[align={1:left}]
      \NC\text{\tt module}\ \text{\tt main} \text{\tt (...);}\NR
      \NC\quad\vec{m}\NR
      \NC\text{\tt endmodule}\NR
    \stopmatrix\right) \downarrow_{\text{program}} (\Gamma''\ //\
  \Delta'')} \stopformula

The main execution of the module $\downarrow_{\text{module}}$ is split into
$\downarrow_{\text{module}^{+}}$ and $\downarrow_{\text{module}^{-}}$, which are rules that only
execute always-blocks triggered at the positive and at the negative edge respectively. The
positive-edge-triggered always-blocks are processed in the same way as in the original {\sc Module}
rule. The output maps $\Gamma'$ and $\Delta'$ are then merged and passed as the blocking assignments
map into the negative edge execution, so that all the blocking and nonblocking assignments are
present. Finally, all the negative-edge-triggered always-blocks are processed and merged to give the
final state.

\subsubsection[adding-declarations]{Adding declarations}

Explicit support for declaring inputs, outputs and internal variables was added to the semantics to
make sure that the generated Verilog also contains the correct declarations. This adds some
guarantees to the generated Verilog and ensures that it synthesises and simulates correctly.

\subsubsection[removing-support-for-external-inputs-to-modules]{Removing support for external inputs
  to modules}

Support for receiving external inputs was removed from the semantics for simplicity, as these are
not needed for an HLS target. The main module in Verilog models the main function in C, and since
the inputs to a C function should not change during its execution, there is no need for external
inputs for Verilog modules.

\subsubsection[simplifying-representation-of-bitvectors]{Simplifying representation of bitvectors}

Finally, we use 32-bit integers to represent bitvectors rather than arrays of booleans. This is
because Vericert (currently) only supports types represented by 32 bits.

\subsection[sec:hls:verilog:integrating]{Integrating the Verilog Semantics into CompCert's Model}

\startplacefigure[reference={fig:inference_module},title={Top-level semantics used in CompCert to
    initiate the first call to \type{main} and well as return the final result of the \type{main}
    function.}]
\startformula \startmathalignment[n=1]
  \NC\text{\sc Step }\ \frac{\startmatrix[n=1]
    \NC \Gamma_r[\mathit{rst}] = 0 \qquad \Gamma_r[\mathit{fin}] = 0 \NR
    \NC(m, (\Gamma_r, \Gamma_a))\ \downarrow_{\text{program}} (\Gamma_r', \Gamma_a') \NR
  \stopmatrix}{\text{\tt State}\ \mathit{sf}\ m\ \ \Gamma_r[\sigma]\ \ \Gamma_r\ \Gamma_a
    \longrightarrow \text{\tt State}\ \mathit{sf}\ m\ \ \Gamma_r'[\sigma]\ \ \Gamma_r'\ \Gamma_a'}\NR
%
  \NC\text{\sc Finish }\ \frac{\Gamma_r[\mathit{fin}] = 1}{\text{\tt State}\ \mathit{sf}\ m\ \sigma\
    \Gamma_r\ \Gamma_a \longrightarrow \text{\tt Returnstate}\ \mathit{sf}\ \Gamma_r[ \mathit{ret}]}\NR
%
  \NC\text{\sc Call }\ \frac{}{\startmatrix[n=1]
    \NC\text{\tt Callstate}\ \mathit{sf}\ m\ \vec{r}\longrightarrow\NR
    \NC
    \text{\tt State}\ \mathit{sf}\ m\ n\ ((\text{\tt init\_params}\ \vec{r}\ a)[\sigma \mapsto n,
      \mathit{fin} \mapsto 0, \mathit{rst} \mapsto 0])\ \epsilon \NR
  \stopmatrix
}\NR
%
  \NC\text{\sc Return }\ \frac{}{\startmatrix[n=1]
    \NC\text{\tt Returnstate}\ (\text{\tt Stackframe}\ r\ m\ \mathit{pc}\
      \Gamma_r\ \Gamma_a :: \mathit{sf})\ v \NR
    \NC\longrightarrow \text{\tt State}\ \mathit{sf}\ m\ \mathit{pc}\ (\Gamma_{r} [ \sigma \mapsto
      \mathit{pc}, r \mapsto v ])\ \Gamma_{a}\NR
    \stopmatrix}\NR
\stopmathalignment \stopformula
\stopplacefigure

The CompCert computation model defines a set of states through which execution passes. In this
subsection, we explain how we extend our Verilog semantics with four special-purpose registers in
order to integrate it into CompCert.

CompCert executions pass through three main states:

\desc{\type{State} $\mathit{sf}$ $m$ $v$ $\Gamma_{r}$ $\Gamma_{a}$} The main state when executing a
function, with stack frame $\mathit{sf}$, current module $m$, current state $v$ and variable states
$\Gamma_{r}$ and $\Gamma_{a}$.

\desc{\type{Callstate} $\mathit{sf}$ $m$ $\vec{r}$} The state that is reached when a function is
called, with the current stack frame $\mathit{sf}$, current module $m$ and arguments $\vec{r}$.

\desc{\type{Returnstate} $\mathit{sf}$ $v$} The state that is reached when a function returns back
to the caller, with stack frame $\mathit{sf}$ and return value $v$.

To support this computational model, we extend the Verilog module we generate with the following
four registers and a RAM block:

\desc{program counter} The program counter can be modelled using a register that keeps track of the
state, denoted as $\sigma$.

\desc{function entry point} When a function is called, the entry point denotes the first instruction
that will be executed. This can be modelled using a reset signal that sets the state accordingly,
denoted as $\mathit{rst}$.

\desc{return value} The return value can be modelled by setting a finished flag to 1 when the result
is ready, and putting the result into a 32-bit output register. These are denoted as $\mathit{fin}$
and $\mathit{ret}$ respectively.

\desc{stack} The function stack can be modelled as a RAM block, which is implemented using an array
in the module, and denoted as $\mathit{stk}$.

\in{Figure}[fig:inference_module] shows the inference rules for moving between the computational
states. The first, {\sc Step}, is the normal rule of execution. It defines one step in the
\type{State} state, assuming that the module is not being reset, that the finish state has not been
reached yet, that the current and next state are $v$ and $v'$, and that the module runs from state
$\Gamma$ to $\Gamma'$ using the {\sc Step} rule. The {\sc Finish} rule returns the final value of
running the module and is applied when the $\mathit{fin}$ register is set; the return value is then
taken from the $\mathit{ret}$ register.

Note that there is no step from \type{State} to \type{Callstate}; this is because function calls are
not supported, and it is therefore impossible in our semantics ever to reach a \type{Callstate}
except for the initial call to main. So the {\sc Call} rule is only used at the very beginning of
execution; likewise, the {\sc Return} rule is only matched for the final return value from the main
function. Therefore, in addition to the rules shown in \in{Figure}[fig:inference_module], an initial
state and final state need to be defined:

\placeformula\startformula\startmathalignment[n=1]
  \NC\text{\sc Initial }\ \frac{\text{\tt is\_internal}\ P.\text{\tt main}}{\text{\tt initial\_state}\
    (\text{\tt Callstate}\ []\ P.\text{\tt main}\ [])}\NR
  \NC\text{\sc Final }\ \frac{}{\text{\tt final\_state}\ (\text{\tt Returnstate}\ []\ n)\ n}\NR
\stopmathalignment\stopformula

\noindent where the initial state is the \type{Callstate} with an empty stack frame and no arguments
for the \type{main} function of program $P$, where this \type{main} function needs to be in the
current translation unit. The final state results in the program output of value $n$ when reaching a
\type{Returnstate} with an empty stack frame.

\subsection[sec:hls:verilog:memory]{Memory Model}

The Verilog semantics do not define a memory model for Verilog, as this is not needed for a hardware
description language. There is no preexisting architecture that Verilog will produce; it can
describe any memory layout that is needed. Instead of having specific semantics for memory, the
semantics only needs to support the language features that can produce these different memory
layouts, these being Verilog arrays.  We therefore define semantics for updating Verilog arrays
using blocking and nonblocking assignment. We then have to prove that the C memory model that
CompCert uses matches with the interpretation of arrays used in Verilog. The CompCert memory model
is infinite, whereas our representation of arrays in Verilog is inherently finite. There have
already been efforts to define a general finite memory model for all intermediate languages in
CompCert, such as CompCertS~\cite[besson18_compc] or CompCert-TSO~\cite[sevcik13_compc], or keeping
the intermediate languages intact and translate to a more concrete finite memory model in the back
end, such as in CompCertELF~\cite[wang20_compc]. We also define such a translation from CompCert's
standard infinite memory model to finite arrays that can be represented in Verilog. There is
therefore no more notion of an abstract memory model and all the interactions to memory are encoded
in the hardware itself.

\definecolor[compcertmemmodel][x=E2CCEA]
\definecolor[vericertmemmodel][x=CBE1DB]

\startplacefigure[reference={fig:memory_model_transl},title={Change in the memory model during the
    translation of 3AC into HTL.  The state of the memories in each case is right after the
    execution of the store to memory.}]
  \hbox{\starttikzpicture
  \fill[compcertmemmodel,rounded corners=3pt] (0,0) rectangle (5,-5);
    \fill[vericertmemmodel,rounded corners=3pt] (7,0) rectangle (12,-5);
    \node[right] at (0,-0.3) {\rmx {\bf CompCert's Memory Model}};
    \node[right] at (7,-0.3) {\rmx {\bf Verilog Memory Representation}};
    \node[right] (x0) at (0.2,-1.9) {\rmx 0};
    \node[right] (x1) at (0.2,-2.5) {\rmx 1};
    \node[rotate=90] (x2) at (0.43,-3.1) {$\cdots$};
    \foreach \x in {0,...,6}{%
      \node[right] (s\x) at (2.5,-1-\x*0.3) {\rmx \x};
      \node[right] (t\x) at (4,-1-\x*0.3) {};
      \draw[->] (s\x) -- (t\x);
    }

    \node[right] at (t0) {\rmx {\tt DE}};
    \node[right] at (t1) {\rmx {\tt AD}};
    \node[right] at (t2) {\rmx {\tt BE}};
    \node[right] at (t3) {\rmx {\tt EF}};
    \node[right] at (t4) {\rmx {\tt 12}};
    \node[right] at (t5) {\rmx {\tt 34}};
    \node[right] at (t6) {\rmx {\tt 56}};
    \node[right] at (3.1,-3.1) {$\cdots$};

    \node[right] at (3.1,-4) {$\cdots$};
    \node[scale=1.3] at (6,-2.5) {\rmd $\Rightarrow$};

    \draw[->] (x0) -- (s3);
    \draw[->] (x1) -- (2.5,-4);
    \draw (0,-4.3) -- (5,-4.3);
    \node at (2.5,-4.7) {\rmx {\tt x[0] = 0xDEADBEEF;}};

    \draw (7.2,-1.2) rectangle (9.4,-3.9);
    \draw (9.6,-1.2) rectangle (11.8,-3.9);

    \foreach \x in {0,...,8}{%
      \draw (7.2,-1.2-\x*0.3) -- (9.4,-1.2-\x*0.3);
      \draw (9.6,-1.2-\x*0.3) -- (11.8,-1.2-\x*0.3);
      \node (b\x) at (8.3,-1.35-\x*0.3) {};
      \node (nb\x) at (10.7,-1.35-\x*0.3) {};
    }

    \node at (b0) {{\ttxx 0: Some 00000000}};
    \node at (b1) {{\ttxx 1: Some 12345600}};
    \node at (b2) {{\ttxx 2: Some 00000000}};
    \node at (b3) {{\ttxx 3: Some 00000000}};
    \node at (b4) {{\ttxx 4: Some 00000000}};
    \node at (b5) {{\ttxx 5: Some 00000000}};
    \node at (b6) {{\ttxx 6: Some 00000000}};
    \node at ($(b7) - (0,0.05)$) {$\cdots$};
    \node at (b8) {\rmxx{\tt N: Some 00000000}};

    \node at (nb0) {\rmxx{\tt 0: Some DEADBEEF}};
    \node[left] at (nb1) {\rmxx{\tt 1: None}};
    \node[left] at (nb2) {\rmxx{\tt 2: None}};
    \node[left] at (nb3) {\rmxx{\tt 3: None}};
    \node[left] at (nb4) {\rmxx{\tt 4: None}};
    \node[left] at (nb5) {\rmxx{\tt 5: None}};
    \node[left] at (nb6) {\rmxx{\tt 6: None}};
    \node at ($(nb7) - (0,0.05)$) {$\cdots$};
    \node[left] at (nb8) {\rmxx{\tt N: None}};

    \node at (8.3,-1) {$\Gamma_{a}$};
    \node at (10.7,-1) {$\Delta_{a}$};

    \draw (7,-4.3) -- (12,-4.3);
    \node at (9.5,-4.7) {\rmx {\tt stack[0] <= 0xDEADBEEF;}};
\stoptikzpicture}
\stopplacefigure

This translation is represented in \in{Figure}[fig:memory_model_transl].  CompCert's memory model
defines a map from blocks to maps from memory addresses to memory contents. Each block represents an
area in memory; for example, a block can represent a global variable or a stack for a function. As
there are no global variables, the main stack can be assumed to be block 0, and this is the only
block we translate. Meanwhile, our Verilog semantics defines two finite arrays of optional values,
one for the blocking assignments map $\Gamma_{\rm a}$ and one for the nonblocking assignments map
$\Delta_{\rm a}$. The optional values are present to ensure correct merging of the two association
maps at the end of the clock cycle. The invariant used in the proofs is that block 0 should be
equivalent to the merged representation of the $\Gamma_{\rm a}$ and $\Delta_{\rm a}$ maps.

\section[sec:hls:proof]{Correctness Proof}

Now that the Verilog semantics have been adapted to the CompCert model, we are in a position to
formally prove the correctness of our C-to-Verilog compilation. This section describes the main
correctness theorem that was proven and the key ideas in the proof. The full Coq proof is available
online~.

\subsection[main-challenges-in-the-proof]{Main Challenges in the Proof}

The proof of correctness of the Verilog back end is quite different from the usual proofs performed
in CompCert, mainly because of the difference in the memory model and semantic differences between
Verilog and CompCert's existing intermediate languages.

\startitemize
\item
  As already mentioned in \in{Section}[sec:hls:verilog:memory], because the memory model in our Verilog
  semantics is finite and concrete, but the CompCert memory model is more abstract and infinite with
  additional bounds, the equivalence of these models needs to be proven.  Moreover, our memory is
  word-addressed for efficiency reasons, whereas CompCert's memory is byte-addressed.
\item
  Second, the Verilog semantics operates quite differently to the usual intermediate languages in
  CompCert. All the CompCert intermediate languages use a map from control-flow nodes to
  instructions. An instruction can therefore be selected using an abstract program
  pointer. Meanwhile, in the Verilog semantics the whole design is executed at every clock cycle,
  because hardware is inherently parallel. The program pointer is part of the design as well, not
  just part of an abstract state. This makes the semantics of Verilog simpler, but comparing it to
  the semantics of 3AC becomes more challenging, as one has to map the abstract notion of the state
  to concrete values in registers.
\stopitemize

Together, these differences mean that translating 3AC directly to Verilog is infeasible, as the
differences in the semantics are too large. Instead, HTL, which was introduced in
\in{Section}[sec:hls:design], bridges the gap in the semantics between the two languages. HTL still
consists of maps, like many of the other CompCert languages, but each state corresponds to a Verilog
statement.

\subsection[formulating-the-correctness-theorem]{Formulating the Correctness Theorem}

The main correctness theorem is analogous to that stated in
CompCert~\cite{leroy09_formal_verif_realis_compil}: for all Clight source programs $C$, if the
translation to the target Verilog code succeeds, $\mathit{Safe}(C)$ holds and the target Verilog has
behaviour $B$ when simulated, then $C$ will have the same behaviour $B$.  $\mathit{Safe}(C)$ means
all observable behaviours of $C$ are safe, which can be defined as
$\forall B,\ C \Downarrow B \implies B \in \text{\tt Safe}$. A behaviour is in \type{Safe} if it is
either a final state (in the case of convergence) or divergent, but it cannot \quote{go
  wrong}. (This means that the source program must not contain undefined behaviour.) In , a
behaviour is also associated with a trace of I/O events, but since external function calls are not
supported in , this trace will always be empty.

Whenever the translation from $C$ succeeds and produces Verilog $V$, and all observable behaviours
of $C$ are safe, then $V$ has behaviour $B$ only if $C$ has behaviour $B$.

\placeformula\startformula
  \startmathalignment[n=1,align={1:right}]
    \NC \forall C, V, B,\quad \text{\tt HLS} (C) = \text{\tt OK} (V) \land \mathit{Safe}(C) \NR
    \NC \implies (V \Downarrow B \implies C \Downarrow B). \NR
  \stopmathalignment
\stopformula

Why is this correctness theorem also the right one for HLS? It could be argued that hardware
inherently runs forever and therefore does not produce a definitive final result. This would mean
that the correctness theorem would probably be unhelpful with proving hardware correctness, as the
behaviour would always be divergent. However, in practice, HLS does not normally produce the
top-level of the design that needs to connect to other components, therefore needing to run
forever. Rather, HLS often produces smaller components that take an input, execute, and then
terminate with an answer. To start the execution of the hardware and to signal to the HLS component
that the inputs are ready, the $\mathit{rst}$ signal is set and unset. Then, once the result is
ready, the $\mathit{fin}$ signal is set and the result value is placed in $\mathit{ret}$. These
signals are also present in the semantics of execution shown in
\in{Figure}[fig:inference_module]. The correctness theorem therefore also uses these signals, and
the proof shows that once the $\mathit{fin}$ flag is set, the value in $\mathit{ret}$ is correct
according to the semantics of Verilog and Clight. Note that the compiler is allowed to fail and not
produce any output; the correctness theorem only applies when the translation succeeds.

How can we prove this theorem? First, note that the theorem is a \quote{backwards simulation} result
(every target behaviour must also be a source behaviour), following the terminology used in the
literature~.  The reverse direction (every source behaviour must also be a target behaviour) is not
demanded because compilers are permitted to resolve any non-determinism present in their source
programs. However, since Clight programs are all deterministic, as are the Verilog programs in the
fragment we consider, we can actually reformulate the correctness theorem above as a forwards
simulation result (following standard practice), which makes it easier to prove. To prove this
forward simulation, it suffices to prove forward simulations between each pair of consecutive
intermediate languages, as these results can be composed to prove the correctness of the whole HLS
tool. The forward simulation from 3AC to HTL is stated in \in{Lemma}[lemma:htl]
(\in{Section}[sec:hls:proof:3ac_htl]), the forward simulation for the RAM insertion is shown in
\in{Lemma}[lemma:htl_ram] (\in{Section}[sec:hls:proof:ram_insertion]), then the forward simulation
between HTL and Verilog is shown in \in{Lemma}[lemma:verilog] (\in{Section}[sec:hls:proof:htl_verilog]),
and finally, the proof that Verilog is deterministic is given in \in{Lemma}[lemma:deterministic]
(\in{Section}[sec:hls:proof:deterministic]).

\subsection[sec:hls:proof:3ac_htl]{Forward Simulation from 3AC to HTL}

As HTL is quite far removed from 3AC, this first translation is the most involved and therefore
requires a larger proof, because the translation from 3AC instructions to Verilog statements needs
to be proven correct in this step. In addition to that, the semantics of HTL are also quite
different to the 3AC semantics. Instead of defining small-step semantics for each construct in
Verilog, the semantics are defined over one clock cycle and mirror the semantics defined for
Verilog.  \in{Lemma}[lemma:htl] shows the result that needs to be proven in this subsection.

\startlemma[lemma:htl]
Writing \type{tr_htl} for the translation from 3AC to HTL, we have:
\startformula
\forall c, h, B \in \text{\tt Safe},\quad \text{\tt tr\_htl} (c) = \text{\tt OK} (h) \land c
\Downarrow B \implies h \Downarrow B.
\stopformula
\stoplemma

\startproof
We prove this lemma by first establishing a specification of the translation
function $\text{\tt tr\_htl}$ that captures its important properties, and then splitting the proof into
two parts: one to show that the translation function does indeed meet its specification, and one to
show that the specification implies the desired simulation result. This strategy is in keeping with
standard practice.
\stopproof

\subsubsection[sec:hls:proof:3ac_htl:specification]{From Implementation to Specification}

The specification for the translation of 3AC instructions into HTL data-path and control logic can
be defined by the following predicate:

\startformula \text{\tt spec\_instr}\ \mathit{fin}\ \mathit{ret}\ \sigma\ \mathit{stk}\ i\
  \mathit{data}\ \mathit{control} \stopformula

Here, the $\mathit{control}$ and $\mathit{data}$ parameters are the statements that the current 3AC
instruction $i$ should translate to. The other parameters are the special registers defined in
\in{Section}[sec:hls:verilog:integrating].  An example of a rule describing the translation of an
arithmetic/logical operation from 3AC is the following:

\startformula
  \text{\sc Iop}\ \frac{\text{\tt tr\_op}\ \mathit{op}\ \vec{a} = \text{\tt OK}\ e}{\text{\tt spec\_instr}\
    \mathit{fin}\ \mathit{ret}\ \sigma\ \mathit{stk}\ (\text{\tt Iop}\ \mathit{op}\ \vec{a}\ d\ n)\
    (d\ \text{\tt <=}\ e)\ (\sigma\ \text{\tt <=}\ n)}
\stopformula

Assuming that the translation of the operator $\mathit{op}$ with operands $\vec{a}$ is successful
and results in expression $e$, the rule describes how the destination register $d$ is updated to $e$
via a non-blocking assignment in the data path, and how the program counter $\sigma$ is updated to
point to the next CFG node $n$ via another non-blocking assignment in the control logic.

In the following lemma, $\text{\tt spec\_htl}$ is the top-level specification predicate, which is built
using $\text{\tt spec\_instr}$ at the level of instructions.

\startlemma[lemma:specification]
  If a 3AC program $c$ is translated correctly to an HTL program $h$, then the specification of the
  translation holds.

\startformula \forall c, h,\quad \text{\tt tr\_htl} (c) = \text{\tt OK}(h) \implies \text{\tt
  spec\_htl}\ c\ h. \stopformula
\stoplemma

\subsubsection[from-specification-to-simulation]{From Specification to Simulation}

To prove that the specification predicate implies the desired forward simulation, we must first
define a relation that matches each 3AC state to an equivalent HTL state. This relation also
captures the assumptions made about the 3AC code that we receive from . These assumptions then have
to be proven to always hold assuming the HTL code was created by the translation algorithm. Some of
the assumptions that need to be made about the 3AC and HTL code for a pair of states to match are:

\startitemize
\item
  The 3AC register file $R$ needs to be \quote{less defined} than the HTL register map $\Gamma_{r}$
  (written $R \le \Gamma_{r}$). This means that all entries should be equal to each other, unless a
  value in $R$ is undefined, in which case any value can match it.
\item
  The RAM values represented by each Verilog array in $\Gamma_{a}$ need to match the 3AC function's
  stack contents, which are part of the memory $M$; that is: $M \le \Gamma_{a}$.
\item
  The state is well formed, which means that the value of the state register matches the current
  value of the program counter; that is: $\mathit{pc} = \Gamma_{r}[\sigma]$.
\stopitemize

We also define the following set $\mathcal{I}$ of invariants that must hold for the current state to
be valid:

\startitemize
\item
  that all pointers in the program use the stack as a base pointer,
\item
  that any loads or stores to locations outside of the bounds of the stack result in undefined
  behaviour (and hence we do not need to handle them),
\item
  that $\mathit{rst}$ and $\mathit{fin}$ are not modified and therefore stay at a constant 0
  throughout execution, and
\item
  that the stack frames match.
\stopitemize

We can now define the simulation diagram for the translation. The 3AC state can be represented by
the tuple $(R,M,\mathit{pc})$, which captures the register file, memory, and program counter. The
HTL state can be represented by the pair $(\Gamma_{r}, \Gamma_{a})$, which captures the states of
all the registers and arrays in the module.  Finally, $\mathcal{I}$ stands for the other invariants
that need to hold for the states to match.

\startlemma[lemma:simulation_diagram]
  Given the 3AC state $(R,M,\mathit{pc})$ and the matching HTL state $(\Gamma_{r}, \Gamma_{a})$,
  assuming one step in the 3AC semantics produces state $(R',M',\mathit{pc}')$, there exist one or
  more steps in the HTL semantics that result in matching states $(\Gamma_{r}', \Gamma_{a}')$. This
  is all under the assumption that the specification $\text{\tt spec\_{htl}}$ holds for the
  translation.
\stoplemma

\startproof
This simulation diagram is proven by induction over the operational semantics of
3AC, which allows us to find one or more steps in the HTL semantics that will produce the same final
matching state.
\stopproof

\subsection[sec:hls:proof:ram_insertion]{Forward Simulation of RAM Insertion}

\startplacefigure[reference={fig:htl_ram_spec},title={Specification for the memory implementation in
    HTL, where $r$ is the RAM, which is then implemented by equivalent Verilog code.}]
  \startformula \startmathalignment[n=1]
  \NC \text{\sc Idle}\ \frac{\Gamma_{\rm r}[\mathit{r.en}] = \Gamma_{\rm r}[\mathit{r.u_{en}}]}{((\Gamma_{\rm r}, \Gamma_{\rm a}), \Delta, r) \downarrow_{\text{ram}} \Delta}\NR
%
  \NC \text{\sc Load}\ \frac{\Gamma_{\rm r}[\mathit{r.en}] \ne \Gamma_{\rm
      r}[\mathit{r.u_{en}}]\qquad \Gamma_{\rm r}[\mathit{r.wr_{en}}] = 0}{((\Gamma_{\rm r},
    \Gamma_{\rm a}), (\Delta_{\rm r}, \Delta_{\rm a}), r) \downarrow_{\text{ram}} \left(\Delta_{\rm
      r}\left[\startmatrix[n=1]
\NC\mathit{r.en} \mapsto \mathit{r.u_{en}},\NR
\NC\mathit{r.d_{out}} \mapsto (\Gamma_{\rm a}[\mathit{r.mem}])[ \mathit{r.addr}]\NR\stopmatrix\right], \Delta_{\rm a}\right) }\NR
%
  \NC \text{\sc Store}\ \frac{\Gamma_{\rm r}[\mathit{r.en}] \ne \Gamma_{\rm r}[\mathit{r.u_{en}}]\qquad
    \Gamma_{\rm r}[\mathit{r.wr_{en}}] = 1}{((\Gamma_{\rm r}, \Gamma_{\rm a}), (\Delta_{\rm r},
    \Delta_{\rm a}), r) \downarrow_{\text{ram}} \left(\startmatrix[n=1]
\NC \Delta_{\rm r}[\mathit{r.en} \mapsto
      \mathit{r.u\_en}], \NR
\NC \Delta_{\rm a}[\mathit{r.mem} \mapsto (\Gamma_{\rm a}[
        \mathit{r.mem}])[\mathit{r.addr} \mapsto \mathit{r.d_{in}}]]\NR\stopmatrix\right) } \NR
  \stopmathalignment \stopformula
\stopplacefigure

HTL can only represent a single state machine, so we must model the RAM abstractly to reason about
the correctness of replacing the direct read and writes to the array by loads and stores to a
RAM. The specification for the RAM is shown in \in{Figure}[fig:htl_ram_spec], which defines how the
RAM $r$ will behave for all the possible combinations of the input signals.

\subsubsection[from-implementation-to-specification]{From Implementation to Specification}

The first step in proving the simulation correct is to build a specification of the translation
algorithm. There are three possibilities for the transformation of an instruction. For each Verilog
statement in the map at location $i$, the statement is either a load, a store, or neither. The load
or store is translated to the equivalent representation using the RAM specification and all other
instructions are left intact. An example of the specification for the translation of the store
instruction is shown below, where $\sigma$ is state register, $r$ is the RAM, $d$ and $c$ are the
input data-path and control logic maps, and $i$ is the current state. ($n$ is the newly inserted
state, which only applies to the translation of loads.)

\startformula
  \text{\sc Store Spec}\ \frac{ d[i] = (r.mem\text{\tt [}e_{1}\text{\tt ]}\ \text{\tt <= } e_{2})
    \quad t = \left(\startmatrix[n=1]
      \NC r.u\_en\ \text{\tt <= } \neg r.u\_en; \NR
      \NC r.wr\_en\ \text{\tt <= } 1; \NR
      \NC r.d\_in\ \text{\tt <= } e_{2}; \NR
      \NC r.addr\ \text{\tt <= } e_{1}\NR\stopmatrix\right)}%
  {\text{\tt spec\_ram\_tr}\ \sigma\ r\ d\ c\ d[i \mapsto t]\ c\ i\ n}\stopformula

A similar specification is created for the load. We then also prove that the implementation of the
translation proves that the specification holds.

\subsubsection[from-specification-to-simulation-1]{From Specification to Simulation}

Another simulation proof is performed to prove that the insertion of the RAM is semantics
preserving. As in \index{simulation diagram}\in{Lemma}[lemma:simulation_diagram], we require some
invariants that always hold at the start and end of the simulation. The invariants needed for the
simulation of the RAM insertion are quite different to the previous ones, so we can define these
invariants $\mathcal{I}_{r}$ to be the following:

\startitemize
\item
  The \index{association map}association map for arrays $\Gamma_{a}$ always needs to have the same
  arrays present, and these arrays should never change in size.
\item
  The RAM should always be disabled at the start and the end of each simulation step. (This is why
  self-disabling RAM is needed.)
\stopitemize

The other \pindex{invariants}invariants and assumptions for defining two matching states in HTL are
quite similar to the simulation performed in \in{Lemma}[lemma:simulation_diagram], such as ensuring
that the states have the same value, and that the values in the registers are less defined. In
particular, the less defined relation matches up all the registers, except for the new registers
introduced by the RAM.

\startlemma[lemma:htl_ram]
  Given an HTL program, the forward-simulation relation should hold after inserting the RAM and
  wiring the load, store, and control signals.

\startformula
  \forall h, h', B \in \text{\tt Safe},\quad \text{\tt tr\_ram\_ins}(h) = h' \land h \Downarrow B
  \implies h' \Downarrow B.
\stopformula
\stoplemma

\subsection[sec:hls:proof:htl_verilog]{Forward Simulation from HTL to Verilog}

The HTL-to-Verilog simulation is conceptually simple, as the only transformation is from the map
representation of the code to the case-statement representation. The proof is more involved, as the
semantics of a map structure is quite different to that of the case-statement to which it is
converted.

\startlemma[lemma:verilog]
  In the following, we write $\text{\tt tr\_verilog}$ for the \pindex{translation+HTL to
    Verilog}translation from HTL to Verilog.  (Note that this translation cannot fail, so we do not
  need the constructor here.)

  \startformula
    \forall h, V, B \in \text{\tt Safe},\quad \text{\tt tr\_verilog} (h) = V \land h \Downarrow B
    \implies V \Downarrow B.
  \stopformula
\stoplemma

\startproof
  The translation from maps to case-statements is done by turning each node of the
  tree into a case-expression containing the same statements. The main difficulty is that a
  random-access structure is being transformed into an inductive structure where a certain number of
  constructors need to be called to get to the correct case.
\stopproof

\subsection[sec:hls:proof:deterministic]{Deterministic Verilog Semantics}

The final lemma we need is that the \pindex{determinism}Verilog semantics is deterministic.  This
result allows us to replace the forwards simulation we have proved with the backwards simulation we
desire.

\startlemma[lemma:deterministic]
If a Verilog program $V$ admits behaviours $B_1$ and $B_2$, then
$B_1$ and $B_2$ must be the same.

  \startformula
    \forall V, B_{1}, B_{2},\quad V \Downarrow B_{1} \land V \Downarrow B_{2} \implies B_{1} =
    B_{2}.
  \stopformula
\stoplemma

\startproof
  The Verilog semantics is deterministic because the order of operation of all the constructs is
  defined, so there is only one way to evaluate the module, and hence only one possible behaviour.
  This was proven for the small-step semantics shown in \in{Figure}[fig:inference_module].
\stopproof

\subsection[coq-mechanisation]{Coq Mechanisation}

\startnotmode[nolmtx]
\startplacetable[reference={tab:proof-statistics},title={Statistics about the numbers of lines of
    code in the proof and implementation of Vericert.}]
  \starttabulate[|l|r|r|r|r|r|]
    \FL
    \NC \NS[1][c] {\bf Coq code} \NS[1][c] {\bf Spec} \NC {\bf Total} \NC \NR
    \ML
    \NC Data structures and libraries \NC 280 \NC --- \NC --- \NC 500 \NC 780 \NC \NR
    \NC Integers and values \NC 98 \NC --- \NC 15 \NC 968 \NC 1081 \NC \NR
    \NC HTL semantics \NC 50 \NC --- \NC 181 \NC 65 \NC 296 \NC \NR
    \NC HTL generation \NC 590 \NC --- \NC 66 \NC 3069 \NC 3725 \NC \NR
    \NC RAM generation \NC 253 \NC --- \NC --- \NC 2793 \NC 3046 \NC \NR
    \NC Verilog semantics \NC 78 \NC --- \NC 431 \NC 235 \NC 744 \NC \NR
    \NC Verilog generation \NC 104 \NC --- \NC --- \NC 486 \NC 590 \NC \NR
    \NC Top-level driver, pretty printers \NC 318 \NC 775 \NC --- \NC 189 \NC 1282 \NC \NR
    \LL
    \NC {\bf Total} \NC 1721 \NC 775 \NC 693 \NC 8355 \NC 11544 \NC \NR
    \BL
  \stoptabulate
\stopplacetable
\stopnotmode

\startmode[nolmtx]
\startplacetable[reference={tab:proof-statistics},title={Statistics about the numbers of lines of
    code in the proof and implementation of Vericert.}]
  \starttabulate[|l|r|r|r|r|r|]
    \HL
    \NC \NC {\bf Coq code} \NC \NC {\bf Spec} \NC \NC {\bf Total} \NC \NR
    \HL
    \NC Data structures and libraries \NC 280 \NC --- \NC --- \NC 500 \NC 780 \NC \NR
    \NC Integers and values \NC 98 \NC --- \NC 15 \NC 968 \NC 1081 \NC \NR
    \NC HTL semantics \NC 50 \NC --- \NC 181 \NC 65 \NC 296 \NC \NR
    \NC HTL generation \NC 590 \NC --- \NC 66 \NC 3069 \NC 3725 \NC \NR
    \NC RAM generation \NC 253 \NC --- \NC --- \NC 2793 \NC 3046 \NC \NR
    \NC Verilog semantics \NC 78 \NC --- \NC 431 \NC 235 \NC 744 \NC \NR
    \NC Verilog generation \NC 104 \NC --- \NC --- \NC 486 \NC 590 \NC \NR
    \NC Top-level driver, pretty printers \NC 318 \NC 775 \NC --- \NC 189 \NC 1282 \NC \NR
    \HL
    \NC {\bf Total} \NC 1721 \NC 775 \NC 693 \NC 8355 \NC 11544 \NC \NR
    \HL
  \stoptabulate
\stopplacetable
\stopmode

The lines of code for the implementation and proof of can be found in
\in{Table}[tab:proof-statistics]. Overall, it took about 1.5 person-years to build -- about three
person-months on implementation and 15 person-months on proofs. The largest proof is the correctness
proof for the HTL generation, which required equivalence proofs between all integer operations
supported by and those supported in hardware. From the 3069 lines of proof code in the HTL
generation, 1189 are for the correctness proof of just the load and store instructions. These were
tedious to prove correct because of the substantial difference between the memory models used, and
the need to prove properties such as stores outside of the allocated memory being undefined, so that
a finite array could be used. In addition to that, since pointers in HTL and Verilog are represented
as integers, instead of as a separate \quote{pointer} type like in the semantics, it was painful to
reason about them. Many new theorems had to be proven about them in to prove the conversion from
pointer to integer. Moreover, the second-largest proof of the correct RAM generation includes many
proofs about the extensional equality of array operations, such as merging arrays with different
assignments. As the negative edge implies that two merges take place every clock cycle, the proofs
about the equality of the contents in memory and in the merged arrays become more tedious too.

Looking at the trusted computing base of Vericert, the Verilog semantics is 431 lines of code. This
and the Clight semantics from are the only parts of the compiler that need to be trusted. The
Verilog semantics specification is therefore much smaller compared to the 1721 lines of the
implementation that are written in Coq, which are the verified parts of the HLS tool, even when the
Clight semantics are added. In addition to that, understanding the semantics specification is
simpler than trying to understand the translation algorithm. We conclude that the trusted base has
been successfully reduced.

\stopcomponent