manual/PRESENTATION_ExOth.tex

\section{Yosys by example -- Beyond Synthesis}

\begin{frame}
\sectionpage
\end{frame}

\begin{frame}{Overview}
This section contains 2 subsections:
\begin{itemize}
\item Interactive Design Investigation
\item Symbolic Model Checking
\end{itemize}
\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\subsection{Interactive Design Investigation}

\begin{frame}
\subsectionpage
\subsectionpagesuffix
\end{frame}

\begin{frame}{\subsecname}
Yosys can also be used to investigate designs (or netlists created
from other tools).

\begin{itemize}
\item
The selection mechanism (see slides ``Using Selections''), especially patterns such
as {\tt \%ci} and {\tt \%co}, can be used to figure out how parts of the design
are connected.

\item
Commands such as {\tt submod}, {\tt expose}, {\tt splice}, \dots can be used
to transform the design into an equivalent design that is easier to analyse.

\item
Commands such as {\tt eval} and {\tt sat} can be used to investigate the
behavior of the circuit.
\end{itemize}
\end{frame}

\begin{frame}[t, fragile]{Example: Reorganizing a module}
\begin{columns}
\column[t]{4cm}
\lstinputlisting[basicstyle=\ttfamily\fontsize{6pt}{7pt}\selectfont, language=verilog]{PRESENTATION_ExOth/scrambler.v}
\column[t]{7cm}
\begin{lstlisting}[basicstyle=\ttfamily\fontsize{8pt}{10pt}\selectfont, language=ys, frame=single]
read_verilog scrambler.v

hierarchy; proc;;

cd scrambler
submod -name xorshift32 \
           xs %c %ci %D %c %ci:+[D] %D \
           %ci*:-$dff xs %co %ci %d
\end{lstlisting}
\end{columns}

\hfil\includegraphics[width=11cm,trim=0 0cm 0 1.5cm]{PRESENTATION_ExOth/scrambler_p01.pdf}

\hfil\includegraphics[width=11cm,trim=0 0cm 0 2cm]{PRESENTATION_ExOth/scrambler_p02.pdf}
\end{frame}

\begin{frame}[t, fragile]{Example: Analysis of circuit behavior}
\begin{lstlisting}[basicstyle=\ttfamily\fontsize{8pt}{10pt}\selectfont, language=ys]
> read_verilog scrambler.v
> hierarchy; proc;; cd scrambler
> submod -name xorshift32 xs %c %ci %D %c %ci:+[D] %D %ci*:-$dff xs %co %ci %d

> cd xorshift32
> rename n2 in
> rename n1 out

> eval -set in 1 -show out
Eval result: \out = 270369.

> eval -set in 270369 -show out
Eval result: \out = 67634689.

> sat -set out 632435482
Signal Name                 Dec        Hex                                   Bin
-------------------- ---------- ---------- -------------------------------------
\in                   745495504   2c6f5bd0      00101100011011110101101111010000
\out                  632435482   25b2331a      00100101101100100011001100011010
\end{lstlisting}
\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\subsection{Symbolic Model Checking}

\begin{frame}
\subsectionpage
\subsectionpagesuffix
\end{frame}

\begin{frame}{\subsecname}
Symbolic Model Checking (SMC) is used to formally prove that a circuit has
(or has not) a given property.

\bigskip
One application is Formal Equivalence Checking: Proving that two circuits
are identical. For example this is a very useful feature when debugging custom
passes in Yosys.

\bigskip
Other applications include checking if a module conforms to interface
standards.

\bigskip
The {\tt sat} command in Yosys can be used to perform Symbolic Model Checking.
\end{frame}

\begin{frame}[t]{Example: Formal Equivalence Checking (1/2)}
Remember the following example?
\vskip1em

\vbox to 0cm{
\vskip-0.3cm
\lstinputlisting[basicstyle=\ttfamily\fontsize{6pt}{7pt}\selectfont, language=verilog]{PRESENTATION_ExSyn/techmap_01_map.v}
}\vbox to 0cm{
\vskip-0.5cm
\lstinputlisting[xleftmargin=5cm, basicstyle=\ttfamily\fontsize{8pt}{10pt}\selectfont, frame=single, language=verilog]{PRESENTATION_ExSyn/techmap_01.v}
\lstinputlisting[xleftmargin=5cm, basicstyle=\ttfamily\fontsize{8pt}{10pt}\selectfont, language=ys, frame=single]{PRESENTATION_ExSyn/techmap_01.ys}}

\vskip5cm\hskip5cm
Lets see if it is correct..
\end{frame}

\begin{frame}[t, fragile]{Example: Formal Equivalence Checking (2/2)}
\begin{lstlisting}[basicstyle=\ttfamily\fontsize{8pt}{10pt}\selectfont, language=ys, frame=single]
# read test design
read_verilog techmap_01.v
hierarchy -top test

# create two version of the design: test_orig and test_mapped
copy test test_orig
rename test test_mapped

# apply the techmap only to test_mapped
techmap -map techmap_01_map.v test_mapped

# create a miter circuit to test equivalence
miter -equiv -make_assert -make_outputs test_orig test_mapped miter
flatten miter

# run equivalence check
sat -verify -prove-asserts -show-inputs -show-outputs miter
\end{lstlisting}

\dots
\begin{lstlisting}[basicstyle=\ttfamily\fontsize{8pt}{10pt}\selectfont]
Solving problem with 945 variables and 2505 clauses..
SAT proof finished - no model found: SUCCESS!
\end{lstlisting}
\end{frame}

\begin{frame}[t, fragile]{Example: Symbolic Model Checking (1/2)}
\small
The following AXI4 Stream Master has a bug. But the bug is not exposed if the
slave keeps {\tt tready} asserted all the time. (Something a test bench might do.)

\medskip
Symbolic Model Checking can be used to expose the bug and find a sequence
of values for {\tt tready} that yield the incorrect behavior.

\vskip-1em
\begin{columns}
\column[t]{5cm}
\lstinputlisting[basicstyle=\ttfamily\fontsize{5pt}{6pt}\selectfont, language=verilog]{PRESENTATION_ExOth/axis_master.v}
\column[t]{5cm}
\lstinputlisting[basicstyle=\ttfamily\fontsize{5pt}{6pt}\selectfont, language=verilog]{PRESENTATION_ExOth/axis_test.v}
\end{columns}
\end{frame}

\begin{frame}[t, fragile]{Example: Symbolic Model Checking (2/2)}
\begin{lstlisting}[basicstyle=\ttfamily\fontsize{8pt}{10pt}\selectfont, language=ys, frame=single]
read_verilog -sv axis_master.v axis_test.v
hierarchy -top axis_test

proc; flatten;;
sat -seq 50 -prove-asserts
\end{lstlisting}

\bigskip
\dots with unmodified {\tt axis\_master.v}:
\begin{lstlisting}[basicstyle=\ttfamily\fontsize{8pt}{10pt}\selectfont]
Solving problem with 159344 variables and 442126 clauses..
SAT proof finished - model found: FAIL!
\end{lstlisting}

\bigskip
\dots with fixed {\tt axis\_master.v}:
\begin{lstlisting}[basicstyle=\ttfamily\fontsize{8pt}{10pt}\selectfont]
Solving problem with 159144 variables and 441626 clauses..
SAT proof finished - no model found: SUCCESS!
\end{lstlisting}
\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\subsection{Summary}

\begin{frame}{\subsecname}
\begin{itemize}
\item Yosys provides useful features beyond synthesis.
\item The commands {\tt sat} and {\tt eval} can be used to analyse the behavior of a circuit.
\item The {\tt sat} command can also be used for symbolic model checking.
\item This can be useful for debugging and testing designs and Yosys extensions alike.
\end{itemize}

\bigskip
\bigskip
\begin{center}
Questions?
\end{center}

\bigskip
\bigskip
\begin{center}
\url{http://www.clifford.at/yosys/}
\end{center}
\end{frame}