126 lines
4.9 KiB
TeX
126 lines
4.9 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{cite}
|
|
\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}
|
|
|
|
\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{abstract}
|
|
\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 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
|
|
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 \todo{the?} main developer of FL
|
|
\todo{(?, acronym?)} at Intel, a functional programming language integrating
|
|
many features useful to get insights of a circuit, testing it and proving it.
|
|
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.\\
|
|
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.
|
|
|
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
\section{Context \& AST}
|
|
|
|
\todo{Rename this section}\\
|
|
\todo{}
|
|
|
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
\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{}
|
|
|
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
\section{Signatures}
|
|
\todo{}
|
|
|
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
\section{Group equality}
|
|
\todo{}
|
|
|
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
\section{Pattern-match}
|
|
\todo{}
|
|
|
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
\section{Performance}
|
|
\todo{}
|
|
|
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
|
\printbibliography{}
|
|
|
|
\end{document}
|