From 68f397d2c94e4ec32d08beb0314e575082010831 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Fri, 20 Nov 2020 12:47:40 +0000
Subject: Modify diagrams

---
 algorithm.tex | 144 ++++++++++++++++++++++++++++++----------------------------
 1 file changed, 74 insertions(+), 70 deletions(-)

(limited to 'algorithm.tex')

diff --git a/algorithm.tex b/algorithm.tex
index 4a31df0..80131dc 100644
--- a/algorithm.tex
+++ b/algorithm.tex
@@ -67,9 +67,9 @@ We select CompCert's three-address code (3AC)\footnote{This is known as register
 
 3AC is also attractive because it is the closest intermediate language to LLVM IR, which is used by several existing HLS compilers. It has an unlimited number of pseudo-registers, and is represented as a control flow graph (CFG) where each instruction is a node with links to the instructions that can follow it. One difference between LLVM IR and 3AC is that 3AC includes operations that are specific to the chosen target architecture; we chose x86\_32 because each instruction maps well to hardware.
 
-\begin{figure}
+\begin{figure*}
   \centering
-  \begin{subfigure}[b]{0.49\linewidth}
+  \begin{subfigure}[b]{0.24\linewidth}
 \begin{minted}{c}
 int main() {
   int x[3] = {1, 2, 3};
@@ -83,7 +83,7 @@ int main() {
 \end{minted}
     \caption{Input C code.}\label{fig:accumulator_c}
   \end{subfigure}\hspace*{-4mm}
-  \begin{subfigure}[b]{0.49\linewidth}
+  \begin{subfigure}[b]{0.24\linewidth}
 \begin{minted}[fontsize=\footnotesize]{c}
 main() {
  15:  x8 = 1
@@ -104,9 +104,77 @@ main() {
 }
 \end{minted}
     \caption{3AC produced by \compcert{}.}\label{fig:accumulator_rtl}
-  \end{subfigure}
+  \end{subfigure}\hfill%
+\begin{subfigure}[b]{0.45\linewidth}
+\begin{minted}[fontsize=\tiny]{verilog}
+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_7,
+             reg_5, reg_3;
+  always @(posedge clk)
+    case (state)
+      32'd15: reg_8 <= 32'd1;
+      32'd14: stack[32'd0] <= reg_8;
+      32'd13: reg_7 <= 32'd2;
+      32'd12: stack[32'd1] <= reg_7;
+      32'd11: reg_6 <= 32'd3;
+      32'd10: stack[32'd2] <= reg_7;
+      32'd9: reg_2 <= 32'd0;
+      32'd8: reg_1 <= 32'd0;
+      32'd7: reg_5 <= 32'd0;
+      32'd6: reg_4 <= stack[{{{reg_5 + 32'd0}
+        + {reg_1 * 32'd4}} / 32'd4}];
+      32'd5: reg_2 <= {reg_2 + {reg_4 + 32'd0}};
+      32'd4: reg_1 <= {reg_1 + 32'd1};
+      32'd3: ;
+      32'd2: reg_3 <= reg_2;
+      32'd1: begin
+        finish = 1'd1;
+        return_val = reg_3;
+      end
+      default:;
+    endcase
+\end{minted}
+    %\caption{Verilog always block describing the datapath of the module.}\label{fig:accumulator_v_1}
+  %\end{subfigure}\hfill%
+  %\begin{subfigure}[b]{0.49\linewidth}
+\vspace*{-63mm}
+\begin{minted}[xleftmargin=44mm, fontsize=\tiny]{verilog}
+  always @(posedge clk)
+    if ({reset == 1'd1})
+      state <= 32'd16;
+    else
+      case (state)
+        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
+\end{minted}
+\caption{Verilog produce by \vericert{}.  The intermediate language HTL is an abstraction that uses maps from states to the Verilog statements instead of case statements.}\label{fig:accumulator_rtl}
+\end{subfigure}
   \caption{Using \compcert{} to translate a simple program from C to three address code (3AC).}\label{fig:accumulator_c_rtl}
-\end{figure}
+\end{figure*}
 
 \subsection{Translating C to Verilog, by example}
 
@@ -233,71 +301,7 @@ have the same size.
 \begin{figure}
   \centering
   %\begin{subfigure}[b]{0.49\linewidth}
-\begin{minted}[fontsize=\tiny]{verilog}
-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_7,
-             reg_5, reg_3;
-  always @(posedge clk)
-    case (state)
-      32'd15: reg_8 <= 32'd1;
-      32'd14: stack[32'd0] <= reg_8;
-      32'd13: reg_7 <= 32'd2;
-      32'd12: stack[32'd1] <= reg_7;
-      32'd11: reg_6 <= 32'd3;
-      32'd10: stack[32'd2] <= reg_7;
-      32'd9: reg_2 <= 32'd0;
-      32'd8: reg_1 <= 32'd0;
-      32'd7: reg_5 <= 32'd0;
-      32'd6: reg_4 <= stack[{{{reg_5 + 32'd0}
-        + {reg_1 * 32'd4}} / 32'd4}];
-      32'd5: reg_2 <= {reg_2 + {reg_4 + 32'd0}};
-      32'd4: reg_1 <= {reg_1 + 32'd1};
-      32'd3: ;
-      32'd2: reg_3 <= reg_2;
-      32'd1: begin
-        finish = 1'd1;
-        return_val = reg_3;
-      end
-      default:;
-    endcase
-\end{minted}
-    %\caption{Verilog always block describing the datapath of the module.}\label{fig:accumulator_v_1}
-  %\end{subfigure}\hfill%
-  %\begin{subfigure}[b]{0.49\linewidth}
-\vspace*{-63mm}
-\begin{minted}[xleftmargin=44mm, fontsize=\tiny]{verilog}
-  always @(posedge clk)
-    if ({reset == 1'd1})
-      state <= 32'd16;
-    else
-      case (state)
-        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
-\end{minted}
+
     %\caption{Verilog always block describing the control logic of the module.}\label{fig:accumulator_v_2}
   %\end{subfigure}
   \caption{Verilog output for our running example, as generated by \vericert{}. The left column contains the datapath and the right column contains the control logic.}\label{fig:accumulator_v}
-- 
cgit 

