From 1814e21f8541ca37058ec494cda63f8985ce15a8 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Tue, 16 Jun 2020 01:00:34 +0100
Subject: Added more to RTL

---
 main.tex | 15 ++++++++++++++-
 1 file changed, 14 insertions(+), 1 deletion(-)

(limited to 'main.tex')

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}
 
-- 
cgit 

