path: root/presentation/presentation.tex

\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: