Added more to RTL

1 files changed, 14 insertions, 1 deletions

diff --git a/main.tex b/main.tex
index 43c7852..2f44d77 100644
--- a/main.tex
+++ b/main.tex
@@ -264,7 +264,20 @@ RTL function definitions are a sequence of instructions encoded in a control-flo
 
 \subsection{HTL}
 
-RTL is first translated to an intermediate language called hardware transfer language (HTL), which is a finite state machine with datapath (FSMD) representation of the RTL code.  HTL, like all CompCert intermediate languages, has the same program structure as RTL, but internal functions now contain logic to control the order of execution, and a datapath that transforms the data in the registers.  This is represented by having two maps that link states to the control logic and to the current position in the datapath, which are both expressed using Verilog statements.
+RTL is first translated to an intermediate language called hardware transfer language (HTL), which is a finite state machine with datapath (FSMD) representation of the RTL code.  HTL, like all CompCert intermediate languages, has the same program structure as RTL, but internal functions now contain logic to control the order of execution, and a datapath that transforms the data in the registers.  This is represented by having two maps that link states to the control logic and to the current position in the datapath, which are both expressed using Verilog statements.  The syntax for HTL functions are the following:
+
+\begin{align*}
+  \mathit{g} \quad &::= \quad n \mapsto s\\
+  \mathit{d_{r}} \quad &::= \quad r \mapsto (io? * n)\\
+  \mathit{d_{a}} \quad &::= \quad r \mapsto (io? * n * n)\\
+  \mathit{F} \quad &::= \quad \big\{\ \mathtt{params} : \vec{r}\\
+                                     &\mathtt{datapath} : g\\
+                                     &\mathtt{controllogic} : g\\
+                                     &\mathtt{entrypoint} : n\\
+                                     &\mathtt{st, stk, finish, return, start, reset, clk} : r\\
+                                     &\mathtt{scldecls} : d_{r}\\
+                                     &\mathtt{arrdecls} : d_{a}\ \big\}
+\end{align*}
 
 \subsection{HLS Algorithm}