\section{Adding an HLS back end to CompCert}

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

% - Explain main differences between translating C to software and to hardware.

%   + This can be done by going through the simple example.

\begin{figure*}
  \centering
  \includegraphics[scale=0.3,trim={10cm 10cm 7cm 7cm},clip=true]{data/accumulator_fsmd2.pdf}
  \caption{Accumulator hardware diagram.}\label{fig:accumulator_diagram}
\end{figure*}

\begin{figure}
  \centering
  \begin{subfigure}[b]{0.5\linewidth}
    \inputminted{c}{data/accumulator.c}
    \caption{Accumulator C code.}\label{fig:accumulator_c}
  \end{subfigure}%
  \begin{subfigure}[b]{0.5\linewidth}
    \inputminted[fontsize=\footnotesize]{c}{data/accumulator.rtl}
    \caption{Accumulator RTL code.}\label{fig:accumulator_rtl}
  \end{subfigure}
  \caption{Accumulator example using CompCert to translate from C to three address code (3AC).}\label{fig:accumulator_c_rtl}
\end{figure}

\begin{figure}
  \centering
  \begin{subfigure}[b]{0.5\linewidth}
    \inputminted[fontsize=\tiny]{systemverilog}{data/accumulator1.v}
    \caption{Accumulator HTL code.}\label{fig:accumulator_v_1}
  \end{subfigure}%
  \begin{subfigure}[b]{0.5\linewidth}
    \inputminted[fontsize=\tiny]{systemverilog}{data/accumulator2.v}
    \caption{Accumulator Verilog code.}\label{fig:accumulator_v_2}
  \end{subfigure}
  \caption{Accumulator example using CompCert to translate from HTL to Verilog.\YH{I feel like these examples take up too much space, but don't really know of a different way to show off a complete example without the long code.} \JW{Ok, what about drawing the FSMD in some sort of pictorial way? I think you tried drawing it as a schematic previously, but that was too big and clumsy. What about drawing the FSMD as a state machine, with sixteen states and labelled edges between them? Or might that be too abstract?}}\label{fig:accumulator_v}
\end{figure}

Taking a simple accumulator program shown in Figure~\ref{fig:accumulator_c}, we can describe the main translation that is performed in Vericert to go from the behaviour description into a hardware design.  

%   + TODO Explain the main mapping in a short simple way

% - Explain why we chose 3AC (RTL) as the branching off point.

\begin{figure}
  \centering
  \resizebox{0.47\textwidth}{!}{
  \begin{tikzpicture}
    [language/.style={fill=white,rounded corners=2pt}]
    \fill[compcert,rounded corners=3pt] (-1,-1) rectangle (9,1.5);
    \fill[formalhls,rounded corners=3pt] (-1,-1.5) rectangle (9,-2.5);
    \node[language] at (0,0) (clight) {Clight};
    \node[language] at (2,0) (cminor) {C\#minor};
    \node[language] at (4,0) (rtl) {3AC};
    \node[language] at (6,0) (ltl) {LTL};
    \node[language] at (8,0) (ppc) {PPC};
    \node[language] at (4,-2) (dfgstmd) {HTL};
    \node[language] at (7,-2) (verilog) {Verilog};
    \node at (0,1) {CompCert};
    \node at (0,-2) {Vericert};
    \draw[->] (clight) -- (cminor);
    \draw[->,dashed] (cminor) -- (rtl);
    \draw[->] (rtl) -- (ltl);
    \draw[->,dashed] (ltl) -- (ppc);
    \draw[->] (rtl) -- (dfgstmd);
    \draw[->] (dfgstmd) -- (verilog);
  \end{tikzpicture}}
  \caption{Verilog backend branching off at the 3AC stage in CompCert.}%
  \label{fig:rtlbranch}
\end{figure}

%   + TODO Clarify connection between CFG and FSMD

%   + TODO Explain how memory is mapped

%%% Local Variables:
%%% mode: latex
%%% TeX-master: "main"
%%% TeX-command-extra-options: "-shell-escape"
%%% End: