diff options
| -rw-r--r-- | main.tex | 1 | ||||
| -rw-r--r-- | verilog.tex | 81 | ||||
| -rw-r--r-- | verilog_notes.tex | 8 |
3 files changed, 38 insertions, 52 deletions
@@ -47,6 +47,7 @@ \usepackage{mathpartir} \usepackage{subcaption} \usepackage{tikz} +\usepackage{minted} \newif\ifCOMMENTS \COMMENTStrue diff --git a/verilog.tex b/verilog.tex index cf4baa4..5024121 100644 --- a/verilog.tex +++ b/verilog.tex @@ -22,10 +22,16 @@ The Verilog semantics are based on the semantics proposed by \citet{loow19_verif |&\; \text{\tt always @(posedge clk)}\ s \end{align*} -The main addition to the Verilog syntax is the explicit declaration of inputs and outputs, as well as variables and arrays. This means that the declarations have to be handled explicitly in the semantics as well, adding the safety that all the registers are declared properly with the right size, as this affects how the Verilog module is synthesised and simulated. In addition to that, literal values cannot be represented by a list of nested boolean values, instead they are represented by a size and its value. Finally, the last difference is that the syntax supports memories in Verilog explicitly and we have separate semantics to handle nonblocking and blocking assignments to memory correctly. +The main addition to the Verilog syntax is the explicit declaration of inputs and outputs, as well as variables and arrays. This means that the declarations have to be handled in the semantics as well, adding to the safety that all the registers are declared properly with the right size, as this affects how the Verilog module is synthesised and simulated. In addition to that, literal values are not represented by a list of nested boolean values, but instead they are represented by a size and its value, meaning a boolean is represented as a value with size one. Finally, the last difference is that the syntax supports two dimensional arrays in Verilog explicitly which model memory so that we can reason about array loads and stores properly. \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: + +\begin{minted}{systemverilog} +always @(posedge clk) +\end{minted} + 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} @@ -33,59 +39,30 @@ However, adjustments to these semantics had to be made to make it compatible wit s = (\Gamma, \Delta) \end{equation} -Definition of stmntrun. \JW{stmtntrun has four parameters, and if I read the rules correctly, it looks like the fourth parameter is uniquely determined by the first three. So, you could consider presenting stmntrun simply as a recursive definition, e.g. `stmntrun f s Vskip = s', `stmntrun f s0 (Vseq st1 st2) = stmntrun f (stmntrun f s0 st1) st2', and so on. That might (\emph{might}) be easier to read than the inference rule format.} - -\YH{It works well for Seq and Skip, but I think that CaseMatch and CaseNoMatch, or even if statements will be a bit clunky? We would have to use case statements in the function to do different things -based on what they evaluate to. For case I think that would end up being a three way choice. I'll try it out though and see how nice it is.} - -\JP{I suppose this would essentially be an ``interpreter'' style semantics but we can prove equivalence pretty easily.} +Definition of stmntrun. -\YH{To add to that, I used to have both in the Coq code, but commented the recursive definition out, and now only have the inductive definition, which is basically what I copy pasted here.} \JW{Fair enough. Whatever you think ends up being the easiest to read and understand, really. There's something to be said for staying close to the Coq definitions anyway.} \YH{I have added more rules, we can always switch from one to the other now. One more thing I noticed though is that recursive definitions will need an \texttt{option} type.} \JW{Oh, then my suggestion of `stmntrun f s0 (Vseq st1 st2) = stmntrun f (stmntrun f s0 st1) st2' is a bit ill-typed then, unless the second parameter becomes option-typed too. Maybe the inference rules are better overall then.} \YH{Ah yes, I actually didn't even notice that, it would need the do notation, just like the implementation in Coq, so it may be easier to just use the inference rules.} - -\begin{equation} +\begin{gather*} \label{eq:1} - \inferrule[Skip]{ }{\text{srun}\ f\ s\ \mathtt{Vskip} = s} -\end{equation} - -\begin{equation} - \label{eq:4} - \inferrule[Seq]{\text{srun}\ f\ s_{0}\ \mathit{st}_{1}\ s_{1} \\ \text{srun}\ f\ s_{1}\ \mathit{st}_{2}\ s_{2}}{\text{srun}\ f\ s_{0}\ (\mathtt{Vseq}\ \mathit{st}_{1}\ \mathit{st}_{2})\ s_{2}} -\end{equation} - -\begin{equation} - \label{eq:2} - \inferrule[CondTrue]{\text{erun}\ f\ \Gamma_{0}\ c\ v_{c} \\ \text{valToB}\ v_{c} = \mathtt{true} \\ \text{srun}\ f\ s_{0}\ \mathit{stt}\ s_{1}}{\text{srun}\ f\ s_{0}\ (\mathtt{Vcond}\ c\ \mathit{stt}\ \mathit{stf})\ s_{1}} -\end{equation} - -\begin{equation} - \label{eq:3} - \inferrule[CondFalse]{\text{erun}\ f\ \Gamma_{0}\ c\ v_{c} \\ \text{valToB}\ v_{c} = \mathtt{false} \\ \text{srun}\ f\ s_{0}\ \mathit{stf}\ s_{1}}{\text{srun}\ f\ s_{0}\ (\mathtt{Vcond}\ c\ \mathit{stt}\ \mathit{stf})\ s_{1}} -\end{equation} - -\begin{equation} - \label{eq:5} - \inferrule[CaseNoMatch]{\text{srun}\ f\ s_{0}\ (\mathtt{Vcase}\ e\ cs\ \mathit{def})\ s_{1} \\ \text{erun}\ f\ \Gamma_{0}\ me\ mve \\ \text{erun}\ f\ \Gamma_{0}\ e\ ve \\ mve \neq ve}{\text{srun}\ f\ s_{0}\ (\mathtt{Vcase}\ e\ ((me,\ sc) :: cs)\ \mathit{def})\ s_{1}} -\end{equation} - -\begin{equation} - \label{eq:6} - \inferrule[CaseMatch]{\text{srun}\ f\ s_{0}\ sc\ s_{1} \\ \text{erun}\ f\ \Gamma_{0}\ e\ ve \\ \text{erun}\ f\ \Gamma_{0}\ me\ mve \\ mve = ve}{\text{srun}\ f\ s_{0}\ (\mathtt{Vcase}\ e\ ((me,\ sc) :: cs)\ \mathit{def})\ s_{1}} -\end{equation} - -\begin{equation} - \label{eq:7} - \inferrule[CaseDefault]{\text{srun}\ f\ s_{0}\ st\ s_{1}}{\text{srun}\ f\ s_{0}\ (\mathtt{Vcase}\ e\ []\ (\mathtt{Some}\ st))\ s_{1}} -\end{equation} - -\begin{equation} - \label{eq:8} - \inferrule[Blocking]{\text{name}\ \mathit{lhs} = \mathtt{OK}\ n \\ \text{erun}\ f\ \Gamma\ \mathit{rhs}\ v_{\mathit{rhs}}}{\text{srun}\ f\ (\Gamma, \Delta)\ (\mathtt{Vblock}\ \mathit{lhs}\ \mathit{rhs})\ (\Gamma ! n \rightarrow v_{\mathit{rhs}}, \Delta)} -\end{equation} - -\begin{equation} - \label{eq:9} - \inferrule[Nonblocking]{\text{name}\ \mathit{lhs} = \mathtt{OK}\ n \\ \text{erun}\ f\ \Gamma\ \mathit{rhs}\ v_{\mathit{rhs}}}{\text{srun}\ f\ (\Gamma, \Delta)\ (\mathtt{Vnonblock}\ \mathit{lhs}\ \mathit{rhs}) (\Gamma, \Delta ! n \rightarrow v_{\mathit{rhs}})} -\end{equation} + \inferrule[Skip]{ }{\texttt{srun}\ f\ s\ \texttt{Vskip} = s}\\ +% + \inferrule[Seq]{\texttt{srun}\ f\ s_{0}\ \textit{st}_{1}\ s_{1} \\ \texttt{srun}\ f\ s_{1}\ \textit{st}_{2}\ s_{2}}{\texttt{srun}\ f\ s_{0}\ (\texttt{Vseq}\ \textit{st}_{1}\ \textit{st}_{2})\ s_{2}}\\ +% + \inferrule[CondTrue]{\texttt{erun}\ f\ \Gamma_{0}\ c\ v_{c} \\ \texttt{valToB}\ v_{c} = \texttt{true} \\ \texttt{srun}\ f\ s_{0}\ \textit{stt}\ s_{1}}{\texttt{srun}\ f\ s_{0}\ (\texttt{Vcond}\ c\ \textit{stt}\ \textit{stf}\,)\ s_{1}}\\ +% + \inferrule[CondFalse]{\texttt{erun}\ f\ \Gamma_{0}\ c\ v_{c} \\ \texttt{valToB}\ v_{c} = \texttt{false} \\ \texttt{srun}\ f\ s_{0}\ \textit{stf}\ s_{1}}{\texttt{srun}\ f\ s_{0}\ (\texttt{Vcond}\ c\ \textit{stt}\ \textit{stf}\,)\ s_{1}}\\ +% + \inferrule[CaseNoMatch]{\texttt{srun}\ f\ s_{0}\ (\texttt{Vcase}\ e\ cs\ \textit{def})\ s_{1} \\ \texttt{erun}\ f\ \Gamma_{0}\ me\ mve \\ \texttt{erun}\ f\ \Gamma_{0}\ e\ ve \\ mve \neq ve}{\texttt{srun}\ f\ s_{0}\ (\texttt{Vcase}\ e\ ((me,\ sc) :: cs)\ \textit{def})\ s_{1}}\\ +% + \inferrule[CaseMatch]{\texttt{srun}\ f\ s_{0}\ sc\ s_{1} \\ \texttt{erun}\ f\ \Gamma_{0}\ e\ ve \\ \texttt{erun}\ f\ \Gamma_{0}\ me\ mve \\ mve = ve}{\texttt{srun}\ f\ s_{0}\ (\texttt{Vcase}\ e\ ((me,\ sc) :: cs)\ \textit{def})\ s_{1}}\\ +% + \inferrule[CaseDefault]{\texttt{srun}\ f\ s_{0}\ st\ s_{1}}{\texttt{srun}\ f\ s_{0}\ (\texttt{Vcase}\ e\ []\ (\texttt{Some}\ st))\ s_{1}}\\ +% + \inferrule[Blocking]{\texttt{name}\ \textit{lhs} = \texttt{OK}\ n \\ \texttt{erun}\ f\ \Gamma\ \textit{rhs}\ v_{\textit{rhs}}}{\texttt{srun}\ f\ (\Gamma, \Delta)\ (\texttt{Vblock}\ \textit{lhs}\ \textit{rhs})\ (\Gamma ! n \rightarrow v_{\textit{rhs}}, \Delta)}\\ +% + \inferrule[Nonblocking]{\texttt{name}\ \textit{lhs} = \texttt{OK}\ n \\ \texttt{erun}\ f\ \Gamma\ \textit{rhs}\ v_{\textit{rhs}}}{\texttt{srun}\ f\ (\Gamma, \Delta)\ (\texttt{Vnonblock}\ \textit{lhs}\ \textit{rhs}) (\Gamma, \Delta ! n \rightarrow v_{\textit{rhs}})}\\ +\end{gather*} + +\input{verilog_notes} %%% Local Variables: %%% mode: latex diff --git a/verilog_notes.tex b/verilog_notes.tex new file mode 100644 index 0000000..99f7e24 --- /dev/null +++ b/verilog_notes.tex @@ -0,0 +1,8 @@ +\JW{stmtntrun has four parameters, and if I read the rules correctly, it looks like the fourth parameter is uniquely determined by the first three. So, you could consider presenting stmntrun simply as a recursive definition, e.g. `stmntrun f s Vskip = s', `stmntrun f s0 (Vseq st1 st2) = stmntrun f (stmntrun f s0 st1) st2', and so on. That might (\emph{might}) be easier to read than the inference rule format.} + +\YH{It works well for Seq and Skip, but I think that CaseMatch and CaseNoMatch, or even if statements will be a bit clunky? We would have to use case statements in the function to do different things +based on what they evaluate to. For case I think that would end up being a three way choice. I'll try it out though and see how nice it is.} + +\JP{I suppose this would essentially be an ``interpreter'' style semantics but we can prove equivalence pretty easily.} + +\YH{To add to that, I used to have both in the Coq code, but commented the recursive definition out, and now only have the inductive definition, which is basically what I copy pasted here.} \JW{Fair enough. Whatever you think ends up being the easiest to read and understand, really. There's something to be said for staying close to the Coq definitions anyway.} \YH{I have added more rules, we can always switch from one to the other now. One more thing I noticed though is that recursive definitions will need an \texttt{option} type.} \JW{Oh, then my suggestion of `stmntrun f s0 (Vseq st1 st2) = stmntrun f (stmntrun f s0 st1) st2' is a bit ill-typed then, unless the second parameter becomes option-typed too. Maybe the inference rules are better overall then.} \YH{Ah yes, I actually didn't even notice that, it would need the do notation, just like the implementation in Coq, so it may be easier to just use the inference rules.} |