% 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}