More details about the processor

This commit is contained in:
Théophile Bastian 2017-08-28 19:20:24 +02:00
parent 9f3120f0aa
commit c7d1841af7
2 changed files with 41 additions and 22 deletions

View file

@ -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}
}

View file

@ -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}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%