Merge branch 'master' of git.ymhg.org:private/formal_hls

1 files changed, 32 insertions, 32 deletions

diff --git a/presentation/presentation.org b/presentation/presentation.org
index 97d7baa..3786da0 100644
--- a/presentation/presentation.org
+++ b/presentation/presentation.org
@@ -305,7 +305,7 @@ Current progress: fully verified HLS tool for a subset of C.
 Support for: all *control flow*, *fixedpoint*, *non-recursive functions* and *local arrays/structs/unions*.
 
 * Example
-** Example: RTL :B_frame:
+** Example: 3AC :B_frame:
 
 *** Code example :B_column:
 :PROPERTIES:
@@ -333,7 +333,7 @@ int main() {
 :BEAMER_ACT: <2>
 :END:
 
-- *three address code (RTL)* instructions are represented as a control-flow graph (CFG).
+- *three address code (3AC)* instructions are represented as a control-flow graph (CFG).
 - Each instruction links to the next one.
 
 *** Text :B_column:
@@ -350,7 +350,7 @@ int main() {
 
 Example of a very simple program performing loads and stores.
 
-**** RTL Code 5 :B_onlyenv:
+**** 3AC Code 5 :B_onlyenv:
 :PROPERTIES:
 :BEAMER_env: onlyenvNH
 :BEAMER_ACT: <2>
@@ -370,7 +370,7 @@ main() {
 }
 #+end_src
 
-** Example: HTL Overview
+** Example: HTL Overview :noexport:
 
 The representation of the *finite state-machine with datapath (FSMD)* is abstract and called **HTL**.
 
@@ -401,7 +401,7 @@ Record module: Type := mkmodule {
   }.
 #+end_src
 
-** Example: Translation (RTL $\rightarrow$ HTL)
+** Example: Translation (3AC $\rightarrow$ HTL)
 
 Translation from *control-flow graph (CFG)* into a *finite state-machine with datapath (FSMD)*.
 
@@ -410,7 +410,7 @@ Translation from *control-flow graph (CFG)* into a *finite state-machine with da
 
 #+attr_beamer: :overlay <+->
 - *Control-flow* is translated into a *finite state-machine*.
-- Each *RTL instructions* translated into equivalent *Verilog statements*.
+- Each *3AC instructions* translated into equivalent *Verilog statements*.
 - Function *stack* implemented as *RAM*.
 - Pointers for loads and stores translated to RAM addresses.
   - *Byte* addressed to *word* addressed.
@@ -630,7 +630,7 @@ endmodule
 - Control logic is translated into another case statement with a reset.
 
 * Verification
-** Verilog Syntax :noexport:
+** Verilog Syntax
 
 *** Column 1 :B_column:
 :PROPERTIES:
@@ -873,7 +873,7 @@ where
 \end{align*}
 #+end_export
 
-** RTL $\to$ HTL: Build a Specification :noexport:
+** 3AC $\to$ HTL: Build a Specification :noexport:
 
 Assuming $\yhfunction{HLS} (C) = \yhconstant{OK} (V)$ requires reasoning about implementation details.
 
@@ -890,7 +890,7 @@ Instead we build a model of the translation which we can use.
 
 #+beamer: \pause
 
-*** RTL to HTL operator conversion :B_example:
+*** 3AC to HTL operator conversion :B_example:
 :PROPERTIES:
 :BEAMER_env: example
 :BEAMER_ACT: <2->
@@ -902,7 +902,7 @@ Instead we build a model of the translation which we can use.
 \end{equation*}
 #+end_export
 
-** RTL $\to$ HTL: Prove Forward Simulation :noexport:
+** 3AC $\to$ HTL: Prove Forward Simulation :noexport:
 
 *** Column 1
 :PROPERTIES:
@@ -952,9 +952,9 @@ Prove the simulation diagram correct:
 #+beamer: \pause
 
 #+attr_beamer: :overlay <+->
-- Assuming an initial match between the RTL state $S_1$ and Verilog state $R_1$,
+- Assuming an initial match between the 3AC state $S_1$ and Verilog state $R_1$,
 - there exists 1 or more steps in Verilog,
-- such that after 1 step in RTL, the resulting states match.
+- such that after 1 step in 3AC, the resulting states match.
 
 * Results
 
@@ -1176,8 +1176,8 @@ Many optimisations missing:
 
 Currently implemented two new languages for it:
 
-- ~RTLBlock~ :: RTL with basic blocks.
-- ~RTLPar~ :: RTL with basic blocks made up of parallel constructs.
+- ~3ACBlock~ :: 3AC with basic blocks.
+- ~3ACPar~ :: 3AC with basic blocks made up of parallel constructs.
 
 #+beamer: \vspace{1.5em}
 
@@ -1187,7 +1187,7 @@ Currently implemented two new languages for it:
 :BEAMER_OPT: 10cm
 :END:
 
-**** RTLBlock Basic Block
+**** 3ACBlock Basic Block
 :PROPERTIES:
 :BEAMER_ACT: 2
 :BEAMER_env: onlyenv
@@ -1223,8 +1223,8 @@ Inductive instr: Type :=
 \scalebox{0.8}{\begin{tikzpicture}
   \begin{scope}
     \node[draw,minimum width=3cm,minimum height=1cm,align=center] (imstranslation) at (1.5,2) {\small\texttt{\textcolor{functioncolour}{Iterative Modulo}}\\\small\texttt{\textcolor{functioncolour}{Scheduling}}};
-    \node[draw,ellipse] (input) at (-1.5,2) {\small\texttt{RTLBlock}};
-    \node[draw,ellipse] (output) at (5,2) {\small\texttt{RTLBlock}};
+    \node[draw,ellipse] (input) at (-1.5,2) {\small\texttt{3ACBlock}};
+    \node[draw,ellipse] (output) at (5,2) {\small\texttt{3ACBlock}};
     \draw[->] (input) -- (imstranslation);
     \draw[->] (imstranslation) -- (output);
       \visible<2->{\node[draw,minimum width=3cm,minimum height=1cm,align=center] (verification) at (1.5,0.5) {\small Equivalence\\\small Check};%
@@ -1234,11 +1234,11 @@ Inductive instr: Type :=
       \draw[->] ($(verification.south) - (0.5,0)$) -- (error);%
       \node at (0.3,-0.5) {\footnotesize\texttt{\textcolor{keywordcolour}{false}}};%
       \node at (2,-0.3) {\footnotesize\texttt{\textcolor{keywordcolour}{true}}};%
-      \node[draw,ellipse] (ok) at (5,-0.5) {\small\texttt{\textcolor{constantcolour}{OK}(RTLBlock)}};%
+      \node[draw,ellipse] (ok) at (5,-0.5) {\small\texttt{\textcolor{constantcolour}{OK}(3ACBlock)}};%
       \draw[->] (verification) |- (ok);}
 
       \visible<3->{\node[draw,minimum width=3cm,minimum height=1cm,align=center] (schedtranslation) at (9.5,-0.5) {\small\texttt{\textcolor{functioncolour}{Resource Constrained}}\\\small\texttt{\textcolor{functioncolour}{Scheduling}}};%
-    \node[draw,ellipse] (schedoutput) at (13,-0.5) {\small\texttt{RTLPar}};%
+    \node[draw,ellipse] (schedoutput) at (13,-0.5) {\small\texttt{3ACPar}};%
     \draw[->] (ok) -- (schedtranslation);%
     \draw[->] (schedtranslation) -- (schedoutput);%
       \node[draw,minimum width=3cm,minimum height=1cm,align=center] (schedverification) at (9.5,-2) {\small Equivalence\\\small Check};%
@@ -1248,7 +1248,7 @@ Inductive instr: Type :=
       \draw[->] ($(schedverification.south) - (0.5,0)$) -- (schederror);%
       \node at (8.3,-3) {\footnotesize\texttt{\textcolor{keywordcolour}{false}}};%
       \node at (10,-2.8) {\footnotesize\texttt{\textcolor{keywordcolour}{true}}};%
-      \node[draw,ellipse] (ok) at (13,-3) {\small\texttt{\textcolor{constantcolour}{OK}(RTLPar)}};%
+      \node[draw,ellipse] (ok) at (13,-3) {\small\texttt{\textcolor{constantcolour}{OK}(3ACPar)}};%
       \draw[->] (schedverification) |- (ok);}
   \end{scope}
 \end{tikzpicture}}
@@ -1773,11 +1773,11 @@ r_{3}^{0} + r_{3}^{0} + r_{4}^{0} \stackrel{?}{=} r_{3}^{0} + r_{3}^{0} + r_{4}^
     \fill[formalhls,rounded corners=3pt] (-1,-1.5) rectangle (9,-2.5);
     \node[language] at (0,0) (clight) {Clight};
     \node[language] at (2,0) (cminor) {C\#minor};
-    \node[language] at (4,0) (rtl) {RTL};
+    \node[language] at (4,0) (rtl) {3AC};
     \node[language] at (6,0) (ltl) {LTL};
     \node[language] at (8,0) (ppc) {PPC};
-    \node[language] at (2,-2) (acblock) {\small RTLBlock};
-    \node[language] at (4,-2) (acpar) {\small RTLPar};
+    \node[language] at (2,-2) (acblock) {\small 3ACBlock};
+    \node[language] at (4,-2) (acpar) {\small 3ACPar};
     \node[language] at (6,-2) (dfgstmd) {HTL};
     \node[language] at (8,-2) (verilog) {Verilog};
     \node at (0,1) {CompCert};
@@ -1796,7 +1796,7 @@ r_{3}^{0} + r_{3}^{0} + r_{4}^{0} \stackrel{?}{=} r_{3}^{0} + r_{3}^{0} + r_{4}^
 
 #+beamer: \vspace{1em}
 
-Add two more passes, from *RTLBlock* $\rightarrow$ *RTLBlock* and from *RTLBlock* to *RTLPar*.
+Add two more passes, from *3ACBlock* $\rightarrow$ *3ACBlock* and from *3ACBlock* to *3ACPar*.
 
 ** About Iterative Modulo Scheduling
 
@@ -2073,7 +2073,7 @@ int main() {
 
 Example of simple loop accumulating values in array.
 
-**** RTL Code 2 :B_onlyenv:
+**** 3AC Code 2 :B_onlyenv:
 :PROPERTIES:
 :BEAMER_env: onlyenvNH
 :BEAMER_ACT: <2>
@@ -2100,7 +2100,7 @@ main() {
 }
 #+end_src
 
-**** RTL Code 3 :B_onlyenv:
+**** 3AC Code 3 :B_onlyenv:
 :PROPERTIES:
 :BEAMER_env: onlyenvNH
 :BEAMER_ACT: <3>
@@ -2127,7 +2127,7 @@ main() {
 }
 #+end_src
 
-**** RTL Code 4 :B_onlyenv:
+**** 3AC Code 4 :B_onlyenv:
 :PROPERTIES:
 :BEAMER_env: onlyenvNH
 :BEAMER_ACT: <4>
@@ -2154,7 +2154,7 @@ main() {
 }
 #+end_src
 
-**** RTL Code 5 :B_onlyenv:
+**** 3AC Code 5 :B_onlyenv:
 :PROPERTIES:
 :BEAMER_env: onlyenvNH
 :BEAMER_ACT: <5>
@@ -2181,7 +2181,7 @@ main() {
 }
 #+end_src
 
-**** RTL Code 6 :B_onlyenv:
+**** 3AC Code 6 :B_onlyenv:
 :PROPERTIES:
 :BEAMER_env: onlyenvNH
 :BEAMER_ACT: <6>
@@ -2208,7 +2208,7 @@ main() {
 }
 #+end_src
 
-**** RTL Code 7 :B_onlyenv:
+**** 3AC Code 7 :B_onlyenv:
 :PROPERTIES:
 :BEAMER_env: onlyenvNH
 :BEAMER_ACT: <7>
@@ -2235,7 +2235,7 @@ main() {
 }
 #+end_src
 
-**** RTL Code 8 :B_onlyenv:
+**** 3AC Code 8 :B_onlyenv:
 :PROPERTIES:
 :BEAMER_env: onlyenvNH
 :BEAMER_ACT: <8>
@@ -2262,7 +2262,7 @@ main() {
 }
 #+end_src
 
-**** RTL Code 9 :B_onlyenv:
+**** 3AC Code 9 :B_onlyenv:
 :PROPERTIES:
 :BEAMER_env: onlyenvNH
 :BEAMER_ACT: <9>