From c3ab05db6ae028cb06d7695c9c574042dc5ccdb2 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Fri, 15 Apr 2022 22:54:27 +0100
Subject: Some more tweaking

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

(limited to 'chapters/hls.tex')

diff --git a/chapters/hls.tex b/chapters/hls.tex
index fbaf41a..6bc6c60 100644
--- a/chapters/hls.tex
+++ b/chapters/hls.tex
@@ -51,9 +51,11 @@ function calls, non-32-bit integers, floats, and global variables.
 
 \paragraph{Companion material.} Vericert is fully open source and available on GitHub at
 
+\blank[big]
 \startalignment[center]
   \goto{\hyphenatedurl{https://github.com/ymherklotz/vericert}}[url(https://github.com/ymherklotz/vericert)].
 \stopalignment
+\blank[big]
 
 A snapshot of the Vericert development is also available in a Zenodo
 repository~\cite{yann_herklotz_2021_5093839}.
@@ -742,22 +744,22 @@ operator, which gives priority to the right-hand operand in a conflict. This rul
 nonblocking assignments overwrite at the end of the clock cycle any blocking assignments made during
 the cycle.
 
-\subsection[title={Changes to the
-Semantics},reference={changes-to-the-semantics}]
+\subsection[title={Changes to the Semantics},reference={changes-to-the-semantics}]
 
 Five changes were made to the semantics proposed by to make it suitable as an HLS target.
 
-\subsubsection[title={Adding array
-support},reference={adding-array-support}]
+\subsubsection[title={Adding array support},reference={adding-array-support}]
 
 The main change is the addition of support for arrays, which are needed to model RAM in Verilog. RAM
 is needed to model the stack in C efficiently, without having to declare a variable for each
 possible stack location. Consider the following Verilog code:
 
+\blank[big]
 \starthlverilog
 reg [31:0] x[1:0];
 always @(posedge clk) begin x[0] = 1; x[1] <= 1; end
 \stophlverilog
+\blank[big]
 
 which modifies one array element using blocking assignment and then a second using nonblocking
 assignment. If the existing semantics were used to update the array, then during the merge, the
@@ -1000,14 +1002,13 @@ fragment we consider, we can actually reformulate the correctness theorem above
 simulation result (following standard practice), which makes it easier to prove. To prove this
 forward simulation, it suffices to prove forward simulations between each pair of consecutive
 intermediate languages, as these results can be composed to prove the correctness of the whole HLS
-tool. The forward simulation from 3AC to HTL is stated in Lemma~\goto{{[}lemma:htl{]}}[lemma:htl]
-(Section~\goto{1.3}[sec:proof:3ac_htl]), the forward simulation for the RAM insertion is shown in
-Lemma~\goto{{[}lemma:htl_ram{]}}[lemma:htl_ram] (Section~\goto{1.4}[sec:proof:ram_insertion]), then
-the forward simulation between HTL and Verilog is shown in
-Lemma~\goto{{[}lemma:verilog{]}}[lemma:verilog] (Section~\goto{1.5}[sec:proof:htl_verilog]), and
-finally, the proof that Verilog is deterministic is given in
-Lemma~\goto{{[}lemma:deterministic{]}}[lemma:deterministic]
-(Section~\goto{1.6}[sec:proof:deterministic]).
+tool. The forward simulation from 3AC to HTL is stated in \in{Lemma}[lemma:htl]
+(\in{Section}[sec:proof:3ac_htl]), the forward simulation for the RAM insertion is shown in
+Lemma~\goto{{[}lemma:htl_ram{]}}[lemma:htl_ram] (\in{Section}[sec:proof:ram_insertion]), then the
+forward simulation between HTL and Verilog is shown in
+Lemma~\goto{{[}lemma:verilog{]}}[lemma:verilog] (\in{Section}[sec:proof:htl_verilog]), and finally,
+the proof that Verilog is deterministic is given in
+Lemma~\goto{{[}lemma:deterministic{]}}[lemma:deterministic] (\in{Section}[sec:proof:deterministic]).
 
 \subsection[sec:proof:3ac_htl]{Forward Simulation from 3AC to HTL}
 
@@ -1019,15 +1020,21 @@ Verilog, the semantics are defined over one clock cycle and mirror the semantics
 Verilog.  Lemma~\goto{{[}lemma:htl{]}}[lemma:htl] shows the result that needs to be proven in this
 subsection.
 
-\reference[lemma:htl]{} Writing \type{tr_htl} for the translation from 3AC to HTL, we have:
+\startlemma[lemma:htl]
+Writing \type{tr_htl} for the translation from 3AC to HTL, we have:
+\startformula
+\forall c, h, B \in \mono{Safe},\quad \mono{tr\_htl} (c) = \mono{OK} (h) \land c
+\Downarrow B \implies h \Downarrow B.
+\stopformula
+\stoplemma
 
-%\startformula \forall c, h, B \in \mono{Safe},\quad \yhfunction{tr\_htl} (c) = \yhconstant{OK} (h) \land c \Downarrow B \implies h \Downarrow B. \stopformula
-
-{\em Proof sketch.} We prove this lemma by first establishing a specification of the translation
+\startproof
+We prove this lemma by first establishing a specification of the translation
 function $\mono{tr\_htl}$ that captures its important properties, and then splitting the proof into
 two parts: one to show that the translation function does indeed meet its specification, and one to
 show that the specification implies the desired simulation result. This strategy is in keeping with
-standard practice.~◻
+standard practice.
+\stopproof
 
 \subsubsection[sec:proof:3ac_htl:specification]{From Implementation to Specification}
 
-- 
cgit