diff options
author | Yann Herklotz <git@yannherklotz.com> | 2022-05-04 20:25:25 +0100 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2022-05-04 20:25:25 +0100 |
commit | b90e207d5a9d1871d5ecde168d39ce91c7691fe1 (patch) | |
tree | 5ee4b9fc86ac03edc9220c3cebbc316b4f37d830 /chapters/hls.tex | |
parent | 428e424b75999eda16f5c5ccb4ee48763d99c9d1 (diff) | |
download | lsr22_fvhls-b90e207d5a9d1871d5ecde168d39ce91c7691fe1.tar.gz lsr22_fvhls-b90e207d5a9d1871d5ecde168d39ce91c7691fe1.zip |
Finish the pipelining chapter
Diffstat (limited to 'chapters/hls.tex')
-rw-r--r-- | chapters/hls.tex | 24 |
1 files changed, 17 insertions, 7 deletions
diff --git a/chapters/hls.tex b/chapters/hls.tex index 90dc238..4090218 100644 --- a/chapters/hls.tex +++ b/chapters/hls.tex @@ -782,9 +782,10 @@ inputs for Verilog modules. Finally, we use 32-bit integers to represent bitvectors rather than arrays of booleans. This is because (currently) only supports types represented by 32 bits. -\subsection[sec:verilog:integrating]{Integrating the Verilog Semantics into 's Model} +\subsection[sec:verilog:integrating]{Integrating the Verilog Semantics into CompCert's Model} -\startplacemarginfigure +\startplacefigure[title={Top-level semantics used in CompCert to initiate the first call to + \type{main} and well as return the final result of the \type{main} function.}] \startformula \startalign[n=1] \NC\text{\sc Step }\ \frac{\startmatrix[n=1] \NC \Gamma_r[\mathit{rst}] = 0 \qquad \Gamma_r[\mathit{fin}] = 0 \NR @@ -795,13 +796,22 @@ because (currently) only supports types represented by 32 bits. \NC\text{\sc Finish }\ \frac{\Gamma_r[\mathit{fin}] = 1}{\text{\tt State}\ \mathit{sf}\ m\ \sigma\ \Gamma_r\ \Gamma_a \longrightarrow \text{\tt Returnstate}\ \mathit{sf}\ \Gamma_r[ \mathit{ret}]}\NR % - \NC\text{\sc Call }\ \frac{}{\text{\tt Callstate}\ \mathit{sf}\ m\ \vec{r} \longrightarrow - \text{\tt State}\ \mathit{sf}\ m\ n\ ((\text{\tt init\_params}\ \vec{r}\ a)[\sigma \mapsto n, \mathit{fin} \mapsto 0, \mathit{rst} \mapsto 0])\ \epsilon}\NR + \NC\text{\sc Call }\ \frac{}{\startmatrix[n=1] + \NC\text{\tt Callstate}\ \mathit{sf}\ m\ \vec{r}\longrightarrow\NR + \NC + \text{\tt State}\ \mathit{sf}\ m\ n\ ((\text{\tt init\_params}\ \vec{r}\ a)[\sigma \mapsto n, + \mathit{fin} \mapsto 0, \mathit{rst} \mapsto 0])\ \epsilon \NR + \stopmatrix +}\NR % - \NC\text{\sc Return }\ \frac{}{\text{\tt Returnstate}\ (\text{\tt Stackframe}\ r\ m\ \mathit{pc}\ - \Gamma_r\ \Gamma_a :: \mathit{sf})\ v \longrightarrow \text{\tt State}\ \mathit{sf}\ m\ \mathit{pc}\ (\Gamma_{r} [ \sigma \mapsto \mathit{pc}, r \mapsto v ])\ \Gamma_{a}}\NR + \NC\text{\sc Return }\ \frac{}{\startmatrix[n=1] + \NC\text{\tt Returnstate}\ (\text{\tt Stackframe}\ r\ m\ \mathit{pc}\ + \Gamma_r\ \Gamma_a :: \mathit{sf})\ v \NR + \NC\longrightarrow \text{\tt State}\ \mathit{sf}\ m\ \mathit{pc}\ (\Gamma_{r} [ \sigma \mapsto + \mathit{pc}, r \mapsto v ])\ \Gamma_{a}\NR + \stopmatrix}\NR \stopalign \stopformula -\stopplacemarginfigure +\stopplacefigure The computation model defines a set of states through which execution passes. In this subsection, we explain how we extend our Verilog semantics with four special-purpose registers in order to |