Add verilog section

3 files changed, 32 insertions, 32 deletions

diff --git a/Makefile b/Makefile
new file mode 100644
index 0000000..c2174fa
--- /dev/null
+++ b/Makefile
@@ -0,0 +1,7 @@
+all:
+	latexmk -lualatex -pdf -shell-escape main.tex
+
+.PHONY: all clean
+
+clean:
+	git clean -dfx
diff --git a/evaluation.tex b/evaluation.tex
index 17e2e36..45fcc27 100644
--- a/evaluation.tex
+++ b/evaluation.tex
@@ -2,31 +2,31 @@
 
 \NR{Do we want to collect C-to-Verilog compile time?}
 \begin{table}
-\begin{tabular}{|l|c|c|c|c|c|c|}
-\hline
-Benchmark & Cycles & Frequency & LUTs & Registers & BRAMs\\
-\hline\hline
-adpcm & 30241 &90.05 & 7719 & 12034 & 7\\\hline
-aes & 8489 & 87.83 & 24413 & 23796 & 19 \\\hline
-gsm & 7190 & 119.25 & 6638 & 9201 & 3 \\\hline
-mips & 7754 & 98.95 & 5049 & 4185 & 0 \\\hline
-\hline
-\end{tabular}
-\caption{CHstone programs synthesised in LegUp 5.1}
+  \begin{tabular}{lcccccc}
+    \toprule
+    Benchmark & Cycles & Frequency & LUTs & Registers & BRAMs\\
+    \midrule
+    adpcm & 30241 &90.05 & 7719 & 12034 & 7\\
+    aes & 8489 & 87.83 & 24413 & 23796 & 19 \\
+    gsm & 7190 & 119.25 & 6638 & 9201 & 3 \\
+    mips & 7754 & 98.95 & 5049 & 4185 & 0 \\
+    \bottomrule
+  \end{tabular}
+  \caption{CHstone programs synthesised in LegUp 5.1}
 \end{table}
 
 \begin{table}
-\begin{tabular}{|l|c|c|c|c|c|c|}
-\hline
-Benchmark & Cycles & Frequency & LUTs & Registers & BRAMs\\
-\hline\hline
-adpcm & XXX & XXX & XXX & XXX & XXX  \\\hline
-aes & 41958 & & & & \\\hline
-gsm & 21994 & & & & \\\hline
-mips & 18482 & 78.43 & 10617 & 7690 & 0 \\\hline
-\hline
-\end{tabular}
-\caption{CHstone programs synthesised in CoqUp}
+  \begin{tabular}{lcccccc}
+    \toprule
+    Benchmark & Cycles & Frequency & LUTs & Registers & BRAMs\\
+    \midrule
+    adpcm & XXX & XXX & XXX & XXX & XXX  \\
+    aes & 41958 & & & & \\
+    gsm & 21994 & & & & \\
+    mips & 18482 & 78.43 & 10617 & 7690 & 0 \\
+    \bottomrule
+  \end{tabular}
+  \caption{CHstone programs synthesised in CoqUp}
 \end{table}
 
 The difference in cycle counts shows the degree of  parallelism that LegUp's scheduling and memory system can offer. However, their Verilog generation is not guaranteed to be correct. Although the runtime LegUp outputs are tested to be correct for these programs, this does not provide any confidence on the correctness of Verilog generation of any other programs. Our Coq proof mechanisation guarantees that generated Verilog is correct for any input program that uses the subset of CompCert instructions that we have proven to be correct.
diff --git a/verilog.tex b/verilog.tex
index 5024121..17ccca4 100644
--- a/verilog.tex
+++ b/verilog.tex
@@ -26,18 +26,11 @@ The main addition to the Verilog syntax is the explicit declaration of inputs an
 
 \subsection{Semantics}
 
-In general, Verilog is used to model hardware which is intrinsically parallel.  At the top-level, always block, describing logic which is run everytime some even occurs:
+Existing operational semantics~\cite{loow19_verif_compil_verif_proces} were adapted for the semantics of the language that CoqUp eventually targets.  These semantics are small-step operational semantics at the clock cycle level, as hardware typically does not terminate in any way, however, within each clock cycle the semantics are constructed in a big-step style semantics.  This style of semantics matches the small-step operational semantics of CompCert's register transfer language (RTL) quite well.
 
-\begin{minted}{systemverilog}
-always @(posedge clk)
-\end{minted}
+At the top-level, always blocks describe logic which is run every time some event occurs.  The only event that is supported by these semantics is detecting the positive edge of the clock, so that we can implement synchronous logic.  As soon as an event occurs, the hardware will be executed, meaning if there are multiple always blocks that get triggered by the event, these will run in parallel.  However, as the semantics should be deterministic, we impose an order on the always blocks and execute them sequentially.  However, to preserve the fact that the statements inside of the always block are executed in parallel, nonblocking assignments to variables need to be kept in a different association map compared to blocking assignments to variables.  This preserves the behaviour that blocking assignments change the value of the variable inside of the clock cycle, whereas the nonblocking assignments only take place at the end of the clock cycle, and in parallel.  We can denote these two association maps as $s = (\Gamma, \Delta)$, where $\Gamma$ is the current value of the registers, and $\Delta$ is the value of that variable when the clock cycle ends.
 
-However, adjustments to these semantics had to be made to make it compatible with the CompCert small step semantics.  In addition to that, memory is not directly modelled in their semantics of Verilog, as well as handling of inputs and declarations in modules.
-
-\begin{equation}
-  \label{eq:10}
-  s = (\Gamma, \Delta)
-\end{equation}
+We can then define how one step in the semantics looks like.
 
 Definition of stmntrun.