\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.}

\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