Add examples

5 files changed, 64 insertions, 6 deletions

diff --git a/algorithm.tex b/algorithm.tex
index 849ea05..7d119da 100644
--- a/algorithm.tex
+++ b/algorithm.tex
@@ -33,18 +33,64 @@ Existing HLS compilers usually use LLVM IR as an intermediate representation whe
 
 %%TODO: Maybe add why LTL and the other smaller languages are not that well suited
 
-To describe the translation, we can start with a simple example of how to translate a simple matrix multiplication example.
+\begin{figure}
+  \centering
+  \begin{minipage}{0.5\linewidth}
+\begin{minted}{c}
+int main() {
+    int x[5] = {1, 2, 3, 4, 5};
+    int sum = 0;
+    for (int i = 0; i < 5; i++)
+        sum += x[i];
+    return sum;
+}
+\end{minted}
+  \end{minipage}
+  \caption{Matrix multiply example C code.}\label{fig:matrix_mult_c}
+\end{figure}
+
+To describe the translation, we start with an example of how to translate a simple accumulator example, which is shown in figure~\ref{fig:matrix_mult_c}.
 
 \subsection{CompCert RTL}
 
-All CompCert intermediate language follow the similar structure below: \JW{should `(id * data)' be `(id * data) list'?}
+All CompCert intermediate language follow the similar structure below:
 
 \begin{align*}
-  \mathit{program} \quad ::= \{ &\mathbf{variables} : (\mathit{id} * \mathit{data}), \\
-                 &\mathbf{functions} : (\mathit{id} * \mathit{function\_def}),\\
+  \mathit{program} \quad ::= \{ &\mathbf{variables} : (\mathit{id} * \mathit{data}) \text{ list}, \\
+                 &\mathbf{functions} : (\mathit{id} * \mathit{function\_def}) \text{ list},\\
                  &\mathbf{main} : \mathit{id} \}
 \end{align*}
 
+\begin{figure}
+  \centering
+  \begin{minipage}{0.5\linewidth}
+\begin{minted}{c}
+main() {
+   19:	x10 = 1
+   18:	int32[stack(0)] = x10
+   17:	x9 = 2
+   16:	int32[stack(4)] = x9
+   15:	x8 = 3
+   14:	int32[stack(8)] = x8
+   13:	x7 = 4
+   12:	int32[stack(12)] = x7
+   11:	x6 = 5
+   10:	int32[stack(16)] = x6
+    9:	x2 = 0
+    8:	x1 = 0
+    7:	x5 = stack(0) (int)
+    6:	x4 = int32[x5 + x1 * 4 + 0]
+    5:	x2 = x2 + x4 + 0 (int)
+    4:	x1 = x1 + 1 (int)
+    3:	if (x1 <s 5) goto 7 else goto 2
+    2:	x3 = x2
+    1:	return x3
+}
+\end{minted}
+  \end{minipage}
+  \caption{Matrix multiply example C code.}\label{fig:matrix_mult_rtl}
+\end{figure}
+
 \noindent where function definitions can either be internal or external.  External functions are functions that are not defined in the current translation unit, and are therefore not part of the current translation.  The difference in between the CompCert intermediate languages is therefore how the internal function is defined, as that defines the structure of the language itself.
 
 %% Describe RTL
diff --git a/introduction.tex b/introduction.tex
index 1476d33..c72f788 100644
--- a/introduction.tex
+++ b/introduction.tex
@@ -26,7 +26,7 @@ CompCert~\cite{leroy06_formal_certif_compil_back_end} is a C compiler that has b
 
 %% Contributions of paper
 
-In this paper we describe a fully verified high-level synthesis \JW{HLS} tool called CoqUp, which adds a Verilog back end to CompCert and proves that the behaviour of the C code is preserved with respect to an existing Verilog semantics.  The main contributions of the paper are the following:
+In this paper we describe a fully verified HLS tool called CoqUp, which adds a Verilog back end to CompCert and proves that the behaviour of the C code is preserved with respect to an existing Verilog semantics.  The main contributions of the paper are the following:
 
 \begin{itemize}
   \item First mechanised and formally verified HLS flow from C to Verilog.
diff --git a/main.tex b/main.tex
index a0c8c73..9643bd3 100644
--- a/main.tex
+++ b/main.tex
@@ -49,6 +49,8 @@
 \usepackage{tikz}
 \usepackage{minted}
 
+\setminted{fontsize=\small, baselinestretch=1, frame=lines}
+
 \newif\ifCOMMENTS
 \COMMENTStrue
 \newcommand{\Comment}[3]{\ifCOMMENTS\textcolor{#1}{{\bf [\![#2:} #3{\bf ]\!]}}\fi}
diff --git a/verilog.tex b/verilog.tex
index e68352d..709781f 100644
--- a/verilog.tex
+++ b/verilog.tex
@@ -66,7 +66,7 @@ The two main evaluation functions are then \textit{erun}, which takes in the cur
 %  \inferrule[Nonblocking Array]{\yhkeyword{name}\ \textit{lhs} = \yhkeyword{OK}\ n \\ \textit{erun}\  \Gamma\ \textit{rhs}\ v_{\textit{rhs}}}{\textit{srun}\  (\Gamma_{r}, \Gamma_{a}, \Delta_{r}, \Delta_{a})\ (\textit{lhs} \Leftarrow \textit{rhs})\ (\Gamma_{r}, \Gamma_{a}, \Delta_{r} // \{n \rightarrow v_{\textit{rhs}}\}, \Delta_{a})}
 \end{gather*}
 
-\YH{TODO: Add rules for blocking and nonblocking assignment to arrays.} \JW{The `Skip' rule has an erroneous $=$.} \JW{You could use a bit of colour here, e.g. the keywords like `if' could be coloured for readability.} \JW{The difference between `s' and `st' is hard to remember, since both are prefixes of both `state' and `statement'! It's quite common to use `$\sigma$' for states, so you might consider `$s$' and `$\sigma$' for statements and states?} \JW{The function update syntax is not familiar to me, but perhaps it is what is used in Coq? More typical would be `$\Delta[n\mapsto v]$'.}
+\YH{TODO: Add rules for blocking and nonblocking assignment to arrays.}
 
 Taking the \textsc{CondTrue} rule as an example, this rule will only apply if the Boolean result of running the expression results in a \texttt{true} value.  It then also states that the statement in the true branch of the conditional statement \textit{stt} runs from state $\sigma_{0}$ to state $\sigma_{1}$.  If both of these conditions hold, we then get that the conditional statement will also run from state $\sigma_{0}$ to state $\sigma_{1}$.  The \textsc{Blocking} and \textsc{Nonblocking} rules are a bit more interesting, as these modify the blocking and nonblocking association maps respectively.
 
@@ -89,6 +89,7 @@ We then define the semantics of running the module for one clock cycle in the fo
 \end{gather*}
 
 \YH{TODO:\@ Need to fix the last rule, as it is actually only used for a case that shouldn't ever be hit.}
+\YH{TODO:\@ Explain // notation}
 
 The \textsc{Module} rule is the main rule for the execution of one clock cycle of the module.  Given that the value of the $s_{t}$ register is the value of the program counter at the current instruction and that the value of the $s_{t}$ register in the resulting association map is equal to the next program counter value, we can then say that if all the module items in the body go from one state to another, that the whole module will step from that state to the other.
 
diff --git a/verilog_notes.tex b/verilog_notes.tex
index b28b04f..60e21bb 100644
--- a/verilog_notes.tex
+++ b/verilog_notes.tex
@@ -1,3 +1,12 @@
+\ifCOMMENTS
+\subsection{\textcolor{red!75!black}{Verilog notes}}
 
+\JW{The `Skip' rule has an erroneous $=$.}\YH{Done}
 
+\JW{You could use a bit of colour here, e.g. the keywords like `if' could be coloured for readability.}\YH{Done}
 
+\JW{The difference between `s' and `st' is hard to remember, since both are prefixes of both `state' and `statement'! It's quite common to use `$\sigma$' for states, so you might consider `$s$' and `$\sigma$' for statements and states?}\YH{That is true, changed it to use $\sigma$.}
+
+\JW{The function update syntax is not familiar to me, but perhaps it is what is used in Coq? More typical would be `$\Delta[n\mapsto v]$'.}\YH{I was actually thinking of using a custom merge syntax using //, but that notation is better.  I think I might still use // for merge, just need to explain it somewhere.}
+
+\fi