Update on Overleaf.

1 files changed, 1 insertions, 2 deletions

diff --git a/verilog.tex b/verilog.tex
index 045f6fe..5f37919 100644
--- a/verilog.tex
+++ b/verilog.tex
@@ -66,8 +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{CaseNoMatch and CaseMatch rules both have a mismatched parenthesis.}\YH{Thanks, fixed.} \JW{In CondTrue and CondFalse, the relationship between $\Gamma_0$ and $\sigma_0$ needs clarifying.}\YH{Clarified now in the previous paragraph.} \JW{CaseNoMatch is missing the `default:' and `endcase' keywords.}
-\YH{I've removed the default keyword now, aiming for a more abstract syntax, but added `endcase'} \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{In BlockingReg, erun is taking more parameters than it does elsewhere.}\YH{Yes thank you, fixed that now.} \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!}
+\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{In BlockingReg, erun is taking more parameters than it does elsewhere.}\YH{Yes thank you, fixed that now.} \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.