295 lines
8.5 KiB
TeX
295 lines
8.5 KiB
TeX
% vim: :spell spelllang=fr
|
|
\documentclass[11pt]{beamer}
|
|
\usetheme{Warsaw}
|
|
\usepackage[utf8]{inputenc}
|
|
\usepackage[french]{babel}
|
|
\usepackage[T1]{fontenc}
|
|
\usepackage{amsmath}
|
|
\usepackage{amsfonts}
|
|
\usepackage{amssymb}
|
|
\usepackage{graphicx}
|
|
\usepackage{my_listings}
|
|
%\usepackage{my_hyperref}
|
|
\usepackage{pgfplots}
|
|
\usepackage{math}
|
|
\usepackage{../common/internship}
|
|
\setbeamertemplate{navigation symbols}{}
|
|
|
|
\newcommand{\cf}{\textit{cf.}}
|
|
|
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
\author[Théophile Bastian]{Théophile \textsc{Bastian} \\
|
|
\small{Sous la supervision de Carl Seger et Mary Sheeran}}
|
|
\title{Soutenance de stage, M2}
|
|
\subtitle{Recherche de motifs et substitution dans des circuits électroniques}
|
|
\date{Février\,--\,Juin 2017}
|
|
%\subject{}
|
|
%\logo{}
|
|
\institute{\textit{Chalmers Tekniska Universitet}, Göteborg, Suède}
|
|
\begin{document}
|
|
|
|
\begin{frame}
|
|
\titlepage{}
|
|
\end{frame}
|
|
|
|
\begin{frame}
|
|
\tableofcontents
|
|
\end{frame}
|
|
|
|
\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 Propriétaire~: C. Seger développe une alternative open source
|
|
(Voss II)
|
|
|
|
\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}
|
|
\item \alert{isomatch}~: bibliothèque C++ pour recherche de motifs.
|
|
\end{itemize}
|
|
\end{frame}
|
|
|
|
\section{Problème}
|
|
|
|
\begin{frame}{Problèmes}
|
|
\begin{enumerate}[A]
|
|
\item Deux circuits sont-ils identiques~?
|
|
\item Quelles sont les occurrences de $N$ dans $H$~?
|
|
\pause{}
|
|
\item (Avoir un code documenté, très propre, idiomatique, réutilisable)
|
|
\end{enumerate}
|
|
|
|
\pause{}
|
|
|
|
\begin{itemize}
|
|
\item A~: isomorphisme de graphes ($\implies$ circuits égaux). \\
|
|
NP-hard. Cf. Babai.
|
|
\item B~: isomorphisme de sous-graphes ($\implies$
|
|
sous-circuit égal). \\
|
|
NP-complet.
|
|
|
|
\vspace{1em}
|
|
|
|
\item Circuits~: processeurs entiers~? \emph{Très gros}.
|
|
\item Transformations \emph{interactives}~: doit être \emph{rapide}.
|
|
\end{itemize}
|
|
\end{frame}
|
|
|
|
\begin{frame}{Forme des circuits}
|
|
\begin{itemize}
|
|
\item Portes, plusieurs types (combinatoire, tristate, délai,
|
|
assertion)
|
|
\item Plusieurs pins par porte
|
|
\item Fil~: plusieurs pins connectés \\
|
|
($\implies$ pas un graphe immédiatement)
|
|
\item \alert{Niveaux de hiérarchie}~: porte \og{}groupe~\fg{}
|
|
\end{itemize}
|
|
\end{frame}
|
|
|
|
\section{Approche de résolution}
|
|
|
|
\begin{frame}{Approche générale}
|
|
\begin{itemize}
|
|
\item \alert{Signatures}~: valeur 64 bits décrivant une porte du
|
|
circuit. \\
|
|
Rapide à calculer, rapide à comparer. \\
|
|
Le plus discriminant possible.
|
|
|
|
\pause{}\vspace{1em}
|
|
|
|
\item \alert{Égalité}~: test des permutations, guidé par
|
|
signatures. \\
|
|
Interagit avec les signatures.
|
|
|
|
\pause{}\vspace{1em}
|
|
|
|
\item \alert{Recherche}~: algorithme d'Ullmann, guidé par signatures.
|
|
\end{itemize}
|
|
\end{frame}
|
|
|
|
\subsection{Signatures}
|
|
|
|
\begin{frame}{Signature}
|
|
\begin{itemize}
|
|
\item Doit ignorer la \emph{représentation} du graphe
|
|
\item Doit capturer tout ce qui est \emph{inhérent} au circuit
|
|
\item Oublier les \emph{noms}, \emph{identifiants}~; on oublie les
|
|
\alert{ordres}.
|
|
|
|
\vspace{1em}
|
|
|
|
\item Signature interne~: \emph{hashs} capturant le contenu de la porte
|
|
\item On perd les relations entre portes \\
|
|
$\leadsto$ signature d'ordre $n$.
|
|
\end{itemize}
|
|
\end{frame}
|
|
|
|
\begin{frame}{Signature d'ordre $n$}
|
|
Prendre en compte les voisins, mais pas d'IDs \\
|
|
\quad $\leadsto$ Signature des voisins
|
|
|
|
\pause{}
|
|
|
|
\begin{align*}
|
|
\sig_0(C) :&= \text{signature interne} \\
|
|
\sig_{n+1}(C) :&=
|
|
\sum_{e \in \text{entrée}} \sig_n(e)
|
|
- \sum_{s \in \text{sortie}} \sig_n(s)
|
|
+ \text{sig. I/O}
|
|
+ \sig_0(C)
|
|
\end{align*}
|
|
|
|
\vspace{1em}
|
|
\begin{itemize}
|
|
\item $\sig_n$~: prend en compte \emph{à distance $n$}
|
|
\item Signature I/O~: adjacence aux pins I/O du groupe parent
|
|
\item Calcul~: temps linéaire
|
|
\end{itemize}
|
|
\end{frame}
|
|
|
|
\subsection{Égalité de groupes}
|
|
|
|
\begin{frame}{Égalité de groupes}
|
|
\begin{itemize}
|
|
\item Algorithme naïf~: tester toutes les permutations
|
|
\item Peu de permutations possibles~: \cf{} signatures
|
|
\item Nombre de permutations calculable facilement
|
|
\item Nombre trop élevé~: signatures d'ordre plus élevé
|
|
\begin{itemize}
|
|
\item Calculable linéairement (taille du groupe)
|
|
\end{itemize}
|
|
\item En pratique~: pas plus de 4 permutations
|
|
\end{itemize}
|
|
\end{frame}
|
|
|
|
\subsection{Recherche de motifs}
|
|
|
|
\begin{frame}{Algorithme d'Ullmann}
|
|
\begin{itemize}
|
|
\item Algorithme de backtrack pour isomorphisme de sous-graphes
|
|
\item Quelques heuristiques et optimisations mineures
|
|
\item \emph{Raffinement}
|
|
\end{itemize}
|
|
|
|
\pause{}
|
|
|
|
\begin{itemize}
|
|
\item Pour chaque $i \in$ needle \\
|
|
\quad{} Pour chaque $j \in$ haystack pouvant correspondre
|
|
avec $i$ \\
|
|
\quad\quad{} Pour chaque voisin $k$ de $i$ (needle) \\
|
|
\quad\quad\quad{} Si $k$ ne correspond à aucun voisin de $j$ \\
|
|
\quad\quad\quad\quad{} Supprimer la correspondance
|
|
\item Itérer jusqu'à point fixe
|
|
\end{itemize}
|
|
\end{frame}
|
|
|
|
\section{Performance}
|
|
|
|
\begin{frame}{Performance sur un processeur}
|
|
\begin{itemize}
|
|
\item Mesures~: processeur de \og{}système digital~\fg, architecture
|
|
ARM\@. Opère sur des mots mémoire.
|
|
\item $\sim 2000$ portes terminales, $\sim 240$ groupes
|
|
\item Mesures sur un i7-3770, 8\,Go de RAM % chktex 8
|
|
|
|
\vspace{1em}
|
|
|
|
\item Signature d'ordre 2~: 105\,ms
|
|
\item Signature d'ordre 10~: 224\,ms
|
|
\item Test d'égalité~: 310\,ms
|
|
\item Recherche de tous les (73) MUX~: 113\,ms
|
|
\end{itemize}
|
|
\end{frame}
|
|
|
|
\begin{frame}{Linéarité du temps de signature}
|
|
\begin{figure}
|
|
\centering
|
|
\begin{tikzpicture}[scale=0.8]
|
|
\begin{axis}[
|
|
xlabel={Ordre de signature},
|
|
ylabel={Temps (ms)},
|
|
xmin=0, xmax=16,
|
|
ymin=0, ymax=300,
|
|
legend pos=north west,
|
|
ymajorgrids=true,
|
|
grid style=dashed,
|
|
]
|
|
|
|
\addplot[
|
|
color=blue,
|
|
mark=square,
|
|
]
|
|
coordinates {
|
|
(2,105.4)
|
|
(3,122.6)
|
|
(4,140.1)
|
|
(5,155.4)
|
|
(6,171.2)
|
|
(7,183.9)
|
|
(8,198.3)
|
|
(9,211.2)
|
|
(10,224.3)
|
|
(11,236.7)
|
|
(12,248.5)
|
|
(13,259.3)
|
|
(14,271.7)
|
|
(15,281.4)
|
|
};
|
|
\legend{-O3}
|
|
\end{axis}
|
|
\end{tikzpicture}
|
|
\end{figure}
|
|
\end{frame}
|
|
|
|
\section*{Conclusion}
|
|
|
|
\begin{frame}{Conclusion}
|
|
\begin{itemize}
|
|
\item \emph{isomatch} fonctionne (beaucoup testé)
|
|
\item \emph{isomatch} fonctionne assez vite
|
|
\item En cours d'intégration à Voss II
|
|
\item Passé sous silence~: beaucoup d'étapes de recherche de meilleures
|
|
signatures
|
|
\end{itemize}
|
|
\vspace{2em}
|
|
|
|
\begin{center}
|
|
{\Huge Des questions~?}
|
|
\end{center}
|
|
\end{frame}
|
|
|
|
\end{document}
|