From 2f2f98e6c2b8d0e74d6f8930633d20b2e5e79678 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Fri, 6 May 2022 16:16:01 +0100 Subject: Fix weird alignment issues --- chapters/hls.tex | 17 ++++++++--------- chapters/scheduling.tex | 12 ++++++------ 2 files changed, 14 insertions(+), 15 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 diff --git a/chapters/scheduling.tex b/chapters/scheduling.tex index 916812c..58528cd 100644 --- a/chapters/scheduling.tex +++ b/chapters/scheduling.tex @@ -291,13 +291,13 @@ next sections. \startfloatcombination[nx=2] \startplacefigure[reference={eq:standard},title={Syntax for instructions within a hyperblock.}] \startframedtext[frame=off,offset=none,width={0.45\textwidth}] - \startformula \startalign + \startformula\startmathalignment \NC i\ \ \eqdef \NC \ \ \text{\tt RBnop} \NR \NC \NC |\ \ \text{\tt RBop}\ p?\ \mathit{op}\ \vec{r}\ d \NR \NC \NC |\ \ \text{\tt RBload}\ p?\ \mathit{chunk}\ \mathit{addr}\ \vec{r}\ d \NR \NC \NC |\ \ \text{\tt RBstore}\ p?\ \mathit{chunk}\ \mathit{addr}\ \vec{r}\ s \NR \NC \NC |\ \ \text{\tt RBsetpred}\ p?\ c\ \vec{r}\ d \NR -\stopalign \stopformula +\stopmathalignment\stopformula \stopframedtext \stopplacefigure @@ -333,11 +333,11 @@ branch on a predicate an nests more control-flow instructions inside of it. This for if-conversion, when converting an already converted conditional statement, as depending on the predicate, a different control-flow instruction may be necessary. -\placeformula[fig:hb_def]\startformula\startalign[align={1:left}] +\placeformula[fig:hb_def]\startformula\startmathalignment[align={1:left}] \NC \blockbb \qquad \eqdef \qquad (\text{\tt slist}\ i) \times i_{\mathit{cf}} \NR \NC \parbb \qquad \eqdef \qquad (\text{\tt slist}\ (\text{\tt plist}\ (\text{\tt slist}\ i))) \times i_{\mathit{cf}}\NR -\stopalign\stopformula +\stopmathalignment\stopformula These instructions are use in \rtlblock\ as well as in \rtlpar. The main difference between these two languages is how these instructions are arranged within the hyperblock and the execution @@ -539,7 +539,7 @@ predicated type and append the first predicated type to the second: \subsection[example-of-translation]{Example of translation} -\placeformula[eq:4]\startformula\startalign[n=1,align={1:left}] +\placeformula[eq:4]\startformula \startmathalignment[n=1,align={1:left}] \NC \text{\tt r1} = \startcases \NC \text{\tt r1}^{0} + \text{\tt r4}^{0} + \text{\tt r4}^{0}, \quad \NC \text{\tt p1} \NR @@ -555,7 +555,7 @@ predicated type and append the first predicated type to the second: \NC \text{\tt !p2 \&\& p1}\NR \NC \text{\tt r3}^{0} \times \text{\tt r3}^{0},\quad \NC\text{\tt p2 \&\& p1}\NR \stopcases\NR -\stopalign \stopformula +\stopmathalignment \stopformula Using the example shown in \in{Figure}[fig:op_chain], the \rtlblock\ hyperblock shown in \in{Figure}{a}[fig:op_chain] is scheduled into the hyperblock \rtlpar\ shown in -- cgit