|
|
|
@ -86,7 +86,7 @@ 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 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
|
|
|
|
|
to burn). 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~\cite{hazelhurst1997symbolic} has also its place in the domain,
|
|
|
|
@ -97,18 +97,19 @@ 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
|
|
|
|
|
that were tested, all yielded a correct behaviour. These reasons led to the
|
|
|
|
|
development of proved hardware in the industry. On circuits as complex as
|
|
|
|
|
processors, usually, only sub-components are proved correct with respect to a
|
|
|
|
|
given specification of its behaviour (usually source code that should behave as
|
|
|
|
|
the processor is expected to behave, itself with respect to the written
|
|
|
|
|
documentation draft of the circuit). These proofs are typically valid only
|
|
|
|
|
while the circuit is kept in a specified context, \ie{} a set of valid inputs
|
|
|
|
|
and outputs, etc. --- that should, but is not proved to, be respected by the
|
|
|
|
|
other parts of the circuit. Yet, this trade-off between proved correctness and
|
|
|
|
|
engineer's work time already gives a pretty good confidence in the circuit.
|
|
|
|
|
The previous methods are great cheap strategies to run the first tests on a
|
|
|
|
|
circuit, but give only little confidence in its correction --- it only proves
|
|
|
|
|
that among all the cases that were tested, all yielded a correct behaviour.
|
|
|
|
|
These reasons led to the development of proved hardware in the industry. On
|
|
|
|
|
circuits as complex as processors, usually, only sub-components are proved
|
|
|
|
|
correct with respect to a given specification of its behaviour (usually source
|
|
|
|
|
code that should behave as the processor is expected to behave, itself with
|
|
|
|
|
respect to the written documentation draft of the circuit). These proofs are
|
|
|
|
|
typically valid only while the circuit is kept in a specified context, \ie{} a
|
|
|
|
|
set of valid inputs, tensions, etc. --- that should, but is not proved to, be
|
|
|
|
|
respected by the other parts of the circuit. Yet, this trade-off between proved
|
|
|
|
|
correctness and engineer's work time already gives a pretty good confidence in
|
|
|
|
|
the circuit.
|
|
|
|
|
|
|
|
|
|
In this context, Carl Seger was one of the main developers of fl at
|
|
|
|
|
Intel~\cite{seger1993vos}~\cite{seger2005industrially}~\cite{seger2006design},
|
|
|
|
@ -209,9 +210,10 @@ loading in memory only a part of the circuit, etc.).
|
|
|
|
|
\emph{Isomatch} comes along with a small parser for a toy ad-hoc language,
|
|
|
|
|
designed to allow one to quickly write a test circuit and run the
|
|
|
|
|
\emph{isomatch} functions on it. There was no real apparent need for a better
|
|
|
|
|
language, or a standard circuit description language (such as VSDL), since the
|
|
|
|
|
user will mostly use \emph{isomatch} through fl, and feed it directly with data
|
|
|
|
|
read from fl --- which is able to handle \eg{} VSDL\@.
|
|
|
|
|
language, or a standard circuit description language (such as
|
|
|
|
|
VHDL~\cite{navabi1997vhdl}), since the user will mostly use \emph{isomatch}
|
|
|
|
|
through fl, and feed it directly with data read from fl --- which is able to
|
|
|
|
|
handle \eg{} VHDL\@.
|
|
|
|
|
|
|
|
|
|
\subsection{Codebases}
|
|
|
|
|
|
|
|
|
@ -434,7 +436,7 @@ At this point, we can define the \emph{signature of order $n$} ($n \in
|
|
|
|
|
+ \text{IO adjacency}
|
|
|
|
|
+ \hspace{-2em}\sum\limits_{C_i \in \,\text{neighbours of inputs}}
|
|
|
|
|
\hspace{-2em}\sig_n(C_i) \hspace{1em}
|
|
|
|
|
- \hspace{-2em}\sum\limits_{C_o \in \,\text{neighbours of inputs}}
|
|
|
|
|
- \hspace{-2em}\sum\limits_{C_o \in \,\text{neighbours of outputs}}
|
|
|
|
|
\hspace{-2em}\sig_n(C_o)
|
|
|
|
|
\end{align*}
|
|
|
|
|
|
|
|
|
@ -458,11 +460,11 @@ lazy.
|
|
|
|
|
|
|
|
|
|
To keep those memoized values up to date whenever the structure of the circuit
|
|
|
|
|
is changed (since this is meant to be integrated in a programming language, fl,
|
|
|
|
|
meaning the structure of the circuit will possibly be created, checked for
|
|
|
|
|
signature, altered, then checked again), each circuit keeps track of a
|
|
|
|
|
``timestamp'' of last modification, which is incremented whenever the circuit
|
|
|
|
|
or its children are modified. A memoized data is always stored alongside with a
|
|
|
|
|
timestamp of computation, which invalidates a previous result when needed.
|
|
|
|
|
a standard workflow will possibly be create a circuit, check its signature,
|
|
|
|
|
alter it, then check again), each circuit keeps track of a ``timestamp'' of
|
|
|
|
|
last modification, which is incremented whenever the circuit or its children
|
|
|
|
|
are modified. A memoized data is always stored alongside with a timestamp of
|
|
|
|
|
computation, which invalidates a previous result when needed.
|
|
|
|
|
|
|
|
|
|
One possible path of investigation for future work, if the computation turns
|
|
|
|
|
out to be still too slow in real-world cases --- which looks unlikely, unless
|
|
|
|
@ -480,11 +482,11 @@ Group equality itself is handled as a simple backtracking algorithm, trying to
|
|
|
|
|
establish a match (an isomorphism, that is, a permutation of the gates of one
|
|
|
|
|
of the groups) between the two groups given.
|
|
|
|
|
|
|
|
|
|
The gates of the two groups are matched by equal signatures, equal number of
|
|
|
|
|
inputs and outputs, based on the signature of default order (that is, 2). A few
|
|
|
|
|
checks are made, \eg{} every matching group must have the same size on both
|
|
|
|
|
sides (if not, then, necessary, the two groups won't match). Then, the worst
|
|
|
|
|
case of number of permutations to check is evaluated.
|
|
|
|
|
The gates of the two groups are matched by equal number of inputs and outputs
|
|
|
|
|
and equal signatures --- based on the signature of default order (that is, 2).
|
|
|
|
|
A few checks are made, \eg{} every matching group must have the same size on
|
|
|
|
|
both sides (if not, then, necessarily, the two groups won't match). Then, the
|
|
|
|
|
worst case of number of permutations to check is evaluated.
|
|
|
|
|
|
|
|
|
|
If this number is too high, the signature order will be incremented, and the
|
|
|
|
|
matching groups re-created accordingly, until a satisfyingly low number of
|
|
|
|
@ -683,8 +685,13 @@ occur).
|
|
|
|
|
|
|
|
|
|
\subsection{Implementation optimisations}
|
|
|
|
|
|
|
|
|
|
\paragraph{Pre-check.} The needle will, in most cases, not be found at all in
|
|
|
|
|
a given hierarchy group of the haystack. To avoid wasting computation time, we
|
|
|
|
|
first check that every signature present in the needle is present at least as
|
|
|
|
|
many times in the haystack. This simple check saved a lot of time.
|
|
|
|
|
|
|
|
|
|
\paragraph{Initial permutation matrix.} The matrix is first filled according to
|
|
|
|
|
the signatures matches. Note that only signatures of order 0 --- \ie{} the
|
|
|
|
|
the signatures' matches. Note that only signatures of order 0 --- \ie{} the
|
|
|
|
|
inner data of a vertex --- can be used here: indeed, we cannot rely on the
|
|
|
|
|
context here, since there can be some context in the haystack that is absent
|
|
|
|
|
from the needle, and we cannot check for ``context inclusion'' with our
|
|
|
|
@ -697,11 +704,6 @@ signatures. Thus, two circuits cannot be matched if this condition is not
|
|
|
|
|
respected for each pair of corresponding wires of those circuits, and their
|
|
|
|
|
corresponding cell in the permutation matrix can be nulled.
|
|
|
|
|
|
|
|
|
|
\paragraph{Pre-check.} The needle will, in most cases, not be found at all in
|
|
|
|
|
a given hierarchy group of the haystack. To avoid wasting computation time, we
|
|
|
|
|
first check that every signature present in the needle is present at least as
|
|
|
|
|
many times in the haystack. This simple check saved a lot of time.
|
|
|
|
|
|
|
|
|
|
\paragraph{Conversion to adjacency matrix.} The internal structures and graphs
|
|
|
|
|
are represented as inherited classes of \lstcpp{CircuitTree}, connected to
|
|
|
|
|
various \lstcpp{WireId}s. Thus, there is no adjacency matrix easily available,
|
|
|
|
@ -730,8 +732,7 @@ the usual test set.
|
|
|
|
|
\textbf{Ordering method} & \textbf{Run time (ms)} & \textbf{Loss (\%)} \\
|
|
|
|
|
Wires by degree decreasing, then gates as they come & 48.8 & --- \\
|
|
|
|
|
As they come, gates then wires & 49.1 & 0.6\% \\
|
|
|
|
|
Wires by degree decreasing, then gates by degree decreasing & 49.3
|
|
|
|
|
& 1.0\% \\
|
|
|
|
|
By degree decreasing, wires then gates & 49.3 & 1.0\% \\
|
|
|
|
|
As they come, wires then gates & 49.3 & 1.0\% \\
|
|
|
|
|
Gates as they come, then wires by degree decreasing & 49.5 & 1.4\% \\
|
|
|
|
|
By degree decreasing, all mixed & 49.5 & 1.4\% \\
|
|
|
|
@ -833,11 +834,14 @@ afford really high order signatures (\eg{} 40 or 50, which already means that
|
|
|
|
|
the diameter of the group is 40 or 50) without having a real impact on the
|
|
|
|
|
computation time.
|
|
|
|
|
|
|
|
|
|
This linearity means that we can increase the signature order without too much
|
|
|
|
|
impact, as we do when computing a group equality.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
\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
|
|
|
|
|
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{313\,ms} to
|
|
|
|
@ -939,12 +943,6 @@ 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}
|
|
|
|
|
|
|
|
|
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
|
|
|
|
|
|
|
\printbibliography{}
|
|
|
|
|