From 7be20e38762d6588e94b6318bd038d1558447e2a Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Fri, 6 May 2022 15:35:46 +0100
Subject: Fix final reference issue

---
 chapters/hls.tex | 18 +++++++++++++-----
 1 file 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
-- 
cgit