diff --git a/common/refs.bib b/common/refs.bib
index 48230a0..d400e0c 100644
--- a/common/refs.bib
+++ b/common/refs.bib
@@ -105,3 +105,12 @@
     year=2016
 }
 
+@incollection{hazelhurst1997symbolic,
+  title={Symbolic trajectory evaluation},
+  author={Hazelhurst, Scott and Seger, Carl-Johan H},
+  booktitle={Formal hardware verification},
+  pages={3--78},
+  year={1997},
+  publisher={Springer}
+}
+
diff --git a/report/report.tex b/report/report.tex
index 24fa8ce..3a30199 100644
--- a/report/report.tex
+++ b/report/report.tex
@@ -88,13 +88,14 @@ product's release date. These techniques include of course a lot of testing on
 simulated hardware or FPGAs (since an actual processor is extremely expensive
 to actually print). A lot of testing is run as a routine on the current version
 of the hardware, to catch and notify the designers, since it remains the
-easiest way to test the behaviour of a circuit. Symbolic trajectory evaluation
-has also its place in the domain, allowing one to run a circuit on a few cycles
-(before it becomes too expensive) with symbolic values, \ie{} variables instead
-of zeroes, ones and $X$s (for ``not a value''). This kind of testing is way
-more powerful than plain testing, since its results are more precise; yet it is
-also too expensive to run on a significantly long number of cycles, and
-therefore a lot of bugs are impossible to catch this way.
+easiest way to test the behaviour of a circuit. Symbolic trajectory
+evaluation~\cite{hazelhurst1997symbolic} has also its place in the domain,
+allowing one to run a circuit on a few cycles (before it becomes too expensive)
+with symbolic values, \ie{} variables instead of zeroes, ones and $X$s (for
+``not a value''). This kind of testing is way more powerful than plain testing,
+since its results are more precise; yet it is also too expensive to run on a
+significantly long number of cycles, and therefore a lot of bugs are impossible
+to catch this way.
 
 The previous methods are a good cheap method to test a circuit, but give only
 little confidence in its correction --- it only proves that among all the cases
@@ -497,8 +498,6 @@ recursively on all its matched gates. If this step succeeds, the graph
 structure is then checked. If both steps succeed, the permutation is correct
 and an isomorphism has been found; if not, we move on to the next permutation.
 
-\todo{Anything more to tell here?}
-
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \section{Pattern-match}
 
@@ -759,13 +758,22 @@ i7-3770 CPU (3.40GHz) and 8\,GB of RAM\@. % chktex 8
 The example I used widely during my project to test my program and check its
 efficiency periodically was a small processor designed one year earlier as a
 school project~\cite{sysdig_cpu}. The processor implements a large subset of
-ARM, was conceived as a few hierarchized modules (ALU, registers, opcode
-decoder, \ldots) but was flattened as a plain netlist when generated from its
-python code, so I first had to patch its generator code to make its hierarchy
-apparent.
+ARM\@. It does not feature a multiplier, nor a divider circuit, but supports
+instructions with conditions (ARM-flavoured: a whole lot of conditional
+prefixes can be plugged into an assembly instruction). It was conceived as a
+few recursively hierarchized modules, but was flattened as a plain netlist when
+generated from its python code, so I first had to patch its generator code to
+make its hierarchy apparent.
+
+The circuit is composed, at its root level, of a few modules: a memory unit
+(access to RAM), a flags unit (handling the ALU's flags), two operands units
+(decoding the operands and applying a barrel shifter if needed), an opcode
+decoding unit (decoding the program's opcodes), a registers unit (containing
+the registers) and a result selector (selecting the output between the ALU's
+and the registers' output, based on the opcode).
 
 The processor, in the end, has around 2000 leaf gates (but works at word level)
-and 240 hierarchy groups. \qtodo{Tell us more!}
+and 240 hierarchy groups.
 
 \paragraph{Signature.} First, the time required to sign the whole circuit with
 different levels of signature (\ie{} the order of signature computed for every
@@ -918,21 +926,23 @@ the gates marked with a red dot. Thus, those signatures are exactly the same.
 \section*{Conclusion}
 
 At this point, \textit{isomatch} seems to be fast enough to be plugged into
-VossII, and is being integrated at the moment. On all the cases tested, it
-returned a correct result, Even though there are a handful of ways to
-enhance it, make it faster, etc., it is useable in its current state.
+VossII, and is being integrated at the moment. On all the cases tested --- with
+tests that tried to be as complete as possible by testing each independent
+feature --- it returned a correct result. Even though there are a handful of
+ways to enhance it, make it faster, etc., it is useable in its current state.
 
 This internship led me to develop new strategies to bypass corner cases where
-the heuristics were inefficient. But this project also made me practice again
-my C++, which I had left behind for some time; and forced me to try to have a
-code as clean as possible, challenging me on small details that were easy to
-implement, but hard to implement in an understandable way.
+the heuristics were inefficient, the methods inadequate, \ldots{} But this
+project also made me practice again with C++, which I had left behind for some
+time; and forced me to try to have a code as clean as possible, challenging me
+on small details that were easy to implement, but hard to implement in an
+understandable and bug-proof way.
 
 It also diversified my experience as a student in laboratories, since my only
 other experience was from my 3rd year of Bachelor's degree internship in
 Cambridge.
 
-\todo{find better}
+\todo{Find better}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%