Add modifications

7 files changed, 93 insertions, 62 deletions

diff --git a/Makefile b/Makefile
index 9bfb28c..0732b54 100644
--- a/Makefile
+++ b/Makefile
@@ -5,10 +5,4 @@ PROJNAME=main
 all: $(PROJNAME).pdf
 
 $(PROJNAME).pdf: $(PROJNAME).tex
-	latexmk -pdf -pdflatex="pdflatex -interactive=nonstopmode" -use-make $<
-
-cleanall:
-	latexmk -C
-
-clean:
-	latexmk -c
+	context $<
diff --git a/background.tex b/background.tex
index 253bdc5..4636918 100644
--- a/background.tex
+++ b/background.tex
@@ -1,7 +1,7 @@
-\chapter{Background}
+\startcomponent background
 
-\epigraph{Was there ever in anyone's life span a point free in time, devoid of memory, a night when
-  choice was any more than the sum of all the choices gone before? \\ --- \textsc{Joan Didion},
-  Run, River}
+\chapter{Background}
 
 aroistenaoirstenoiaresntoien
+
+\stopcomponent
diff --git a/hls.tex b/hls.tex
index 734463c..b73b686 100644
--- a/hls.tex
+++ b/hls.tex
@@ -7,19 +7,18 @@
 
 \chapter{High-Level Synthesis}
 
-{\bf Can you trust your high-level synthesis tool?}
-
-As latency, throughput, and energy efficiency become increasingly important, custom hardware
-accelerators are being designed for numerous applications.  Alas, designing these accelerators can
-be a tedious and error-prone process using a hardware description language (HDL) such as Verilog.
-An attractive alternative is \emph{high-level synthesis} (HLS), in which hardware designs are
-automatically compiled from software written in a high-level language like C.  Modern HLS tools such
-as LegUp~\cite{canis11_legup}, Vivado HLS~\cite{xilinx20_vivad_high_synth}, Intel
-i++~\cite{intel_hls}, and Bambu HLS~\cite{bambu_hls} promise designs with comparable performance and
-energy-efficiency to those hand-written in an HDL~\cite{homsirikamol+14, silexicahlshdl, 7818341},
-while offering the convenient abstractions and rich ecosystems of software development.  But
-existing HLS tools cannot always guarantee that the hardware designs they produce are equivalent to
-the software they were given, and this undermines any reasoning conducted at the software level.
+\paragraph{Can you trust your high-level synthesis tool?} As latency, throughput, and energy
+efficiency become increasingly important, custom hardware accelerators are being designed for
+numerous applications.  Alas, designing these accelerators can be a tedious and error-prone process
+using a hardware description language (HDL) such as Verilog.  An attractive alternative is
+\emph{high-level synthesis} (HLS), in which hardware designs are automatically compiled from
+software written in a high-level language like C.  Modern HLS tools such as
+LegUp~\cite{canis11_legup}, Vivado HLS~\cite{xilinx20_vivad_high_synth}, Intel i++~\cite{intel_hls},
+and Bambu HLS~\cite{bambu_hls} promise designs with comparable performance and energy-efficiency to
+those hand-written in an HDL~\cite{homsirikamol+14, silexicahlshdl, 7818341}, while offering the
+convenient abstractions and rich ecosystems of software development.  But existing HLS tools cannot
+always guarantee that the hardware designs they produce are equivalent to the software they were
+given, and this undermines any reasoning conducted at the software level.
 
 Indeed, there are reasons to doubt that HLS tools actually \emph{do} always preserve equivalence.
 For instance, Vivado HLS has been shown to apply pipelining optimisations
@@ -34,12 +33,10 @@ using Csmith~\cite{yang11_findin_under_bugs_c_compil}, and despite restricting t
 programs to the C fragment explicitly supported by all the tools, they still found that on average
 2.5\% of test-cases were compiled to designs that behaved incorrectly.
 
-{\bf Existing workarounds}
-
-Aware of the reliability shortcomings of HLS tools, hardware designers routinely check the generated
-hardware for functional correctness. This is commonly done by simulating the generated design
-against a large test-bench. But unless the test-bench covers all inputs exhaustively -- which is
-often infeasible -- there is a risk that bugs remain.
+\paragraph{Existing workarounds.} Aware of the reliability shortcomings of HLS tools, hardware
+designers routinely check the generated hardware for functional correctness. This is commonly done
+by simulating the generated design against a large test-bench. But unless the test-bench covers all
+inputs exhaustively -- which is often infeasible -- there is a risk that bugs remain.
 
 One alternative is to use \emph{translation validation}~\cite{pnueli98_trans} to prove equivalence
 between the input program and the output design. Translation validation has been successfully
@@ -57,20 +54,17 @@ to date.
 Our position is that none of the above workarounds are necessary if the HLS tool can simply be
 trusted to work correctly.
 
-{\bf Our solution}
-
-We have designed a new HLS tool in the Coq theorem prover and proved that any output design it
-produces always has the same behaviour as its input program. Our tool, called Vericert, is
-automatically extracted to an OCaml program from Coq, which ensures that the object of the proof is
-the same as the implementation of the tool. Vericert is built by extending the CompCert verified C
-compiler~\cite[leroy09_formal_verif_realis_compil] with a new hardware-specific intermediate
-language and a Verilog back end. It supports most C constructs, including integer operations,
-function calls (which are all inlined), local arrays, structs, unions, and general control-flow
-statements, but currently excludes support for case statements, function pointers, recursive
-function calls, non-32-bit integers, floats, and global variables.
+\paragraph{Our solution.} We have designed a new HLS tool in the Coq theorem prover and proved that
+any output design it produces always has the same behaviour as its input program. Our tool, called
+Vericert, is automatically extracted to an OCaml program from Coq, which ensures that the object of
+the proof is the same as the implementation of the tool. Vericert is built by extending the CompCert
+verified C compiler~\cite[leroy09_formal_verif_realis_compil] with a new hardware-specific
+intermediate language and a Verilog back end. It supports most C constructs, including integer
+operations, function calls (which are all inlined), local arrays, structs, unions, and general
+control-flow statements, but currently excludes support for case statements, function pointers,
+recursive function calls, non-32-bit integers, floats, and global variables.
 
-{\bf Contributions and Outline}
-The contributions of this paper are as follows:
+\paragraph{Contributions and Outline.} The contributions of this paper are as follows:
 
 \startitemize[]
   \item We present Vericert, the first mechanically verified HLS tool that compiles C to Verilog. In
@@ -105,8 +99,7 @@ The contributions of this paper are as follows:
         correctness theorem is watertight.
 \stopitemize
 
-{\bf Companion material}
-Vericert is fully open source and available on GitHub at
+\paragraph{Companion material.} Vericert is fully open source and available on GitHub at
 
 \startalignment[center]
 \goto{\hyphenatedurl{https://github.com/ymherklotz/vericert}}[url(https://github.com/ymherklotz/vericert)].
diff --git a/introduction.tex b/introduction.tex
index f4ec3a1..623b56a 100644
--- a/introduction.tex
+++ b/introduction.tex
@@ -1 +1,5 @@
+\startcomponent introduction
+
 \chapter{Introduction}
+
+\stopcomponent
diff --git a/lsr_env.tex b/lsr_env.tex
index ae0684a..771af80 100644
--- a/lsr_env.tex
+++ b/lsr_env.tex
@@ -1,3 +1,4 @@
+%% macros=mkvi
 \startenvironment lsr_env
 
 \setupcolors[state=start]
@@ -38,25 +39,33 @@
     width=middle,
 ]
 
-% @see http://wiki.contextgarden.net/Command/setupinterlinespace
-% Double spacing is line=5.6ex and one and half spacing is line=4.2ex.
-% However, closest we can get like MS Word 1.5 line spacing.
-\setupinterlinespace[line=3.8ex]
-
 % @see http://wiki.contextgarden.net/Command/setuppagenumbering
 \setuppagenumbering[location={footer,middle}]
+\definestructureconversionset [frontpart:pagenumber] [] [romannumerals]
+
+\startsectionblockenvironment [bodypart]
+  \setcounter[userpage][1]
+\stopsectionblockenvironment
 
 % ==========================================================================
 % Headers
 % ==========================================================================
+\setuphead[chapter][
+  style={\bfd},
+  header=empty,
+]
+
+\startsectionblockenvironment [bodypart]
 \setuplabeltext[chapter=Chapter~]
 \setuphead[chapter][
   style={\bfd},
   header=empty,
   align=flushright,
+  commandbefore={\blank[-0.3cm]},
   after={\blank[4*line]},
-  commandbefore={\blank[small]},
+  before={\blank[4*big,force]},
 ]
+\stopsectionblockenvironment
 
 % @see http://wiki.contextgarden.net/Command/setupindenting
 % @see http://wiki.contextgarden.net/Indentation
@@ -151,7 +160,36 @@
 % \setupbtx[default:cite][alternative=authoryear]
 % @see https://tex.stackexchange.com/a/294571
 \usebtxdataset[references]
-\setupbtx[default:cite][alternative=authoryear]
 \usebtxdefinitions[apa]
+\setupbtx[default:cite][alternative=authoryear]
+
+\starttexdefinition mutable protected btx:aps:doi-url #text
+  \ifconditional\btxinteractive
+  \btxdoifelse {doi} {
+    DOI: \goto {\btxflush{doi}} [url(https://dx.doi.org/\btxflush{doi})]
+  } {
+    \btxdoifelse {url} {
+      \goto {\btxflush{url}} [url(\btxflush{url})]
+    } {
+      #text
+    }
+  }
+  \else
+  #text
+  \fi
+\stoptexdefinition
+
+\starttexdefinition mutable protected btx:apa:editor-in
+    \btxdoif {booktitle} {
+        \btxlabeltext{In}
+        \btxspace
+        \texdefinition{btx:apa:composed-title}{booktitle}
+        \btxperiod
+    }
+\stoptexdefinition
+
+\def\paragraph#1{%
+  \bold{#1}%
+}
 
 \stopenvironment
diff --git a/main.tex b/main.tex
index 2c7c250..6d8fb9b 100644
--- a/main.tex
+++ b/main.tex
@@ -22,12 +22,13 @@
 \component title
 
 \startfrontmatter
-  \setuppagenumber[number=1]
   \completecontent
 \stopfrontmatter
 
 \startbodymatter
-  \setuppagenumber[number=1]
+  \setupinterlinespace[line=3.8ex]
+  \component introduction
+  \component background
   \component hls
 \stopbodymatter
 
diff --git a/title.tex b/title.tex
index be4a5ef..a73ea75 100644
--- a/title.tex
+++ b/title.tex
@@ -4,13 +4,11 @@
 \definemakeup[title][align=middle]
 
 \startmakeup[title]
-  \setupinterlinespace[big]
-  {\bfd Formal Verification of High-Level Synthesis}
-  \blank[small]
-  {\bfa Late Stage Review}
-  \blank[big]
-
-  Yann Herklotz Grave
+  {\switchtobodyfont[30pt] Formal Verification of \blank[medium] High-Level Synthesis}
+  \blank[1cm]
+  {\bfb Late Stage Review}
+  \blank[2cm]
+  {\rma Yann Herklotz Grave}
   \blank[5cm]
 
   % http://wiki.contextgarden.net/Command/currentdate
@@ -18,7 +16,10 @@
   \blank[5cm]
 
   \startalignment[flushleft]
-  Supervisor: John Wickerson
+  \setupinterlinespace[line=3.8ex]\rma
+  \bold{Supervisor}: John Wickerson
+
+  \bold{CID}: 01062783
   \stopalignment
 \stopmakeup