summaryrefslogtreecommitdiffstats
path: root/chapters/background.tex
diff options
context:
space:
mode:
Diffstat (limited to 'chapters/background.tex')
-rw-r--r--chapters/background.tex66
1 files changed, 59 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