Add timing diagrams

1 files changed, 1 insertions, 21 deletions

diff --git a/verilog.tex b/verilog.tex
index e77aa97..cb0d243 100644
--- a/verilog.tex
+++ b/verilog.tex
@@ -140,27 +140,7 @@ However, in practice, assigning and reading from an array directly in the state
   \caption{Specification for memory implementation in HTL, which is then implemented by equivalent Verilog code.}\label{fig:htl_ram_spec}
 \end{figure}
 
-\begin{figure}
-  \begin{subfigure}[b]{0.48\linewidth}
-\begin{minted}{verilog}
-  reg [31:0] mem [SIZE-1: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.}\label{fig:verilog_ram_impl}
-  \end{subfigure}\hfill%
-  \begin{subfigure}[b]{0.48\linewidth}
-    \includegraphics[width=\linewidth]{diagrams/load_waveform.pdf}
-    \caption{Example wave form for a load being performed by the Verilog code. \JW{Can we say that the load is loading the value DEADBEEF from address 3 into the variable x, just to help the reader make sense of the signals in the timing diagram? }}
-  \end{subfigure}
-  \caption{RAM representation in Verilog and a trace of its execution.}
-\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}.  There are two interesting parts to the memory template that is used for the stack of the main function.  Firstly, the memory updates are triggered on the negative edge of the clock, out of phase with the rest of the design, which is triggered on the positive edge of the clock.  The main advantage is that instead of loads and stores taking three and two clock cycles respectively, they only take two and one clock cycle instead, greatly improving their performance.  In addition to that, using the negative edge for the clock is supported by many synthesis tools, it therefore does not affect the maximum frequency of the final design.  Secondly, the logic in the enable signal of the RAM (\texttt{en != u\_en}) is also atypical.  To make the proof simpler, the goal is to create a RAM which disables itself after every use, so that firstly, the proof can assume that the RAM is disabled at the start and end of every clock cycle, and secondly so that only the state which contains the load and store need to be modified to ensure this property.  Using a simple enable signal, it would not be possible to disable it in the RAM itself, as well as enabling it in the datapath, as this would result in a register being driven twice from two different locations.  We can instead generate a second enable signal that is set by the user, and the original enable signal is then updated by the RAM to be equal to the value that the user set.  This means that the RAM should be enabled whenever the two signals are different, and disabled otherwise.
+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