diff options
| -rw-r--r-- | proof.tex | 2 | ||||
| -rw-r--r-- | verilog.tex | 2 |
2 files changed, 2 insertions, 2 deletions
@@ -2,7 +2,7 @@ This section describes the main correctness theorem that was proven and the main ideas behind the proofs. -The main correctness theorem states that for all Clight source programs $C$, if the translation from the source to the target Verilog code succeeds, assuming that $C$ has correct observable behaviour $B$ when executed, then the target Verilog code will simulate with the same behaviour $B$. The following backwards simulation theorem describes this property. +The main correctness theorem is the exact same correctness theorem as stated in \compcert{}~\cite{leroy09_formal_verif_realis_compil} and states that for all Clight source programs $C$, if the translation from the source to the target Verilog code succeeds, assuming that $C$ has correct observable behaviour $B$ when executed, then the target Verilog code will simulate with the same behaviour $B$, where behaviour can either be convergent, divergent or ``going wrong'' and is associated with a trace $t$ of any external function calls. The following backwards simulation theorem describes this property, where $\Downarrow_{s}$ and $\Downarrow$ stand for simulation and execution respectively. \begin{equation*} \forall C, V, B \notin \texttt{Wrong},\, \yhfunction{HLS} (C) = \yhconstant{OK} (V) \land V \Downarrow_{s} B \implies C \Downarrow B. diff --git a/verilog.tex b/verilog.tex index 1e75840..a4a637e 100644 --- a/verilog.tex +++ b/verilog.tex @@ -37,7 +37,7 @@ Two types of assignments are supported in always blocks: nonblocking and blockin \inferrule[Module]{(\Gamma, \epsilon, \vec{m})\ \downarrow_{\vec{m}} (\Gamma', \Delta')}{(\Gamma, \yhkeyword{module } \yhconstant{main} \yhkeyword{(...);}\ \vec{m}\ \yhkeyword{endmodule}) \downarrow_{m} (\Gamma' // \Delta')} \end{equation*} -\noindent \JW{On the top of that rule you have two occurrences of $\vec{m}$ -- is that right? If the $\vec{m}$ on the arrow is just the name of the transition type, rather than a variable, then I suggest $\downarrow_{\text{module}}$ or something. And perhaps the bottom of the rule could use $\downarrow_{\text{program}}$ or something.} This rule dictates how the whole module runs in one clock cycle, from an initial state of all the variables $\Gamma$, to a final state $(\Gamma' // \Delta')$, where $//$ defines a merge between the two maps from variable names to values, where the right hand side values take priority if there is a conflict. \JW{Is $//$ a standard notation for this? If so, that's fine. It's just I haven't come across it before.} This rule correctly implements the behaviours for the blocking and nonblocking assignment by overwriting the assignments made through blocking assignment at the end of the clock cycle with the atomic assignments from the nonblocking assignments. +\noindent \JW{On the top of that rule you have two occurrences of $\vec{m}$ -- is that right? If the $\vec{m}$ on the arrow is just the name of the transition type, rather than a variable, then I suggest $\downarrow_{\text{module}}$ or something. And perhaps the bottom of the rule could use $\downarrow_{\text{program}}$ or something.} This rule dictates how the whole module runs in one clock cycle, from an initial state of all the variables $\Gamma$, to a final state $(\Gamma' // \Delta')$, where $//$ defines a merge between the two maps from variable names to values, where the right hand side values take priority if there is a conflict. \JW{Is $//$ a standard notation for this? If so, that's fine. It's just I haven't come across it before.}\YH{It is not, should I use different notation? Is there standard notation?} This rule correctly implements the behaviours for the blocking and nonblocking assignment by overwriting the assignments made through blocking assignment at the end of the clock cycle with the atomic assignments from the nonblocking assignments. \JW{I think most of the following paragraph could be chopped. We've already mentioned that we're only targeting a small fragment of Verilog, so we could mention at that point that in the fragment we target there is no discrepancy between the simulation behaviour and the synthesis behaviour. I don't know how important it is to talk about the details of evaluation order here -- does the reader really need to be aware of this in order to understand your work?} When targeting a hardware description language such as Verilog, it is important to be consistent between simulating the hardware and the behaviour of the synthesised result on actual hardware. In the target Verilog semantics, only clocked always blocks are supported as these ensure that there are not mismatches between simulation and synthesis, as combinational always blocks that trigger on any change of an internal signal may behave differently in simulation or synthesis based on the order of operations. This limitation in the semantics therefore helps keep the Verilog correct and consistent. In addition to that, only nonblocking assignment is used in signals that are used in multiple always blocks, which stops any race conditions from occurring as all the signal updates happen deterministically. \NR{So the semantics allows multiple drivers then?} Finally, a specific order of evaluation for the always blocks is chosen, and because of the limitations listed before, choosing an order is guaranteed to have the same behaviour as executing the always blocks in any order.\NR{Order is not guaranteed if we have multiple drivers.} |