diff options
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 |