Add

7 files changed, 380 insertions, 125 deletions

diff --git a/fonts_env.tex b/fonts_env.tex
new file mode 100644
index 0000000..a186a60
--- /dev/null
+++ b/fonts_env.tex
@@ -0,0 +1,25 @@
+\startenvironment fonts_env
+
+\starttypescript[mono] [iosevka]
+  \definefontsynonym[Iosevka-Regular]    [file:iosevka-fixed-regular]
+  \definefontsynonym[Iosevka-Italic]     [file:iosevka-fixed-italic]
+  \definefontsynonym[Iosevka-Bold]       [file:iosevka-fixed-bold]
+  \definefontsynonym[Iosevka-BoldItalic] [file:iosevka-fixed-bolditalic]
+\stoptypescript
+
+\starttypescript[mono] [iosevka]
+  \setups[font:fallback:mono]
+  \definefontsynonym[Mono]           [Iosevka-Regular]    [features=default]
+  \definefontsynonym[MonoItalic]     [Iosevka-Italic]     [features=default]
+  \definefontsynonym[MonoBold]       [Iosevka-Bold]       [features=default]
+  \definefontsynonym[MonoBoldItalic] [Iosevka-BoldItalic] [features=default]
+\stoptypescript
+
+\starttypescript [ebgaramondlato]
+  \definetypeface [ebgaramondlato] [rm] [serif] [palatino]   [default]
+  \definetypeface [ebgaramondlato] [ss] [sans]  [lato]       [default]
+  \definetypeface [ebgaramondlato] [tt] [mono]  [iosevka]    [default] [rscale=0.9]
+  \definetypeface [ebgaramondlato] [mm] [math]  [default]    [default]
+\stoptypescript
+
+\stopenvironment
diff --git a/hls.tex b/hls.tex
index 4feaa14..734463c 100644
--- a/hls.tex
+++ b/hls.tex
@@ -1,10 +1,13 @@
-\chapter{Formal Verification of High-Level Synthesis}
+\startcomponent hls
+\product main
 
-\newcommand{\slowdownOrig}{27}
-\newcommand{\slowdownDiv}{2}
-\newcommand{\areaIncr}{1.1}
+\def\slowdownOrig{27}
+\def\slowdownDiv{2}
+\def\areaIncr{1.1}
 
-\paragraph{Can you trust your high-level synthesis tool?}
+\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
@@ -20,18 +23,18 @@ the software they were given, and this undermines any reasoning conducted at the
 
 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
-incorrectly\footnote{\url{https://bit.ly/vivado-hls-pipeline-bug}} or to silently generate wrong
+incorrectly\footnote{\goto{https://bit.ly/vivado-hls-pipeline-bug}[url(https://bit.ly/vivado-hls-pipeline-bug)]} or to silently generate wrong
 code should the programmer stray outside the fragment of C that it
-supports.\footnote{\url{https://bit.ly/vivado-hls-pointer-bug}} Meanwhile,
-\citet{lidbury15_many_core_compil_fuzzin} had to abandon their attempt to fuzz-test Altera's (now
+supports.\footnote{\goto{https://bit.ly/vivado-hls-pointer-bug}[url(https://bit.ly/vivado-hls-pointer-bug)]} Meanwhile,
+\cite{lidbury15_many_core_compil_fuzzin} had to abandon their attempt to fuzz-test Altera's (now
 Intel's) OpenCL compiler since it ``either crashed or emitted an internal compiler error'' on so
 many of their test inputs.  More recently,
-\citet{herklotz21_empir_study_reliab_high_level_synth_tools} fuzz-tested three commercial HLS tools
+\cite{herklotz21_empir_study_reliab_high_level_synth_tools} fuzz-tested three commercial HLS tools
 using Csmith~\cite{yang11_findin_under_bugs_c_compil}, and despite restricting the generated
 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.
 
-\paragraph{Existing workarounds}
+{\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
@@ -45,40 +48,40 @@ optimisations~\cite{kim04_autom_fsmd,karfa06_formal_verif_method_sched_high_synt
 Nevertheless, it is an expensive task, especially for large designs, and it must be repeated every
 time the compiler is invoked.  For example, the translation validation for Catapult
 C~\cite{mentor20_catap_high_level_synth} may require several rounds of expert
-`adjustments'~\cite[p.~3]{slec_whitepaper} to the input C program before validation succeeds. And
+`adjustments'~\cite[alternative=authoryear,right={, p.~3)}][slec_whitepaper] to the input C program before validation succeeds. And
 even when it succeeds, translation validation does not provide watertight guarantees unless the
 validator itself has been mechanically proven
-correct~\cite[e.g.][]{tristan08_formal_verif_trans_valid}, which has not been the case in HLS tools
+correct~\cite[tristan08_formal_verif_trans_valid], which has not been the case in HLS tools
 to date.
 
 Our position is that none of the above workarounds are necessary if the HLS tool can simply be
 trusted to work correctly.
 
-\paragraph{Our solution}
+{\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
+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{Contributions and Outline}
+{\bf Contributions and Outline}
 The contributions of this paper are as follows:
 
-\begin{itemize}
+\startitemize[]
   \item We present Vericert, the first mechanically verified HLS tool that compiles C to Verilog. In
         Section~\ref{sec:design}, we describe the design of Vericert, including certain
         optimisations related to memory accesses and division.
   \item We state the correctness theorem of Vericert with respect to an existing semantics for
-        Verilog due to \citet{loow19_proof_trans_veril_devel_hol}. In Section~\ref{sec:verilog}, we
-        describe how we extended this semantics to make it suitable as an HLS target.  We also
-        describe how the Verilog semantics is integrated into CompCert's language execution model
-        and its framework for performing simulation proofs. A mapping of CompCert's infinite memory
-        model onto a finite Verilog array is also described.
+    Verilog due to \cite[authoryear][loow19_proof_trans_veril_devel_hol]. In
+    Section~\ref{sec:verilog}, we describe how we extended this semantics to make it suitable as an
+    HLS target.  We also describe how the Verilog semantics is integrated into CompCert's language
+    execution model and its framework for performing simulation proofs. A mapping of CompCert's
+    infinite memory model onto a finite Verilog array is also described.
   \item In Section~\ref{sec:proof}, we describe how we proved the correctness theorem. The proof
         follows standard CompCert techniques -- forward simulations, intermediate specifications,
         and determinism results -- but we encountered several challenges peculiar to our
@@ -100,9 +103,16 @@ The contributions of this paper are as follows:
         on our campaign to fuzz-test Vericert using over a hundred thousand random C programs
         generated by Csmith~\cite{yang11_findin_under_bugs_c_compil} in order to confirm that its
         correctness theorem is watertight.
-\end{itemize}
+\stopitemize
 
-\paragraph{Companion material}
+{\bf Companion material}
 Vericert is fully open source and available on GitHub at
-\url{https://github.com/ymherklotz/vericert}. A snapshot of the Vericert development is also
-available in a Zenodo repository~\cite{yann_herklotz_2021_5093839}.
+
+\startalignment[center]
+\goto{\hyphenatedurl{https://github.com/ymherklotz/vericert}}[url(https://github.com/ymherklotz/vericert)].
+\stopalignment
+
+A snapshot of the Vericert development is also available in a Zenodo
+repository~\cite{yann_herklotz_2021_5093839}.
+
+\stopcomponent
diff --git a/lsr_env.tex b/lsr_env.tex
new file mode 100644
index 0000000..ae0684a
--- /dev/null
+++ b/lsr_env.tex
@@ -0,0 +1,157 @@
+\startenvironment lsr_env
+
+\setupcolors[state=start]
+
+% ==========================================================================
+% PDF
+% ==========================================================================
+% @see http://wiki.contextgarden.net/PDF_Bookmarks_and_Headers
+% @see http://wiki.contextgarden.net/Command/setupinteraction
+\setupinteraction[
+    state=start,
+    title={Formal Verification of High-Level Synthesis},
+    author={Yann Herklotz},
+    color=darkgreen,
+    contrastcolor=darkgreen,
+    openaction=ToggleViewer,
+    focus=width,
+    click=yes,
+]
+%\placebookmarks[chapter,section,subsection,subsubsection][chapter,section]
+%\setupinteractionscreen[option=bookmark]
+
+% ==========================================================================
+% Layout
+% ==========================================================================
+\setuppapersize[A4][A4]
+\setupbodyfont[ebgaramondlato,11pt]
+%\setupalign[hz,hanging,nothyphenated]
+\setupalign[hz,hanging]
+\setuptolerance[stretch,tolerant]
+\setuplayout[
+    backspace=3cm,
+    margin=2cm,
+    topspace=1.25cm,
+    header=1.25cm,
+    footer=1.25cm,
+    height=middle,
+    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}]
+
+% ==========================================================================
+% Headers
+% ==========================================================================
+\setuplabeltext[chapter=Chapter~]
+\setuphead[chapter][
+  style={\bfd},
+  header=empty,
+  align=flushright,
+  after={\blank[4*line]},
+  commandbefore={\blank[small]},
+]
+
+% @see http://wiki.contextgarden.net/Command/setupindenting
+% @see http://wiki.contextgarden.net/Indentation
+% Indent all paragraph after all section headers.
+\setupindenting[yes,medium,next]
+%\setupheads[section, subsection][
+%    indentnext=yes,
+%    numberwidth=1.27cm,
+%    style=bold,
+%    before={\blank[3*line]},
+%    after={\blank[1*line]},
+%]
+%
+%\setupheads[subsubsection][
+%    indentnext=yes,
+%    numberwidth=1.27cm,
+%    style=bold,
+%    before={\blank[1*line]},
+%    after={\blank[1*line]},
+%]
+
+% ==========================================================================
+% Table of Contents
+% ==========================================================================
+%\definehead[headers][title]
+%\setuphead[headers][
+%    style={\bf},
+%    incrementnumber=list,
+%]
+%
+%\setupheadtext[content=Table of Contents]
+%\setuphead[title][incrementnumber=list]
+%\setupcombinedlist[content][
+%    list={headers,title,chapter,section,subsection, subsubsection},
+%    alternative=b,
+%]
+%
+%\setuplist[headers][margin=0mm, style={\bf}, pagenumber=no, after={\blank[1*line]}]
+%\setuplist[title][margin=30mm, style={\bf}]
+%\setuplist[chapter][margin=10mm, width=20mm, style={\bf}]
+%\setuplist[section][width=18mm, margin=30mm]
+%\setuplist[subsection][width=18mm, margin=48mm]
+%\setuplist[subsubsection][width=18mm, margin=66mm]
+%
+%\definestructureconversionset[frontpart:pagenumber][][romannumerals]
+%\definestructureconversionset[bodypart:pagenumber][][numbers]
+
+% \writetolist[headers]{}{Chapter \hfill Title \hfill Page}
+
+% @see https://tex.stackexchange.com/a/243726
+\setupcaptions[table][location=top]
+
+% ==========================================================================
+% Figure
+% ==========================================================================
+\setupcaptions[figure][location=bottom]
+
+% ==========================================================================
+% Abbreviation
+% ==========================================================================
+% @see https://tex.stackexchange.com/a/389791/141902
+\definehspace[abbrwidth][1em]
+\definesynonyms[abbreviation][abbreviations][\infull]
+\setupsynonyms[abbreviation][
+    criterium=all,
+    textstyle=normal,
+    synonymstyle=normal,
+    width=3.5em,
+    style={--\hspace[abbrwidth]},
+    character=normal,
+]
+
+% ==========================================================================
+% Appendices
+% ==========================================================================
+%\setuplabeltext[appendix=APPENDIX~]
+%\definehead[appendix][chapter]
+%
+%\definelist[appendix][criterium=all]
+%\setuplist[appendix][
+%    alternative=b,
+%    margin=10mm,
+%    width=20mm,
+%]
+
+% ==========================================================================
+% Bibliography
+% ==========================================================================
+% @see http://wiki.contextgarden.net/Bibliography_mkiv
+% \usebtxdataset[bibliography.bib]
+% \usebtxdefinitions[apa]
+% \setupbtx[default:cite][alternative=authoryear]
+% @see https://tex.stackexchange.com/a/294571
+\usebtxdataset[references]
+\setupbtx[default:cite][alternative=authoryear]
+\usebtxdefinitions[apa]
+
+\stopenvironment
diff --git a/main.tex b/main.tex
index 5aea965..2c7c250 100644
--- a/main.tex
+++ b/main.tex
@@ -1,83 +1,40 @@
-\documentclass{scrreprt}
-
-\title{Formal Verification of High-Level Synthesis}
-\subtitle{Late Stage Review\\Imperial College London}
-\author{Yann Herklotz Grave}
-\date{April 2022}
-
-\includeonly{
-  introduction,
-  background,
-  hls,
-  scheduling,
-  pipelining,
-  dynamic,
-  schedule,
-  conclusion
-}
-
-\linespread{1.3}
-
-\usepackage{graphicx}
-\usepackage{amsmath}
-\usepackage{amsthm}
-
-\usepackage[british]{babel}
-%\usepackage[utf8]{inputenc}
-\usepackage[sc]{mathpazo}
-\usepackage{newpxmath}
-\usepackage{newpxtext}
-\usepackage{inconsolata}
-\usepackage{microtype}
-\addtokomafont{disposition}{\rmfamily}
-
-\usepackage[natbib=true,style=alphabetic,maxbibnames=10]{biblatex}
-\addbibresource{references.bib}
-\AtBeginBibliography{\small}
-
-\usepackage{epigraph}
-\setlength\epigraphwidth{1\textwidth}
-\setlength\epigraphrule{0pt} % no line between
-\setlength\beforeepigraphskip{1\baselineskip} % space before and after epigraph
-\setlength\afterepigraphskip{2\baselineskip}
-\renewcommand*{\textflush}{flushright}
-\renewcommand*{\epigraphsize}{\normalsize\itshape}
-
-\usepackage{xcolor}
-
-\definecolor{ymhfwcol}{HTML}{5F506B}
-\definecolor{ymhwipcol}{HTML}{76949F}
-\newcommand{\ymhfw}{\textcolor{ymhfwcol}{FW}}
-\newcommand{\ymhwip}{\textcolor{ymhwipcol}{WIP}}
-
-\newtheorem{theorem}{Theorem}
-\newtheorem{lemma}{Lemma}
-\newtheorem*{remark}{Remark}
-
-\hyphenation{Comp-Cert}
-\hyphenation{Veri-cert}
-\hyphenation{Poly-Bench}
-\hyphenation{Leg-Up}
-\hyphenation{straight-for-ward}
-\hyphenation{cor-re-la-tion}
-\hyphenation{gram-schmi-dt}
-\hyphenation{de-riche}
-
-\begin{document}
-
-\maketitle
-
-\tableofcontents
-
-\include{introduction}
-\include{background}
-\include{hls}
-\include{scheduling}
-\include{pipelining}
-\include{dynamic}
-\include{schedule}
-\include{conclusion}
-
-\printbibliography{}
-
-\end{document}
+\startproduct main
+\enabletrackers[fonts.missing]
+
+% Common module shared by all.
+% @see http://wiki.contextgarden.net/Dummy_text
+% \usemodule[visual]
+
+\mainlanguage[en]
+
+% Common layout settings.
+\environment fonts_env
+\environment lsr_env
+
+% \showlayout
+% \showsetups
+% \showgrid
+% \showmakeup
+%\showframe
+% \showbodyfontenvironment
+%\showbodyfont
+
+\component title
+
+\startfrontmatter
+  \setuppagenumber[number=1]
+  \completecontent
+\stopfrontmatter
+
+\startbodymatter
+  \setuppagenumber[number=1]
+  \component hls
+\stopbodymatter
+
+\startbackmatter
+  \startchapter[title=Bibliography]
+    \placelistofpublications
+  \stopchapter
+\stopbackmatter
+
+\stopproduct
diff --git a/main_other.tex b/main_other.tex
new file mode 100644
index 0000000..d5f975c
--- /dev/null
+++ b/main_other.tex
@@ -0,0 +1,82 @@
+\documentclass{scrreprt}
+
+\title{Formal Verification of High-Level Synthesis}
+\subtitle{Late Stage Review\\Imperial College London}
+\author{Yann Herklotz Grave}
+\date{April 2022}
+
+\includeonly{
+  introduction,
+  background,
+  hls,
+  scheduling,
+  pipelining,
+  dynamic,
+  schedule,
+  conclusion
+}
+
+\usepackage{graphicx}
+\usepackage{amsmath}
+\usepackage{amsthm}
+
+\usepackage[british]{babel}
+%\usepackage[utf8]{inputenc}
+\usepackage[sc]{mathpazo}
+\usepackage{newpxmath}
+\usepackage{newpxtext}
+\linespread{1.05}
+\usepackage{inconsolata}
+\usepackage{microtype}
+\addtokomafont{disposition}{\rmfamily}
+
+\usepackage[natbib=true,style=alphabetic,maxbibnames=10]{biblatex}
+\addbibresource{references.bib}
+\AtBeginBibliography{\small}
+
+\usepackage{epigraph}
+\setlength\epigraphwidth{1\textwidth}
+\setlength\epigraphrule{0pt} % no line between
+\setlength\beforeepigraphskip{1\baselineskip} % space before and after epigraph
+\setlength\afterepigraphskip{2\baselineskip}
+\renewcommand*{\textflush}{flushright}
+\renewcommand*{\epigraphsize}{\normalsize\itshape}
+
+\usepackage{xcolor}
+
+\definecolor{ymhfwcol}{HTML}{5F506B}
+\definecolor{ymhwipcol}{HTML}{76949F}
+\newcommand{\ymhfw}{\textcolor{ymhfwcol}{FW}}
+\newcommand{\ymhwip}{\textcolor{ymhwipcol}{WIP}}
+
+\newtheorem{theorem}{Theorem}
+\newtheorem{lemma}{Lemma}
+\newtheorem*{remark}{Remark}
+
+\hyphenation{Comp-Cert}
+\hyphenation{Veri-cert}
+\hyphenation{Poly-Bench}
+\hyphenation{Leg-Up}
+\hyphenation{straight-for-ward}
+\hyphenation{cor-re-la-tion}
+\hyphenation{gram-schmi-dt}
+\hyphenation{de-riche}
+
+\begin{document}
+
+\maketitle
+
+\tableofcontents
+
+\include{introduction}
+\include{background}
+\include{hls}
+\include{scheduling}
+\include{pipelining}
+\include{dynamic}
+\include{schedule}
+\include{conclusion}
+
+\printbibliography{}
+
+\end{document}
diff --git a/references.bib b/references.bib
index bf2ec87..1ed2e1f 100644
--- a/references.bib
+++ b/references.bib
@@ -186,7 +186,7 @@ year = {2020},
 }
 
 @inproceedings{gupta03_spark,
-  author          = {S. {Gupta} and N. {Dutt} and R. {Gupta} and A. {Nicolau}},
+  author          = {{Gupta}, S. and {Dutt}, N. and {Gupta}, R. and {Nicolau}, A.},
   title           = {{SPARK}: a high-level synthesis framework for applying parallelizing compiler
                   transformations},
   booktitle       = {16th International Conference on VLSI Design, 2003. Proceedings.},
@@ -199,7 +199,7 @@ year = {2020},
 }
 
 @article{chouksey20_verif_sched_condit_behav_high_level_synth,
-  author          = {R. {Chouksey} and C. {Karfa}},
+  author          = {Chouksey, R. and Karfa, C.},
   title           = {Verification of Scheduling of Conditional Behaviors in
                   High-Level Synthesis},
   journal         = {IEEE Transactions on Very Large Scale Integration (VLSI)
@@ -215,7 +215,7 @@ year = {2020},
 }
 
 @inproceedings{pnueli98_trans,
-  author          = "Pnueli, A.  and Siegel, M.  and Singerman, E.",
+  author          = "Pnueli, A. and Siegel, M. and Singerman, E.",
   title           = "Translation validation",
   booktitle       = "Tools and Algorithms for the Construction and Analysis of Systems",
   year            = 1998,
@@ -228,7 +228,7 @@ year = {2020},
 }
 
 @article{chouksey19_trans_valid_code_motion_trans_invol_loops,
-  author =       {R. {Chouksey} and C. {Karfa} and P. {Bhaduri}},
+  author =       {{Chouksey}, R. and {Karfa}, C. and {Bhaduri}, P.},
   title =        {Translation Validation of Code Motion Transformations
                   Involving Loops},
   journal =      {IEEE Transactions on Computer-Aided Design of Integrated
@@ -243,7 +243,7 @@ year = {2020},
 }
 
 @article{banerjee14_verif_code_motion_techn_using_value_propag,
-  author = {K. {Banerjee} and C. {Karfa} and D. {Sarkar} and C. {Mandal}},
+  author = {{Banerjee}, K. and {Karfa}, C. and {Sarkar}, D. and {Mandal}, C.},
   title = {Verification of Code Motion Techniques Using Value
                   Propagation},
   journal = {IEEE Transactions on Computer-Aided Design of Integrated
@@ -258,7 +258,7 @@ year = {2020},
 }
 
 @inproceedings{kim04_autom_fsmd,
-  author = { {Youngsik Kim} and S. {Kopuri} and N. {Mansouri}},
+  author = { {Youngsik Kim} and {Kopuri}, S. and {Mansouri}, N.},
   title = {Automated formal verification of scheduling process using
                   finite state machines with datapath (FSMD)},
   booktitle = {International Symposium on Signals, Circuits and
@@ -306,7 +306,7 @@ year = {2020},
 }
 
 @book{bertot04_inter_theor_provin_progr_devel,
-  author          = {Yves Bertot and Pierre Cast{\'{e}}ran},
+  author          = {Bertot, Yves and Cast{\'{e}}ran, Pierre},
   title           = {Interactive Theorem Proving and Program Development},
   year            = 2004,
   publisher       = {Springer Berlin Heidelberg},
@@ -345,7 +345,7 @@ year = {2020},
 }
 
 @inproceedings{chapman92_verif_bedroc,
-  author          = {R. {Chapman} and G. {Brown} and M. {Leeser}},
+  author          = {{Chapman}, R. and {Brown}, G. and {Leeser}, M.},
   title           = {Verified high-level synthesis in BEDROC},
   booktitle       = {[1992] Proceedings The European Conference on Design Automation},
   year            = 1992,
@@ -356,7 +356,7 @@ year = {2020},
 }
 
 @article{hwang91_formal_approac_to_sched_probl,
-  author = {C. -. {Hwang} and J. -. {Lee} and Y. -. {Hsu}},
+  author = {{Hwang}, C. -. and {Lee}, J. -. and {Hsu}, Y. -.},
   title = {A Formal Approach To the Scheduling Problem in High Level
                   Synthesis},
   journal = {IEEE Transactions on Computer-Aided Design of Integrated
@@ -381,7 +381,7 @@ year = {2020},
 }
 
 @inproceedings{grass94_high,
-  author = {W. {Grass} and M. {Mutz} and W. -. {Tiedemann}},
+  author = {{Grass}, W. and {Mutz}, M. and {Tiedemann}, W. -.},
   title = {High level synthesis based on formal methods},
   booktitle = {Proceedings of Twentieth Euromicro Conference. System
                   Architecture and Integration},
@@ -404,7 +404,7 @@ year = {2020},
 }
 
 @article{perna12_mechan_wire_wise_verif_handel_c_synth,
-  author = "Juan Perna and Jim Woodcock",
+  author = "Perna, Juan and Woodcock, Jim",
   title = {Mechanised Wire-Wise Verification of {Handel-C} Synthesis},
   journal = "Science of Computer Programming",
   volume = 77,
@@ -470,8 +470,8 @@ year = {2020},
 }
 
 @inproceedings{canis11_legup,
-  author          = {Andrew Canis and Jongsok Choi and Mark Aldham and Victor Zhang and Ahmed
-                  Kammoona and Jason Helge Anderson and Stephen Dean Brown and Tomasz S. Czajkowski},
+  author          = {Canis, Andrew and Choi, Jongsok and Aldham, Mark and Zhang, Victor and
+                  Kammoona, Ahmed and Anderson, Jason Helge and Brown, Stephen Dean and Czajkowski, Tomasz S.},
   title           = {{LegUp}: high-level synthesis for {FPGA}-based processor/accelerator systems},
   booktitle       = {{FPGA}},
   year            = 2011,
@@ -481,7 +481,7 @@ year = {2020},
 }
 
 @INPROCEEDINGS{choi+18,
-  author={Y. {Choi} and J. {Cong}},
+  author={{Choi}, Y. and {Cong}, J.},
   booktitle={2018 IEEE/ACM International Conference on Computer-Aided Design (ICCAD)},
   title={HLS-Based Optimization and Design Space Exploration for Applications with Variable Loop Bounds},
   year={2018},
@@ -557,8 +557,7 @@ year = {2020},
 }
 
 @inproceedings{homsirikamol+14,
-  author    = {Ekawat Homsirikamol and
-               Kris Gaj},
+  author    = {Homsirikamol, Ekawat and Gaj, Kris},
   title     = {Can high-level synthesis compete against a hand-written code in the
                cryptographic domain? {A} case study},
   booktitle = {ReConFig},
@@ -979,7 +978,7 @@ series = {CPP 2021}
 	doi = {10.1109/RECONFIG.2017.8279807}
 }
 
-@software{yann_herklotz_2021_5093839,
+@misc{yann_herklotz_2021_5093839,
   author       = {Yann Herklotz and
                   James D. Pollard and
                   Nadesh Ramanathan and
diff --git a/title.tex b/title.tex
new file mode 100644
index 0000000..be4a5ef
--- /dev/null
+++ b/title.tex
@@ -0,0 +1,25 @@
+\startcomponent title
+\product main
+
+\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
+  \blank[5cm]
+
+  % http://wiki.contextgarden.net/Command/currentdate
+  \currentdate[month,year]
+  \blank[5cm]
+
+  \startalignment[flushleft]
+  Supervisor: John Wickerson
+  \stopalignment
+\stopmakeup
+
+\stopcomponent