From 2fa27381a18e65b4af2d860dc9be17489ff26258 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Mon, 27 Jun 2022 15:01:51 +0100
Subject: Add changes

---
 chapters/hls.tex | 34 ++++++++++++++++------------------
 1 file changed, 16 insertions(+), 18 deletions(-)

(limited to 'chapters/hls.tex')

diff --git a/chapters/hls.tex b/chapters/hls.tex
index 0be3f99..8a75fee 100644
--- a/chapters/hls.tex
+++ b/chapters/hls.tex
@@ -484,7 +484,7 @@ making it easier to prove optimisations like proper RAM insertion.
 \stoptikzpicture
 \stopplacemarginfigure
 
-\paragraph{Translating memory} Typically, HLS-generated hardware consists of a sea of registers and
+\paragraph{Translating memory.} Typically, HLS-generated hardware consists of a sea of registers and
 RAMs.  This memory view is very different from the C memory model, so we perform the following
 translation from CompCert's abstract memory model to a concrete RAM.  Variables that do not have
 their address taken are kept in registers, which correspond to the registers in 3AC.  All
@@ -500,17 +500,15 @@ and would instead implement it using many registers.  This interface is shown on
 Verilog code in \in{Figure}{a}[fig:accumulator_c_rtl].  A high-level overview of the architecture
 and of the RAM interface can be seen in \in{Figure}[fig:accumulator_diagram].
 
-\paragraph{Translating instructions}
-
-Most 3AC instructions correspond to hardware constructs.  For example, line 2 in
-\in{Figure}{d}[fig:accumulator_c_rtl] shows a 32-bit register \type{x5} being initialised to 3,
-after which the control flow moves execution to line 3. This initialisation is also encoded in the
-Verilog generated from HTL at state 8 in both the control logic and data-path always-blocks, shown
-at lines 33 and 16 respectively in \in{Figure}{a}[fig:accumulator_c_rtl].  Simple operator
-instructions are translated in a similar way.  For example, the add instruction is just translated
-to the built-in add operator, similarly for the multiply operator.  All 32-bit instructions can be
-translated in this way, but some special instructions require extra care. One such instruction is
-the \type{Oshrximm} instruction, which is discussed further in
+\paragraph{Translating instructions.} Most 3AC instructions correspond to hardware constructs.  For
+example, line 2 in \in{Figure}{d}[fig:accumulator_c_rtl] shows a 32-bit register \type{x5} being
+initialised to 3, after which the control flow moves execution to line 3. This initialisation is
+also encoded in the Verilog generated from HTL at state 8 in both the control logic and data-path
+always-blocks, shown at lines 33 and 16 respectively in \in{Figure}{a}[fig:accumulator_c_rtl].
+Simple operator instructions are translated in a similar way.  For example, the add instruction is
+just translated to the built-in add operator, similarly for the multiply operator.  All 32-bit
+instructions can be translated in this way, but some special instructions require extra care. One
+such instruction is the \type{Oshrximm} instruction, which is discussed further in
 \in{Section}[sec:algorithm:optimisation:oshrximm].  Another is the \type{Oshldimm} instruction,
 which is a left rotate instruction that has no Verilog equivalent and therefore has to be
 implemented in terms of other operations and proven to be equivalent.  The only 32-bit instructions
@@ -983,12 +981,12 @@ in the hardware itself.
 \stoptikzpicture}
 \stopplacefigure
 
-This translation is represented in \in{Section}[fig:memory_model_transl].  defines a map from blocks
-to maps from memory addresses to memory contents. Each block represents an area in memory; for
-example, a block can represent a global variable or a stack for a function. As there are no global
-variables, the main stack can be assumed to be block 0, and this is the only block we
-translate. Meanwhile, our Verilog semantics defines two finite arrays of optional values, one for
-the blocking assignments map $\Gamma_{\rm a}$ and one for the nonblocking assignments map
+This translation is represented in \in{Figure}[fig:memory_model_transl].  CompCert's memory model
+defines a map from blocks to maps from memory addresses to memory contents. Each block represents an
+area in memory; for example, a block can represent a global variable or a stack for a function. As
+there are no global variables, the main stack can be assumed to be block 0, and this is the only
+block we translate. Meanwhile, our Verilog semantics defines two finite arrays of optional values,
+one for the blocking assignments map $\Gamma_{\rm a}$ and one for the nonblocking assignments map
 $\Delta_{\rm a}$. The optional values are present to ensure correct merging of the two association
 maps at the end of the clock cycle. The invariant used in the proofs is that block 0 should be
 equivalent to the merged representation of the $\Gamma_{\rm a}$ and $\Delta_{\rm a}$ maps.
-- 
cgit 

