Add inferrence rules

1 files changed, 33 insertions, 0 deletions

diff --git a/verilog.tex b/verilog.tex
index d0dd74c..0cf13ab 100644
--- a/verilog.tex
+++ b/verilog.tex
@@ -111,6 +111,39 @@ Therefore, in addition to the rules shown in Figure~\ref{fig:inferrence_module},
 
 \subsection{Memory Model}
 
+The Verilog semantics do not define a memory model for Verilog, as this is not needed for a hardware description language.  There is no preexisting architecture that Verilog will produce, it can describe any memory layout that is needed.  Instead of having specific semantics for memory, the semantics only need to support the language features that can produce these different memory layouts, these being Verilog arrays.
+
+However, in practice, assigning and reading from an array directly in the state machine will not produce a memory in the final hardware design, as the synthesis tool cannot identify the array as having the necessary properties that a RAM needs, such as only reading and writing to the array once per clock cycles.  Instead, the synthesis tool expects a specific template that ensures these properties, and will then transform the template into a proper RAM during synthesis.  We can therefore
+
+\begin{figure}
+  \centering
+  \begin{minipage}{1.0\linewidth}
+    \begin{gather*}
+      \inferrule[None]{ }{\textit{exec\_ram}\ \Gamma\ \Delta\ \yhconstant{None}\ \Delta}\qquad
+%
+      \inferrule[Idle]{\Gamma_{\rm r}\ !\ \textit{r.en} = \Gamma_{\rm r}\ !\ \textit{r.u\_{en}}}{\textit{exec\_ram}\ (\Gamma_{\rm r}, \Gamma_{\rm a})\ \Delta\ (\yhconstant{Some}\ r)\ \Delta}\\
+%
+      \inferrule[Read]{\Gamma_{\rm r}\ !\ \textit{r.en} \ne \Gamma_{\rm r}\ !\ \textit{r.u\_en} \\ \Gamma_{\rm r}\ !\ \textit{r.wr\_en} = 0}{ \textit{exec\_ram}\ (\Gamma_{\rm r}, \Gamma_{\rm a})\ (\Delta_{\rm r}, \Delta_{\rm a})\ (\yhconstant{Some}\ r)\ (\Delta_{\rm r}[\textit{r.en} \mapsto \textit{r.u\_en}, \textit{r.d\_out} \mapsto (\Gamma_{\rm a}\ !\ \textit{r.mem})\ !\ \textit{r.addr}], \Delta_{\rm a}) }\\
+%
+      \inferrule[Write]{\Gamma_{\rm r}\ !\ \textit{r.en} \ne \Gamma_{\rm r}\ !\ \textit{r.u\_en} \\ \Gamma_{\rm r}\ !\ \textit{r.wr\_en} = 1}{ \textit{exec\_ram}\ (\Gamma_{\rm r}, \Gamma_{\rm a})\ (\Delta_{\rm r}, \Delta_{\rm a})\ (\yhconstant{Some}\ r)\ (\Delta_{\rm r}[\textit{r.en} \mapsto \textit{r.u\_en}], \Delta_{\rm a}[\textit{r.mem} \mapsto (\Gamma_{\rm a}\ !\ \textit{r.mem})[\textit{r.addr} \mapsto \textit{r.d\_in}]]) }
+    \end{gather*}
+  \end{minipage}
+  \caption{Specification for memory implementation in HTL, which is then implemented by equivalent Verilog code.}\label{fig:verilog_syntax}
+\end{figure}
+
+\begin{figure}
+\begin{minted}{verilog}
+  reg [31:0] mem [2047:0];
+  always @(negedge clk)
+    if (en ^ u_en) begin
+      if (wr_en) mem[addr] <= d_in;
+      else d_out <= mem[addr];
+      en <= u_en;
+    end
+\end{minted}
+  \caption{Implementation of memory specification in Verilog of its HTL specification.}
+\end{figure}
+
 \begin{figure}
   \centering
   \begin{subfigure}[t]{0.48\linewidth}