Add initial filesHEADmaster

1 files changed, 1309 insertions, 0 deletions

diff --git a/presentation/presentation.tex b/presentation/presentation.tex
new file mode 100644
index 0000000..e1500e0
--- /dev/null
+++ b/presentation/presentation.tex
@@ -0,0 +1,1309 @@
+\documentclass[10pt,aspectratio=169,table]{beamer}
+
+\def\ymhgistrue{1}
+\def\ymhgextended{0}
+
+\usepackage{minted}
+\usepackage{tikz}
+\usepackage{pgfplots}
+\usepackage{booktabs}
+\usepackage{multicol}
+\usepackage{multirow}
+\usepackage{graphicx}
+
+% \usepackage{pgfpages}
+% \setbeameroption{show notes}
+% \setbeameroption{show notes on second screen=right}
+
+% Ideas for xilinx
+% - Explain XORed circuit
+% - Go over difficulties that were encountered when fuzzing tools
+% - Explain SMT in detail and how the equivalence check is done
+% -
+
+\usetheme{metropolis}
+
+\usetikzlibrary{calc,arrows.meta}
+\usetikzlibrary{decorations,patterns,arrows,decorations.pathmorphing}
+\usetikzlibrary{circuits.logic.US,calc}
+% \usetikzlibrary{external}
+% \usepgfplotslibrary{external}
+
+\pgfplotsset{every x tick label/.append style={font=\footnotesize, yshift=0.5ex}}
+
+% \definecolor{imperialbg}{HTML}{002147}
+
+% \setbeamercolor{palette primary}{bg=imperialbg,fg=black!2}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
+%%% Declarations                                                        %%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
+
+\newsavebox{\codebox}
+\newsavebox{\codeboxbody}
+\newsavebox{\codeboxassign}
+\newsavebox{\codeboxinit}
+\newsavebox{\codeboxtoplevel}
+\newsavebox{\codeboxextra}
+\newsavebox{\codeboxsynthesised}
+\newsavebox{\codeboxreduction}
+\newsavebox{\background}
+\newsavebox{\codeboxresult}
+\newsavebox{\motivationa}
+\newsavebox{\motivationb}
+\newsavebox{\motivationc}
+\newsavebox{\motivationd}
+\newsavebox{\motivatione}
+\newsavebox{\motivationf}
+
+\definecolor{palette1}{HTML}{f5793a}
+\definecolor{palette2}{HTML}{a95aa1}
+\definecolor{palette3}{HTML}{85c0f9}
+\definecolor{palette4}{HTML}{0f2080}
+
+\definecolor{ribbon1}{HTML}{66c2a5}
+\definecolor{ribbon2}{HTML}{fc8d62}
+\definecolor{ribbon3}{HTML}{8da0cb}
+\definecolor{ribbon4}{HTML}{e78ac3}
+\definecolor{ribbon5}{HTML}{a6d854}
+\definecolor{ribbon6}{HTML}{ffd92f}
+
+\definecolor{diag1}{HTML}{ccebc5}
+\definecolor{diag2}{HTML}{b3cde3}
+\definecolor{diagerr}{HTML}{fbb4ae}
+\definecolor{rred}{HTML}{c0504d}
+
+\definecolor{distr1}{HTML}{1b9e77}
+\definecolor{distr2}{HTML}{d95f02}
+\definecolor{distr3}{HTML}{7570b3}
+\definecolor{distr4}{HTML}{e7298a}
+\definecolor{distr5}{HTML}{66a61e}
+\definecolor{distr6}{HTML}{e6ab02}
+\definecolor{distr7}{HTML}{a6761d}
+\definecolor{distr8}{HTML}{666666}
+
+\definecolor{pltblue}{HTML}{1f77b4}
+
+\colorlet{mintedhlcolor}{palette4!20}
+\colorlet{presentationbg}{black!2}
+
+\definecolor{verireduce}{HTML}{e66101}
+\definecolor{creduce}{HTML}{5e3c99}
+
+\pgfplotsset{
+  verismith missynth/.style={verireduce, draw=verireduce, mark=*},
+  creduce missynth/.style={creduce, draw=creduce, mark=triangle*},
+  verismith crash/.style={verireduce, draw=verireduce, mark=o},
+  creduce crash/.style={creduce, draw=creduce, mark=triangle}
+}
+
+\setminted{fontsize=\small,breaklines,highlightcolor=mintedhlcolor}
+
+\setlength{\fboxsep}{2pt}
+
+\newcommand{\tool}[2][]{%
+  \ifx\hfuzz#1\hfuzz #2%
+  \else #2 #1%
+  \fi}%
+\newcommand{\xilinx}[1][]{\tool[#1]{Xilinx}}%
+\newcommand{\intel}[1][]{\tool[#1]{Intel}}%
+\newcommand{\quartus}[1][]{\tool[#1]{Quartus Prime}}%
+\newcommand{\quartuslite}[1][]{\tool[#1]{Quartus Prime Lite}}%
+\newcommand{\yosys}[1][]{\tool[#1]{Yosys}}%
+\newcommand{\xst}[1][]{\tool[#1]{XST}}%
+\newcommand{\vivado}[1][]{\tool[#1]{Vivado}}%
+\newcommand{\verismith}[1][]{\tool[#1]{Verismith}}%
+\newcommand{\iverilog}[1][]{\tool[#1]{Icarus Verilog}}%
+
+\newcommand{\ymhgifextend}{\ifx\ymhgistrue\ymhgextended}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
+%%% TIKZ EXTERNALIZE                                                    %%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
+% 
+% \makeatletter
+% \newcommand*{\overlaynumber}{\number\beamer@slideinframe}
+% \tikzset{
+%   beamer externalizing/.style={%
+%     execute at end picture={%
+%       \tikzifexternalizing{%
+%         \ifbeamer@anotherslide
+%         \pgfexternalstorecommand{\string\global\string\beamer@anotherslidetrue}%
+%         \fi
+%       }{}%
+%     }%
+%   },
+%   external/optimize=false
+% }
+% \let\orig@tikzsetnextfilename=\tikzsetnextfilename
+% \renewcommand\tikzsetnextfilename[1]{\orig@tikzsetnextfilename{#1-\overlaynumber}}
+% \makeatother
+% 
+% \tikzset{every picture/.style={beamer externalizing}}
+% 
+% \tikzexternalize
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
+%%% Row colours                                                         %%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
+
+\makeatletter
+\def\rowcolor{\noalign{\ifnum0=`}\fi\bmr@rowcolor}
+\newcommand<>{\bmr@rowcolor}{%
+  \alt#1%
+  {\global\let\CT@do@color\CT@@do@color\@ifnextchar[\CT@rowa\CT@rowb}%
+  {\ifnum0=`{\fi}\@gooble@rowcolor}%
+}
+
+\newcommand{\@gooble@rowcolor}[2][]{\@gooble@rowcolor@}
+\newcommand{\@gooble@rowcolor@}[1][]{\@gooble@rowcolor@@}
+\newcommand{\@gooble@rowcolor@@}[1][]{\ignorespaces}
+\makeatother
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
+%%% Content                                                             %%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
+
+\title{Finding and Understanding Bugs in FPGA Synthesis Tools}
+\subtitle{Verismith: FPGA Synthesis Tool Fuzzer}
+
+\author{\underline{Yann Herklotz}, John Wickerson}
+\institute{Imperial College London}
+
+\begin{document}
+
+\maketitle
+
+\note{Trust synthesis tool (Can we and should we?). They have a privileged position and we have to trust them. There is an effective bug finding method that can be used (fuzzing), which is effective at finding bugs.}
+
+\begin{frame}
+  \frametitle{Why find bugs?}
+  \large
+  \visible<1->{
+    \begin{itemize}
+    \item Designers have to trust the synthesis tool to do the right job
+    \item Bugs that generate wrong code can be hard to debug
+    \item Bugs that crash the tool can affect tool flows
+    \end{itemize}
+  }
+  \visible<2>{
+    \vspace{2em}
+
+    \begin{itemize}
+    \item Use \textbf{Verismith} to improve reliability of synthesis tools
+    \end{itemize}
+  }
+\end{frame}
+
+\note[itemize]{%
+\item We often assume correctness of Synthesis tools
+\item If our netlist does not work correctly, we assume there must be a mistake in the design.
+\item Find bugs in C programs, fuzzing was effective.
+}
+
+\begin{frame}
+  \frametitle{Verismith}
+  \begin{center}
+    \begin{tikzpicture}
+      \only<1>{\node[draw,fill=palette3!50,text width=2cm,align=center] (verilog) at (0,0)
+        {Verilog generation};}
+      \only<2->{\node[draw,fill=palette1!50,text width=2cm,align=center] (verilog) at (0,0)
+        {Verilog generation};}
+      \node[draw,fill=palette2!50,circle,text width=1.5cm,align=center,inner sep=-3pt]
+      (verdes) at (2.5,0) {\small Verilog design};
+      \node[draw,fill=palette2!50,circle,text width=1.5cm,align=center,inner sep=-3pt]
+      (vernet) at (6.5,0) {\small Verilog netlist};
+      \node[draw,fill=palette2!50,circle,text width=1.5cm,align=center,inner sep=-3pt]
+      (vertest) at (0,-2) {\footnotesize Reduced test case};
+      \node[draw,fill=palette3!50,minimum height=1cm] (synth) at (4.5,0) {Synthesis};
+      \node[draw,fill=palette3!50,minimum height=1cm,text width=2cm,align=center]
+      (equiv) at (6,-2) {Equivalence check};
+      \only<1>{\node[draw,fill=palette3!50,minimum height=1cm,text width=2cm,align=center]
+        (reduce) at (2.5,-2) {Reduction};}
+      \only<2->{\node[draw,fill=palette1!50,minimum height=1cm,text width=2cm,align=center]
+        (reduce) at (2.5,-2) {Reduction};}
+      \node at (4.3,-2.4) {{\color{rred} \small fail}};
+      \node at (3.8,-1.2) {{\color{rred} \small crash}};
+      \draw[very thick,->] (verilog) -- (verdes);
+      \draw[very thick,->] (verdes) -- (synth);
+      \draw[very thick,->] (synth) -- (vernet);
+      \draw[->] (verdes) -- ($ (equiv.north) + (-0.5,0) $);
+      \draw[very thick,->] (vernet) -- ($ (equiv.north) + (0.5,0) $);
+      \draw[rred,very thick,dashed,->] (synth.south) to [out=270,in=0] ($ (reduce.east) + (0,0.25) $);
+      \draw[->] (verdes) -- ($ (reduce.north) $);
+      \draw[rred,very thick,dashed,->] (equiv) to [out=180,in=0] ($ (reduce.east) + (0,-0.25) $);
+      \draw[very thick,->] (reduce) -- (vertest);
+    \end{tikzpicture}
+  \end{center}
+
+  \vspace{1em}
+  \large
+  \begin{columns}
+    \begin{column}{0.6\textwidth}
+      \textbf{Main contributions}
+      \begin{itemize}
+      \item Synthesis tool fuzzing framework
+      \item<2-> Behavioural and deterministic Verilog generation
+      \item<2-> Efficient Verilog Reduction
+      \end{itemize}
+    \end{column}
+    \begin{column}{0.4\textwidth}
+      \visible<3>{%
+        \textbf{Synthesis tools tested}
+        \begin{itemize}
+        \item[] Quartus \hspace{2em} Vivado
+        \item[] XST \hspace{4em} Yosys
+        \end{itemize}
+        \vspace{2.5em}
+      }
+    \end{column}
+  \end{columns}
+\end{frame}
+
+\begin{lrbox}{\background}
+  \begin{tikzpicture}
+    \node (chosen) at (0,1) {\textbf{Chosen}};
+    \node (subset) at (0,0.6) {\textbf{subset}};
+    \node (deterministic) at (3,1) {\textbf{Deterministic}};
+    \node (synthesisable) at (-3,1) {\textbf{Synthesisable}};
+    \node (semantic) at (0,3.5) {\textbf{Semantically correct}};
+    \node (syntactic) at (0,2) [draw,very thick,minimum width=12cm,minimum height=7.5cm] {};
+    \node (text) at (-3,5) {\textbf{Syntactically correct}};
+    \draw[very thick]
+    (0,0.8) ellipse (1cm and 0.7cm)
+    (-1.5,1) ellipse (3cm and 2cm)
+    (1.5,1) ellipse (3cm and 2cm)
+    (0,1.5) ellipse (5cm and 3cm)
+    ;
+  \end{tikzpicture}
+\end{lrbox}
+
+\begin{frame}
+  \frametitle{Background}
+  \large
+  \begin{columns}
+    \begin{column}{0.3\textwidth}
+      \textbf{Verilog 2005 standards}
+
+      \begin{itemize}
+      \item Verilog for simulation
+      \item Synthesisable Verilog
+      \end{itemize}
+
+    \end{column}%
+    \begin{column}{0.7\textwidth}
+      \scalebox{0.8}{\usebox{\background}}
+    \end{column}
+  \end{columns}
+\end{frame}
+
+\begin{frame}
+  \frametitle{Background}
+  \large
+
+
+  \textbf{What is deterministic Verilog?}
+  \begin{itemize}
+  \item Only one interpretation of the design
+  \item Nondeterminism example:
+
+    Any undefined values can be 1 or 0
+  \end{itemize}
+
+  \vspace{2em}
+
+  \visible<2>{%
+    \textbf{What is a bug?}
+    \begin{itemize}
+    \item Synthesis tool crashes
+    \item Synthesis tool outputs the wrong netlist
+    \end{itemize}
+  }
+\end{frame}
+
+\note[itemize]{%
+\item Determinism in terms of the spec
+\item Code will only be generated that does not give any ambiguity about its value
+}
+
+\begin{frame}[fragile]
+  \frametitle{Motivating Bug: Yosys}
+  \large
+  \begin{lrbox}{\motivationa}
+    \begin{minipage}{.8\textwidth}
+\begin{minted}[fontsize=\large]{verilog}
+module top (output y, input [2:0] w);
+  assign y = 1'b1 >> (w * (3'b110));
+endmodule
+\end{minted}
+    \end{minipage}
+  \end{lrbox}
+  \begin{lrbox}{\motivationb}
+    \begin{minipage}{.8\textwidth}
+\begin{minted}[fontsize=\large]{verilog}
+module top (output y, input [2:0] w);
+  assign y = 1'b1 >> (3'b100 * (3'b110));
+endmodule
+\end{minted}
+    \end{minipage}
+  \end{lrbox}
+  \begin{lrbox}{\motivationc}
+    \begin{minipage}{.8\textwidth}
+\begin{minted}[escapeinside=||,fontsize=\large]{verilog}
+module top (output y, input [2:0] w);
+  assign y = 1'b1 >> |\colorbox{red!20}{6'b110000}|;
+endmodule
+\end{minted}
+    \end{minipage}
+  \end{lrbox}
+  \begin{lrbox}{\motivationd}
+    \begin{minipage}{.8\textwidth}
+\begin{minted}[escapeinside=||,fontsize=\large]{verilog}
+module top (output y, input [2:0] w);
+  assign y = |\colorbox{red!20}{1'b0}|;
+endmodule
+\end{minted}
+    \end{minipage}
+  \end{lrbox}
+  \begin{lrbox}{\motivatione}
+    \begin{minipage}{.8\textwidth}
+\begin{minted}[fontsize=\large]{verilog}
+module top (output y, input [2:0] w);
+  assign y = 1'b1 >> 3'b000;
+endmodule
+\end{minted}
+    \end{minipage}
+  \end{lrbox}
+  \begin{lrbox}{\motivationf}
+    \begin{minipage}{.8\textwidth}
+\begin{minted}[fontsize=\large]{verilog}
+module top (output y, input [2:0] w);
+  assign y = 1'b1;
+endmodule
+\end{minted}
+    \end{minipage}
+  \end{lrbox}
+  \begin{center}%
+    \only<1>{\usebox{\motivationa}}%
+    \only<2>{\usebox{\motivationb}}%
+    \only<3>{\usebox{\motivationc}}%
+    \only<4>{\usebox{\motivationd}}%
+    \only<5>{\usebox{\motivatione}}%
+    \only<6>{\usebox{\motivationf}}%
+  \end{center}
+
+  \vspace{3em}
+
+  \begin{itemize}
+  \item Bug in a development version of Yosys\footnotemark
+  \item Result not truncated properly, which results in an unwanted shift
+  \end{itemize}
+  \footnotetext{\url{https://github.com/YosysHQ/yosys/issues/1047}}
+\end{frame}
+
+\note[itemize]{%
+\item Bug found in dev version of Yosys between 0.8 and 0.9.
+\item Multiplication not truncated which results in shifts that should not occur.
+}
+
+\section{Example Verismith Run}
+
+\begin{frame}
+  \frametitle{Run Outline: Verilog Generation}
+  \begin{center}
+    \scalebox{1.3}{
+      \begin{tikzpicture}
+        \draw[palette1,fill=palette1,draw opacity=0,fill opacity=0.3,very thick] (0.9,0) ellipse (2.5cm and 1.2cm);
+        \node[draw,fill=palette1!50,text width=2cm,align=center] (verilog) at (0,0)
+        {Verilog generation};
+        \node[draw,fill=palette1!50,circle,text width=1.5cm,align=center,inner sep=-3pt]
+        (verdes) at (2.5,0) {\small Verilog design};
+        \node[draw,fill=palette2!50,circle,text width=1.5cm,align=center,inner sep=-3pt]
+        (vernet) at (6.5,0) {\small Verilog netlist};
+        \node[draw,fill=palette2!50,circle,text width=1.5cm,align=center,inner sep=-3pt]
+        (vertest) at (0,-2) {\footnotesize Reduced test case};
+        \node[draw,fill=palette3!50,minimum height=1cm] (synth) at (4.5,0) {Synthesis};
+        \node[draw,fill=palette3!50,minimum height=1cm,text width=2cm,align=center]
+        (equiv) at (6,-2) {Equivalence check};
+        \node[draw,fill=palette3!50,minimum height=1cm,text width=2cm,align=center]
+        (reduce) at (2.5,-2) {Reduction};
+        \node at (4.3,-2.4) {{\color{rred} \small fail}};
+        \node at (3.8,-1.2) {{\color{rred} \small crash}};
+        \draw[palette1,very thick,->] (verilog) -- (verdes);
+        \draw[very thick,->] (verdes) -- (synth);
+        \draw[very thick,->] (synth) -- (vernet);
+        \draw[->] (verdes) -- ($ (equiv.north) + (-0.5,0) $);
+        \draw[very thick,->] (vernet) -- ($ (equiv.north) + (0.5,0) $);
+        \draw[rred,very thick,dashed,->] (synth.south) to [out=270,in=0] ($ (reduce.east) + (0,0.25) $);
+        \draw[->] (verdes) -- ($ (reduce.north) $);
+        \draw[rred,very thick,dashed,->] (equiv) to [out=180,in=0] ($ (reduce.east) + (0,-0.25) $);
+        \draw[very thick,->] (reduce) -- (vertest);
+      \end{tikzpicture}
+    }
+  \end{center}
+\end{frame}
+
+\begin{lrbox}{\codebox}
+  \begin{minipage}{2\textwidth}
+    \vspace{4em}
+    \inputminted{verilog}{ExampleRun/output2/fuzz_1/identity/syn_identity.v}
+  \end{minipage}
+\end{lrbox}
+
+\begin{frame}[fragile]
+  \frametitle{Verilog generation}
+  \large
+  \begin{columns}
+    \begin{column}{0.4\textwidth}
+      \scalebox{0.2}{\usebox{\codebox}}
+      % \tikzset{external/export next=false}
+      \begin{tikzpicture}[overlay]
+        \begin{scope}[shift={(0,0.05)}]
+          \only<4->{%
+            \draw[fill=palette1,fill opacity=0.5,thick] (0,5.05) rectangle (5,6.65);
+            \draw[fill=palette1,fill opacity=0.5,thick] (0,0.8) rectangle (5,1.85);
+          }
+          \only<3->{%
+            \draw[fill=palette2,fill opacity=0.5,thick] (0,4.85) rectangle (5,5.05);
+            \draw[fill=palette2,fill opacity=0.5,thick] (0,0.7) rectangle (5,0.8);
+          }
+          \only<2->{%
+            \draw[fill=palette3,fill opacity=0.5,thick] (0,2.1) rectangle (5,4.85);
+            \draw[fill=palette3,fill opacity=0.5,thick] (0,0.05) rectangle (5,0.7);
+          }
+        \end{scope}
+      \end{tikzpicture}
+    \end{column}%
+    \begin{column}{0.6\textwidth}
+      Example of generated Verilog by Verismith
+      \begin{itemize}
+      \item Bug of uninitialised variable in Yosys 0.8
+      \end{itemize}
+
+      \vspace{2em}
+
+      \begin{itemize}
+      \item<2-> Random module items in the body
+      \item<3-> Assignment of the internal state to the output
+      \item<4-> Definition of nets and initialisation of variables
+      \end{itemize}
+    \end{column}
+  \end{columns}
+\end{frame}
+
+\note[itemize]{%
+\item Bug found in Yosys 0.8.
+\item There are 3 main sections in the Verilog code: initialisation, assignment to output and random Verilog section.
+\item There can also be multiple modules in the Verilog code.
+}
+
+\begin{lrbox}{\codeboxbody}%
+  \begin{minipage}{0.9\textwidth}%
+    \vspace{2em}%
+    \inputminted[firstline=23,lastline=42]{verilog}{ExampleRun/output2/fuzz_1/identity/syn_identity.v}
+  \end{minipage}%
+\end{lrbox}%
+
+{
+  \setbeamercolor{frametitle}{%
+    fg=black!90,
+    bg=palette3!80%
+  }
+  \begin{frame}
+    \frametitle{Generation of the body}
+    \large
+    \begin{columns}
+      \begin{column}{0.6\textwidth}
+        \scalebox{0.6}{\usebox{\codeboxbody}}
+      \end{column}%
+      \begin{column}{0.4\textwidth}
+        \only<1>{%
+          Generate Verilog node-by-node to:
+
+          \begin{itemize}
+          \item Ensure determinism
+          \item Generate behavioural constructs
+          \item Avoid logic loops
+          \end{itemize}
+        }%
+        \only<2>{%
+          Unsupported constructs:
+          \begin{itemize}
+          \item function definitions
+          \item alternate ranges (\texttt{+:}, \texttt{-:})
+          \end{itemize}
+        }
+      \end{column}
+    \end{columns}
+  \end{frame}
+}
+
+{
+  \setbeamercolor{frametitle}{%
+    fg=black!90,
+    bg=palette2!80%
+  }
+  \begin{frame}
+    \frametitle{Internal State Assignment}
+    \inputminted[firstline=21,lastline=22]{verilog}{ExampleRun/output2/fuzz_1/identity/syn_identity.v}
+    \vspace{2em}
+    Need to assign all the internal state to the output \texttt{y}.
+
+    \begin{itemize}
+    \item As all the wires and variables are assigned a value, this concatenation can never be undefined.
+    \item Any changes in the internal state are reflected in \texttt{y}.
+    \end{itemize}
+  \end{frame}
+}
+
+{
+  \setbeamercolor{frametitle}{%
+    fg=black!90,
+    bg=palette1!80%
+  }
+  \begin{frame}
+    \frametitle{Initialisation}
+    \large
+    \only<2>{
+      \setminted{highlightlines={3-8}}
+    }
+    \only<3>{
+      \setminted{highlightlines={9-12,18-20}}
+    }
+    \only<4>{
+      \setminted{highlightlines={13-17}}
+    }
+    \begin{lrbox}{\codeboxinit}
+      \begin{minipage}{0.6\textwidth}
+        \vspace{2em}
+        \inputminted[firstline=3,lastline=20]{verilog}{ExampleRun/output2/fuzz_1/identity/syn_identity.v}
+      \end{minipage}
+    \end{lrbox}
+    \begin{columns}
+      \begin{column}{0.45\textwidth}
+        \scalebox{0.8}{\usebox{\codeboxinit}}
+      \end{column}
+      \begin{column}{0.55\textwidth}
+        \begin{itemize}
+        \item<2-> Define the inputs and outputs of the module with random sizes.
+        \item<3-> Define nets that get assigned in the module.
+        \item<4-> Define and initialise variables to 0.
+        \end{itemize}
+      \end{column}
+    \end{columns}
+  \end{frame}
+
+  \note[itemize]{%
+  \item The verilog has to be correct meaning we have to correctly initialise the inputs and outputs.
+  \item We also declare the wires with random sizes.
+  }
+}
+
+\begin{frame}
+  \frametitle{Run Outline: Synthesis}
+  \begin{center}
+    \scalebox{1.3}{
+      \begin{tikzpicture}
+        \draw[palette1,fill=palette1,draw opacity=0,fill opacity=0.3,very thick] (4.5,0) ellipse (3cm and 1.2cm);
+        \node[draw,fill=palette3!50,text width=2cm,align=center] (verilog) at (0,0)
+        {Verilog generation};
+        \node[draw,fill=palette1!50,circle,text width=1.5cm,align=center,inner sep=-3pt]
+        (verdes) at (2.5,0) {\small Verilog design};
+        \node[draw,fill=palette1!50,circle,text width=1.5cm,align=center,inner sep=-3pt]
+        (vernet) at (6.5,0) {\small Verilog netlist};
+        \node[draw,fill=palette2!50,circle,text width=1.5cm,align=center,inner sep=-3pt]
+        (vertest) at (0,-2) {\footnotesize Reduced test case};
+        \node[draw,fill=palette1!50,minimum height=1cm] (synth) at (4.5,0) {Synthesis};
+        \node[draw,fill=palette3!50,minimum height=1cm,text width=2cm,align=center]
+        (equiv) at (6,-2) {Equivalence check};
+        \node[draw,fill=palette3!50,minimum height=1cm,text width=2cm,align=center]
+        (reduce) at (2.5,-2) {Reduction};
+        \node at (4.3,-2.4) {{\color{rred} \small fail}};
+        \node at (3.8,-1.2) {{\color{rred} \small crash}};
+        \draw[very thick,->] (verilog) -- (verdes);
+        \draw[palette1,very thick,->] (verdes) -- (synth);
+        \draw[palette1,very thick,->] (synth) -- (vernet);
+        \draw[->] (verdes) -- ($ (equiv.north) + (-0.5,0) $);
+        \draw[very thick,->] (vernet) -- ($ (equiv.north) + (0.5,0) $);
+        \draw[rred,very thick,dashed,->] (synth.south) to [out=270,in=0] ($ (reduce.east) + (0,0.25) $);
+        \draw[->] (verdes) -- ($ (reduce.north) $);
+        \draw[rred,very thick,dashed,->] (equiv) to [out=180,in=0] ($ (reduce.east) + (0,-0.25) $);
+        \draw[very thick,->] (reduce) -- (vertest);
+      \end{tikzpicture}
+    }
+  \end{center}
+\end{frame}
+
+\begin{lrbox}{\codeboxsynthesised}
+  \begin{minipage}{\textwidth}
+    \vspace{3em}
+    \inputminted[firstline=800,lastline=820]{verilog}{ExampleRun/output2/fuzz_1/yosys/syn_yosys.v}
+  \end{minipage}
+\end{lrbox}
+
+\begin{frame}
+  \frametitle{Yosys Synthesis}
+  \large
+  \begin{columns}
+    \begin{column}{0.65\textwidth}
+      \scalebox{0.6}{\usebox{\codeboxbody}}
+    \end{column}
+    \begin{column}{0.35\textwidth}
+      \begin{center}
+        \scalebox{0.6}{\usebox{\codeboxsynthesised}}
+      \end{center}
+    \end{column}
+  \end{columns}
+  \scalebox{0.7}{
+    % \tikzset{external/export next=false}
+    \begin{tikzpicture}[overlay]
+      \begin{scope}[shift={(10,4.5)}]
+        \draw[draw,rounded corners,very thick] (0,0) -- (2,0) -- (3,0.5) -- (2,1) -- (0,1) -- (0.5,0.5) -- cycle;
+        \node at (1.5,0.5) {Synthesis};
+      \end{scope}
+    \end{tikzpicture}
+  }
+\end{frame}
+
+\begin{frame}
+  \frametitle{Run Outline: Equivalence Check}
+  \begin{center}
+    \scalebox{1.3}{
+      \begin{tikzpicture}
+        \draw[palette1,fill=palette1,draw opacity=0,fill opacity=0.3,very thick] (6,-2) ellipse (1.5cm and 1cm);
+        \node[draw,fill=palette3!50,text width=2cm,align=center] (verilog) at (0,0)
+        {Verilog generation};
+        \node[draw,fill=palette1!50,circle,text width=1.5cm,align=center,inner sep=-3pt]
+        (verdes) at (2.5,0) {\small Verilog design};
+        \node[draw,fill=palette1!50,circle,text width=1.5cm,align=center,inner sep=-3pt]
+        (vernet) at (6.5,0) {\small Verilog netlist};
+        \node[draw,fill=palette2!50,circle,text width=1.5cm,align=center,inner sep=-3pt]
+        (vertest) at (0,-2) {\footnotesize Reduced test case};
+        \node[draw,fill=palette3!50,minimum height=1cm] (synth) at (4.5,0) {Synthesis};
+        \node[draw,fill=palette1!50,minimum height=1cm,text width=2cm,align=center]
+        (equiv) at (6,-2) {Equivalence check};
+        \node[draw,fill=palette3!50,minimum height=1cm,text width=2cm,align=center]
+        (reduce) at (2.5,-2) {Reduction};
+        \node at (4.3,-2.4) {{\color{rred} \small fail}};
+        \node at (3.8,-1.2) {{\color{rred} \small crash}};
+        \draw[very thick,->] (verilog) -- (verdes);
+        \draw[very thick,->] (verdes) -- (synth);
+        \draw[very thick,->] (synth) -- (vernet);
+        \draw[palette1,->] (verdes) -- ($ (equiv.north) + (-0.5,0) $);
+        \draw[palette1,very thick,->] (vernet) -- ($ (equiv.north) + (0.5,0) $);
+        \draw[rred,very thick,dashed,->] (synth.south) to [out=270,in=0] ($ (reduce.east) + (0,0.25) $);
+        \draw[->] (verdes) -- ($ (reduce.north) $);
+        \draw[rred,very thick,dashed,->] (equiv) to [out=180,in=0] ($ (reduce.east) + (0,-0.25) $);
+        \draw[very thick,->] (reduce) -- (vertest);
+      \end{tikzpicture}
+    }
+  \end{center}
+\end{frame}
+
+\ymhgifextend%
+\begin{frame}
+  \frametitle{Equivalence check: What is an SMT solver?}
+  \large
+
+\end{frame}
+
+\begin{frame}
+  \frametitle{Equivalence check: What is ABC?}
+  \large
+\end{frame}
+\fi
+
+\begin{frame}
+  \frametitle{Equivalence check}
+  \large
+  \begin{lrbox}{\codeboxtoplevel}
+    \begin{minipage}{0.8\textwidth}
+      \vspace{2em}
+      \only<1>{\inputminted{verilog}{ExampleRun/output2/fuzz_1/equiv_identity_yosys/top.v}}
+      \only<2>{\inputminted[highlightlines={2}]{verilog}{ExampleRun/output2/fuzz_1/equiv_identity_yosys/top.v}}
+      \only<3>{\inputminted[highlightlines={3}]{verilog}{ExampleRun/output2/fuzz_1/equiv_identity_yosys/top.v}}
+      \only<4>{\inputminted[highlightlines={6}]{verilog}{ExampleRun/output2/fuzz_1/equiv_identity_yosys/top.v}}
+    \end{minipage}
+  \end{lrbox}
+  \begin{columns}
+    \begin{column}{0.6\textwidth}
+      \begin{tikzpicture}[circuit logic US]
+        \node[xor gate,scale=2] (comp) at (4.7,-0.5) {};
+        \node[or gate] (comb) at (6.5,-0.5) {};
+        
+        \draw (0,0) rectangle (3,2);
+        \node at (1.5,1) {Design};
+        \foreach \i in {0,...,3} {
+          \node at (0.4,0.8+0.3*\i) {\tiny wire\i};}
+        \draw (0,0.2) -- (0.1,0.3) -- (0,0.4);
+        \node at (2.8,0.3) {\tiny y};
+
+        \draw (0,-3) rectangle (3,-1);
+        \node at (1.5,-2) {Netlist};
+        \foreach \i in {0,...,3} {
+          \node at (0.4,0.8+0.3*\i-3) {\tiny wire\i};}
+        \draw (0,0.2-3) -- (0.1,0.3-3) -- (0,0.4-3);
+        \node at (2.8,-1.3) {\tiny y};
+
+        \draw[very thick] (3,-1.3) -- (3.5,-1.3) |- (comp.input 2);
+        \draw (3.2,-1.5) -- (3.3,-1.1);
+        \node at (3.25,-0.9) {\footnotesize N};
+        \draw[very thick] (3,0.3) -- (3.5,0.3) |- (comp.input 1);
+        \draw (3.2,0.1) -- (3.3,0.5);
+        \node at (3.25,0.7) {\footnotesize N};
+        \draw[very thick] (comp.output) -- (comb.west);
+        \draw (comb.output) -- ($(comb.output) + (0.2,0)$);
+        \draw ($(comp.output) + (0.3,0.2)$) -- ($(comp.output) + (0.2,-0.2)$);
+        \node at ($(comp.output) + (0.25,0.4)$) {\footnotesize N};
+
+        \foreach \i in {0,...,3} {
+          \draw[very thick] (-1,-1+\i*0.3) -| (-0.5+0.1*\i,-1+\i*0.3) |- (0,0.8+0.3*\i);
+          \draw[very thick] (-0.5+0.1*\i,-1+\i*0.3) |- (0,0.8+0.3*\i-3);
+          \draw (-0.9,-1+\i*0.3-0.2) -- (-0.8,-1+\i*0.3+0.2);
+          \node at (-1.5,-1+\i*0.3) {\tiny wire\i};}
+
+        \draw (-1,-1.3) -| (-0.6,-1.3) |- (0,0.3);
+        \draw (-0.6,-1.3) |- (0,0.3-3);
+        \node at (-1.4,-1.3) {\tiny clk};
+      \end{tikzpicture}
+    \end{column}%
+    \begin{column}{0.4\textwidth}
+      Equivalence check done using an SMT solver (Z3) through Yosys
+      \begin{itemize}
+      \item<2-> Instantiate generated design with output \texttt{y\_1}
+      \item<3-> Instantiate synthesised netlist with output \texttt{y\_2}
+      \item<4-> Should be equal at every clock edge
+      \end{itemize}
+    \end{column}
+  \end{columns}
+\end{frame}
+
+\begin{frame}
+  \frametitle{Run Outline: Reduction}
+  \begin{center}
+    \scalebox{1.3}{
+      \begin{tikzpicture}
+        \draw[palette1,fill=palette1,draw opacity=0,fill opacity=0.3,very thick] (1.5,-2) ellipse (2.7cm and 1.2cm);
+        \node[draw,fill=palette3!50,text width=2cm,align=center] (verilog) at (0,0)
+        {Verilog generation};
+        \node[draw,fill=palette1!50,circle,text width=1.5cm,align=center,inner sep=-3pt]
+        (verdes) at (2.5,0) {\small Verilog design};
+        \node[draw,fill=palette2!50,circle,text width=1.5cm,align=center,inner sep=-3pt]
+        (vernet) at (6.5,0) {\small Verilog netlist};
+        \node[draw,fill=palette1!50,circle,text width=1.5cm,align=center,inner sep=-3pt]
+        (vertest) at (0,-2) {\footnotesize Reduced test case};
+        \node[draw,fill=palette3!50,minimum height=1cm] (synth) at (4.5,0) {Synthesis};
+        \node[draw,fill=palette3!50,minimum height=1cm,text width=2cm,align=center]
+        (equiv) at (6,-2) {Equivalence check};
+        \node[draw,fill=palette1!50,minimum height=1cm,text width=2cm,align=center]
+        (reduce) at (2.5,-2) {Reduction};
+        \node at (4.3,-2.4) {{\color{rred} \small fail}};
+        \node at (3.8,-1.2) {{\color{rred} \small crash}};
+        \draw[very thick,->] (verilog) -- (verdes);
+        \draw[very thick,->] (verdes) -- (synth);
+        \draw[very thick,->] (synth) -- (vernet);
+        \draw[->] (verdes) -- ($ (equiv.north) + (-0.5,0) $);
+        \draw[very thick,->] (vernet) -- ($ (equiv.north) + (0.5,0) $);
+        \draw[rred,very thick,dashed,->] (synth.south) to [out=270,in=0] ($ (reduce.east) + (0,0.25) $);
+        \draw[palette1,->] (verdes) -- ($ (reduce.north) $);
+        \draw[rred,very thick,dashed,->] (equiv) to [out=180,in=0] ($ (reduce.east) + (0,-0.25) $);
+        \draw[palette1,very thick,->] (reduce) -- (vertest);
+      \end{tikzpicture}
+    }
+  \end{center}
+\end{frame}
+
+\begin{frame}
+  \frametitle{Reduction}
+  \large
+  \begin{lrbox}{\codeboxreduction}
+    \begin{minipage}{1.2\textwidth}
+      \vspace{2em}
+      \only<1>{\inputminted{verilog}{ExampleRun/output2/fuzz_1/identity/syn_identity.v}}
+      \only<2>{\inputminted[escapeinside=¬¬,highlightlines={20,46,56-77},highlightcolor=red!30]{verilog}{ExampleRun/output2/fuzz_1/identity/syn_identity_colour.v}}
+      \only<3>{\inputminted{verilog}{ExampleRun/output2/fuzz_1/identity/syn_identity_red1.v}}
+      \only<4>{\inputminted[escapeinside=¬¬,highlightlines={9-12,45-51},highlightcolor=red!30]{verilog}{ExampleRun/output2/fuzz_1/identity/syn_identity_red1_colour.v}}
+      % \only<5>{\inputminted{verilog}{ExampleRun/output2/fuzz_1/identity/syn_identity_red2.v}}
+      % \only<6>{\inputminted[escapeinside=¬¬,highlightlines={9-12,17-36},highlightcolor=green!30]{verilog}{ExampleRun/output2/fuzz_1/identity/syn_identity_red2_colour.v}}
+      % \only<7>{\inputminted[escapeinside=¬¬,highlightlines={14-15,37-39},highlightcolor=red!30]{verilog}{ExampleRun/output2/fuzz_1/identity/syn_identity_red2_colour2.v}}
+      % \only<8>{\inputminted{verilog}{ExampleRun/output2/fuzz_1/identity/syn_identity_red3.v}}
+      % \only<9>{\inputminted{verilog}{ExampleRun/output2/fuzz_1/identity/syn_identity_red4.v}}
+      % \only<10>{\inputminted{verilog}{ExampleRun/output2/fuzz_1/identity/syn_identity_red5.v}}
+      \only<5->{\inputminted{verilog}{ExampleRun/output2/fuzz_1/reduce_identity_yosys.v}}
+    \end{minipage}
+  \end{lrbox}
+  \begin{lrbox}{\codeboxresult}
+    \begin{minipage}{0.55\textwidth}
+      \vspace{3em}
+      \only<6>{\inputminted[highlightcolor=red!30,highlightlines={6}]{verilog}{ExampleRun/output2/fuzz_1/actual_wrong.v}}
+      \only<7>{\inputminted{verilog}{ExampleRun/output2/fuzz_1/actual_correct.v}}
+    \end{minipage}
+  \end{lrbox}
+  \only<1-5>{
+    \begin{columns}
+      \begin{column}{0.35\textwidth}
+        \only<1-2>{\scalebox{0.2}{\usebox{\codeboxreduction}}}
+        \only<3-4>{\scalebox{0.3}{\usebox{\codeboxreduction}}}
+        \only<5>{\scalebox{0.8}{\usebox{\codeboxreduction}}}
+        % \only<9-10>{\scalebox{0.4}{\usebox{\codeboxreduction}}}
+      \end{column}%
+      \begin{column}{0.65\textwidth}
+        \only<1-2>{%
+          \begin{itemize}
+          \item Verilog has to be reduced to a minimal representation to identify the bug.
+          \item Perform binary search on \textbf{syntax tree}.
+          \item Traditional methods perform search on source code.
+          \end{itemize}%
+        }%
+        \only<3-4>{%
+          Search is performed on different levels of granularity:
+          \begin{itemize}
+          \item Modules
+          \item Module items
+          \item Statements inside always blocks
+          \item Expressions
+          \end{itemize}
+        }%
+        \only<5>{%
+          \hspace{5em} We then get a minimal testcase
+        }
+      \end{column}
+    \end{columns}
+  }
+  \only<6->{
+    \begin{columns}
+      \begin{column}{0.5\textwidth}
+        \begin{center}
+          \textbf{\Large Input design}
+        \end{center}
+      \end{column}
+      \begin{column}{0.5\textwidth}
+        \begin{center}
+          \textbf{\Large Yosys netlist}
+        \end{center}
+      \end{column}
+    \end{columns}
+    \begin{columns}
+      \begin{column}{0.5\textwidth}
+        \begin{center}
+          \scalebox{0.8}{\usebox{\codeboxreduction}}
+        \end{center}
+      \end{column}
+      \begin{column}{0.5\textwidth}
+        \begin{center}
+          \scalebox{0.8}{\usebox{\codeboxresult}}
+        \end{center}
+      \end{column}
+    \end{columns}
+  }
+\end{frame}
+
+\section{Experiments and Results}
+
+\begin{frame}
+  \frametitle{Bugs found}
+  \large
+  \scalebox{0.7}{
+    \rowcolors{1}{}{lightgray!20}
+    \begin{tabular}{lrp{5mm}rrrr}
+      \toprule
+      \textbf{Tool} & \multicolumn{1}{p{2cm}}{\centering \textbf{Total test cases}} & \multicolumn{3}{r}{\textbf{Failing test cases}} & \multicolumn{1}{p{3cm}}{\centering \textbf{Distinct failing test cases}} & \multicolumn{1}{p{2cm}}{\centering \textbf{Bug reports}} \\
+      \midrule
+      \rowcolor<4>{palette1!30} \yosys{ 0.8}                                            & 26400 & & 7164 & (27.1\%) & $\ge 1$ & 0 \\
+      \rowcolor<5>{palette1!30} \yosys{ 3333e00}                                        & 51000 & & 7224 & (14.2\%) & $\ge 4$ & 3 \\
+      \rowcolor<5>{palette2!30} \yosys{ 70d0f38} (crash)                                        & 11 & & 1 & (9.09\%) & 1 & 1 \\
+      \rowcolor<4>{palette1!30} \yosys{ 0.9}                                            & 26400 & & 611  & (2.31\%) & $\ge 1$ & 1 \\
+      \rowcolor<3>{palette1!30} \vivado{ 2018.2}                                          & 47992 & & 1134 & (2.36\%) & $\ge 5$ & 3 \\
+      \rowcolor<3>{palette2!30} \vivado{ 2018.2} (crash)                                & 47992 & & 566  & (1.18\%) & 5       & 2 \\
+      \rowcolor<3>{palette1!30} \xst{ 14.7}                                             & 47992 & & 539  & (1.12\%) & $\ge 2$ & 0 \\
+      \rowcolor<2>{palette1!30} \quartus{ 19.2}                                         & 80300 & & 0    & (0\%)    & 0       & 0 \\
+      \rowcolor<2>{palette1!30} \quartuslite{ 19.1}                                    & 43    & & 17   & (39.5\%) & 1       & 0 \\
+      \rowcolor<2>{palette1!30} \quartuslite{ 19.1} (No \texttt{\$signed})             & 137   & & 0    & (0\%)    & 0       & 0 \\
+      \midrule
+      \rowcolor<6>{palette1!30} \iverilog{ 10.3}                                        & 26400 & & 616  & (2.33\%) & $\ge 1$  & 1 \\
+      \bottomrule
+    \end{tabular}
+  }
+
+  \vspace{1em}
+
+  \only<1>{%
+    \begin{itemize}
+    \item Summary of all the tests run over 18000 CPU hours
+    \end{itemize}
+    \vspace{1.5em}
+  }
+  \only<2>{%
+    \begin{itemize}
+    \item Quartus Prime Light failing because of the handling of \texttt{\$signed}
+    \item No crashes or failures found in Quartus Prime
+    \end{itemize}
+  }
+  \only<3>{%
+    \begin{itemize}
+    \item Vivado was the only stable tool that crashed
+    \end{itemize}
+    \vspace{1.5em}
+  }
+  \only<4>{%
+    \begin{itemize}
+    \item Yosys improved quite a lot between versions
+    \item Yosys 0.9 contains all the bug fixes that were submitted
+    \end{itemize}
+  }
+  \only<5>{%
+    \begin{itemize}
+    \item Yosys development versions also tested to aid development
+    \end{itemize}
+    \vspace{1.5em}
+  }
+  \only<6>{%
+    \begin{itemize}
+    \item Truncation bug in Icarus Verilog found while checking SMT counter examples
+    \end{itemize}
+    \vspace{1.5em}
+  }
+\end{frame}
+
+\begin{frame}
+  \frametitle{Efficiency at different Verilog sizes}
+  \begin{columns}
+    \begin{column}{0.5\textwidth}
+      \begin{tikzpicture}
+        \begin{semilogxaxis}[width=\linewidth,
+          major x tick style=transparent,
+          xlabel=Lines of code in generated programs,
+          legend style={at={(0.5,-0.15)},anchor=north,legend columns=-1},
+          ylabel=Number of test cases,
+          legend pos=north east,
+          legend style={font=\scriptsize},
+          xmin=50,
+          xmax=8800,
+          ybar=-3.6pt,
+          bar width=3.6pt,
+          ymin=0
+          % nodes near coords,
+          % nodes near coords align={vertical}
+          ]
+          \addplot[style={distr1,fill=distr1,mark=none,fill opacity=0.5,draw opacity=0}] coordinates {
+            (50.0,36) (55.2273245010972,42) (61.0011474309897,113) (67.3786032822108,210) (74.422799757947,341) (82.2034422502463,458) (90.7975236052311,501) (100.290086000843,507) (110.77506247623,353) (122.356206440081,241) (135.148118355792,115) (149.27737976296,39) (164.88380585685,11) (182.121829020643,3) (201.162027001128,0) (222.192810849795,0) (245.422289332251,0) (271.080328255088,0) (299.420825088154,0) (330.724221390595,0) (365.300277902221,0) (403.491139760939,0) (445.674722177899,0) (492.268450073103,0) (543.733388676789,0) (600.578805970684,0) (663.36721211649,0) (732.71992573891,0) (809.323222144053,0) (893.935124312463,0) (987.392903866661,0) (1090.6213662385,0) (1204.64200202167,0) (1330.58309506604,0) (1469.69088733773,0) (1623.34191102612,0) (1793.05660992942,0) (1980.51438490818,0) (2187.5702122883,0) (2416.2729996596,0) (2668.88586070881,0) (2947.90850971511,0) (3256.10199731164,0) (3596.51603228401,0) (3972.51915976695,0) (4387.83209446551,0) (4846.56453874751,0) (5353.25584993839,0) (5912.91995923888,0) (6531.09498675799,0) (7213.89804362345,0) (7968.08576346046,0) (8801.12116222408,0)
+          };
+          \addplot[style={distr2,fill=distr2,mark=none,fill opacity=0.5,draw opacity=0}] coordinates {
+            (50.0,0) (55.2273245010972,0) (61.0011474309897,1) (67.3786032822108,2) (74.422799757947,1) (82.2034422502463,6) (90.7975236052311,12) (100.290086000843,29) (110.77506247623,52) (122.356206440081,99) (135.148118355792,128) (149.27737976296,191) (164.88380585685,219) (182.121829020643,323) (201.162027001128,355) (222.192810849795,294) (245.422289332251,209) (271.080328255088,137) (299.420825088154,71) (330.724221390595,28) (365.300277902221,14) (403.491139760939,2) (445.674722177899,1) (492.268450073103,0) (543.733388676789,0) (600.578805970684,0) (663.36721211649,0) (732.71992573891,0) (809.323222144053,0) (893.935124312463,0) (987.392903866661,0) (1090.6213662385,0) (1204.64200202167,0) (1330.58309506604,0) (1469.69088733773,0) (1623.34191102612,0) (1793.05660992942,0) (1980.51438490818,0) (2187.5702122883,0) (2416.2729996596,0) (2668.88586070881,0) (2947.90850971511,0) (3256.10199731164,0) (3596.51603228401,0) (3972.51915976695,0) (4387.83209446551,0) (4846.56453874751,0) (5353.25584993839,0) (5912.91995923888,0) (6531.09498675799,0) (7213.89804362345,0) (7968.08576346046,0) (8801.12116222408,0)
+          };
+          \addplot[style={distr3,fill=distr3,mark=none,fill opacity=0.5,draw opacity=0}] coordinates {
+            (50.0,0) (55.2273245010972,0) (61.0011474309897,0) (67.3786032822108,0) (74.422799757947,0) (82.2034422502463,0) (90.7975236052311,0) (100.290086000843,0) (110.77506247623,0) (122.356206440081,0) (135.148118355792,0) (149.27737976296,0) (164.88380585685,0) (182.121829020643,0) (201.162027001128,0) (222.192810849795,1) (245.422289332251,0) (271.080328255088,3) (299.420825088154,7) (330.724221390595,9) (365.300277902221,12) (403.491139760939,32) (445.674722177899,46) (492.268450073103,74) (543.733388676789,93) (600.578805970684,129) (663.36721211649,166) (732.71992573891,186) (809.323222144053,171) (893.935124312463,116) (987.392903866661,58) (1090.6213662385,43) (1204.64200202167,16) (1330.58309506604,2) (1469.69088733773,1) (1623.34191102612,0) (1793.05660992942,0) (1980.51438490818,0) (2187.5702122883,0) (2416.2729996596,0) (2668.88586070881,0) (2947.90850971511,0) (3256.10199731164,0) (3596.51603228401,0) (3972.51915976695,0) (4387.83209446551,0) (4846.56453874751,0) (5353.25584993839,0) (5912.91995923888,0) (6531.09498675799,0) (7213.89804362345,0) (7968.08576346046,0) (8801.12116222408,0)
+          };
+          \addplot[style={distr4,fill=distr4,mark=none,fill opacity=0.5,draw opacity=0}] coordinates {
+            (50.0,0) (55.2273245010972,0) (61.0011474309897,0) (67.3786032822108,0) (74.422799757947,0) (82.2034422502463,0) (90.7975236052311,0) (100.290086000843,0) (110.77506247623,0) (122.356206440081,0) (135.148118355792,0) (149.27737976296,0) (164.88380585685,0) (182.121829020643,0) (201.162027001128,0) (222.192810849795,0) (245.422289332251,0) (271.080328255088,0) (299.420825088154,0) (330.724221390595,0) (365.300277902221,0) (403.491139760939,0) (445.674722177899,0) (492.268450073103,2) (543.733388676789,2) (600.578805970684,6) (663.36721211649,12) (732.71992573891,14) (809.323222144053,30) (893.935124312463,56) (987.392903866661,65) (1090.6213662385,84) (1204.64200202167,103) (1330.58309506604,123) (1469.69088733773,109) (1623.34191102612,66) (1793.05660992942,45) (1980.51438490818,18) (2187.5702122883,10) (2416.2729996596,1) (2668.88586070881,0) (2947.90850971511,0) (3256.10199731164,0) (3596.51603228401,0) (3972.51915976695,0) (4387.83209446551,0) (4846.56453874751,0) (5353.25584993839,0) (5912.91995923888,0) (6531.09498675799,0) (7213.89804362345,0) (7968.08576346046,0) (8801.12116222408,0)
+          };
+          \addplot[style={distr5,fill=distr5,mark=none,fill opacity=0.5,draw opacity=0}] coordinates {
+            (50.0,0) (55.2273245010972,0) (61.0011474309897,0) (67.3786032822108,0) (74.422799757947,0) (82.2034422502463,0) (90.7975236052311,0) (100.290086000843,0) (110.77506247623,0) (122.356206440081,0) (135.148118355792,0) (149.27737976296,0) (164.88380585685,0) (182.121829020643,0) (201.162027001128,0) (222.192810849795,0) (245.422289332251,0) (271.080328255088,0) (299.420825088154,0) (330.724221390595,0) (365.300277902221,0) (403.491139760939,0) (445.674722177899,0) (492.268450073103,0) (543.733388676789,0) (600.578805970684,0) (663.36721211649,2) (732.71992573891,0) (809.323222144053,2) (893.935124312463,14) (987.392903866661,16) (1090.6213662385,29) (1204.64200202167,50) (1330.58309506604,76) (1469.69088733773,83) (1623.34191102612,99) (1793.05660992942,99) (1980.51438490818,81) (2187.5702122883,49) (2416.2729996596,35) (2668.88586070881,16) (2947.90850971511,3) (3256.10199731164,2) (3596.51603228401,1) (3972.51915976695,1) (4387.83209446551,0) (4846.56453874751,0) (5353.25584993839,0) (5912.91995923888,0) (6531.09498675799,0) (7213.89804362345,0) (7968.08576346046,0) (8801.12116222408,0)
+          };
+          \addplot[style={distr6,fill=distr6,mark=none,fill opacity=0.5,draw opacity=0}] coordinates {
+            (50.0,0) (55.2273245010972,0) (61.0011474309897,0) (67.3786032822108,0) (74.422799757947,0) (82.2034422502463,0) (90.7975236052311,0) (100.290086000843,0) (110.77506247623,0) (122.356206440081,0) (135.148118355792,0) (149.27737976296,0) (164.88380585685,0) (182.121829020643,0) (201.162027001128,0) (222.192810849795,0) (245.422289332251,0) (271.080328255088,0) (299.420825088154,0) (330.724221390595,0) (365.300277902221,0) (403.491139760939,0) (445.674722177899,0) (492.268450073103,0) (543.733388676789,0) (600.578805970684,0) (663.36721211649,0) (732.71992573891,0) (809.323222144053,0) (893.935124312463,0) (987.392903866661,0) (1090.6213662385,2) (1204.64200202167,2) (1330.58309506604,1) (1469.69088733773,2) (1623.34191102612,4) (1793.05660992942,15) (1980.51438490818,16) (2187.5702122883,28) (2416.2729996596,49) (2668.88586070881,58) (2947.90850971511,66) (3256.10199731164,50) (3596.51603228401,59) (3972.51915976695,37) (4387.83209446551,15) (4846.56453874751,7) (5353.25584993839,1) (5912.91995923888,0) (6531.09498675799,0) (7213.89804362345,0) (7968.08576346046,0) (8801.12116222408,0)
+          };
+          \addplot[style={distr7,fill=distr7,mark=none,fill opacity=0.5,draw opacity=0}] coordinates {
+            (50.0,0) (55.2273245010972,0) (61.0011474309897,0) (67.3786032822108,0) (74.422799757947,0) (82.2034422502463,0) (90.7975236052311,0) (100.290086000843,0) (110.77506247623,0) (122.356206440081,0) (135.148118355792,0) (149.27737976296,0) (164.88380585685,0) (182.121829020643,0) (201.162027001128,0) (222.192810849795,0) (245.422289332251,0) (271.080328255088,0) (299.420825088154,0) (330.724221390595,0) (365.300277902221,0) (403.491139760939,0) (445.674722177899,0) (492.268450073103,0) (543.733388676789,0) (600.578805970684,0) (663.36721211649,0) (732.71992573891,0) (809.323222144053,0) (893.935124312463,0) (987.392903866661,1) (1090.6213662385,0) (1204.64200202167,0) (1330.58309506604,0) (1469.69088733773,0) (1623.34191102612,4) (1793.05660992942,4) (1980.51438490818,7) (2187.5702122883,12) (2416.2729996596,23) (2668.88586070881,41) (2947.90850971511,36) (3256.10199731164,51) (3596.51603228401,65) (3972.51915976695,43) (4387.83209446551,37) (4846.56453874751,24) (5353.25584993839,10) (5912.91995923888,3) (6531.09498675799,0) (7213.89804362345,0) (7968.08576346046,0) (8801.12116222408,0)
+          };
+          \addplot[style={distr8,fill=distr8,mark=none,fill opacity=0.5,draw opacity=0}] coordinates {
+            (50.0,0) (55.2273245010972,0) (61.0011474309897,0) (67.3786032822108,0) (74.422799757947,0) (82.2034422502463,0) (90.7975236052311,0) (100.290086000843,0) (110.77506247623,0) (122.356206440081,0) (135.148118355792,0) (149.27737976296,0) (164.88380585685,0) (182.121829020643,0) (201.162027001128,0) (222.192810849795,0) (245.422289332251,0) (271.080328255088,0) (299.420825088154,0) (330.724221390595,0) (365.300277902221,0) (403.491139760939,0) (445.674722177899,0) (492.268450073103,0) (543.733388676789,0) (600.578805970684,0) (663.36721211649,0) (732.71992573891,0) (809.323222144053,0) (893.935124312463,0) (987.392903866661,0) (1090.6213662385,0) (1204.64200202167,0) (1330.58309506604,0) (1469.69088733773,0) (1623.34191102612,0) (1793.05660992942,1) (1980.51438490818,4) (2187.5702122883,0) (2416.2729996596,2) (2668.88586070881,5) (2947.90850971511,8) (3256.10199731164,16) (3596.51603228401,24) (3972.51915976695,24) (4387.83209446551,28) (4846.56453874751,32) (5353.25584993839,25) (5912.91995923888,24) (6531.09498675799,8) (7213.89804362345,2) (7968.08576346046,1) (8801.12116222408,0)
+          };
+          \node at (axis cs: 100,530) {\footnotesize 10};
+          \node at (axis cs: 200,380) {\footnotesize 15};
+          \node at (axis cs: 750,210) {\footnotesize 20};
+          \node at (axis cs:1300,150) {\footnotesize 21};
+          \node at (axis cs:2000,125) {\footnotesize 26};
+          \node at (axis cs:2800, 90) {\footnotesize 27};
+          \node at (axis cs:4300, 85) {\footnotesize 30};
+          \node at (axis cs:6000, 50) {\footnotesize 35};
+        \end{semilogxaxis}
+      \end{tikzpicture}
+    \end{column}
+    \begin{column}{0.5\textwidth}
+      \visible<2>{%
+        \begin{tikzpicture}
+          \begin{axis}[width=\linewidth,
+            major x tick style=transparent,
+            symbolic x coords={91,181,438,792,929,1700,2110,4230},
+            xlabel=Average lines of code in generated programs,
+            ylabel=Number of test cases,
+            clip=false,
+            legend pos=north east,
+            legend style={font=\scriptsize},
+            xtick=data,
+            every axis x label/.style={at={($(ticklabel cs:0.6) + (0,-0.02)$)},anchor=near ticklabel,},
+            ybar=0,
+            bar width=8pt,
+            ymin=0,
+            % nodes near coords,
+            % nodes near coords align={vertical}
+            ]
+            \fill[distr1!50] (axis cs:91,-15) circle (3pt);
+            \fill[distr2!50] (axis cs:181,-15) circle (3pt);
+            \fill[distr3!50] (axis cs:438,-15) circle (3pt);
+            \fill[distr4!50] (axis cs:792,-15) circle (3pt);
+            \fill[distr5!50] (axis cs:929,-15) circle (3pt);
+            \fill[distr6!50] (axis cs:1700,-15) circle (3pt);
+            \fill[distr7!50] (axis cs:2110,-15) circle (3pt);
+            \fill[distr8!50] (axis cs:4230,-15) circle (3pt);
+            \addplot[style={black,fill=black!70,mark=none}] coordinates {
+              (91,122) (181,87) (438,63) (792,56) (929,43)
+              (1700,14) (2110,10) (4230,7)
+            };
+            \addplot[style={red!50,fill=red!50,mark=none}] coordinates {
+              (91,0) (181,2) (438,4) (792,12) (929,10)
+              (1700,8) (2110,12) (4230,17)
+            };
+            \legend{Bugs found,Crashes found};
+          \end{axis}
+        \end{tikzpicture}}
+    \end{column}
+  \end{columns}
+
+  \vspace{1em}
+  \large
+  \begin{itemize}
+  \item Each experiment was run over 3 days with Yosys, Vivado and XST
+  \end{itemize}
+\end{frame}
+
+\begin{frame}
+  \frametitle{Bugs found in Vivado over different versions}
+  \large
+  \begin{columns}
+    \begin{column}{0.65\textwidth}
+      \begin{tikzpicture}
+        \foreach \i in {-1,...,5}
+        {
+          \draw (-1,0.767441860465*\i+0.37) -- (8,0.767441860465*\i+0.37);
+        }
+        \only<2->{
+          \fill[fill=ribbon1] (-0.5,4.2) -- (7,4.2) -- (7.5,3.6) -- (7,3) -- (-0.5,3) --
+          (-0.2,3.6) -- cycle;
+          \node at (1.1,3.6) {15};
+          \fill[fill=ribbon5] (-0.5,3) -- (4.6,3) to [out=0,in=180] (6.6,0.5) --
+          (7,0.5) -- (7.1,0.45) -- (7,0.4) -- (6.6,0.4) to [out=180,in=0] (4.6,2.9) --
+          (-0.5,2.9) -- (-0.4,2.95) -- cycle;
+          \fill[fill=ribbon3] (-0.5,2.9) -- (2.4,2.9) to [out=0,in=180] (6.6,0.4) --
+          (7,0.4) -- (7.3,0.2) -- (7,0) -- (6.6,0) to [out=180,in=0] (2.4,2.5) --
+          (-0.5,2.5) -- (-0.2,2.7) -- cycle;
+          \node at (1.1,2.7) {6};
+          \fill[fill=ribbon2] (-0.5,2.2) -- (2.4,2.2) to [out=0,in=180] (4.4,2.9) --
+          (4.6,2.9) to [out=0,in=180] (6.6,3) -- (7,3) -- (7.4,2.55) -- (7,2.1) --
+          (6.6,2.1) to [out=180,in=0] (4.6,2) -- (4.4,2) to [out=180,in=0] (2.4,1.3) --
+          (-0.5,1.3) -- (-0.2,1.75) -- cycle;
+          \node at (1.1,1.75) {11};
+          \fill[fill=ribbon6] (-0.5,1.3) -- (2.4,1.3) to [out=0,in=180] (4.4,2) -- (4.6,2) to
+          [out=0,in=180] (6.6,0) -- (7,0) -- (7.1,-0.05) -- (7,-0.1) -- (6.6,-0.1) to
+          [out=180,in=0] (4.6,1.9) -- (4.4,1.9) to [out=180,in=0] (2.4,1.2) --
+          (-0.5,1.2) -- (-0.5,1.25) -- cycle;
+          \fill[fill=ribbon4] (-0.5,1.2) -- (3,1.2) to [out=0,in=180] (6.6,2.1)
+          -- (7,2.1) -- (7.5,1.5) -- (7,0.9)
+          -- (6.6,0.9) to [out=180,in=0] (3,0) -- (-0.5,0) -- (-0.1,0.6) -- cycle;
+          \node at (1.1,0.6) {17};
+        }
+        \filldraw[fill] (-0.1,2.5) rectangle (0.3,4.2);
+        \filldraw[fill] (2.1,2.5) rectangle (2.5,4.2);
+        \filldraw[fill] (4.3,1.9) rectangle (4.7,4.2);
+        \filldraw[fill] (6.5,0.9) rectangle (6.9,4.2);
+        \node at (0.1,4.6) {2016.1};
+        \node at (2.3,4.6) {2016.2};
+        \node at (4.5,4.6) {2017.4};
+        \node at (6.7,4.6) {2018.2};
+        \node at (0.1,2.7) {\color{presentationbg}{22}};
+        \node at (2.3,2.7) {\color{presentationbg}{22}};
+        \node at (4.5,2.1) {\color{presentationbg}{28}};
+        \node at (6.7,1.1) {\color{presentationbg}{43}};
+        \node at (3.4,5.3) {Vivado version};
+      \end{tikzpicture}
+    \end{column}%
+    \begin{column}{0.35\textwidth}
+      \begin{itemize}
+      \item Total number of bugs increase with versions
+      \item This does not mean there are more bugs, just that they were more commonly found
+      \end{itemize}
+    \end{column}
+  \end{columns}
+\end{frame}
+
+\note{One can see from the arrows that there are at least 3 different bugs in Vivado 2018.2, however, we identified 5 different ones in total.}
+
+\ymhgifextend%
+\begin{frame}
+  \frametitle{Reduction efficiency}
+  \large
+  \begin{center}
+    \begin{tikzpicture}
+      \begin{loglogaxis}[
+        width=0.65\linewidth,
+        legend style={nodes={scale=0.7, transform shape}},
+        legend pos=south east,
+        xlabel=Final size of reduced test case (lines of code),
+        ylabel=Time taken for reduction (s),
+        xticklabel style={
+          /pgf/number format/fixed,
+          /pgf/number format/precision=2
+        },
+        scaled x ticks=false,
+        grid=major,
+        major grid style={line width=.2pt,draw=black!20},
+        legend columns=2,
+        legend cell align=left,
+        ymin=0.4
+        ]
+        \addplot[only marks, verismith missynth]
+        coordinates {
+          (8,24.228676396) (12,48.020800025) (9,239.19471845) (19,78.85903502) (11,73.373059156) (265,396.931663908) (9,28.596337771) (9,121.520180855) (56,392.16407163) (12,9.194543707) (443,1106.024588047) (9,88.786871352) (9,166.899571358) (120,142.222511227) (9,73.07548465) (9,71.661578111) (26,47.691798645) (87,153.32273806) (9,89.500623124)
+        };
+        \addplot[only marks, creduce missynth]
+        coordinates {
+          (23,546.138) (40,549.916) (63,2954.062) (66,2565.887) (65,4355.297) (59,1695.4) (32,2355.947) (60,5091.577) (64,1611.466) (15,89.294) (137,6825.607) (74,13896.513) (64,9126.388) (90,4550.126) (43,5553.653) (27,1096.045) (16,340.533) (68,2814.821) (85,10592.831)
+        };
+        \addplot[only marks, verismith crash]
+        coordinates {
+          (462,31.025951033) (405,32.882851417) (75,49.630976912) (49,4.096207305) (234,10.081659552) (191,23.921349163) (99,10.894472949) (115,16.908927877) (32,18.313146602) (12,1.4856776) (230,30.366253517)
+        };
+        \addplot[only marks, creduce crash]
+        coordinates {
+          (30,225.177) (69,289.044) (33,136.239) (33,194.167) (52,352.996) (60,313.808) (54,285.255) (63,221.02) (60,137.885) (34,223.37) (54,213.942)
+        };
+        \legend{\verismith{}: mis-synthesis,C-Reduce: mis-synthesis,\verismith{}: crash,C-Reduce: crash}
+      \end{loglogaxis}
+    \end{tikzpicture}
+  \end{center}
+\end{frame}
+\fi
+
+\begin{frame}
+  \frametitle{Summary}
+  \large
+  Verismith can find hard-to-find bugs in synthesis tools by:
+
+  \begin{itemize}
+  \item Generating behavioural and deterministic Verilog.
+  \item Reducing it to a minimal representation if it is not.
+  \end{itemize}
+
+  In total 11 unique bugs were found, reported and fixed by tool vendors.
+
+  \vspace{2em}
+
+  Future work could be by supporting:
+  \begin{itemize}
+  \item A larger subset of Verilog
+  \item Controlled nondeterminism
+  \end{itemize}
+\end{frame}
+
+{
+  \setbeamercolor{footnote}{%
+    fg=black!2,
+    bg=mDarkTeal%
+  }
+  \begin{frame}[standout]
+    \Large
+    Finding and Understanding Bugs in FPGA Synthesis Tools
+
+    \vspace{1.5em}
+
+    \begin{columns}
+      \begin{column}{0.35\textwidth}
+        \begin{center}
+          Verismith Github\footnotemark
+
+          \vspace{1em}
+
+          \scalebox{0.5}{\includegraphics{verismith-github.pdf}}
+        \end{center}
+      \end{column}
+      \begin{column}{0.35\textwidth}
+        \begin{center}
+          Link to paper\footnotemark
+
+          \vspace{1em}
+
+          \scalebox{0.5}{\includegraphics{paper-code.pdf}}
+        \end{center}
+      \end{column}
+    \end{columns}
+    \addtocounter{footnote}{-1}
+    \footnotetext{\url{https://github.com/ymherklotz/verismith}}
+    \stepcounter{footnote}\footnotetext{\url{https://yannherklotz.com/papers/fubfst_fpga2020.pdf}}
+  \end{frame}
+}
+
+\begin{frame}[fragile]
+  \frametitle{Motivating Bug 2: Vivado}
+  \begin{columns}
+    \begin{column}{0.5\textwidth}
+      \definecolor{minline1}{named}{presentationbg}
+      \definecolor{minline2}{named}{presentationbg}
+      \definecolor{minline3}{named}{presentationbg}
+      \setminted{highlightlines={}}
+      \only<2>{
+        \definecolor{minline2}{named}{mintedhlcolor}
+        \definecolor{minline3}{named}{mintedhlcolor}
+      }
+      \only<3>{\setminted{highlightlines={4-5}}}
+      \only<4>{\setminted{highlightlines={8,11}}}
+      \only<5>{
+        \setminted{highlightlines={9-10}}
+        \definecolor{minline1}{named}{mintedhlcolor}
+        \definecolor{minline3}{named}{mintedhlcolor}
+      }
+      \only<6>{
+        \definecolor{minline1}{named}{mintedhlcolor}
+        \definecolor{minline3}{named}{mintedhlcolor}
+      }
+\begin{minted}[escapeinside=||]{verilog}
+module top (output [1:0] y,
+            input clk,
+            input [1:0] |\colorbox{minline2}{w0}|);
+   reg [1:0] r0 = 2'b0;
+   reg [2:0] r1 = 3'b0;
+   assign y = r1;
+   always @(posedge clk) begin
+      r0 <= 1'b1;
+      if (r0)
+        |\colorbox{minline1}{r1}| <= r0 ? |\colorbox{minline1}{\colorbox{minline3}{w0}[0:0]}| : 1'b0;
+      else r1 <= 3'b1;
+   end
+endmodule
+\end{minted}
+    \end{column}%
+    \begin{column}{0.5\textwidth}
+      Bug found in Vivado 2019.1.\footnotemark
+      \begin{itemize}
+      \item<2-> Assume \texttt{w0 = 2'b10},
+      \item<3-> initialise \texttt{r0 = 2'b0},
+
+        \texttt{r1 = 3'b0},
+      \item<4-> first \texttt{clk} edge sets \texttt{r0 = 1'b1},
+
+        \texttt{r1 = 3'b1},
+      \item<5-> next \texttt{clk} edge enters the \texttt{if} statement,
+      \item<6-> sets \texttt{r1 = w0[0:0] = 3'b0}
+
+        Vivado returns \texttt{r1 = w0[0:0] = 3'b010}
+      \end{itemize}
+    \end{column}
+  \end{columns}
+  \footnotetext{\tiny\url{https://forums.xilinx.com/t5/Synthesis/Vivado-2019-1-Bit-selection-synthesis-mismatch/td-p/982419}}
+\end{frame}
+
+\note[itemize]{%
+\item Assume that \texttt{w0 = 2'b10}.
+\item Everything else is initialised to \texttt{1'b0}.
+\item First edge sets \texttt{r0 = 2'b1}
+\item Therefore it should enter the if statement on the next iteration and assign \texttt{r1 = 3'b0} as that is the LSB of w0.
+\item However, \texttt{3'b010} is assigned instead which results in an output of \texttt{2'b10} instead of \texttt{2'b00}
+}
+
+\end{document}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: t
+%%% ymhg/TeX-expand-shell-escape: t
+%%% End: