From 0575bfd3f5e2b0e153d427b092838d2b712d1024 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Th=C3=A9ophile=20Bastian?= <contact@tobast.fr>
Date: Sat, 19 Aug 2017 12:30:11 +0200
Subject: [PATCH] Switch to biblatex

---
 common/refs.bib   |  8 ++++++++
 report/report.tex | 36 ++++++++++++++++++++++++++++--------
 2 files changed, 36 insertions(+), 8 deletions(-)

diff --git a/common/refs.bib b/common/refs.bib
index d7cc631..d013305 100644
--- a/common/refs.bib
+++ b/common/refs.bib
@@ -7,6 +7,14 @@
   publisher={Springer}
 }
 
+@online{nicely_fdiv,
+    author = {Thomas Nicely},
+    title={Pentium FDIV flaw FAQ},
+    year = {2011},
+    url = {http://www.trnicely.net/pentbug/pentbug.html},
+    urldate = {2017-08-10}
+}
+
 @inproceedings{harrison2003formal,
   title={Formal verification at intel},
   author={Harrison, John},
diff --git a/report/report.tex b/report/report.tex
index 1a73b51..3d7bb25 100644
--- a/report/report.tex
+++ b/report/report.tex
@@ -7,8 +7,9 @@
 \usepackage{graphicx}
 \usepackage{indentfirst}
 \usepackage{enumerate}
-\usepackage{cite}
+%\usepackage{cite}
 \usepackage{caption}
+\usepackage[backend=biber,style=trad-alpha]{biblatex}
 \usepackage[left=2cm,right=2cm,top=2cm,bottom=2cm]{geometry}
 
 
@@ -18,8 +19,11 @@
 \usepackage{my_listings}
 \usepackage{my_hyperref}
 
+\bibliography{../common/refs}
+
 \title{Pattern-matching and substitution in electronic circuits}
-\author{Théophile Bastian, under supervision of Carl-Johan Seger\\
+\author{Théophile Bastian, under supervision of Carl-Johan Seger
+        and Mary Sheeran\\
     \small{Chalmers University, Göteborg, Sweden}}
 \date{February~--~June 2017}
 
@@ -44,11 +48,12 @@ increasing interest in the computer science community, as people realised how
 hard bugs are to track down. But hardware bugs are even more tedious to find
 and fix, and can easily lead to disastrous consequences, as those cannot be
 patched on existing hardware. For instance, the well-known Pentium
-``\textsc{fdiv}'' bug~\ref{pratt1995fdiv} that affected a large number of
+``\textsc{fdiv}'' bug~\cite{pratt1995fdiv} that affected a large number of
 Pentium processors lead to wrong results for some floating point divisions.
-Intel had to replace \todo{how many?} CPUs, leading to a loss of \todo{how
-much?}. Even recently, the Skylake and Kiby Lake \todo{(?)} hyperthreading bug
-had to be patched using microcode, loosing performance and reliability.
+Intel had to replace \todo{how many?} CPUs, leading to an announced loss of 475
+million dollars~\cite{nicely_fdiv}. Even recently, the Skylake and Kaby Lake
+hyperthreading bug had to be patched using microcode, loosing performance and
+reliability.
 
 To avoid such disasters, the industry nowadays uses a wide range of techniques
 to catch bugs as early as possible -- which, hopefully, is before the product's
@@ -79,6 +84,22 @@ understand, and make it easier to understand to work more efficiently.
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \section{General approach}
+
+Among many others, one idea that proved itself efficient at Intel for circuit
+verification was to prove the correctness of a ``simple'' circuit, that is, a
+circuit that is not too optimized, on which the various features and parts can
+be easily seen and properties can be expressed cleanly. This circuit could then
+be refined afterwards, only by means of proved transformations mostly
+resulting from a somewhat large database of usual transformations, along with
+their proofs of correctness.
+
+This process of replacement was mostly done through a ``search and replace''
+tool. The tool would basically search every (non-overlapping) occurrence of a
+given ``pattern'', remove these occurrences from the circuit, and plug the
+replacement version of the pattern in its place. A pattern, in this context,
+consists in a piece of circuit, along with in- and outbound wires to be
+reconnected in the right place afterwards.
+
 \todo{}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -99,7 +120,6 @@ understand, and make it easier to understand to work more efficiently.
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
-\bibliography{../common/refs}
-\bibliographystyle{alpha}
+\printbibliography{}
 
 \end{document}