diff options
author | Yann Herklotz <git@yannherklotz.com> | 2022-05-06 15:35:46 +0100 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2022-05-06 15:35:46 +0100 |
commit | 7be20e38762d6588e94b6318bd038d1558447e2a (patch) | |
tree | 6a5dbd7dc08d41d9966136f3054ba4f73c381ab6 | |
parent | f6add5b74e9ec6e251d8c744d3084f5b869f8d48 (diff) | |
download | lsr22_fvhls-7be20e38762d6588e94b6318bd038d1558447e2a.tar.gz lsr22_fvhls-7be20e38762d6588e94b6318bd038d1558447e2a.zip |
Fix final reference issue
-rw-r--r-- | chapters/hls.tex | 18 |
1 files changed, 13 insertions, 5 deletions
diff --git a/chapters/hls.tex b/chapters/hls.tex index ad2b32c..71a4c1b 100644 --- a/chapters/hls.tex +++ b/chapters/hls.tex @@ -100,7 +100,7 @@ tools, such as Kiwi~\cite{greaves08_kiwi}, and LLHD~\cite{schuiki20_llhd} has be as an intermediate language for hardware design, but neither are suitable for us because they lack formal semantics. -\startplacefigure[title={Vericert as a Verilog back end to CompCert.}] +\startplacefigure[reference={fig:rtlbranch},title={Vericert as a Verilog back end to CompCert.}] \hbox{\starttikzpicture [language/.style={fill=white,rounded corners=3pt,minimum height=7mm}, continuation/.style={}, linecount/.style={rounded corners=3pt,dashed}] @@ -707,8 +707,12 @@ $v$. Finally, the following rule dictates how the whole module runs in one clock cycle: \placeformula\startformula \text{\sc Module }\ \frac{(\Gamma, \epsilon, \vec{m})\ - \downarrow_{\text{module}} (\Gamma', \Delta')}{\left(\Gamma, \startmatrix\NC\text{\tt module}\ \text{\tt main} - \text{\tt (...);}\NR\NC\vec{m}\NR\NC \text{\tt endmodule}\NR\stopmatrix\right) \downarrow_{\text{program}} (\Gamma'\ //\ + \downarrow_{\text{module}} (\Gamma', \Delta')}{\left(\Gamma, + \startmatrix[align={1:left}] + \NC\text{\tt module}\ \text{\tt main} \text{\tt (...);}\NR + \NC\quad\vec{m}\NR + \NC\text{\tt endmodule}\NR + \stopmatrix\right) \downarrow_{\text{program}} (\Gamma'\ //\ \Delta')} \stopformula where $\Gamma$ is the initial state of all the variables, $\epsilon$ is the empty map because the @@ -759,8 +763,12 @@ rule shown below: \startmatrix (\NC \Gamma, \epsilon, \vec{m})\ \downarrow_{\text{module}^{+}} (\Gamma', \Delta') \NR\NC (\Gamma'\ //\ \Delta', \epsilon, \vec{m}) - \downarrow_{\text{module}^{-}} (\Gamma'', \Delta'')\NR\stopmatrix}{\left(\Gamma, \startmatrix\NC\text{\tt module}\ \text{\tt main} - \text{\tt (...);}\NR\NC\vec{m}\NR\NC \text{\tt endmodule}\NR\stopmatrix\right) \downarrow_{\text{program}} (\Gamma''\ //\ + \downarrow_{\text{module}^{-}} (\Gamma'', \Delta'')\NR\stopmatrix}{\left(\Gamma, + \startmatrix[align={1:left}] + \NC\text{\tt module}\ \text{\tt main} \text{\tt (...);}\NR + \NC\quad\vec{m}\NR + \NC\text{\tt endmodule}\NR + \stopmatrix\right) \downarrow_{\text{program}} (\Gamma''\ //\ \Delta'')} \stopformula The main execution of the module $\downarrow_{\text{module}}$ is split into |