work on flow diagram

1 files changed, 41 insertions, 36 deletions

diff --git a/verified_resource_sharing.tex b/verified_resource_sharing.tex
index 5f6684f..903a7d5 100644
--- a/verified_resource_sharing.tex
+++ b/verified_resource_sharing.tex
@@ -81,44 +81,49 @@ In the 3AC language, each function in the program is represented as a numbered l
 \section{Rough notes}
 
 \begin{figure}
-\subcaptionbox{\label{fig:flow:compcert}}{
-\begin{tikzpicture}
-\node[anchor=west](C) at (0.4,0) {C};
-\node(TAC) at (4,0) {3AC};
-\node[anchor=east](Asm) at (8,0) {Assembly};
-\draw[->] (C) to node [auto] {CompCert frontend} (TAC);
-\draw[->] (TAC) to [loop above] node [auto] {selective inlining} (TAC);
-\draw[->] (TAC) to (Asm);
+\begin{tikzpicture}[yscale=-1]
+\node(fun1) at (1.5,1.5) {function};
+\node(fun2) at (0,1.5) {function};
+\node[anchor=west](C) at (-2.5,1.5) {\bf C};
+\node(CFG1) at (1.5,3) {CFG};
+\node(CFG2) at (0,3) {CFG};
+\node(CFG) at (0.75,4) {CFG};
+\node[anchor=west](TAC) at (-2.5,3) {\bf 3AC};
+\node(FSMD) at (0.75,5) {FSMD};
+\node[anchor=west](HTL) at (-2.5,5) {\bf HTL};
+\node(module) at (0.75,6) {module};
+\node[anchor=west](Verilog) at (-2.5,6) {\bf Verilog};
+\draw[->] (fun1) to node [auto, align=left] {CompCert \\ frontend} (CFG1);
+\draw[->] (fun2) to (CFG2);
+\draw[->] (CFG1) to node [auto, pos=0.2] {inlining} (CFG);
+\draw[->] (CFG2) to (CFG);
+\draw[->] (CFG) to node [auto] {FSMD generation} (FSMD);
+\draw[->] (FSMD) to node [auto] {Verilog generation} (module);
 \end{tikzpicture}
-}
-\subcaptionbox{\label{fig:flow:vericert}}{
-\begin{tikzpicture}
-\node[anchor=west](C2) at (0.4,0) {C};
-\node(TAC2) at (4,0) {3AC};
-\node(HTL) at (5.5,0) {HTL};
-\node[anchor=east](Verilog) at (8,0) {Verilog};
-\draw[->] (C2) to node [auto] {CompCert frontend} (TAC2);
-\draw[->] (TAC2) to [loop above] node [auto] {full inlining} (TAC2);
-\draw[->] (TAC2) to (HTL);
-\draw[->] (HTL) to (Verilog);
+\caption{Key compilation passes and intermediate languages in Vericert~\cite{vericert}}
+\label{fig:vericert_flow}
+
+\begin{tikzpicture}[yscale=-1]
+\node(fun1) at (1.5,1.5) {function};
+\node(fun2) at (0,1.5) {function};
+\node(CFG1) at (1.5,3) {CFG};
+\node(CFG2) at (0,3) {CFG};
+\node(FSMD1) at (1.5,4) {FSMDE};
+\node(FSMD2) at (0,4) {FSMDE};
+\node(FSMD3) at (1.5,5) {FSMDE};
+\node(FSMD4) at (0,5) {FSMDE};
+\node(module) at (0.75,6) {module};
+\draw[->] (fun1) to node [auto, align=left] {CompCert \\ frontend} (CFG1);
+\draw[->] (fun2) to (CFG2);
+\draw[->] (CFG1) to node [auto] {FSMD generation} (FSMD1);
+\draw[->] (CFG2) to (FSMD2);
+\draw[->, dashed] (FSMD1) to node [auto] {renaming} (FSMD3);
+\draw[->, dashed] (FSMD2) to (FSMD4);
+\draw[->, dashed] (FSMD3) to node [auto, pos=0.2] {Verilog generation} (module);
+\draw[->, dashed] (FSMD4) to (module);
 \end{tikzpicture}
-}
-
-\subcaptionbox{\label{fig:flow:vericertfun}}{
-\begin{tikzpicture}
-\node[anchor=west](C3) at (0.4,0) {C};
-\node(TAC3) at (4,0) {3AC};
-\node(HTL3) at (5.5,0) {HTL};
-\node[anchor=east](Verilog3) at (8,0) {Verilog};
-\draw[->] (C3) to node [auto] {CompCert frontend} (TAC3);
-\draw[->] (TAC3) to [loop above] node [auto] {selective inlining} (TAC3);
-\draw[->] (TAC3) to (HTL3);
-\draw[->, dashed] (HTL3) to (Verilog3);
-\end{tikzpicture}
-}
-
-\caption{Key compilation passes and intermediate languages in (a) CompCert~\cite{compcert}, (b) Vericert~\cite{vericert}, and (c) Vericert-Fun (this paper). Dashed arrows indicate passes that have been implemented but not verified.}
-\label{fig:flow}
+\caption{Key compilation passes and intermediate languages in Vericert-Fun, with dashed arrows indicating passes that have been implemented but not verified}
+\label{fig:vericert-fun_flow}
 \end{figure}