various

2 files changed, 257 insertions, 224 deletions

diff --git a/stash.tex b/stash.tex
new file mode 100644
index 0000000..a452c1f
--- /dev/null
+++ b/stash.tex
@@ -0,0 +1,92 @@
+%add (clk, rst, start, a, b, ret, fin) {
+%  input clk, rst, start;
+%  input [31:0] a, b;
+%  output reg [31:0] ret;
+%  output reg fin;
+%  
+%  reg [31:0] reg_4;
+%  reg [31:0] reg_3;
+\begin{figure}
+\begin{lstlisting}
+add (x2, x1) {
+  externctrl { clk -> main.clk }
+  controllogic {
+    2: state <= 1;
+    1: state <= 3;
+    3: ;
+  }
+  datapath {
+    2: reg_3 <= {{x2 + x1} + 0};
+    1: fin = 1;
+       ret = reg_3;
+    3: fin <= 0;
+  }
+}
+\end{lstlisting}
+\caption{Example HTL code (part 1)}
+\label{fig:example_HTL1}
+\end{figure}
+\begin{figure}
+%main (clk, rst, start, ret, fin) {
+%  input clk, rst, start;
+%  output reg [31:0] ret;
+%  output reg fin;
+%  
+%  reg[31:0] reg_1, reg_2, reg_3, reg_4, reg_5, reg_6, reg_7,
+%    add_0_rst, add_0_a, add_0_b, add_0_ret, add_0_fin,
+%    add_1_rst, add_1_a, add_1_b, add_1_ret, add_1_fin;
+\begin{lstlisting}
+main () {
+  externctrl {
+    |\HL2{add\_0\_x2 -> add.param[0];}|
+    |\HL2{add\_0\_x1 -> add.param[1];}|
+    |\HL2{add\_0\_fin -> add.fin;}|
+    |\HL2{add\_0\_rst -> add.rst;}|
+    |\HL2{add\_0\_ret -> add.ret;}|
+    |\HL3{add\_1\_x2 -> add.param[0];}|
+    |\HL3{add\_1\_x1 -> add.param[1];}|
+    |\HL3{add\_1\_fin -> add.fin;}|
+    |\HL3{add\_1\_rst -> add.rst;}|
+    |\HL3{add\_1\_ret -> add.ret;}|
+    |\HL0{clk -> main.clk;}|
+  }
+  controllogic {
+    |\HL1{9: state <= 8;}|
+    |\HL2{8: state <= 7;}|
+    |\HL2{7: state <= 12;}|
+   |\HL2{12: if ({add\_0\_fin == 1}) state <= 6;}|
+    |\HL2{6: state <= 5;}|
+    |\HL3{5: state <= 4;}|
+    |\HL3{4: state <= 10;}|
+   |\HL3{10: if ({add\_1\_fin == 1}) state <= 3;}|
+    |\HL3{3: state <= 2;}|
+    |\HL4{2: state <= 1;}|
+    |\HL4{1: state <= 11;}|
+   |\HL0{11: ;}|
+  }
+  datapath {
+    |\HL1{9: reg\_3 <= 0;}|
+    |\HL2{8: reg\_6 <= 1;}|
+    |\HL2{7: add\_0\_rst <= 1;}|
+       |\HL2{add\_0\_a <= reg\_3;}|
+       |\HL2{add\_0\_b <= reg\_6;}|
+   |\HL2{12: add\_0\_rst <= 0;}|
+       |\HL2{reg\_1 <= add\_0\_ret;}|
+    |\HL2{6: reg\_3 <= reg\_1;}|
+    |\HL3{5: reg\_5 <= 2;}|
+    |\HL3{4: add\_1\_rst <= 1;}|
+       |\HL3{add\_1\_a <= reg\_3;}|
+       |\HL3{add\_1\_b <= reg\_5;}|
+   |\HL3{10: add\_1\_rst <= 0;}|
+       |\HL3{reg\_2 <= add\_1\_ret;}|
+    |\HL3{3: reg\_3 <= reg\_2;}|
+    |\HL4{2: reg\_4 <= reg\_3;}|
+    |\HL4{1: fin = 1;}|
+       |\HL4{ret = reg\_4;}|
+   |\HL0{11: fin <= 0;}|
+  }
+}
+\end{lstlisting}
+\caption{Example HTL code (part 2)}
+\label{fig:example_HTL2}
+\end{figure}
\ No newline at end of file
diff --git a/verified_resource_sharing.tex b/verified_resource_sharing.tex
index 0f7c879..2b9c6da 100644
--- a/verified_resource_sharing.tex
+++ b/verified_resource_sharing.tex
@@ -26,6 +26,7 @@ escapeinside=||,
 \definecolor{highlight2}{HTML}{fcfcdc} % ffffb3
 \definecolor{highlight3}{HTML}{c9c7d6} % bebada
 \definecolor{highlight4}{HTML}{fcc1bb} % fb8072
+\definecolor{highlight5}{HTML}{a9c2d4} % 80b1d3
 
 \newcommand\HL[2]{\colorbox{highlight#1}{\vphantom{A}\smash{#2}}}
 
@@ -104,11 +105,23 @@ In the 3AC language, each function in the program is represented as a numbered l
 
 \section{Implementation of Vericert-Fun}
 
+\tikzset{
+st/.style={draw=black, fill=white, rounded corners, align=left, font=\tt\footnotesize, minimum width=40mm},
+ed/.style={draw, ->},
+exted/.style={draw, thick, dotted, ->, rounded corners},
+lab/.style={anchor=south west, inner sep=1pt, font=\tiny},
+tit/.style={anchor=north west, font=\tt\footnotesize},
+edlab/.style={auto, inner sep=2pt, align=left, font=\tt\footnotesize}
+}
+
 Figure~\ref{fig:example_C} shows a simple C file that we shall employ as a worked example.
 
 \begin{figure}
+\centering
 \begin{lstlisting}
-int add(int a, int b) { |\HL0{return a + b;}| }
+int add(int a, int b) { 
+  |\HL5{return a + b;}| 
+}
 
 int main() {
   |\HL1{int v = 0;}|
@@ -124,119 +137,55 @@ int main() {
 Figure~\ref{fig:example_3AC} shows the 3AC that the CompCert frontend obtains from the C program in Fig.~\ref{fig:example_C}. Highlighting is used to show the correspondence between C instructions and 3AC instructions. \JW{In the HTL, the parameters to add are called a and b, but in the 3AC they're called x2 and x1. Presumably the HTL should use x2 and x1 too, right?}\YH{Yes, I definitely agree}
 
 \begin{figure}
-\begin{lstlisting}
-add (x2, x1) {
-  |\HL0{2: x3 = x2 + x1 + 0 (int)}|
-  |\HL0{1: return x3}|
-}
-main () {
-  |\HL1{9: x3 = 0}|
-  |\HL2{8: x6 = 1}|
-  |\HL2{7: x1 = "add"(x3, x6)}|
-  |\HL2{6: x3 = x1}|
-  |\HL3{5: x5 = 2}|
-  |\HL3{4: x2 = "add"(x3, x5)}|
-  |\HL3{3: x3 = x2}|
-  |\HL4{2: x4 = x3}|
-  |\HL4{1: return x4}|
-}
-\end{lstlisting}
-\caption{Example 3AC code}
+% \begin{lstlisting}
+% add (x2, x1) {
+%   |\HL5{2: x3 = x2 + x1 + 0 (int)}|
+%   |\HL5{1: return x3}|
+% }
+% main () {
+%   |\HL1{9: x3 = 0}|
+%   |\HL2{8: x6 = 1}|
+%   |\HL2{7: x1 = "add"(x3, x6)}|
+%   |\HL2{6: x3 = x1}|
+%   |\HL3{5: x5 = 2}|
+%   |\HL3{4: x2 = "add"(x3, x5)}|
+%   |\HL3{3: x3 = x2}|
+%   |\HL4{2: x4 = x3}|
+%   |\HL4{1: return x4}|
+% }
+% \end{lstlisting}
+\begin{tikzpicture}[node distance=2mm]
+\node[st, fill=highlight5]    (a2) at (0,-1) {x3 = x2 + x1 + 0 (int)};
+\node[st, fill=highlight5, below=of a2] (a1) {return x3};
+\draw[ed] (a2) to (a1);
+\node[tit] at (-2.4,-0.2) (labmain) {add(x2, x1) \{};
+\node[tit] at (-2.4,-1.9) (labmain2) {\}};
+\begin{scope}[yshift=-24mm]
+\node[st, fill=highlight1]    (m9) at (0,-1) {x3 = 0};
+\node[st, fill=highlight2, below=of m9] (m8) {x6 = 1};
+\node[st, fill=highlight2, below=of m8] (m7) {x1 = "add"(x3, x6)};
+\node[st, fill=highlight2, below=of m7] (m6) {x3 = x1};
+\node[st, fill=highlight3, below=of m6] (m5) {x5 = 2};
+\node[st, fill=highlight3, below=of m5] (m4) {x2 = "add"(x3, x5)};
+\node[st, fill=highlight3, below=of m4] (m3) {x3 = x2};
+\node[st, fill=highlight4, below=of m3] (m2) {x4 = x3};
+\node[st, fill=highlight4, below=of m2] (m1) {return x4};
+\draw[ed] (m9) to (m8);
+\draw[ed] (m8) to (m7);
+\draw[ed] (m7) to (m6);
+\draw[ed] (m6) to (m5);
+\draw[ed] (m5) to (m4);
+\draw[ed] (m4) to (m3);
+\draw[ed] (m3) to (m2);
+\draw[ed] (m2) to (m1);
+\node[tit] at (-2.4,-0.2) (labadd) {main() \{};
+\node[tit] at (-2.4,-6.1) (labadd2) {\}};
+\end{scope}
+\end{tikzpicture}
+\caption{Example CFG}
 \label{fig:example_3AC}
 \end{figure}
 
-%add (clk, rst, start, a, b, ret, fin) {
-%  input clk, rst, start;
-%  input [31:0] a, b;
-%  output reg [31:0] ret;
-%  output reg fin;
-%  
-%  reg [31:0] reg_4;
-%  reg [31:0] reg_3;
-\begin{figure}
-\begin{lstlisting}
-add (x2, x1) {
-  externctrl { clk -> main.clk }
-  controllogic {
-    2: state <= 1;
-    1: state <= 3;
-    3: ;
-  }
-  datapath {
-    2: reg_3 <= {{x2 + x1} + 0};
-    1: fin = 1;
-       ret = reg_3;
-    3: fin <= 0;
-  }
-}
-\end{lstlisting}
-\caption{Example HTL code (part 1)}
-\label{fig:example_HTL1}
-\end{figure}
-\begin{figure}
-%main (clk, rst, start, ret, fin) {
-%  input clk, rst, start;
-%  output reg [31:0] ret;
-%  output reg fin;
-%  
-%  reg[31:0] reg_1, reg_2, reg_3, reg_4, reg_5, reg_6, reg_7,
-%    add_0_rst, add_0_a, add_0_b, add_0_ret, add_0_fin,
-%    add_1_rst, add_1_a, add_1_b, add_1_ret, add_1_fin;
-\begin{lstlisting}
-main () {
-  externctrl {
-    |\HL2{add\_0\_x2 -> add.param[0];}|
-    |\HL2{add\_0\_x1 -> add.param[1];}|
-    |\HL2{add\_0\_fin -> add.fin;}|
-    |\HL2{add\_0\_rst -> add.rst;}|
-    |\HL2{add\_0\_ret -> add.ret;}|
-    |\HL3{add\_1\_x2 -> add.param[0];}|
-    |\HL3{add\_1\_x1 -> add.param[1];}|
-    |\HL3{add\_1\_fin -> add.fin;}|
-    |\HL3{add\_1\_rst -> add.rst;}|
-    |\HL3{add\_1\_ret -> add.ret;}|
-    |\HL0{clk -> main.clk;}|
-  }
-  controllogic {
-    |\HL1{9: state <= 8;}|
-    |\HL2{8: state <= 7;}|
-    |\HL2{7: state <= 12;}|
-   |\HL2{12: if ({add\_0\_fin == 1}) state <= 6;}|
-    |\HL2{6: state <= 5;}|
-    |\HL3{5: state <= 4;}|
-    |\HL3{4: state <= 10;}|
-   |\HL3{10: if ({add\_1\_fin == 1}) state <= 3;}|
-    |\HL3{3: state <= 2;}|
-    |\HL4{2: state <= 1;}|
-    |\HL4{1: state <= 11;}|
-   |\HL0{11: ;}|
-  }
-  datapath {
-    |\HL1{9: reg\_3 <= 0;}|
-    |\HL2{8: reg\_6 <= 1;}|
-    |\HL2{7: add\_0\_rst <= 1;}|
-       |\HL2{add\_0\_a <= reg\_3;}|
-       |\HL2{add\_0\_b <= reg\_6;}|
-   |\HL2{12: add\_0\_rst <= 0;}|
-       |\HL2{reg\_1 <= add\_0\_ret;}|
-    |\HL2{6: reg\_3 <= reg\_1;}|
-    |\HL3{5: reg\_5 <= 2;}|
-    |\HL3{4: add\_1\_rst <= 1;}|
-       |\HL3{add\_1\_a <= reg\_3;}|
-       |\HL3{add\_1\_b <= reg\_5;}|
-   |\HL3{10: add\_1\_rst <= 0;}|
-       |\HL3{reg\_2 <= add\_1\_ret;}|
-    |\HL3{3: reg\_3 <= reg\_2;}|
-    |\HL4{2: reg\_4 <= reg\_3;}|
-    |\HL4{1: fin = 1;}|
-       |\HL4{ret = reg\_4;}|
-   |\HL0{11: fin <= 0;}|
-  }
-}
-\end{lstlisting}
-\caption{Example HTL code (part 2)}
-\label{fig:example_HTL2}
-\end{figure}
 
 \begin{figure}
 \begin{tikztimingtable}[timing/d/background/.style={fill=white}, timing/xunit=1em]
@@ -261,32 +210,23 @@ main () {
 \definecolor{background}{HTML}{eeeeee}
 \begin{figure}
 \centering
-\tikzset{
-st/.style={draw=black, fill=white, rounded corners, align=left, font=\tt\footnotesize, minimum width=40mm},
-ed/.style={draw, ->},
-exted/.style={draw, thick, dotted, ->, rounded corners},
-lab/.style={anchor=south west, inner sep=1pt, font=\tiny},
-tit/.style={anchor=north west, font=\tt\footnotesize},
-edlab/.style={auto, inner sep=2pt, align=left, font=\tt\footnotesize},
-node distance=5mm
-}
-\begin{tikzpicture}
-\node[st] (m9) at (0,0) {reg\_3 <= 0;};
-\node[st, below=of m9] (m8) {reg\_6 <= 1;};
-\node[st, below=of m8] (m7) {add.rst <= 1; \\ add.param\_0 <= reg\_3; \\ add.param\_1 <= reg\_6;};
-\node[st, below=of m7] (m12) {add.rst <= 0; \\ reg\_1 <= add.ret;};
-\node[st, below=of m12] (m6) {reg\_3 <= reg\_1;};
-\node[st, below=of m6] (m5) {reg\_5 <= 2;};
-\node[st, below=of m5] (m4) {add.rst <= 1; \\ add.param\_0 <= reg\_3; \\ add.param\_1 <= reg\_5;};
-\node[st, below=of m4] (m10) {add.rst <= 0; \\ reg\_2 <= add.ret;};
-\node[st, below=of m10] (m3) {reg\_3 <= reg\_2;};
-\node[st, below=of m3] (m2) {reg\_4 <= reg\_3;};
-\node[st, below=of m2] (m1) {fin = 1; \\ ret = reg\_4;};
-\node[st, below=of m1] (m11) {fin <= 0;};
-
-\node[st, below=2cm of m11] (a2) {reg\_7 <= \{\{x2 + x1\} + 0\};};
-\node[st, below=of a2] (a1) {fin = 1; \\ ret = reg\_7;};
-\node[st, below=of a1] (a3) {fin <= 0;};
+\begin{tikzpicture}[node distance=5mm]
+\node[st, fill=highlight1] (m9) at (0,0)     {reg\_3 <= 0;};
+\node[st, fill=highlight2, below=of m9] (m8) {reg\_6 <= 1;};
+\node[st, fill=highlight2, below=of m8] (m7) {add.rst <= 1; \\ add.param\_0 <= reg\_3; \\ add.param\_1 <= reg\_6;};
+\node[st, fill=highlight2, below=of m7] (m12) {add.rst <= 0; \\ reg\_1 <= add.ret;};
+\node[st, fill=highlight2, below=of m12] (m6) {reg\_3 <= reg\_1;};
+\node[st, fill=highlight3, below=of m6] (m5)  {reg\_5 <= 2;};
+\node[st, fill=highlight3, below=of m5] (m4) {add.rst <= 1; \\ add.param\_0 <= reg\_3; \\ add.param\_1 <= reg\_5;};
+\node[st, fill=highlight3, below=of m4] (m10) {add.rst <= 0; \\ reg\_2 <= add.ret;};
+\node[st, fill=highlight3, below=of m10] (m3) {reg\_3 <= reg\_2;};
+\node[st, fill=highlight4, below=of m3] (m2)  {reg\_4 <= reg\_3;};
+\node[st, fill=highlight4, below=of m2] (m1)  {fin = 1; \\ ret = reg\_4;};
+\node[st, fill=highlight4, below=of m1] (m11) {fin <= 0;};
+
+\node[st, fill=highlight5, above=40mm of m9] (a2) {reg\_7 <= \{\{x2 + x1\} + 0\};};
+\node[st, fill=highlight5, below=of a2] (a1) {fin = 1; \\ ret = reg\_7;};
+\node[st, fill=highlight5, below=of a1] (a3) {fin <= 0;};
 
 \draw[ed] (m9) to node[edlab] {!rst} (m8);
 \draw[ed] (m8) to node[edlab] {!rst} (m7);
@@ -330,101 +270,18 @@ node distance=5mm
   \node[lab] at (m\i.north west) {\i};
 \foreach\i in {1,2,3}
   \node[lab] at (a\i.north west) {\i};
-  
 
-
-\draw[exted] (m7.west) -- ++(-9mm,0) |- ([yshift=-1mm]a2.west);
-\draw[exted] (m4.west) -- ++(-7mm,0) |- ([yshift=1mm]a2.west);
-\draw[exted] ([yshift=-1mm]a3.east) -- ++(18mm,0) |- (m6.east);
-\draw[exted] ([yshift=1mm]a3.east) -- ++(16mm,0) |- (m3.east);
+\draw[exted] (m7.west) -- ++(-7mm,0) |- ([yshift=-1mm]a2.west);
+\draw[exted] (m4.west) -- ++(-9mm,0) |- ([yshift=1mm]a2.west);
+\draw[exted] ([yshift=-1mm]a3.east) -- ++(16mm,0) |- (m6.east);
+\draw[exted] ([yshift=1mm]a3.east) -- ++(18mm,0) |- (m3.east);
 
 \end{tikzpicture}
 \caption{Two FSMDs. A few points to make: (1) the dotted lines don't mean anything, and are just indicative of how control moves between the state machines, (2) meaning of the asterisk.}
 \label{fig:fsmds}
 \end{figure}
 
-\begin{figure}
-% NB: reg_3 renamed to reg_7
-\begin{lstlisting}
-module main (clk, rst, ret, fin) {
-  reg add_rst, add_fin;
-  reg[31:0] add_ret, add_x2, add_x1, reg_7, add_state;
-  
-  always @(posedge clk) // control logic for "add"
-    if ({add_rst == 1}) begin 
-      add_state <= 2; 
-      add_fin <= 0; 
-    end else begin 
-      case (add_state)
-        2: add_state <= 1;
-        1: add_state <= 3;
-        3: ;
-        default: ;
-      endcase
-    end   
-    
-  always @(posedge clk) // datapath for "add"    
-    case (add_state)
-      2: reg_7 <= {{add_x2 + add_x1} + 0};
-      1: add_fin = 1;
-         add_ret = reg_7;
-      3: add_fin <= 0;
-    endcase
-    
-  input clk, rst, start;
-  output reg [31:0] ret;
-  output reg fin;
-  reg[31:0] state; 
-  reg[31:0] reg_1, reg_2, reg_3, reg_4, reg_5, reg_6;
-  
-  always @(posedge clk) // control logic for "main"
-    if ({rst == 1}) begin 
-      state <= 9; 
-      fin <= 0; 
-    end else begin
-      case (state)
-        |\HL1{9: state <= 8;}|
-        |\HL2{8: state <= 7;}|
-        |\HL2{7: state <= 12;}|
-       |\HL2{12: if ({add\_fin == 1}) state <= 6;}|
-        |\HL2{6: state <= 5;}|
-        |\HL3{5: state <= 4;}|
-        |\HL3{4: state <= 10;}|
-       |\HL3{10: if ({add\_fin == 1}) state <= 3;}|
-        |\HL3{3: state <= 2;}|
-        |\HL4{2: state <= 1;}|
-        |\HL4{1: state <= 11;}|
-       |\HL0{11: ;}|
-      endcase
-    end
 
-  always @(posedge clk) // datapath for "main"
-    case (state)
-      |\HL1{9: reg\_3 <= 0;}|
-      |\HL2{8: reg\_6 <= 1;}|
-      |\HL2{7: add\_rst <= 1;}|
-         |\HL2{add\_x2 <= reg\_3;}|
-         |\HL2{add\_x1 <= reg\_6;}|
-     |\HL2{12: add\_rst <= 0;}|
-         |\HL2{reg\_1 <= add\_ret;}|
-      |\HL2{6: reg\_3 <= reg\_1;}|
-      |\HL3{5: reg\_5 <= 2;}|
-      |\HL3{4: add\_rst <= 1;}|
-         |\HL3{add\_x2 <= reg\_3;}|
-         |\HL3{add\_x1 <= reg\_5;}|
-     |\HL3{10: add\_rst <= 0;}|
-         |\HL3{reg\_2 <= add\_ret;}|
-      |\HL3{3: reg\_3 <= reg\_2;}|
-      |\HL4{2: reg\_4 <= reg\_3;}|
-      |\HL4{1: fin = 1;}|
-         |\HL4{ret = reg\_4;}|
-     |\HL0{11: fin <= 0;}|
-    endcase
-endmodule
-\end{lstlisting}
-\caption{Example Verilog code}
-\label{fig:example_Verilog}
-\end{figure}
 
 \begin{figure}
 \begin{tikzpicture}[yscale=-1]
@@ -500,6 +357,90 @@ A few points that we might want to answer at some point:
 \end{itemize}
 
 
+\appendix
+
+\begin{figure}
+% NB: reg_3 renamed to reg_7
+\begin{lstlisting}
+module main (clk, rst, ret, fin)
+  input clk, rst;
+  output reg [31:0] ret;
+  output reg fin;
+  reg[31:0] state, reg_1, reg_2, reg_3, reg_4, reg_5, reg_6;
+  reg add_rst, add_fin; 
+  reg[31:0] add_ret, add_x2, add_x1, reg_7, add_state;
+  
+  always @(posedge clk) // control logic for "add"
+    if ({add_rst == 1}) begin 
+      add_state <= 2; add_fin <= 0; 
+    end else begin 
+      case (add_state)
+        |\HL5{2: add\_state <= 1;}|
+        |\HL5{1: add\_state <= 3;}|
+        3: ;
+        default: ;
+      endcase
+    end   
+    
+  always @(posedge clk) // datapath for "add"    
+    case (add_state)
+      |\HL5{2: reg\_7 <= {{add\_x2 + add\_x1} + 0};}|
+      |\HL5{1: add\_fin = 1;}|
+         |\HL5{add\_ret = reg\_7;}|
+      3: add_fin <= 0;
+    endcase
+
+  always @(posedge clk) // control logic for "main"
+    if ({rst == 1}) begin 
+      state <= 9; fin <= 0; 
+    end else begin
+      case (state)
+        |\HL1{9: state <= 8;}|
+        |\HL2{8: state <= 7;}|
+        |\HL2{7: state <= 12;}|
+       |\HL2{12: if ({add\_fin == 1}) state <= 6;}|
+        |\HL2{6: state <= 5;}|
+        |\HL3{5: state <= 4;}|
+        |\HL3{4: state <= 10;}|
+       |\HL3{10: if ({add\_fin == 1}) state <= 3;}|
+        |\HL3{3: state <= 2;}|
+        |\HL4{2: state <= 1;}|
+        |\HL4{1: state <= 11;}|
+       |\HL0{11: ;}|
+      endcase
+    end
+
+  always @(posedge clk) // datapath for "main"
+    case (state)
+      |\HL1{9: reg\_3 <= 0;}|
+      |\HL2{8: reg\_6 <= 1;}|
+      |\HL2{7: add\_rst <= 1;}|
+         |\HL2{add\_x2 <= reg\_3;}|
+         |\HL2{add\_x1 <= reg\_6;}|
+     |\HL2{12: add\_rst <= 0;}|
+         |\HL2{reg\_1 <= add\_ret;}|
+      |\HL2{6: reg\_3 <= reg\_1;}|
+      |\HL3{5: reg\_5 <= 2;}|
+      |\HL3{4: add\_rst <= 1;}|
+         |\HL3{add\_x2 <= reg\_3;}|
+         |\HL3{add\_x1 <= reg\_5;}|
+     |\HL3{10: add\_rst <= 0;}|
+         |\HL3{reg\_2 <= add\_ret;}|
+      |\HL3{3: reg\_3 <= reg\_2;}|
+      |\HL4{2: reg\_4 <= reg\_3;}|
+      |\HL4{1: fin = 1;}|
+         |\HL4{ret = reg\_4;}|
+     |\HL0{11: fin <= 0;}|
+    endcase
+endmodule
+\end{lstlisting}
+\caption{Example Verilog code}
+\label{fig:example_Verilog}
+\end{figure}
+
+
+
+
 \bibliographystyle{ACM-Reference-Format}
 \bibliography{references}