Add text to background and pipelining

4 files changed, 103 insertions, 7 deletions

diff --git a/chapters/background.tex b/chapters/background.tex
index 19a8c15..305f72a 100644
--- a/chapters/background.tex
+++ b/chapters/background.tex
@@ -11,13 +11,62 @@
   describing dynamic scheduling which is becoming a popular alternative.
 \stopsynopsis
 
-\section{Implementation: High-level Synthesis}
+\section{Verification}
+
+There are different kinds of verification tools, which can mostly be placed into two categories:
+automatic theorem provers described in \in{Section}[sec:background:automatic] and interactive
+theorem provers described in \in{Section}[sec:background:interactive].
+
+\subsection[sec:background:automatic]{Automatic theorem provers}
+
+Automatic theorem provers such as \SAT\ or \SMT\ solvers can be characterised as decision procedures
+that will answer, for example, if a formula is satisfiable or not.  However, by default these tools
+will only give the answer to the initial query, without showing the reasoning.  The reasoning is
+often quite complex as the \SAT\ or \SMT\ tool will implement many optimisations to improve the
+performance of the decision procedure.
+
+The main advantage of using an automatic theorem prover is that if one is working in its constrained
+decidable theory, then it will be efficient at proving or disproving if a formula is a theorem.
+However, if the theorem requires inductive arguments to prove, then the theorem prover might need
+some manual help from the user by adding the right lemmas to its collection of facts which the
+automatic procedure can use.  The proof itself though will still be automatic, which means that many
+of the tedious cases in the proofs can be ignored.
+
+However, this is also the main disadvantage of automatic theorem provers, because they do not
+provide details about the proof itself and often cannot communicate why they cannot prove a theorem.
+This means that as a user one has to guess what theorems the prover is missing and try and add these
+to the fact database.
+
+Finally, automatic theorem provers do not provide reasoning for their final answer by default,
+meaning one cannot check if the result is actually correct.  However, some SMT solvers support the
+generation of proof witnesses, which can then be checked and reused in other theorem provers.  Some
+examples of these are veriT~\cite[bouton09], and these can then be integrated into Coq using
+SMTCoq~\cite[armand11_modul_integ_sat_smt_solver].
+
+\subsection[sec:background:interactive]{Interactive theorem provers}
+
+Interactive theorem provers, on the other hand, focus on the checking proofs that are provided to
+them.  These can either be written manually by the user, or automatically generated by some decision
+procedure.  However, these two ways of generating proofs can be combined, so the general proof
+structure can be manually written, and simpler steps inside of the proof can be automatically
+solved.
+
+The main benefit of using an interactive theorem prover is that the proof is there and can be
+checked by a small, trusted kernel.  This kernel does not need to be heavily optimised, and can
+therefore be reasoned about.
+
+The main cost of using an interactive theorem prover is the time it takes to prove theorems, and the
+amount of formalisation that is needed to make the proofs pass.  For a proof to be completed, one
+has to remove any axioms from the proof, meaning even the smallest detail must be proven to
+continue.
+
+\section[sec:background:hls]{High-level Synthesis}
 
 \HLS\ is the transformation of software directly into hardware.  There are many different types of
 \HLS, which can vary greatly with what languages they accept, however, they often share similar
 steps in how the translation is performed, as they all go from a higher-level, behavioural
 description of the algorithm to a timed hardware description.  The main steps performed in the
-translation are the following~\cite{coussy09_introd_to_high_level_synth,canis13_legup}:
+translation are the following~\cite[coussy09_introd_to_high_level_synth,canis13_legup]:
 
 \desc{Compilation of specification} First, the input specification has to be compiled into a
 representation that can be used to apply all the necessary optimisations.  This can be an
@@ -25,11 +74,11 @@ intermediate language such as the lower-level virtual machine intermediate repre
 or a custom representation of the code.
 
 \desc{Hardware resource allocation} It is possible to select a device to target, which gives
-information about how many LUTs can be used to implement the logic.  However, tools often assume
-that an unlimited amount of resources are available instead.  This is resource sharing can be too
-expensive for adders, as the logic for sharing the adder would have approximately the same cost as
-adding a separate adder.  However, multiplies and divide blocks should be shared, especially as
-divide blocks are often implemented in LUTs and are therefore quite expensive.
+information about how many resources are available and can be used to implement the logic.  However,
+tools often assume that an unlimited amount of resources are available instead.  This is resource
+sharing can be too expensive for adders, as the logic for sharing the adder would have approximately
+the same cost as adding a separate adder.  However, multipliers and divider blocks should be shared,
+especially as divider blocks are often implemented in logic and are therefore quite expensive.
 
 \desc{Operation scheduling} The operations then need to be scheduled into a specific clock cycle, as
 the input specification language is normally an untimed behavioural representation.  This is where
@@ -338,4 +387,7 @@ correct manner.  In addition to that, the assumption is made that the semantics
 same in Handel-C as well as in the netlist format that is generated, which could be proven if the
 constructs are shown to behave in the exact same way as the handel-C constructs.
 
+% \section{Bibliography}
+% \placelistofpublications
+
 \stopcomponent
diff --git a/chapters/pipelining.tex b/chapters/pipelining.tex
index 5e07bd7..9bdacc1 100644
--- a/chapters/pipelining.tex
+++ b/chapters/pipelining.tex
@@ -5,4 +5,19 @@
 
 \chapter[sec:pipelining]{Loop Pipelining}
 
+\startsynopsis
+  This section describes the future plans of implementing loop pipelining in Vericert, also called
+  loop scheduling.  This addresses the final major issue with Vericert, which is efficiently
+  handling loops.
+\stopsynopsis
+
+Standard instruction scheduling only addresses parallelisation inside hyperblocks, which are linear
+sections of code.  However, loops are often the most critical sections in code, and scheduling only
+addresses parallelisation within one iteration.
+
+\section{Introduction to loop pipelining}
+
+\section{Bibliography}
+\placelistofpublications
+
 \stopcomponent
diff --git a/lsr_env.tex b/lsr_env.tex
index 371f8ca..c20063e 100644
--- a/lsr_env.tex
+++ b/lsr_env.tex
@@ -291,6 +291,7 @@
 \abbreviation{II}{initiation interval}
 \abbreviation{ASAP}{as soon as possible}
 \abbreviation{ALAP}{as late as possible}
+\abbreviation{LUT}{look-up table}
 
 % ==========================================================================
 % Appendices
diff --git a/lsr_refs.bib b/lsr_refs.bib
index 4ac943b..1833535 100644
--- a/lsr_refs.bib
+++ b/lsr_refs.bib
@@ -30,6 +30,21 @@
 	type = {Standard}
 }
 
+@InProceedings{armand11_modul_integ_sat_smt_solver,
+	keywords = {SAT, verification, coq},
+	author = {Armand, Michael and Faure, Germain and Grégoire, Benjamin and Keller, Chantal and Théry, Laurent and Werner, Benjamin},
+	editor = "Jouannaud, Jean-Pierre
+and Shao, Zhong",
+	title = "A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses",
+	booktitle = "Certified Programs and Proofs",
+	year = "2011",
+	publisher = "Springer Berlin Heidelberg",
+	address = "Berlin, Heidelberg",
+	pages = "135--150",
+	abstract = "We present a way to enjoy the power of SAT and SMT provers in Coq without compromising soundness. This requires these provers to return not only a yes/no answer, but also a proof witness that can be independently rechecked. We present such a checker, written and fully certified in Coq. It is conceived in a modular way, in order to tame the proofs' complexity and to be extendable. It can currently check witnesses from the SAT solver ZChaff and from the SMT solver veriT. Experiments highlight the efficiency of this checker. On top of it, new reflexive Coq tactics have been built that can decide a subset of Coq's logic by calling external provers and carefully checking their answers.",
+	isbn = "978-3-642-25379-9"
+}
+
 @article{aubury96_handel_c_languag_refer_guide,
 	author = {Aubury, Matthew and Page, Ian and Randall, Geoff and Saul, Jonathan and Watts, Robin},
 	title = {Handel-C Language Reference Guide},
@@ -150,6 +165,19 @@
 	series = {PLDI 2020}
 }
 
+@InProceedings{bouton09,
+	author = {Bouton, Thomas and Caminha B. de Oliveira, Diego and Déharbe, David and Fontaine, Pascal},
+	editor = "Schmidt, Renate A.",
+	title = "veriT: An Open, Trustable and Efficient SMT-Solver",
+	booktitle = "Automated Deduction -- CADE-22",
+	year = "2009",
+	publisher = "Springer Berlin Heidelberg",
+	address = "Berlin, Heidelberg",
+	pages = "151--156",
+	abstract = "This article describes the first public version of the satisfiability modulo theory (SMT) solver veriT. It is open-source, proof-producing, and complete for quantifier-free formulas with uninterpreted functions and difference logic on real numbers and integers.",
+	isbn = "978-3-642-02959-2"
+}
+
 @article{bowen98_handel_c_languag_refer_manual,
 	author = {Bowen, Matthew},
 	title = {Handel-C Language Reference Manual},