From ac15b33e1bc6faad4b09fb508caf969e813b43db Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Thu, 15 Apr 2021 19:42:53 +0100
Subject: Add more

---
 verilog.tex | 22 ++--------------------
 1 file changed, 2 insertions(+), 20 deletions(-)

(limited to 'verilog.tex')

diff --git a/verilog.tex b/verilog.tex
index 061444b..e0d1257 100644
--- a/verilog.tex
+++ b/verilog.tex
@@ -73,9 +73,9 @@ The main execution of the module $\downarrow_{\text{module}}$ is split into $\do
   \centering
   \begin{minipage}{1.0\linewidth}
     \begin{gather*}
-      \inferrule[Step]{\Gamma_r[\textit{rst}] = \yhconstant{Some } 0 \\ \Gamma_r[\textit{fin}] = \yhconstant{Some } 0 \\ \Gamma_r[\sigma] = \yhconstant{Some } v \\ (m, (\Gamma_r, \Gamma_a))\ \downarrow_{\text{program}} (\Gamma_r', \Gamma_a') \\ \Gamma_r'[\sigma] = \yhconstant{Some } v'}{\yhconstant{State } \textit{sf }\ m\ v\ \Gamma_r\ \Gamma_a \longrightarrow \yhconstant{State } \textit{sf }\ m\ v'\ \Gamma_r'\ \Gamma_a'}\\
+      \inferrule[Step]{\Gamma_r[\textit{rst}] = 0 \\ \Gamma_r[\textit{fin}] = 0 \\ (m, (\Gamma_r, \Gamma_a))\ \downarrow_{\text{program}} (\Gamma_r', \Gamma_a')}{\yhconstant{State } \textit{sf }\ m\ \ \Gamma_r[\sigma]\ \ \Gamma_r\ \Gamma_a \longrightarrow \yhconstant{State } \textit{sf }\ m\ \ \Gamma_r'[\sigma]\ \ \Gamma_r'\ \Gamma_a'}\\
       %
-      \inferrule[Finish]{\Gamma_r[\textit{fin}] = \yhconstant{Some } 1 \\ \Gamma_r[ \textit{ret}] = \yhconstant{Some } r}{\yhconstant{State } \textit{sf }\ m\ \sigma\ \Gamma_r\ \Gamma_a \longrightarrow \yhconstant{Returnstate } \textit{sf }\ r}\\
+      \inferrule[Finish]{\Gamma_r[\textit{fin}] = 1}{\yhconstant{State } \textit{sf }\ m\ \sigma\ \Gamma_r\ \Gamma_a \longrightarrow \yhconstant{Returnstate } \textit{sf }\ \Gamma_r[ \textit{ret}]}\\
       %
       \inferrule[Call]{ }{\yhconstant{Callstate } \textit{sf }\ m\ \vec{r} \longrightarrow \yhconstant{State } \textit{sf }\ m\ n\ ((\yhfunction{init\_params}\ \vec{r}\ a)[\sigma \mapsto n, \textit{fin} \mapsto 0, \textit{rst} \mapsto 0])\ \epsilon}\\
       %
@@ -130,24 +130,6 @@ This translation is represented in Figure~\ref{fig:memory_model_transl}, where \
 
 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, even though this is the most natural formulation of memory.  Even though theoretically the memory will only be read from once per clock cycle, the synthesis tool cannot ensure that this is true, and will instead create a register for each memory location.  This increases the size of the circuit dramatically, as the RAM on the FPGA chip will not be reused.  Instead, the synthesis tool expects a specific template that ensures these properties, and will then transform the template into a proper RAM during synthesis.  Therefore, a translation has to be performed from the naive use of memory in the state machine, to a proper use of a memory template.
 
-\begin{figure}
-  \centering
-  \begin{minipage}{1.0\linewidth}
-    \begin{gather*}
-      \inferrule[None]{ }{(\Gamma,\Delta, \yhconstant{None}) \downarrow_{\text{ram}} \Delta}\qquad
-%
-      \inferrule[Idle]{\Gamma_{\rm r}[\textit{r.en}] = \Gamma_{\rm r}[\textit{r.u\_{en}}]}{((\Gamma_{\rm r}, \Gamma_{\rm a}), \Delta, \yhconstant{Some}\ r) \downarrow_{\text{ram}} \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}{((\Gamma_{\rm r}, \Gamma_{\rm a}), (\Delta_{\rm r}, \Delta_{\rm a}), \yhconstant{Some}\ r) \downarrow_{\text{ram}} (\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}{((\Gamma_{\rm r}, \Gamma_{\rm a}), (\Delta_{\rm r}, \Delta_{\rm a}), \yhconstant{Some}\ r) \downarrow_{\text{ram}} (\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:htl_ram_spec}
-\end{figure}
-
-This memory template can be represented using the following semantics shown in Figure~\ref{fig:htl_ram_spec}, which is then translated to the equivalent Verilog implementation shown in Figure~\ref{fig:verilog_ram_impl}.
-
 %\begin{figure}
 %  \centering
 %  \begin{subfigure}[t]{0.48\linewidth}
-- 
cgit 

