diff options
| -rw-r--r-- | algorithm.tex | 2 | ||||
| -rw-r--r-- | evaluation.tex | 2 | ||||
| -rw-r--r-- | verilog.tex | 11 | ||||
| -rw-r--r-- | verilog_notes.tex | 5 |
4 files changed, 8 insertions, 12 deletions
diff --git a/algorithm.tex b/algorithm.tex index 6035581..849ea05 100644 --- a/algorithm.tex +++ b/algorithm.tex @@ -37,7 +37,7 @@ To describe the translation, we can start with a simple example of how to transl \subsection{CompCert RTL} -All CompCert intermediate language follow the similar structure below: +All CompCert intermediate language follow the similar structure below: \JW{should `(id * data)' be `(id * data) list'?} \begin{align*} \mathit{program} \quad ::= \{ &\mathbf{variables} : (\mathit{id} * \mathit{data}), \\ diff --git a/evaluation.tex b/evaluation.tex index 704d352..b5206f6 100644 --- a/evaluation.tex +++ b/evaluation.tex @@ -1,6 +1,6 @@ \section{Evaluation} -\NR{Do we want to collect C-to-Verilog compile time?} +\NR{Do we want to collect C-to-Verilog compile time?} \JW{Yes that would be great.} \begin{table} \begin{tabular}{lcccccc} \toprule diff --git a/verilog.tex b/verilog.tex index 13fee98..431bca1 100644 --- a/verilog.tex +++ b/verilog.tex @@ -22,15 +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 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 \JW{But I wouldn't use `$*$' to separate the size and the value here, because it makes it look like you're multiplying them together. You could use the apostrophe symbol like real Verilog? \texttt{4'b5} and so on?}, 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. +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 \JW{Boolean} values, but instead they are represented by a size and its value \JW{But I wouldn't use `$*$' to separate the size and the value here, because it makes it look like you're multiplying them together. You could use the apostrophe symbol like real Verilog? \texttt{4'b5} and so on?}, 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. \JW{In the $m$ category, should it be `reg d; m' rather than just `reg d;'?} \subsection{Semantics} -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. +Existing operational semantics~\cite{loow19_verif_compil_verif_proces} were adapted for the semantics of the language that CoqUp eventually targets. These semantics are \JW{This semantics is a} 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. -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_{r}, \Gamma_{a}, \Delta_{r}, \Delta_{a})$, where $\Gamma_{r}$ is the current value of the registers, $\Gamma_{a}$ is the current value of the array, and $\Delta_{r}$ and $\Delta_{a}$ are the values of the variables and arrays when the clock cycle ends. +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 +\JW{rising} 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_{r}, \Gamma_{a}, \Delta_{r}, \Delta_{a})$, where $\Gamma_{r}$ is the current value of the registers, $\Gamma_{a}$ is the current value of the array, and $\Delta_{r}$ and $\Delta_{a}$ are the values of the variables and arrays when the clock cycle ends. -We can then define how one step in the semantics looks like. We therefore first need to define the structure of the main module which will contain the logic for the program. In general, functions that are translated to hardware will require basic handshaking signals so that the translated function can be used in hardware. Firstly, they require an input for the clock, so that all the sequential circuits are run at the right time. They then require a start and reset input, so that the hardware generated from the function can be reused multiple times. Finally, they need a finish and return signal, where finish will go high when the result is ready to be read. In addition to that, the function could take an arbitrary number of inputs which act as arguments to the function, so that the function can be called with different arguments. However, in addition to inputs and outputs to the module, we also need to keep track of some internal signals and properties about the module. Firstly, we need to keep track of the internal variables that contain the current state of the module, and the current contents of the stack. Finally, the module will contain the entry point of the module and the list of module items that declare all of the internal registers and contain the encoding of the state machine that behaves in the same way as the function. We can therefore declare it in the following way: +We can then define how one step in the semantics looks like. We therefore first need to define the structure of the main module which will contain the logic for the program. In general, functions that are translated to hardware will require basic handshaking signals so that the translated function can be used in hardware. Firstly, they require an input for the clock, so that all the sequential circuits are run at the right time. They then require a start and reset input, so that the hardware generated from the function can be reused multiple times. Finally, they need a finish and return signal, where finish will go high when the result is ready to be read. In addition to that, the function could take an arbitrary number of inputs which act as arguments to the function, so that the function can be called with different arguments. However, in addition to inputs and outputs to the module, we also need to keep track of some internal signals and properties about the module. Firstly, we need to keep track of the internal variables that contain the current state of the module, and the current contents of the stack. Finally, the module will contain the entry point of the module and the list of module items that declare all of the internal registers and contain the encoding of the state machine that behaves in the same way as the function. We can therefore declare it in the following way: \JW{I'd be inclined to write `$r~\mathrm{list}$' rather than $\vec{r}$, as it's a little more readable. (Assuming it's more-or-less the same thing?)} \begin{align*} \mathit{M} \quad ::= \quad \big\{\ &\mathtt{args} : \vec{r}\\ @@ -67,7 +68,7 @@ The two main evaluation functions are then \textit{erun}, which takes in the cur % \inferrule[Nonblocking Array]{\texttt{name}\ \textit{lhs} = \texttt{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.} +\YH{TODO: Add rules for blocking and nonblocking assignment to arrays.} \JW{The `Skip' rule has an erroneous $=$.} \JW{You could use a bit of colour here, e.g. the keywords like `if' could be coloured for readability.} \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?} \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]$'.} 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 $s_{0}$ to state $s_{1}$. If both of these conditions hold, we then get that the conditional statement will also run from state $s_{0}$ to state $s_{1}$. The \textsc{Blocking} and \textsc{Nonblocking} rules are a bit more interesting, as these modify the blocking and nonblocking association maps respectively. diff --git a/verilog_notes.tex b/verilog_notes.tex index 99f7e24..b28b04f 100644 --- a/verilog_notes.tex +++ b/verilog_notes.tex @@ -1,8 +1,3 @@ -\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.} |