diff options
Diffstat (limited to 'chapters/hls.tex')
| -rw-r--r-- | chapters/hls.tex | 17 |
1 files changed, 8 insertions, 9 deletions
diff --git a/chapters/hls.tex b/chapters/hls.tex index b4f75d6..7e1f79e 100644 --- a/chapters/hls.tex +++ b/chapters/hls.tex @@ -804,7 +804,7 @@ because Vericert (currently) only supports types represented by 32 bits. \startplacefigure[reference={fig:inference_module},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] +\startformula \startmathalignment[n=1] \NC\text{\sc Step }\ \frac{\startmatrix[n=1] \NC \Gamma_r[\mathit{rst}] = 0 \qquad \Gamma_r[\mathit{fin}] = 0 \NR \NC(m, (\Gamma_r, \Gamma_a))\ \downarrow_{\text{program}} (\Gamma_r', \Gamma_a') \NR @@ -828,7 +828,7 @@ because Vericert (currently) only supports types represented by 32 bits. \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 +\stopmathalignment \stopformula \stopplacefigure The CompCert computation model defines a set of states through which execution passes. In this @@ -879,11 +879,11 @@ execution; likewise, the {\sc Return} rule is only matched for the final return function. Therefore, in addition to the rules shown in \in{Figure}[fig:inference_module], an initial state and final state need to be defined: -\placeformula\startformula \startalign[n=1] +\placeformula\startformula\startmathalignment[n=1] \NC\text{\sc Initial }\ \frac{\text{\tt is\_internal}\ P.\text{\tt main}}{\text{\tt initial\_state}\ (\text{\tt Callstate}\ []\ P.\text{\tt main}\ [])}\NR \NC\text{\sc Final }\ \frac{}{\text{\tt final\_state}\ (\text{\tt Returnstate}\ []\ n)\ n}\NR -\stopalign \stopformula +\stopmathalignment\stopformula \noindent where the initial state is the \type{Callstate} with an empty stack frame and no arguments for the \type{main} function of program $P$, where this \type{main} function needs to be in the @@ -1046,10 +1046,10 @@ Whenever the translation from $C$ succeeds and produces Verilog $V$, and all obs of $C$ are safe, then $V$ has behaviour $B$ only if $C$ has behaviour $B$. \placeformula\startformula - \startalign[n=1,align={1:right}] + \startmathalignment[n=1,align={1:right}] \NC \forall C, V, B,\quad \text{\tt HLS} (C) = \text{\tt OK} (V) \land \mathit{Safe}(C) \NR \NC \implies (V \Downarrow B \implies C \Downarrow B). \NR - \stopalign + \stopmathalignment \stopformula Why is this correctness theorem also the right one for HLS? It could be argued that hardware @@ -1204,7 +1204,7 @@ matching state. \startplacefigure[reference={fig:htl_ram_spec},title={Specification for the memory implementation in HTL, where $r$ is the RAM, which is then implemented by equivalent Verilog code.}] - \startformula \startalign[n=1] + \startformula \startmathalignment[n=1] \NC \text{\sc Idle}\ \frac{\Gamma_{\rm r}[\mathit{r.en}] = \Gamma_{\rm r}[\mathit{r.u_{en}}]}{((\Gamma_{\rm r}, \Gamma_{\rm a}), \Delta, r) \downarrow_{\text{ram}} \Delta}\NR % \NC \text{\sc Load}\ \frac{\Gamma_{\rm r}[\mathit{r.en}] \ne \Gamma_{\rm @@ -1221,7 +1221,7 @@ matching state. \mathit{r.u\_en}], \NR \NC \Delta_{\rm a}[\mathit{r.mem} \mapsto (\Gamma_{\rm a}[ \mathit{r.mem}])[\mathit{r.addr} \mapsto \mathit{r.d_{in}}]]\NR\stopmatrix\right) } \NR - \stopalign \stopformula + \stopmathalignment \stopformula \stopplacefigure HTL can only represent a single state machine, so we must model the RAM abstractly to reason about @@ -1300,7 +1300,6 @@ converted. \startformula \forall h, V, B \in \text{\tt Safe},\quad \text{\tt tr\_verilog} (h) = V \land h \Downarrow B \implies V \Downarrow B. - \stopformula \stoplemma |