Everything is said. Would deserve some polish.

This commit is contained in:
Théophile Bastian 2017-09-08 00:46:33 +02:00
parent 4cd3ee0eaf
commit 6e38932d5a

View file

@ -10,9 +10,13 @@
\usepackage{graphicx} \usepackage{graphicx}
\usepackage{my_listings} \usepackage{my_listings}
%\usepackage{my_hyperref} %\usepackage{my_hyperref}
\usepackage{pgfplots}
\usepackage{math} \usepackage{math}
\usepackage{../common/internship}
\setbeamertemplate{navigation symbols}{} \setbeamertemplate{navigation symbols}{}
\newcommand{\cf}{\textit{cf.}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\author[Théophile Bastian]{Théophile \textsc{Bastian} \\ \author[Théophile Bastian]{Théophile \textsc{Bastian} \\
\small{Sous la supervision de Carl Seger et Mary Sheeran}} \small{Sous la supervision de Carl Seger et Mary Sheeran}}
@ -60,6 +64,9 @@
\item \alert{fl}~: langage fonctionnel, BDDs, STE, \ldots \\ \item \alert{fl}~: langage fonctionnel, BDDs, STE, \ldots \\
Langage généraliste du prouveur hardware, utilisé chez Intel 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 \item \emph{Idée}~: prouver un circuit simple puis le raffiner est plus
aisé. aisé.
@ -70,22 +77,28 @@
\end{itemize} \end{itemize}
\item Raffinements~: \alert{recherche de motifs} \item Raffinements~: \alert{recherche de motifs}
\item \alert{isomatch}~: bibliothèque C++ pour recherche de motifs.
\end{itemize} \end{itemize}
\end{frame} \end{frame}
\section{Problème} \section{Problème}
\begin{frame}{Problèmes} \begin{frame}{Problèmes}
Deux problèmes à résoudre~:
\begin{enumerate}[A] \begin{enumerate}[A]
\item Deux circuits sont-ils identiques~? \item Deux circuits sont-ils identiques~?
\item Quelles sont les occurrences de $N$ dans $H$~? \item Quelles sont les occurrences de $N$ dans $H$~?
\pause{}
\item (Avoir un code documenté, très propre, idiomatique, réutilisable)
\end{enumerate} \end{enumerate}
\pause{}
\begin{itemize} \begin{itemize}
\item A~: isomorphisme de graphes, NP-hard. Cf. Babai. \item A~: isomorphisme de graphes ($\implies$ circuits égaux). \\
\item B~: isomorphisme de sous-graphes, NP-complet. NP-hard. Cf. Babai.
\item B~: isomorphisme de sous-graphes ($\implies$
sous-circuit égal). \\
NP-complet.
\vspace{1em} \vspace{1em}
@ -137,23 +150,145 @@
\vspace{1em} \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{itemize}
\end{frame} \end{frame}
\subsection{Égalité de groupes} \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} \end{frame}
\subsection{Recherche de motifs} \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} \end{frame}
\section{Performance} \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{frame}
\end{document} \end{document}