Add changes

6 files changed, 53 insertions, 61 deletions

diff --git a/algorithm.tex b/algorithm.tex
index 5e7868d..908f488 100644
--- a/algorithm.tex
+++ b/algorithm.tex
@@ -4,6 +4,7 @@
 
 \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);
@@ -23,8 +24,9 @@
     \draw[->,dashed] (ltl) -- (ppc);
     \draw[->] (rtl) -- (dfgstmd);
     \draw[->] (dfgstmd) -- (verilog);
-  \end{tikzpicture}
-  \caption{Verilog backend branching off at the RTL stage.}\label{fig:rtlbranch}
+  \end{tikzpicture}}
+  \caption{Verilog backend branching off at the RTL stage.}%
+  \label{fig:rtlbranch}
 \end{figure}
 
 This section covers the main architecture of the HLS tool, and the way in which the backend was added to CompCert.
@@ -61,11 +63,11 @@ Existing HLS compilers usually use LLVM IR as an intermediate representation whe
   \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.}}\label{fig:accumulator_htl_v}
 \end{figure}
 
-\begin{figure}
-  \centering
-  \includegraphics[width=0.9\textwidth]{data/accumulator_fsmd}
-  \caption{Accumulator example translated to a finite state-machine with datapath (FSMD).}\label{fig:accumulator_fsmd}
-\end{figure}
+%\begin{figure}
+%  \centering
+%  \includegraphics[width=0.47\textwidth]{data/accumulator_fsmd}
+%  \caption{Accumulator example translated to a finite state-machine with datapath (FSMD).}\label{fig:accumulator_fsmd}
+%\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:accumulator_c}.  Using this example, the different stages of the translation can be explained, together with the way they were proven.
 
diff --git a/introduction.tex b/introduction.tex
index 3d1cef0..6549fd1 100644
--- a/introduction.tex
+++ b/introduction.tex
@@ -21,7 +21,7 @@ However, the fact that the behaviour is preserved after HLS cannot be guaranteed
 %%\NR{Focus on more high-level of "why this work is interesting"? Two key points we want to get across to the reader is that in existing works: validation is neccessary every time a new program is compiled and the verifying algorithm is not verified.}
 %%\NR{Also define words like validation, verifying algorithm (can you use the word ``verifier'',mechanisation)}
 %%\NR{Having said that, keep the text for related work section.}\YH{Added into related works.}
-To mitigate the problems about the unreliability of synthesis tool, it is often required to check the generated hardware for functional correctness.  This is commonly done by simulating the design with a large test-bench, however, the guarantees are only as good as the test-bench, meaning if all the inputs were not covered, is a risk that bugs remain in the untested code.  To ensure that the hardware does indeed behave in the same way as the C code, it may therefore be necessary to prove that they are equivalent.  Translation validation~\cite{pnueli98_trans} is the main method which is used to prove that the HLS translation was successful, and has been successfully applied to many HLS optimisations~\cite{kim04_autom_fsmd,karfa06_formal_verif_method_sched_high_synth,chouksey20_verif_sched_condit_behav_high_level_synth,banerjee14_verif_code_motion_techn_using_value_propag,chouksey19_trans_valid_code_motion_trans_invol_loops}.  However, the main problem is that the validator itself has often not been mechanically proven correct, meaning that the implementation is quite separate from the proof.  In addition to that, with large designs it may not be feasible to perform translation validation, as the state space would grow exponentially. \JW{Does this link back to Mentor's Catapult-C, which you mentioned earlier? Does Catapult-C attempt to do translation validation as part of its HLS process? And if so, can you make the point that this effort is largely ineffective because once the design is a reasonable size, the translation validation usually fails anyway?}\YH{TODO: Currently I only have a whitepaper which goes over the translation validation in a very high level, but they do actually mention some flakiness and state that the user would have to manually change the code to fix that.  So I think I can actually make that point.  I just realised they have a pretty funny diagram of verification $\rightarrow$ differences $\rightarrow$ adjustments $\rightarrow$ ... until it is finally verified.} A mechanically verified HLS tool would remove the need to perform simulation after the synthesis process if one has proven desirable properties about the C code.  In addition to that, it would allow for the implementation of translation validated optimisation passes which are also proven correct mechanically, thereby greatly improving the reliability of these passes.
+To mitigate the problems about the unreliability of synthesis tool, it is often required to check the generated hardware for functional correctness.  This is commonly done by simulating the design with a large test-bench, however, the guarantees are only as good as the test-bench, meaning if all the inputs were not covered, is a risk that bugs remain in the untested code.  To ensure that the hardware does indeed behave in the same way as the C code, it may therefore be necessary to prove that they are equivalent.  Translation validation~\cite{pnueli98_trans} is the main method which is used to prove that the HLS translation was successful, and has been successfully applied to many HLS optimisations~\cite{kim04_autom_fsmd,karfa06_formal_verif_method_sched_high_synth,chouksey20_verif_sched_condit_behav_high_level_synth,banerjee14_verif_code_motion_techn_using_value_propag,chouksey19_trans_valid_code_motion_trans_invol_loops}.  However, the main problem is that the validator itself has often not been mechanically proven correct, meaning that the implementation is quite separate from the proof.  In addition to that, with large designs it may not be feasible to perform translation validation, as the state space would grow exponentially. \JW{Does this link back to Mentor's Catapult-C, which you mentioned earlier? Does Catapult-C attempt to do translation validation as part of its HLS process? And if so, can you make the point that this effort is largely ineffective because once the design is a reasonable size, the translation validation usually fails anyway?}\YH{TODO: Currently I only have a whitepaper which goes over the translation validation in a very high level, but they do actually mention some flakiness and state that the user would have to manually change the code to fix that.  So I think I can actually make that point.  I just realised they have a pretty funny diagram of verification $\rightarrow$ differences $\rightarrow$ adjustments $\rightarrow$ ... until it is finally verified.} A mechanically verified HLS tool would remove the need to perform simulation after the synthesis process if one has proven desirable properties about the C code.  In addition to that, it would allow for the implementation of optimisation passes which are also proven correct mechanically by translation validation, thereby greatly improving the reliability of these passes.
 
 CompCert~\cite{leroy06_formal_certif_compil_back_end} is a C compiler that has been written and formally verified in the Coq theorem prover~\cite{bertot04_inter_theor_provin_progr_devel}.  First of all, most of the compiler passes in CompCert have been proven correct, meaning that once the compiler is built, the proofs can be erased as the algorithm has been shown to be correct independent of the input.  However, some optimisation passes such as software pipelining require translation validation~\cite{tristan08_formal_verif_trans_valid}, in which case the correctness of the compiler pass needs to be checked at runtime.  However, even in this case the verifier itself is proven to only verify code correct that does indeed behave in the same way.
 
diff --git a/main.tex b/main.tex
index 2c0cb01..5dd538f 100644
--- a/main.tex
+++ b/main.tex
@@ -1,5 +1,6 @@
 %% For double-blind review submission, w/o CCS and ACM Reference (max submission space)
-\documentclass[pagebackref=true,acmsmall,review]{acmart}\settopmatter{printfolios=true,printccs=false,printacmref=false}
+\documentclass[sigplan,10pt,pagebackref=true,review,anonymous]{acmart}\settopmatter{printfolios=true,printccs=false,printacmref=false}
+%\documentclass[pagebackref=true,acmsmall,review]{acmart}\settopmatter{printfolios=true,printccs=false,printacmref=false}
 %% For double-blind review submission, w/ CCS and ACM Reference
 %\documentclass[acmsmall,review,anonymous]{acmart}\settopmatter{printfolios=true}
 %% For single-blind review submission, w/o CCS and ACM Reference (max submission space)
@@ -35,13 +36,6 @@
 %% Citation style
 \citestyle{acmauthoryear}
 
-\renewcommand*{\backrefalt}[4]{%
-    \ifcase #1%
-          \or [Page~#2.]%
-          \else [Pages~#2.]%
-    \fi%
-    }
-
 \usepackage{amsmath}
 \usepackage{booktabs}
 \usepackage{mathpartir}
@@ -67,7 +61,7 @@
 \definecolor{constantcolour}{HTML}{0000bb}
 
 \newcommand\yhkeywordsp[1]{\;\;\texttt{\textcolor{keywordcolour}{#1}}}
-\newcommand\yhkeyword[1]{\texttt{\textcolor{keywordcolour}{#1}}}4
+\newcommand\yhkeyword[1]{\texttt{\textcolor{keywordcolour}{#1}}}
 \newcommand\yhfunctionsp[1]{\;\;\texttt{\textcolor{functioncolour}{#1}}}
 \newcommand\yhfunction[1]{\texttt{\textcolor{functioncolour}{#1}}}
 \newcommand\yhconstant[1]{\texttt{\textcolor{constantcolour}{#1}}}
@@ -101,13 +95,7 @@
 \author{Yann Herklotz}
 \orcid{0000-0002-2329-1029}
 \affiliation{
-%  \position{PhD Student}
-%  \department{EEE}
   \institution{Imperial College London}
-%  \streetaddress{South Kensington Campus}
-%  \city{London}
-%  \state{}
-%  \postcode{SW7 2AZ}
   \country{UK}
 }
 \email{yann.herklotz15@imperial.ac.uk}
@@ -115,13 +103,7 @@
 \author{James Pollard}
 \orcid{0000-0003-1404-1527}
 \affiliation{
-%  \position{}
-%  \department{EEE}
   \institution{Imperial College London}
-%  \streetaddress{South Kensington Campus}
-%  \city{London}
-%  \state{}
-%  \postcode{SW7 2AZ}
   \country{UK}
 }
 \email{james.pollard16@imperial.ac.uk}
@@ -129,13 +111,7 @@
 \author{Nadesh Ramanathan}
 \orcid{0000-0000-0000-0000}
 \affiliation{
-%  \position{}
-%  \department{EEE}
   \institution{Imperial College London}
-%  \streetaddress{South Kensington Campus}
-%  \city{London}
-%  \state{}
-%  \postcode{SW7 2AZ}
   \country{UK}
 }
 \email{n.ramanathan14@imperial.ac.uk}
@@ -143,30 +119,17 @@
 \author{John Wickerson}
 \orcid{0000-0000-0000-0000}
 \affiliation{
-%  \position{}
-%  \department{EEE}
   \institution{Imperial College London}
-%  \streetaddress{South Kensington Campus}
-%  \city{London}
-%  \state{}
-%  \postcode{SW7 2AZ}
   \country{UK}
 }
 \email{j.wickerson@imperial.ac.uk}
 
-% High-level synthesis (HLS) refers to the automatic compilation of software into hardware. In a world increasingly reliant on application-specific hardware accelerators, HLS allows developers to enjoy the high-level abstractions and mature tooling associated with software development, while still benefitting from the performance and energy-efficiency of custom hardware. However, its adoption in safety-critical contexts is limited because no existing HLS tool guarantees that the output hardware is behaviourally equivalent to the input software. Indeed, there is empirical evidence that existing HLS tools, being complex pieces of software that implement delicate algorithms, are quite buggy. This undermines any assurance provided by software-level analysis.
-
-% Aiming to rectify that shortcoming, we present the first HLS tool that is mechanically verified to be semantics-preserving. Our tool, called CoqUp, is realised as an extension to the CompCert verified C compiler. It consists of a new hardware-oriented intermediate language and a new Verilog-producing back-end, all proven correct in Coq. CoqUp supports the full C language as input, except recursion and non-integer datatypes. An evaluation on the standard CHStone benchmark indicates that CoqUp generates hardware that is slower than, but has a comparable area to, that generated by two existing (unverified) HLS tools.
-
-
-%% Abstract
 \begin{abstract}
   High-level synthesis (HLS) refers to automatically compiling software into hardware.  In a world increasingly reliant on application-specific hardware accelerators, HLS provides a higher-level of abstraction for hardware designers, while also benefitting from the rich software ecosystem to verify the functionality of their designs.  However, adoption of HLS in safety-critical applications is still limited, because current tools cannot verify that the hardware implements the same behaviour as the software it was generated from, eliminating the benefits that software verification may provide.  There is even evidence that HLS tools tend to be quite unreliable instead, either generating wrong hardware or sometimes not generating any hardware at all.
 
   We present the first mechanically verified HLS tool that preserves the behaviour of the software according to our semantics.  Our tool, called VeriCert, extends the CompCert verified C compiler and consists of a new hardware specific intermediate language and a Verilog back end, which has been proven correct in Coq.  VeriCert supports all C constructs except for function pointers, recursive function calls, non-integer types and global variables.  It has been evaluated on all suitable PolyBench benchmarks, which indicates that it generates hardware with area and cycle count around a magnitude larger than an existing, unverified HLS tool.
 \end{abstract}
 
-
 %% 2012 ACM Computing Classification System (CSS) concepts
 %% Generate at 'http://dl.acm.org/ccs/ccs.cfm'.
 \begin{CCSXML}
diff --git a/references.bib b/references.bib
index ec8304d..ee57c3b 100644
--- a/references.bib
+++ b/references.bib
@@ -396,3 +396,24 @@
   year      = {2018}
 }
 
+@book{micheli94_synth_optim_digit_circuit,
+  author          = {De Micheli, Giovanni},
+  title           = {Synthesis and Optimization of Digital Circuits},
+  year            = 1994,
+  publisher       = {McGraw-Hill Higher Education},
+  abstract        = {From the Publisher:Synthesis and Optimization of Digital Circuits offers a
+                  modern, up-to-date look at computer-aided design (CAD) of very large-scale
+                  integration (VLSI) circuits. In particular, this book covers techniques for
+                  synthesis and optimization of digital circuits at the architectural and logic
+                  levels, i.e., the generation of performance-and/or area-optimal circuits
+                  representations from models in hardware description languages. The book provides a
+                  thorough explanation of synthesis and optimization algorithms accompanied by a
+                  sound mathematical formulation and a unified notation. The text covers the
+                  following topics: modern hardware description languages (e.g., VHDL, Verilog);
+                  architectural-level synthesis of data flow and control units, including algorithms
+                  for scheduling and resource binding; combinational logic optimization algorithms
+                  for two-level and multiple-level circuits; sequential logic optimization methods;
+                  and library binding techniques, including those applicable to FPGAs.},
+  edition         = {1st},
+  isbn            = 0070163332,
+}
diff --git a/verilog.tex b/verilog.tex
index f11b6a2..6274dcb 100644
--- a/verilog.tex
+++ b/verilog.tex
@@ -2,7 +2,7 @@
 
 Verilog is a hardware description language commonly used to design hardware.  A Verilog design can then be synthesised into more basic logic which describes how different gates connect to each other, called a netlist.  This representation can then be put onto either a field-programmable gate array (FPGA) or turned into an application-specific integrated circuit (ASIC) to implement the design that was described in Verilog.  The Verilog standard is quite large though, and not all Verilog features are needed to be able to describe hardware.  Many Verilog features are only useful for simulation and do not affect the actual hardware itself, which means that these features do not have to be modelled in the semantics.  In addition to that, as the HLS algorithm dictates which Verilog constructs are generated, meaning the Verilog subset that has to be modelled by the semantics can be reduced even further to only support the constructs that are needed.  Only supporting a smaller subset in the semantics also means that there is less chance that the standard is misunderstood, and that the semantics actually model how the Verilog is simulated.
 
-The Verilog semantics are based on the semantics proposed by \citet{loow19_verif_compil_verif_proces}, which were used to create a formal translation from HOL logic into a Verilog circuit.  These semantics are quite practical as they restrict themselves to a small subset of Verilog, which can nonetheless be used to model all hardware constructs one would want to design. An abstraction of the Verilog syntax that is generated is shown below: \JW{This verilog syntax looks weird to me. I didn't think there was a `then' keyword, for instance. Perhaps you're aiming more at some sort of abstracted syntax of Verilog? What does the semicolon on its own mean? Some sort of skip statement? The case statement looks weird too -- how do you get multiple cases in a single switch statement, and where is the default case? }\YH{I think I have fixed most cases, yes the single semicolon is a skip statement, should I make that more obvious by naming it? } \JW{It still looks a bit funny to me -- a bit of a halfway-house between `proper' Verilog syntax and `abstract' Verilog syntax. E.g. the way `begin...end' blocks contain exactly two statements, or the way that you get an erroneous double semicolon by combining the `begin...end' rule with the `e=e;' rule. People who are very familiar with C-like syntax will know that this isn't quite right... but then again, it doesn't really matter whether you handle the full syntax, because you only have to pretty-print a subset of it. So, why not stick here with a slightly abstracted Verilog syntax? It would make the operational semantics easier to read, for instance. Basically like you had it before, but explicitly labelled as a simplified syntax, so readers don't get confused!}\YH{Yeah, the syntax is a bit funny, mostly because this is actually how it is also encoded in Coq.  The main weird rule is the Seq rule, basically because it actually doesn't have a semicolon in between and no begin and end block, but it looks a bit strange to just put two $s$ next to each other.  We therefore don't really have begin and end blocks, and basically glue them to each statement instead, so in our semantics, the if statement actually looks like: if $e$ begin $s$ end else begin $s$ end, but it gets very verbose for case statements.  I got rid of the sequence for now, but now it just looks like function application, so the semi colon kind of acted like a constructor.  I can just add a \texttt{Seq} constructor though, which might be clearer.}
+The Verilog semantics are based on the semantics proposed by \citet{loow19_verif_compil_verif_proces}, which were used to create a formal translation from HOL logic into a Verilog circuit.  These semantics are quite practical as they restrict themselves to a small subset of Verilog, which can nonetheless be used to model all hardware constructs one would want to design. An abstraction of the Verilog syntax that is generated is shown below:
 
 \begin{align*}
   v\quad ::=&\; \mathit{sz} \yhkeyword{'d} n\\
@@ -66,8 +66,6 @@ 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{In CondTrue and CondFalse, the relationship between $\Gamma_0$ and $\sigma_0$ needs clarifying.}\YH{Clarified now in the previous paragraph.} \JW{Hm, why not just make `erun' take the entire $\sigma$ rather than just two of its fields? That would avoid this confusion altogether.}\YH{I guess I just wanted to make it explicit that erun never looks at the nonblocking assignments, but yes, it could also just take the whole $\sigma$} \JW{In CaseNoMatch, it feels weird to me that you keep evaluating $e$ for each case of the switch, rather than just once at the start of the switch statement. I guess it's ok because a failed match doesn't change the state. Just a bit quirky, I guess.}\YH{Yes that is a bit annoying actually, however, I couldn't really figure out the best way to only evaluate it once, as there isn't really a start to the case statement, we just describe that you could start anywhere in the case statement and evaluate it.  One solution would be to define a separate inductive rule that finds a matching case based on an evaluated value, which may be cleaner actually.} \JW{In CaseDefault, I was slightly surprised to see `Some' -- is that necessary?}\YH{That's true, currently it's a \texttt{Some} because the default case is optional, however, we actually always use it, so we could change it to be mandatory.} \JW{When using subscripted variables like $\Gamma_r$, I prefer $\Gamma_{\rm r}$ because $r$ is a fixed name (short for `register'), not a variable.}\YH{That is much nicer actually!}
-
 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.
 
 One main difference between these semantics and the Verilog semantics by \citet{loow19_verif_compil_verif_proces} is that there is no function for external nondeterministic effects, such as memories and inputs and outputs.  These are instead handled explicitly in the semantics by using two dimensional unpacked arrays to model memories and assuming that inputs to modules cannot change.  Another difference with these semantics is that partial updates to arrays are fully supported, due to the fact that there are two different queues for arrays and variables.  Originally, if there was a blocking assignment to an array, and then a nonblocking assignment to a different region in the array, then the blocking assignment would disappear at the end of the clock cycle.  This is because the complete array would be overwritten with the updated array in the nonblocking association maps.  However, in our semantics, only the values that were changed in the array are actually recorded in the nonblocking assignment queue, meaning once the blocking and nonblocking array association maps are merged, only the actual indices that changed with nonblocking assignment are updated in the blocking assignment map.
@@ -78,18 +76,22 @@ To integrate our semantics with CompCert, we need to define the same states that
 
 We then define the semantics of running the module for one clock cycle in the following way:
 
-\begin{gather*}
-  \inferrule[Module]{\Gamma_{r} ! s_{t} = \texttt{Some } v \\ (m_{i}, \Gamma_{r}^{0}, \Gamma_{a}^{0}, \epsilon, \epsilon\ l)\ \longrightarrow_{\vec{m}} (m_{i}, \Gamma_{r}^{1}, \Gamma_{a}^{1}, \Delta_{r}^{1}, \Delta_{a}^{1}) \\ (\Gamma_{r}^{1} // \Delta_{r}^{1}) ! s_{t} = \texttt{Some } v'}{\texttt{State } \textit{sf }\ m\ v\ \Gamma_{r}^{0}\ \Gamma_{a}^{0} \longrightarrow \texttt{State } \textit{sf }\ m\ v'\ (\Gamma_{r}^{1} // \Delta_{r}^{1})\ (\Gamma_{a}^{1} // \Delta_{a}^{1})}\\
-%
-  \inferrule[Finish]{\Gamma_{r}!\textit{fin} = \texttt{Some } 1 \\ \Gamma_{r}!\textit{ret} = \texttt{Some } r}{\texttt{State } \textit{sf }\ m\ s_{t}\ \Gamma_{r}\ \Gamma_{a} \longrightarrow \texttt{Returnstate } \textit{sf }\ r}\\
-%
-  \inferrule[Call]{ }{\texttt{Callstate } \textit{sf }\ m\ \vec{r} \longrightarrow \texttt{State } \textit{sf }\ m\ n\ (\textit{init\_params }\ \vec{r}\ a // \{s_{t} \rightarrow n\})}\\
-%
-  \inferrule[Return]{ }{\texttt{Returnstate } (\texttt{Stackframe } r\ m\ \textit{pc }\ \Gamma_{r}\ \Gamma_{a} :: \textit{sf}) \longrightarrow \texttt{State } \textit{sf }\ m\ \textit{pc }\ (\Gamma_{r} // \{ \textit{st} \rightarrow \textit{pc}, r \rightarrow i \})\ \epsilon}
-\end{gather*}
+\begin{figure*}
+  \centering
+  \begin{gather*}
+    \inferrule[Module]{\Gamma_{r} ! s_{t} = \texttt{Some } v \\ (m_{i}, \Gamma_{r}^{0}, \Gamma_{a}^{0}, \epsilon, \epsilon\ l)\ \longrightarrow_{\vec{m}} (m_{i}, \Gamma_{r}^{1}, \Gamma_{a}^{1}, \Delta_{r}^{1}, \Delta_{a}^{1}) \\ (\Gamma_{r}^{1} // \Delta_{r}^{1}) ! s_{t} = \texttt{Some } v'}{\texttt{State } \textit{sf }\ m\ v\ \Gamma_{r}^{0}\ \Gamma_{a}^{0} \longrightarrow \texttt{State } \textit{sf }\ m\ v'\ (\Gamma_{r}^{1} // \Delta_{r}^{1})\ (\Gamma_{a}^{1} // \Delta_{a}^{1})}\\
+    % 
+    \inferrule[Finish]{\Gamma_{r}!\textit{fin} = \texttt{Some } 1 \\ \Gamma_{r}!\textit{ret} = \texttt{Some } r}{\texttt{State } \textit{sf }\ m\ s_{t}\ \Gamma_{r}\ \Gamma_{a} \longrightarrow \texttt{Returnstate } \textit{sf }\ r}\\
+    % 
+    \inferrule[Call]{ }{\texttt{Callstate } \textit{sf }\ m\ \vec{r} \longrightarrow \texttt{State } \textit{sf }\ m\ n\ (\textit{init\_params }\ \vec{r}\ a // \{s_{t} \rightarrow n\})}\\
+    % 
+    \inferrule[Return]{ }{\texttt{Returnstate } (\texttt{Stackframe } r\ m\ \textit{pc }\ \Gamma_{r}\ \Gamma_{a} :: \textit{sf}) \longrightarrow \texttt{State } \textit{sf }\ m\ \textit{pc }\ (\Gamma_{r} // \{ \textit{st} \rightarrow \textit{pc}, r \rightarrow i \})\ \epsilon}
+  \end{gather*}
+  \caption{Inferrence rules for modules}%
+  \label{fig:inferrence_module}
+\end{figure*}
 
 \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 60e21bb..1bb5c3a 100644
--- a/verilog_notes.tex
+++ b/verilog_notes.tex
@@ -9,4 +9,8 @@
 
 \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.}
 
+\JW{This verilog syntax looks weird to me. I didn't think there was a `then' keyword, for instance. Perhaps you're aiming more at some sort of abstracted syntax of Verilog? What does the semicolon on its own mean? Some sort of skip statement? The case statement looks weird too -- how do you get multiple cases in a single switch statement, and where is the default case? }\YH{I think I have fixed most cases, yes the single semicolon is a skip statement, should I make that more obvious by naming it? } \JW{It still looks a bit funny to me -- a bit of a halfway-house between `proper' Verilog syntax and `abstract' Verilog syntax. E.g. the way `begin...end' blocks contain exactly two statements, or the way that you get an erroneous double semicolon by combining the `begin...end' rule with the `e=e;' rule. People who are very familiar with C-like syntax will know that this isn't quite right... but then again, it doesn't really matter whether you handle the full syntax, because you only have to pretty-print a subset of it. So, why not stick here with a slightly abstracted Verilog syntax? It would make the operational semantics easier to read, for instance. Basically like you had it before, but explicitly labelled as a simplified syntax, so readers don't get confused!}\YH{Yeah, the syntax is a bit funny, mostly because this is actually how it is also encoded in Coq.  The main weird rule is the Seq rule, basically because it actually doesn't have a semicolon in between and no begin and end block, but it looks a bit strange to just put two $s$ next to each other.  We therefore don't really have begin and end blocks, and basically glue them to each statement instead, so in our semantics, the if statement actually looks like: if $e$ begin $s$ end else begin $s$ end, but it gets very verbose for case statements.  I got rid of the sequence for now, but now it just looks like function application, so the semi colon kind of acted like a constructor.  I can just add a \texttt{Seq} constructor though, which might be clearer.}
+
+\YH{TODO: Add rules for blocking and nonblocking assignment to arrays.} \JW{In CondTrue and CondFalse, the relationship between $\Gamma_0$ and $\sigma_0$ needs clarifying.}\YH{Clarified now in the previous paragraph.} \JW{Hm, why not just make `erun' take the entire $\sigma$ rather than just two of its fields? That would avoid this confusion altogether.}\YH{I guess I just wanted to make it explicit that erun never looks at the nonblocking assignments, but yes, it could also just take the whole $\sigma$} \JW{In CaseNoMatch, it feels weird to me that you keep evaluating $e$ for each case of the switch, rather than just once at the start of the switch statement. I guess it's ok because a failed match doesn't change the state. Just a bit quirky, I guess.}\YH{Yes that is a bit annoying actually, however, I couldn't really figure out the best way to only evaluate it once, as there isn't really a start to the case statement, we just describe that you could start anywhere in the case statement and evaluate it.  One solution would be to define a separate inductive rule that finds a matching case based on an evaluated value, which may be cleaner actually.}
+
 \fi