Add macros for vericert and compcert

1 files changed, 40 insertions, 38 deletions

diff --git a/algorithm.tex b/algorithm.tex
index 425e1b0..684975c 100644
--- a/algorithm.tex
+++ b/algorithm.tex
@@ -1,17 +1,40 @@
-\section{Adding an HLS back end to CompCert}
+\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.
+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.
+
+\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 to Compcert, branching off at the three address code (3AC), at which point the three address code is transformed into a state machine.  Finally, it is transformed to a hardware description of the state machine in Verilog.}%
+  \label{fig:rtlbranch}
+\end{figure}
+
+The main work flow of \vericert{} is shown in Figure~\ref{fig:rtlbranch}, which shows the parts of the translation that are performed in \compcert{}, and which have been added with \vericert{}.
 
 % - 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}
@@ -22,7 +45,7 @@ This section covers the main architecture of the HLS tool, and the way in which
     \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}
+  \caption{Accumulator example using \compcert{} to translate from C to three address code (3AC).}\label{fig:accumulator_c_rtl}
 \end{figure}
 
 \begin{figure}
@@ -35,42 +58,21 @@ This section covers the main architecture of the HLS tool, and the way in which
     \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}
+  \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.  
+Taking the 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.
+
+\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*}
 
 %   + 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