From b90e207d5a9d1871d5ecde168d39ce91c7691fe1 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Wed, 4 May 2022 20:25:25 +0100
Subject: Finish the pipelining chapter

---
 chapters/hls.tex | 24 +++++++++++++++++-------
 1 file changed, 17 insertions(+), 7 deletions(-)

(limited to 'chapters/hls.tex')

diff --git a/chapters/hls.tex b/chapters/hls.tex
index 90dc238..4090218 100644
--- a/chapters/hls.tex
+++ b/chapters/hls.tex
@@ -782,9 +782,10 @@ inputs for Verilog modules.
 Finally, we use 32-bit integers to represent bitvectors rather than arrays of booleans. This is
 because (currently) only supports types represented by 32 bits.
 
-\subsection[sec:verilog:integrating]{Integrating the Verilog Semantics into 's Model}
+\subsection[sec:verilog:integrating]{Integrating the Verilog Semantics into CompCert's Model}
 
-\startplacemarginfigure
+\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.}]
 \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
@@ -795,13 +796,22 @@ because (currently) only supports types represented by 32 bits.
   \NC\text{\sc Finish }\ \frac{\Gamma_r[\mathit{fin}] = 1}{\text{\tt State}\ \mathit{sf}\ m\ \sigma\
     \Gamma_r\ \Gamma_a \longrightarrow \text{\tt Returnstate}\ \mathit{sf}\ \Gamma_r[ \mathit{ret}]}\NR
 %
-  \NC\text{\sc Call }\ \frac{}{\text{\tt Callstate}\ \mathit{sf}\ m\ \vec{r} \longrightarrow
-    \text{\tt State}\ \mathit{sf}\ m\ n\ ((\text{\tt init\_params}\ \vec{r}\ a)[\sigma \mapsto n, \mathit{fin} \mapsto 0, \mathit{rst} \mapsto 0])\ \epsilon}\NR
+  \NC\text{\sc Call }\ \frac{}{\startmatrix[n=1]
+    \NC\text{\tt Callstate}\ \mathit{sf}\ m\ \vec{r}\longrightarrow\NR
+    \NC
+    \text{\tt State}\ \mathit{sf}\ m\ n\ ((\text{\tt init\_params}\ \vec{r}\ a)[\sigma \mapsto n,
+      \mathit{fin} \mapsto 0, \mathit{rst} \mapsto 0])\ \epsilon \NR
+  \stopmatrix
+}\NR
 %
-  \NC\text{\sc Return }\ \frac{}{\text{\tt Returnstate}\ (\text{\tt Stackframe}\ r\ m\ \mathit{pc}\
-    \Gamma_r\ \Gamma_a :: \mathit{sf})\ v \longrightarrow \text{\tt State}\ \mathit{sf}\ m\ \mathit{pc}\ (\Gamma_{r} [ \sigma \mapsto \mathit{pc}, r \mapsto v ])\ \Gamma_{a}}\NR
+  \NC\text{\sc Return }\ \frac{}{\startmatrix[n=1]
+    \NC\text{\tt Returnstate}\ (\text{\tt Stackframe}\ r\ m\ \mathit{pc}\
+      \Gamma_r\ \Gamma_a :: \mathit{sf})\ v \NR
+    \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
-\stopplacemarginfigure
+\stopplacefigure
 
 The computation model defines a set of states through which execution passes. In this subsection, we
 explain how we extend our Verilog semantics with four special-purpose registers in order to
-- 
cgit