From ab17a1a71f174115bd16759b8fbd21fddc2fda03 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Fri, 6 May 2022 15:00:06 +0100 Subject: Fix some of the maths --- chapters/hls.tex | 46 +++++++++++++++++++++++++++------------------- figures/timing-1.pdf | Bin 26407 -> 26407 bytes figures/timing-2.pdf | Bin 26760 -> 26760 bytes figures/timing-3.pdf | Bin 23394 -> 23394 bytes fonts_env.tex | 8 ++++---- lsr_env.tex | 2 ++ 6 files changed, 33 insertions(+), 23 deletions(-) diff --git a/chapters/hls.tex b/chapters/hls.tex index 1a5374c..6a86107 100644 --- a/chapters/hls.tex +++ b/chapters/hls.tex @@ -791,8 +791,9 @@ because Vericert (currently) only supports types represented by 32 bits. \subsection[sec:verilog:integrating]{Integrating the Verilog Semantics into CompCert's Model} -\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.}] +\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] \NC\text{\sc Step }\ \frac{\startmatrix[n=1] \NC \Gamma_r[\mathit{rst}] = 0 \qquad \Gamma_r[\mathit{fin}] = 0 \NR @@ -853,13 +854,13 @@ and $\mathit{ret}$ respectively. \desc{stack} The function stack can be modelled as a RAM block, which is implemented using an array in the module, and denoted as $\mathit{stk}$. -\in{Figure}[fig:inference_module] shows the inference rules for moving -between the computational states. The first, {\sc Step}, is the normal rule of execution. It defines -one step in the \type{State} state, assuming that the module is not being reset, that the finish -state has not been reached yet, that the current and next state are $v$ and $v'$, and that the -module runs from state $\Gamma$ to $\Gamma'$ using the {\sc Step} rule. The {\sc Finish} rule -returns the final value of running the module and is applied when the $\mathit{fin}$ register is -set; the return value is then taken from the $\mathit{ret}$ register. +\in{Figure}[fig:inference_module] shows the inference rules for moving between the computational +states. The first, {\sc Step}, is the normal rule of execution. It defines one step in the +\type{State} state, assuming that the module is not being reset, that the finish state has not been +reached yet, that the current and next state are $v$ and $v'$, and that the module runs from state +$\Gamma$ to $\Gamma'$ using the {\sc Step} rule. The {\sc Finish} rule returns the final value of +running the module and is applied when the $\mathit{fin}$ register is set; the return value is then +taken from the $\mathit{ret}$ register. Note that there is no step from \type{State} to \type{Callstate}; this is because function calls are not supported, and it is therefore impossible in our semantics ever to reach a \type{Callstate} @@ -1014,16 +1015,17 @@ Verilog and CompCert's existing intermediate languages. Together, these differences mean that translating 3AC directly to Verilog is infeasible, as the differences in the semantics are too large. Instead, HTL, which was introduced in -\in{Section}[sec:design], bridges the gap in the semantics between the two languages. HTL still +\in{Section}[sec:hls:design], bridges the gap in the semantics between the two languages. HTL still consists of maps, like many of the other CompCert languages, but each state corresponds to a Verilog statement. \subsection[formulating-the-correctness-theorem]{Formulating the Correctness Theorem} -The main correctness theorem is analogous to that stated in ~: for all Clight source programs $C$, -if the translation to the target Verilog code succeeds, $\mathit{Safe}(C)$ holds and the target -Verilog has behaviour $B$ when simulated, then $C$ will have the same behaviour $B$. -$\mathit{Safe}(C)$ means all observable behaviours of $C$ are safe, which can be defined as +The main correctness theorem is analogous to that stated in +CompCert~\cite{leroy09_formal_verif_realis_compil}: for all Clight source programs $C$, if the +translation to the target Verilog code succeeds, $\mathit{Safe}(C)$ holds and the target Verilog has +behaviour $B$ when simulated, then $C$ will have the same behaviour $B$. $\mathit{Safe}(C)$ means +all observable behaviours of $C$ are safe, which can be defined as $\forall B,\ C \Downarrow B \implies B \in \text{\tt Safe}$. A behaviour is in \type{Safe} if it is either a final state (in the case of convergence) or divergent, but it cannot \quote{go wrong}. (This means that the source program must not contain undefined behaviour.) In , a @@ -1033,8 +1035,12 @@ supported in , this trace will always be empty. Whenever the translation from $C$ succeeds and produces Verilog $V$, and all observable behaviours of $C$ are safe, then $V$ has behaviour $B$ only if $C$ has behaviour $B$. -\placeformula\startformula \forall C, V, B,\quad \text{\tt HLS} (C) = \text{\tt OK} (V) \land -\mathit{Safe}(C) \implies (V \Downarrow B \implies C \Downarrow B). \stopformula +\placeformula\startformula + \startalign[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 +\stopformula Why is this correctness theorem also the right one for HLS? It could be argued that hardware inherently runs forever and therefore does not produce a definitive final result. This would mean @@ -1105,9 +1111,11 @@ instruction $i$ should translate to. The other parameters are the special regist Section~\goto{{[}sec:verilog:integrating{]}}[sec:verilog:integrating]. An example of a rule describing the translation of an arithmetic/logical operation from 3AC is the following: -\startformula \text{\sc Iop}{\text{\tt tr\_op}\ \mathit{op}\ \vec{a} = \text{\tt OK}\ e}{\text{\tt - spec\_instr}\ \mathit{fin}\ \mathit{ret}\ \sigma\ \mathit{stk}\ (\text{\tt Iop}\ \mathit{op}\ - \vec{a}\ d\ n)\ (d\ \text{\tt <=}\ e)\ (\sigma\ \text{\tt <=}\ n)} \stopformula +\startformula + \text{\sc Iop}\ \frac{\text{\tt tr\_op}\ \mathit{op}\ \vec{a} = \text{\tt OK}\ e}{\text{\tt spec\_instr}\ + \mathit{fin}\ \mathit{ret}\ \sigma\ \mathit{stk}\ (\text{\tt Iop}\ \mathit{op}\ \vec{a}\ d\ n)\ + (d\ \text{\tt <=}\ e)\ (\sigma\ \text{\tt <=}\ n)} +\stopformula Assuming that the translation of the operator $\mathit{op}$ with operands $\vec{a}$ is successful and results in expression $e$, the rule describes how the destination register $d$ is updated to $e$ diff --git a/figures/timing-1.pdf b/figures/timing-1.pdf index 8591313..24f8edd 100644 Binary files a/figures/timing-1.pdf and b/figures/timing-1.pdf differ diff --git a/figures/timing-2.pdf b/figures/timing-2.pdf index 67b3a8e..36075c6 100644 Binary files a/figures/timing-2.pdf and b/figures/timing-2.pdf differ diff --git a/figures/timing-3.pdf b/figures/timing-3.pdf index dd18ea9..68f4cf8 100644 Binary files a/figures/timing-3.pdf and b/figures/timing-3.pdf differ diff --git a/fonts_env.tex b/fonts_env.tex index 157d4f3..313a2ea 100644 --- a/fonts_env.tex +++ b/fonts_env.tex @@ -18,10 +18,10 @@ \definefallbackfamily[lsrfont][math][modern][range={uppercasescript,lowercasescript}] \starttypescript [lsrfont] - \definetypeface [lsrfont] [rm] [serif] [palatino] [default] - \definetypeface [lsrfont] [ss] [sans] [heros] [default] - \definetypeface [lsrfont] [tt] [mono] [modern] [default] - \definetypeface [lsrfont] [mm] [math] [eulernova] [default] + \definetypeface [lsrfont] [rm] [serif] [palatino] [default] + \definetypeface [lsrfont] [ss] [sans] [heros] [default] + \definetypeface [lsrfont] [tt] [mono] [modern] [default] + \definetypeface [lsrfont] [mm] [math] [palatino] [default] \stoptypescript \stopenvironment diff --git a/lsr_env.tex b/lsr_env.tex index 01a549b..5073992 100644 --- a/lsr_env.tex +++ b/lsr_env.tex @@ -21,6 +21,8 @@ style=\rm, ] +\placebookmarks[chapter,section,subsection] + \usecolors[crayola] %\placebookmarks[chapter,section,subsection,subsubsection][chapter,section] %\setupinteractionscreen[option=bookmark] -- cgit