From 803fd33db9c103a4b918ae8528dd9ff0c02ec410 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Thu, 15 Apr 2021 13:59:17 +0100
Subject: Add new data

---
 verilog.tex | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'verilog.tex')

diff --git a/verilog.tex b/verilog.tex
index c698b51..061444b 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}] = \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[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}] = \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[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}\\
       %
@@ -136,11 +136,11 @@ However, in practice, assigning and reading from an array directly in the state
     \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[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[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}]]) }
+      \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}
-- 
cgit