diff options
Diffstat (limited to 'algorithm.tex')
| -rw-r--r-- | algorithm.tex | 20 |
1 files changed, 10 insertions, 10 deletions
diff --git a/algorithm.tex b/algorithm.tex index 45d3a42..6811137 100644 --- a/algorithm.tex +++ b/algorithm.tex @@ -55,16 +55,16 @@ RTL function definitions are a sequence of instructions encoded in a control-flo 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\} + g \quad &::= \quad n \mapsto s\\ + d_{r} \quad &::= \quad r \mapsto (io? * n)\\ + d_{a} \quad &::= \quad r \mapsto (io? * n * n)\\ + F \quad &::= \quad \big\{\ \texttt{params} : \vec{r}\\ + &\texttt{datapath} : g\\ + &\texttt{controllogic} : g\\ + &\texttt{entrypoint} : n\\ + &\texttt{st, stk, finish, return, start, reset, clk} : r\\ + &\texttt{scldecls} : d_{r}\\ + &\texttt{arrdecls} : d_{a}\ \big\} \end{align*} \subsection{HLS Algorithm} |