Add circuit AST
This commit is contained in:
parent
f623ad1191
commit
0f04918c33
|
|
@ -7,7 +7,6 @@
|
|||
\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}
|
||||
|
|
@ -18,6 +17,7 @@
|
|||
\usepackage{leftrule_theorems}
|
||||
\usepackage{my_listings}
|
||||
\usepackage{my_hyperref}
|
||||
\usepackage{../common/internship}
|
||||
|
||||
\bibliography{../common/refs}
|
||||
|
||||
|
|
@ -50,56 +50,106 @@ 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.
|
||||
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
|
||||
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
|
||||
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.
|
||||
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.\\
|
||||
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{Context \& AST}
|
||||
|
||||
\todo{Rename this section}\\
|
||||
\todo{}
|
||||
\todo{Rename this section}
|
||||
|
||||
\begin{figure}[!h]
|
||||
\begin{align*}
|
||||
\textbf{Integer constant } n, m, \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{c}{n})
|
||||
&\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}
|
||||
|
||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||
\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{}
|
||||
|
||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||
|
|
|
|||
Loading…
Reference in New Issue