diff --git a/slides/slides.tex b/slides/slides.tex index 5d7bc69..474e12b 100644 --- a/slides/slides.tex +++ b/slides/slides.tex @@ -10,9 +10,13 @@ \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}} @@ -60,6 +64,9 @@ \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é. @@ -70,22 +77,28 @@ \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} - Deux problèmes à résoudre~: - \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, NP-hard. Cf. Babai. - \item B~: isomorphisme de sous-graphes, NP-complet. + \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} @@ -137,23 +150,145 @@ \vspace{1em} - \item TODO + \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} +\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} +\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} +\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}