First few slides

This commit is contained in:
Théophile Bastian 2017-09-07 16:13:10 +02:00
parent fb8c99bb13
commit e36ed54167

View file

@ -35,11 +35,63 @@
\section{Contexte}
\begin{frame}{Contexte}
Matériel faillible
\begin{itemize}
\item Intel FDIV (Pentium, 1994)
\item Skylake, Kaby Lake (2017)
\item \ldots
\end{itemize}
$\implies$ dangereux, cher pour l'industrie. Solutions~?
\begin{itemize}
\item Tester, tester, tester. Simulation, FPGA, matériel, \ldots
\item Test dirigé~? \emph{Symbolic Trajectory Evaluation}
\item \alert{Matériel prouvé}
\begin{itemize}
\item Dès la conception~?
\item Après coup~?
\end{itemize}
\end{itemize}
\end{frame}
\begin{frame}{Voss II}
\begin{itemize}
\item \alert{fl}~: langage fonctionnel, BDDs, STE, \ldots \\
Langage généraliste du prouveur hardware, utilisé chez Intel
\item \emph{Idée}~: prouver un circuit simple puis le raffiner est plus
aisé.
\item Workflow~:
\begin{itemize}
\item Prouver un circuit simple~;
\item le raffiner \emph{par transformations prouvées}.
\end{itemize}
\item Raffinements~: \alert{recherche de motifs}
\end{itemize}
\end{frame}
\section{Problème}
\begin{frame}
Deux problèmes à résoudre~:
\begin{enumerate}[A]
\item Deux circuits sont-ils identiques~?
\item Quelles sont les occurrences de $N$ dans $H$~?
\end{enumerate}
\begin{itemize}
\item A~: isomorphisme de graphes, NP-hard. Cf. Babai.
\item B~: isomorphisme de sous-graphes, NP-complet.
\vspace{1em}
\item Circuits~: processeurs entiers~? \emph{Très gros}.
\item Transformations \emph{interactives}~: doit être \emph{rapide}.
\end{itemize}
\end{frame}
\section{Approche de résolution}