diff options
| -rw-r--r-- | verified_resource_sharing.tex | 28 |
1 files changed, 17 insertions, 11 deletions
diff --git a/verified_resource_sharing.tex b/verified_resource_sharing.tex index 903a7d5..861fa21 100644 --- a/verified_resource_sharing.tex +++ b/verified_resource_sharing.tex @@ -80,20 +80,22 @@ In the 3AC language, each function in the program is represented as a numbered l \section{Rough notes} + + \begin{figure} \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(fun1) at (1.5,2) {function}; +\node(fun2) at (0,2) {function}; +\node[anchor=west](C) at (-2,2) {\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[anchor=west](TAC) at (-2,3) {\bf 3AC:}; \node(FSMD) at (0.75,5) {FSMD}; -\node[anchor=west](HTL) at (-2.5,5) {\bf HTL}; +\node[anchor=west](HTL) at (-2,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); +\node[anchor=west](Verilog) at (-2,6) {\bf Verilog:}; +\draw[->] (fun1) to node [auto] {CompCert frontend} (CFG1); \draw[->] (fun2) to (CFG2); \draw[->] (CFG1) to node [auto, pos=0.2] {inlining} (CFG); \draw[->] (CFG2) to (CFG); @@ -104,18 +106,22 @@ In the 3AC language, each function in the program is represented as a numbered l \label{fig:vericert_flow} \begin{tikzpicture}[yscale=-1] -\node(fun1) at (1.5,1.5) {function}; -\node(fun2) at (0,1.5) {function}; +\node(fun1) at (1.5,2) {function}; +\node(fun2) at (0,2) {function}; +\node[anchor=west](C) at (-2,2) {\bf C:}; \node(CFG1) at (1.5,3) {CFG}; \node(CFG2) at (0,3) {CFG}; +\node[anchor=west](TAC) at (-2,3) {\bf 3AC:}; \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[anchor=west](HTL) at (-2,4) {\bf HTL:}; \node(module) at (0.75,6) {module}; -\draw[->] (fun1) to node [auto, align=left] {CompCert \\ frontend} (CFG1); +\node[anchor=west](Verilog) at (-2,6) {\bf Verilog:}; +\draw[->] (fun1) to node [auto] {CompCert frontend} (CFG1); \draw[->] (fun2) to (CFG2); -\draw[->] (CFG1) to node [auto] {FSMD generation} (FSMD1); +\draw[->] (CFG1) to node [auto] {FSMDE generation} (FSMD1); \draw[->] (CFG2) to (FSMD2); \draw[->, dashed] (FSMD1) to node [auto] {renaming} (FSMD3); \draw[->, dashed] (FSMD2) to (FSMD4); |