254 lines
11 KiB
TeX
254 lines
11 KiB
TeX
\documentclass[11pt,a4paper]{article}
|
|
\usepackage[utf8]{inputenc}
|
|
\usepackage[T1]{fontenc}
|
|
\usepackage{amsmath}
|
|
\usepackage{amsfonts}
|
|
\usepackage{amssymb}
|
|
\usepackage{graphicx}
|
|
\usepackage{indentfirst}
|
|
\usepackage{enumerate}
|
|
\usepackage{caption}
|
|
\usepackage[backend=biber,style=trad-alpha]{biblatex}
|
|
\usepackage[left=2cm,right=2cm,top=2cm,bottom=2cm]{geometry}
|
|
|
|
|
|
% Custom packages
|
|
\usepackage{todo}
|
|
\usepackage{leftrule_theorems}
|
|
\usepackage{my_listings}
|
|
\usepackage{my_hyperref}
|
|
\usepackage{../common/internship}
|
|
\usepackage{../common/math}
|
|
|
|
\bibliography{../common/refs}
|
|
|
|
\title{Pattern-matching and substitution in electronic circuits}
|
|
\author{Théophile Bastian, under supervision of Carl-Johan Seger
|
|
and Mary Sheeran\\
|
|
\small{Chalmers University, Göteborg, Sweden}}
|
|
\date{February~--~June 2017}
|
|
|
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
|
\begin{document}
|
|
\maketitle
|
|
|
|
\begin{abstract}
|
|
\todo{enhance abstract?}
|
|
|
|
The present report describes and summarizes my 1st year of Master's
|
|
degree's internship at the university of Chalmers, Göteborg, Sweden. I
|
|
worked under supervision of Carl-Johan Seger and Mary Sheeran.
|
|
|
|
The project's goal was to contribute to VossII, a hardware proving tool
|
|
cloning fl, developed at Intel by Carl Seger for internal usage only. It
|
|
led me to work on \emph{pattern-matching} on electronic circuits for a
|
|
\emph{search-and-replace} method, allowing one to apply previously proved
|
|
transformations to a circuit.
|
|
|
|
This problem turns out to be more or less the \emph{subgraph isomorphism
|
|
problem}, which is NP-complete, and must nevertheless be solved fast on
|
|
processor-sized circuits on this particular case.
|
|
|
|
During my internship, I developed a C++ library to perform this task that
|
|
will be integrated in VossII, based on a few well-known algorithms as well
|
|
as some ad-hoc heuristics and algorithm tweaks to better match the context
|
|
of circuits. One of my objectives all along was also to keep a clean and
|
|
well-documented codebase, as the tool will have to be maintainable by
|
|
others later.
|
|
\end{abstract}
|
|
|
|
\tableofcontents
|
|
|
|
\pagebreak
|
|
|
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
\section{Introduction}
|
|
|
|
In the previous years, verification and proved software has gathered an
|
|
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~\cite{pratt1995fdiv} that affected a large number of
|
|
Pentium processors lead to wrong results for some floating point divisions.
|
|
Intel had to offer to replace all the defective 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
|
|
release date. Among those are \todo{list + cite}, but also proved hardware. On
|
|
circuits as complex as processors, usually, only sub-components are proved
|
|
correct in a specified context --- 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, a
|
|
functional ml-inspired programming language integrating many features useful to
|
|
get insights of a circuit, testing it and proving it. It mostly features
|
|
symbolic trajectory evaluation based model checking and theorem proving, and is
|
|
intended to be an all-purpose toolbox for the hardware prover.
|
|
|
|
Among other features, it includes a ``search and replace'' feature, which can
|
|
search every occurrence of a given gates pattern in a circuit, and replace it
|
|
by some other gates pattern, proved observationally equivalent beforehand.
|
|
Time has proved this method very efficient to design circuits: this way, one
|
|
can start from an inefficient, yet simple circuit, prove it, and then refine it
|
|
into an equivalent, yet efficient one, through proved transformations. It is
|
|
also possible to go the other way, and start with an optimized circuit, hard to
|
|
understand, and make it easier to understand to work more efficiently.
|
|
|
|
\paragraph{My internship} lies amid a project shared between Carl-Johan Seger
|
|
and Mary Sheeran, aiming to develop tools for proved design of FPGA circuits.
|
|
One of the keystones of this project is an open-sourced and publicly available
|
|
version of fl, used for the proving part, and is still at the moment under
|
|
development.
|
|
|
|
My part of the work resided on this ``search and replace'' tool. More
|
|
specifically, I focused on writing a C++ library, \emph{isomatch}, which is
|
|
interfaced with the C core of fl and provides it with low-level and very fast
|
|
functions for this task.
|
|
|
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
\section{Problem setting}
|
|
|
|
\subsection{Circuit description}
|
|
|
|
\begin{figure}[!h]
|
|
\begin{align*}
|
|
\textbf{Integer constant } n, m, p, q, \ldots \qquad& \\
|
|
\\
|
|
\textbf{Wire } in0, out0, ctl0, \ldots \qquad& \\
|
|
\\
|
|
\textbf{Vector } \evec{v}{n} & & \textit{($n$ elements of type $v$)} \\
|
|
\\
|
|
\textbf{Circuit } c, d, \ldots ::=~
|
|
&\text{delay} (in0, out0) &\textit{(delay 1 clock tick)} \\
|
|
\vert~&\text{tristate} (in0, out0, ctl0)
|
|
&\textit{(three-state gate)} \\
|
|
\vert~&\text{comb} (\evec{in0}{n}, \evec{out0}{m}, \evec{e}{m})
|
|
&\textit{(combinatorial gate)} \\
|
|
\vert~&\text{assert} (\evec{in0}{n}, \evec{e}{m})
|
|
&\textit{(assertion gate)} \\
|
|
\vert~&\text{group} (\evec{in0}{n}, \evec{out0}{m}, \evec{c}{p})
|
|
&\textit{(circuit hierarchical group)} \\
|
|
\\
|
|
\textbf{Binary operator } \otimes ::=~
|
|
&\wedge & \textit{(and)} \\
|
|
\vert~&\vee & \textit{(or)} \\
|
|
\vert~&\oplus & \textit{(xor)} \\
|
|
\vert~&+ & \textit{(add)} \\
|
|
\vert~&- & \textit{(sub)} \\
|
|
\vert~&\times & \textit{(times)} \\
|
|
\vert~&\div & \textit{(div)} \\
|
|
\vert~&\% & \textit{(mod)} \\
|
|
\vert~&\lsl & \textit{(logical shift left)} \\
|
|
\vert~&\lsr & \textit{(logical shift right)} \\
|
|
\vert~&\asr & \textit{(arithmetic shift right)} \\
|
|
\\
|
|
\textbf{Unary and constant operator } \otimes_0 ::=~
|
|
&\clsl & \textit{(logical shift left of constant)} \\
|
|
\vert~&\clsr & \textit{(logical shift right of constant)} \\
|
|
\vert~&\casr & \textit{(arithmetic shift right of constant)} \\
|
|
\\
|
|
\textbf{Unary operator } \ominus ::=~
|
|
&\lnot & \textit{(logical negation)} \\
|
|
\\
|
|
\textbf{Expression } e, f, \ldots ::=~
|
|
& x & \textit{(variable)} \\
|
|
\vert~& n & \textit{(integer constant)} \\
|
|
\vert~& e \otimes f & \textit{(binary operator)} \\
|
|
\vert~& e \otimes_0 n & \textit{(unary operator with constant)} \\
|
|
\vert~& \ominus e & \textit{(unary operator)} \\
|
|
\vert~& e_{\vert~n \ldots m} & \textit{(slicing: take a subword)}\\
|
|
\vert~& e~\vert~f & \textit{(merging: concatenate two words)} \\
|
|
\end{align*}
|
|
\caption{AST of circuits used}\label{fig:ast}
|
|
\end{figure}
|
|
|
|
The circuits on which \emph{isomatch} is working are described, and internally
|
|
represented, by the AST in Figure~\ref{fig:ast}.
|
|
|
|
The most important thing in the description of circuits here, is that those
|
|
circuits are organized as a hierarchy of \emph{circuit groups}. This hierarchy
|
|
can be seen as the construction of a circuit by assembling smaller integrated
|
|
circuits (ICs), themselves built the same way, etc. A group is composed of
|
|
sub-circuits, input pins and output pins. Each level can of course contain
|
|
``leaf'' gates, like \textit{and} or \textit{delay} gates. This is important,
|
|
because it allows the program to work on smaller areas the circuit (\eg{}
|
|
loading in memory only a part of the circuit, etc.).
|
|
|
|
\subsection{Objective}
|
|
|
|
More precisely, the problems that \emph{isomatch} must solve are the following.
|
|
|
|
\begin{enumerate}
|
|
\item\label{prob:equal} Given two circuit groups, are they structurally
|
|
equivalent? That is, are they the same circuit, arranged in a different
|
|
way, with possibly different names, etc.?
|
|
|
|
\item\label{prob:match} Given two circuits, \emph{needle} and
|
|
\emph{haystack}, find every (non-overlapping) occurrence of \emph{needle} in
|
|
\emph{haystack}. An occurrence is a set $S$ of sub-circuits of
|
|
\emph{haystack} such that there is a one-to-one mapping of structurally
|
|
equivalent circuits of $S$ with circuits of \emph{needle}, and those
|
|
circuits are connected the same way in both circuits.
|
|
\end{enumerate}
|
|
|
|
Both problems are hard. The first one is an instance of graph isomorphism, as
|
|
the actual question is whether there exists a one-to-one mapping between
|
|
sub-circuits of the two groups, such that every mapped circuit is equal to the
|
|
other (either directly if it is a leaf gate, or recursively with the same
|
|
procedure); and whether this mapping respects connections (edges) between those
|
|
circuits. Graph isomorphism is known to be in NP (given a permutation of the
|
|
first graph, it is polynomial to check whether the first is equal to the second
|
|
\wrt{} the permutation), but not known to be in either P or NP-complete. Thus,
|
|
since Babai's work on graph isomorphism~\cite{babai2016graph} is only of
|
|
theoretical interest, the known algorithms remain in worst-case exponential
|
|
time, and require ad-hoc heuristics for specific kind of graphs to get maximum
|
|
efficiency.
|
|
|
|
The second one is an instance of subgraph isomorphism problem, which is known
|
|
to be NP-complete~\cite{cook1971complexity}. Even though a few algorithms
|
|
(discussed later) are known to be efficient in most cases for this problem, it
|
|
is nevertheless necessary to implement them the right way, and with the right
|
|
heuristics, to get the desired efficiency for the given problem.
|
|
|
|
\subsection{Sought efficiency}
|
|
|
|
The goal of \textit{isomatch} is to be applied to large circuits on-the-fly,
|
|
during their conception. Those circuits can (and will probably) be as large as
|
|
a full processor, and the software will be operated by a human, working on
|
|
their circuit. Thus, \textit{isomatch} must be as fast as possible, since
|
|
matching operation will be executed often, and often multiple times in a row.
|
|
It must then remain fast enough for the human not to lose too much time, and
|
|
eventually lose patience.
|
|
|
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
\section{General approach}
|
|
|
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
\section{Signatures}
|
|
\todo{}
|
|
|
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
\section{Group equality}
|
|
\todo{}
|
|
|
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
\section{Pattern-match}
|
|
\todo{}
|
|
|
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
\section{Performance}
|
|
\todo{}
|
|
|
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
|
\printbibliography{}
|
|
|
|
\end{document}
|