Make figures fit onto the page

6 files changed, 100 insertions, 31 deletions

diff --git a/algorithm.tex b/algorithm.tex
index 908f488..1068076 100644
--- a/algorithm.tex
+++ b/algorithm.tex
@@ -39,11 +39,11 @@ Existing HLS compilers usually use LLVM IR as an intermediate representation whe
 
 \begin{figure}
   \centering
-  \begin{subfigure}[b]{0.4\linewidth}
+  \begin{subfigure}[b]{0.5\linewidth}
     \inputminted{c}{data/accumulator.c}
     \caption{Accumulator C code.}\label{fig:accumulator_c}
   \end{subfigure}%
-  \begin{subfigure}[b]{0.6\linewidth}
+  \begin{subfigure}[b]{0.5\linewidth}
     \inputminted[fontsize=\footnotesize]{c}{data/accumulator.rtl}
     \caption{Accumulator RTL code.}\label{fig:accumulator_rtl}
   \end{subfigure}
@@ -53,11 +53,11 @@ Existing HLS compilers usually use LLVM IR as an intermediate representation whe
 \begin{figure}
   \centering
   \begin{subfigure}[b]{0.5\linewidth}
-    \inputminted[fontsize=\tiny]{systemverilog}{data/accumulator.htl}
+    \inputminted[fontsize=\tiny]{systemverilog}{data/accumulator1.v}
     \caption{Accumulator HTL code.}\label{fig:accumulator_htl}
   \end{subfigure}%
   \begin{subfigure}[b]{0.5\linewidth}
-    \inputminted[fontsize=\tiny]{systemverilog}{data/accumulator.v}
+    \inputminted[fontsize=\tiny]{systemverilog}{data/accumulator2.v}
     \caption{Accumulator Verilog code.}\label{fig:accumulator_v}
   \end{subfigure}
   \caption{Accumulator example using CompCert to translate from HTL to Verilog.\YH{I feel like these examples take up too much space, but don't really know of a different way to show off a complete example without the long code.}}\label{fig:accumulator_htl_v}
diff --git a/data/accumulator.c b/data/accumulator.c
index 7d78a61..007ae2b 100644
--- a/data/accumulator.c
+++ b/data/accumulator.c
@@ -1,7 +1,9 @@
 int main() {
     int x[3] = {1, 2, 3};
     int sum = 0, incr = 1;
-    for (int i = 0; i < 3; i=i+incr)
+    for (int i = 0;
+         i < 3;
+         i=i+incr)
         sum += x[i];
     return sum;
 }
diff --git a/data/accumulator.rtl b/data/accumulator.rtl
index a6b528c..bf0af2f 100644
--- a/data/accumulator.rtl
+++ b/data/accumulator.rtl
@@ -1,18 +1,18 @@
 main() {
-   16:	x9 = 1
-   15:	int32[stack(0)] = x9
-   14:	x8 = 2
-   13:	int32[stack(4)] = x8
-   12:	x7 = 3
-   11:	int32[stack(8)] = x7
-   10:	x3 = 0
-    9:	nop
-    8:	x1 = 0
-    7:	x6 = stack(0) (int)
-    6:	x5 = int32[x6 + x1 * 4 + 0]
-    5:	x3 = x3 + x5 + 0 (int)
-    4:	x1 = x1 + 1 (int)
-    3:	if (x1 <s 3) goto 7 else goto 2
-    2:	x4 = x3
-    1:	return x4
+6: x9 = 1
+5: int32[stack(0)] = x9
+4: x8 = 2
+3: int32[stack(4)] = x8
+2: x7 = 3
+1: int32[stack(8)] = x7
+0: x3 = 0
+9: nop
+8: x1 = 0
+7: x6 = stack(0) (int)
+6: x5 = int32[x6 + x1 * 4 + 0]
+5: x3 = x3 + x5 + 0 (int)
+4: x1 = x1 + 1 (int)
+3: if (x1 <s 3) goto 7 else goto 2
+2: x4 = x3
+1: return x4
 }
diff --git a/data/accumulator1.v b/data/accumulator1.v
new file mode 100644
index 0000000..5e9637a
--- /dev/null
+++ b/data/accumulator1.v
@@ -0,0 +1,32 @@
+module main(reset, clk, finish, return_val);
+  reg [31:0] stack [2:0];
+  input [0:0] clk, reset;
+  output reg [31:0] return_val;
+  output reg [0:0] finish;
+  reg [31:0] reg_8, reg_4, state,
+             reg_6, reg_1, reg_9,
+             reg_5, reg_3, reg_7;
+  always @(posedge clk)
+    case (state)
+      32'd16: reg_9 <= 32'd1;
+      32'd15: stack[32'd0] <= reg_9;
+      32'd14: reg_8 <= 32'd2;
+      32'd13: stack[32'd1] <= reg_8;
+      32'd12: reg_7 <= 32'd3;
+      32'd11: stack[32'd2] <= reg_7;
+      32'd10: reg_3 <= 32'd0;
+      32'd9: ;
+      32'd8: reg_1 <= 32'd0;
+      32'd7: reg_6 <= 32'd0;
+      32'd6: reg_5 <= stack[{{{reg_6 + 32'd0}
+        + {reg_1 * 32'd4}} / 32'd4}];
+      32'd5: reg_3 <= {reg_3 + {reg_5 + 32'd0}};
+      32'd4: reg_1 <= {reg_1 + 32'd1};
+      32'd3: ;
+      32'd2: reg_4 <= reg_3;
+      32'd1: begin
+        finish = 1'd1;
+        return_val = reg_4;
+      end
+      default:;
+    endcase
diff --git a/data/accumulator2.v b/data/accumulator2.v
new file mode 100644
index 0000000..c7bcc59
--- /dev/null
+++ b/data/accumulator2.v
@@ -0,0 +1,26 @@
+always @(posedge clk)
+    if ({reset == 1'd1})
+      state <= 32'd16;
+    else
+      case (state)
+        32'd16: state <= 32'd15;
+        32'd15: state <= 32'd14;
+        32'd14: state <= 32'd13;
+        32'd13: state <= 32'd12;
+        32'd12: state <= 32'd11;
+        32'd11: state <= 32'd10;
+        32'd10: state <= 32'd9;
+        32'd9: state <= 32'd8;
+        32'd8: state <= 32'd7;
+        32'd7: state <= 32'd6;
+        32'd6: state <= 32'd5;
+        32'd5: state <= 32'd4;
+        32'd4: state <= 32'd3;
+        32'd3: state <=
+          ({$signed(reg_1) < $signed(32'd3)}
+             ? 32'd7 : 32'd2);
+        32'd2: state <= 32'd1;
+        32'd1: ;
+        default:;
+      endcase
+endmodule
diff --git a/proof.tex b/proof.tex
index 850e225..58a5417 100644
--- a/proof.tex
+++ b/proof.tex
@@ -27,8 +27,10 @@ As HTL is quite different to RTL, this first translation is the most involved tr
 \begin{figure}
   \centering
 \begin{minted}{coq}
-Inductive match_states : RTL.state -> HTL.state -> Prop :=
-| match_state : forall asa asr sf f sp sp' rs mem m st res
+Inductive match_states :
+  RTL.state -> HTL.state -> Prop :=
+| match_state : forall asa asr sf f sp
+    sp' rs mem m st res
     (MASSOC : match_assocmaps f rs asr)
     (TF : tr_module f m)
     (WF : state_st_wf m (HTL.State res m st asr asa))
@@ -36,17 +38,24 @@ Inductive match_states : RTL.state -> HTL.state -> Prop :=
     (MARR : match_arrs m f sp mem asa)
     (SP : sp = Values.Vptr sp' (Integers.Ptrofs.repr 0))
     (RSBP : reg_stack_based_pointers sp' rs)
-    (ASBP : arr_stack_based_pointers sp' mem (f.(RTL.fn_stacksize)) sp)
+    (ASBP : arr_stack_based_pointers sp' mem
+              (f.(RTL.fn_stacksize)) sp)
     (BOUNDS : stack_bounds sp (f.(RTL.fn_stacksize)) mem)
     (CONST : match_constants m asr),
-    match_states (RTL.State sf f sp st rs mem) (HTL.State res m st asr asa)
-| match_returnstate :
-    forall v v' stack mem res (MF : match_frames stack res),
-      val_value_lessdef v v' ->
-      match_states (RTL.Returnstate stack v mem) (HTL.Returnstate res v')
+    match_states
+      (RTL.State sf f sp st rs mem)
+      (HTL.State res m st asr asa)
+| match_returnstate : forall v v' stack mem res
+    (MF : match_frames stack res),
+    val_value_lessdef v v' ->
+    match_states
+      (RTL.Returnstate stack v mem)
+      (HTL.Returnstate res v')
 | match_initial_call :
-    forall f m m0 (TF : tr_module f m),
-      match_states (RTL.Callstate nil (AST.Internal f) nil m0) (HTL.Callstate nil m nil).
+  forall f m m0 (TF : tr_module f m),
+    match_states
+      (RTL.Callstate nil (AST.Internal f) nil m0)
+      (HTL.Callstate nil m nil).
 \end{minted}
   \caption{\texttt{match\_states} predicate used to match an RTL state to the equivalent HTL state.}\label{fig:match_states}
 \end{figure}