diff --git a/common/refs.bib b/common/refs.bib index bd4e349..5afe8ea 100644 --- a/common/refs.bib +++ b/common/refs.bib @@ -98,3 +98,10 @@ publisher={IEEE} } +@misc{sysdig_cpu, + author={Théophile Bastian and Noémie Cartier and Nathanaël Courant}, + title={``Système digital'' project}, + howpublished={\url{https://github.com/tobast/sysdig-full/}}, + year=2016 +} + diff --git a/report/report.tex b/report/report.tex index d9e46eb..c3de008 100644 --- a/report/report.tex +++ b/report/report.tex @@ -9,6 +9,9 @@ \usepackage{enumerate} \usepackage{caption} \usepackage{algorithmicx} +%\usepgfplotslibrary{external} +%\tikzexternalize + \usepackage[backend=biber,style=trad-alpha]{biblatex} \usepackage[left=2cm,right=2cm,top=2cm,bottom=2cm]{geometry} @@ -21,6 +24,8 @@ \usepackage{../common/internship} \usepackage{../common/math} +\usepackage{pgfplots} + \bibliography{../common/refs} \title{Pattern-matching and substitution in electronic circuits} @@ -574,7 +579,84 @@ many times in the haystack. This simple check saved a lot of time. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \section{Performance} -\todo{} +In this section, all the measures were made on a computer with an Intel +i7-3770 CPU (3.40GHz) and 8\,GB of RAM\@. % chktex 8 + +\subsection{Small processor} + +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. + +The processor, in the end, has around 2000 leaf gates (but works at word level) +and 240 hierarchy groups. \qtodo{Tell us more!} + +\paragraph{Signature.} First, the time required to sign the whole circuit with +different levels of signature (\ie{} the order of signature computed for every +part of the circuit). In practice, we never compute high order signatures for a +whole circuit, as signature of subgroups are always computed by default at the +order $2$, unless this particular group needs a more accurate signature. + +The measures were made for 100 consecutive runs of the program (then averaged +for a single run) and measured by the command \texttt{time}. + +\begin{center} + \begin{tikzpicture} + \begin{axis}[ + title={Signature time of the processor for different levels + of signature}, + xlabel={Level of signature}, + ylabel={Time (ms)}, + xmin=0, xmax=16, + ymin=0, ymax=300, + legend pos=north west, + ymajorgrids=true, + grid style=dashed, + ] + + \addplot[ + color=blue, + mark=square, + ] + coordinates { + (2,105.4) + (3,122.6) + (4,140.1) + (5,155.4) + (6,171.2) + (7,183.9) + (8,198.3) + (9,211.2) + (10,224.3) + (11,236.7) + (12,248.5) + (13,259.3) + (14,271.7) + (15,281.4) + }; + \legend{-O3} + \end{axis} + \end{tikzpicture} +\end{center} + + +\paragraph{Equality.} To test the circuit group equality, a small piece of +code takes a circuit, scrambles it as much as possible +--- without altering its structure ---, \eg{} by renaming randomly its parts, +by randomly changing the order of the circuits and groups, \ldots The circuit +is then matched with its unaltered counterpart. + +For the processor described above, it takes about \textbf{477\,ms} to +prove it equal to its scrambled version, and then the other way around. Yet, +the memoized results (essentially the signatures) are kept for the second one, +considerably speeding it up: the same program proving only one way takes about +\textbf{475\,ms}. \todo{explain why} + + \subsection{Corner cases}