Add new diagram

1 files changed, 67 insertions, 2 deletions

diff --git a/verilog.tex b/verilog.tex
index 89a40dd..9b19b87 100644
--- a/verilog.tex
+++ b/verilog.tex
@@ -125,8 +125,73 @@ This translation is represented in Figure~\ref{fig:memory_model_transl}, where \
 
 \begin{figure}
   \centering
-  \includegraphics[width=0.5\linewidth]{diagrams/memory_model.pdf}
-  \caption{Change in the memory model during the translation of 3AC to HTL.  This is immediately after the assignment to the array.\YH{TODO: Update diagram}}\label{fig:memory_model_transl}
+  \begin{tikzpicture}
+    \draw (0,0) rectangle (5,-5);
+    \draw (7,0) rectangle (12,-5);
+    \node[right] at (0,-0.3) {\small \textbf{\compcert{}'s Memory Model}};
+    \node[right] at (7,-0.3) {\small \textbf{Verilog Memory Representation}};
+    \node[right] (x0) at (0.2,-1.9) {\small 0};
+    \node[right] (x1) at (0.2,-2.5) {\small 1};
+    \foreach \x in {0,...,6}{%
+      \node[right] (s\x) at (2.5,-1-\x*0.3) {\small \x};
+      \node[right] (t\x) at (4,-1-\x*0.3) {};
+      \draw[->] (s\x) -- (t\x);
+    }
+
+    \node[right] at (t0) {\small \texttt{DE}};
+    \node[right] at (t1) {\small \texttt{AD}};
+    \node[right] at (t2) {\small \texttt{BE}};
+    \node[right] at (t3) {\small \texttt{EF}};
+    \node[right] at (t4) {\small \texttt{12}};
+    \node[right] at (t5) {\small \texttt{34}};
+    \node[right] at (t6) {\small \texttt{56}};
+    \node[right] at (3.1,-3.1) {$\cdots$};
+
+    \node[right] at (3.1,-4) {$\cdots$};
+    \node[scale=1.3] at (6,-2.5) {\Huge $\Rightarrow$};
+
+    \draw[->] (x0) -- (s3);
+    \draw[->] (x1) -- (2.5,-4);
+    \draw (0,-4.3) -- (5,-4.3);
+    \node at (2.5,-4.7) {\small \texttt{x[0] = 0xDEADBEEF;}};
+
+    \draw (7.2,-1.2) rectangle (9.4,-3.9);
+    \draw (9.6,-1.2) rectangle (11.8,-3.9);
+
+    \foreach \x in {0,...,8}{%
+      \draw (7.2,-1.2-\x*0.3) -- (9.4,-1.2-\x*0.3);
+      \draw (9.6,-1.2-\x*0.3) -- (11.8,-1.2-\x*0.3);
+      \node (b\x) at (8.3,-1.35-\x*0.3) {};
+      \node (nb\x) at (10.7,-1.35-\x*0.3) {};
+    }
+
+    \node[scale=1.2] at (b0) {\tiny\texttt{0: Some 00000000}};
+    \node[scale=1.2] at (b1) {\tiny\texttt{1: Some 12345600}};
+    \node[scale=1.2] at (b2) {\tiny\texttt{2: Some 00000000}};
+    \node[scale=1.2] at (b3) {\tiny\texttt{3: Some 00000000}};
+    \node[scale=1.2] at (b4) {\tiny\texttt{4: Some 00000000}};
+    \node[scale=1.2] at (b5) {\tiny\texttt{5: Some 00000000}};
+    \node[scale=1.2] at (b6) {\tiny\texttt{6: Some 00000000}};
+    \node[scale=1.2] at ($(b7) - (0,0.05)$) {$\cdots$};
+    \node[scale=1.2] at (b8) {\tiny\texttt{N: Some 00000000}};
+
+    \node[scale=1.2] at (nb0) {\tiny\texttt{0: Some DEADBEEF}};
+    \node[left,scale=1.2] at (nb1) {\tiny\texttt{1: None}};
+    \node[left,scale=1.2] at (nb2) {\tiny\texttt{2: None}};
+    \node[left,scale=1.2] at (nb3) {\tiny\texttt{3: None}};
+    \node[left,scale=1.2] at (nb4) {\tiny\texttt{4: None}};
+    \node[left,scale=1.2] at (nb5) {\tiny\texttt{5: None}};
+    \node[left,scale=1.2] at (nb6) {\tiny\texttt{6: None}};
+    \node[scale=1.2] at ($(nb7) - (0,0.05)$) {$\cdots$};
+    \node[left,scale=1.2] at (nb8) {\tiny\texttt{N: None}};
+
+    \node at (8.3,-1) {$\Gamma_{a}$};
+    \node at (10.7,-1) {$\Delta_{a}$};
+
+    \draw (7,-4.3) -- (12,-4.3);
+    \node at (9.5,-4.7) {\small \texttt{stack[0] <= 0xDEADBEEF;}};
+  \end{tikzpicture}
+  \caption{Change in the memory model during the translation of 3AC to HTL.  This is immediately after the assignment to the array.}\label{fig:memory_model_transl}
 \end{figure}
 
 %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 interface that ensures these properties, and will then transform the interface 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 interface.