diff options
Diffstat (limited to 'chapters/hls.tex')
-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 |