manual/PRESENTATION_ExOth.tex


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
pre { line-height: 125%; margin: 0; }
td.linenos pre { color: #000000; background-color: #f0f0f0; padding: 0 5px 0 5px; }
span.linenos { color: #000000; background-color: #f0f0f0; padding: 0 5px 0 5px; }
td.linenos pre.special { color: #000000; background-color: #ffffc0; padding: 0 5px 0 5px; }
span.linenos.special { color: #000000; background-color: #ffffc0; padding: 0 5px 0 5px; }
.highlight .hll { background-color: #ffffcc }
.highlight { background: #ffffff; }
.highlight .c { color: #888888 } /* Comment */
.highlight .err { color: #a61717; background-color: #e3d2d2 } /* Error */
.highlight .k { color: #008800; font-weight: bold } /* Keyword */
.highlight .ch { color: #888888 } /* Comment.Hashbang */
.highlight .cm { color: #888888 } /* Comment.Multiline */
.highlight .cp { color: #cc0000; font-weight: bold } /* Comment.Preproc */
.highlight .cpf { color: #888888 } /* Comment.PreprocFile */
.highlight .c1 { color: #888888 } /* Comment.Single */
.highlight .cs { color: #cc0000; font-weight: bold; background-color: #fff0f0 } /* Comment.Special */
.highlight .gd { color: #000000; background-color: #ffdddd } /* Generic.Deleted */
.highlight .ge { font-style: italic } /* Generic.Emph */
.highlight .gr { color: #aa0000 } /* Generic.Error */
.highlight .gh { color: #333333 } /* Generic.Heading */
.highlight .gi { color: #000000; background-color: #ddffdd } /* Generic.Inserted */
.highlight .go { color: #888888 } /* Generic.Output */
.highlight .gp { color: #555555 } /* Generic.Prompt */
.highlight .gs { font-weight: bold } /* Generic.Strong */
.highlight .gu { color: #666666 } /* Generic.Subheading */
.highlight .gt { color: #aa0000 } /* Generic.Traceback */
.highlight .kc { color: #008800; font-weight: bold } /* Keyword.Constant */
.highlight .kd { color: #008800; font-weight: bold } /* Keyword.Declaration */
.highlight .kn { color: #008800; font-weight: bold } /* Keyword.Namespace */
.highlight .kp { color: #008800 } /* Keyword.Pseudo */
.highlight .kr { color: #008800; font-weight: bold } /* Keyword.Reserved */
.highlight .kt { color: #888888; font-weight: bold } /* Keyword.Type */
.highlight .m { color: #0000DD; font-weight: bold } /* Literal.Number */
.highlight .s { color: #dd2200; background-color: #fff0f0 } /* Literal.String */
.highlight .na { color: #336699 } /* Name.Attribute */
.highlight .nb { color: #003388 } /* Name.Builtin */
.highlight .nc { color: #bb0066; font-weight: bold } /* Name.Class */
.highlight .no { color: #003366; font-weight: bold } /* Name.Constant */
.highlight .nd { color: #555555 } /* Name.Decorator */
.highlight .ne { color: #bb0066; font-weight: bold } /* Name.Exception */
.highlight .nf { color: #0066bb; font-weight: bold } /* Name.Function */
.highlight .nl { color: #336699; font-style: italic } /* Name.Label */
.highlight .nn { color: #bb0066; font-weight: bold } /* Name.Namespace */
.highlight .py { color: #336699; font-weight: bold } /* Name.Property */
.highlight .nt { color: #bb0066; font-weight: bold } /* Name.Tag */
.highlight .nv { color: #336699 } /* Name.Variable */
.highlight .ow { color: #008800 } /* Operator.Word */
.highlight .w { color: #bbbbbb } /* Text.Whitespace */
.highlight .mb { color: #0000DD; font-weight: bold } /* Literal.Number.Bin */
.highlight .mf { color: #0000DD; font-weight: bold } /* Literal.Number.Float */
.highlight .mh { color: #0000DD; font-weight: bold } /* Literal.Number.Hex */
.highlight .mi { color: #0000DD; font-weight: bold } /* Literal.Number.Integer */
.highlight .mo { color: #0000DD; font-weight: bold } /* Literal.Number.Oct */
.highlight .sa { color: #dd2200; background-color: #fff0f0 } /* Literal.String.Affix */
.highlight .sb { color: #dd2200; background-color: #fff0f0 } /* Literal.String.Backtick */
.highlight .sc { color: #dd2200; background-color: #fff0f0 } /* Literal.String.Char */
.highlight .dl { color: #dd2200; background-color: #fff0f0 } /* Literal.String.Delimiter */
.highlight .sd { color: #dd2200; background-color: #fff0f0 } /* Literal.String.Doc */
.highlight .s2 { color: #dd2200; background-color: #fff0f0 } /* Literal.String.Double */
.highlight .se { color: #0044dd; background-color: #fff0f0 } /* Literal.String.Escape */
.highlight .sh { color: #dd2200; background-color: #fff0f0 } /* Literal.String.Heredoc */
.highlight .si { color: #3333bb; background-color: #fff0f0 } /* Literal.String.Interpol */
.highlight .sx { color: #22bb22; background-color: #f0fff0 } /* Literal.String.Other */
.highlight .sr { color: #008800; background-color: #fff0ff } /* Literal.String.Regex */
.highlight .s1 { color: #dd2200; background-color: #fff0f0 } /* Literal.String.Single */
.highlight .ss { color: #aa6600; background-color: #fff0f0 } /* Literal.String.Symbol */
.highlight .bp { color: #003388 } /* Name.Builtin.Pseudo */
.highlight .fm { color: #0066bb; font-weight: bold } /* Name.Function.Magic */
.highlight .vc { color: #336699 } /* Name.Variable.Class */
.highlight .vg { color: #dd7700 } /* Name.Variable.Global */
.highlight .vi { color: #3333bb } /* Name.Variable.Instance */
.highlight .vm { color: #336699 } /* Name.Variable.Magic */
.highlight .il { color: #0000DD; font-weight: bold } /* Literal.Number.Integer.Long */# Generic Architecture Example

This contains a simple, artificial, example of the nextpnr generic API.

 - simple.py procedurally generates a simple FPGA architecture with IO at the edges,
   logic slices in all other tiles, and interconnect only between adjacent tiles
 
 - simple_timing.py annotates cells with timing data (this is a separate script that must be run after packing)

 - write_fasm.py uses the nextpnr Python API to write a FASM file for a design

 - bitstream.py uses write_fasm.py to create a FASM ("FPGA assembly") file for the place-and-routed design

 - Run simple.sh to build an example design on the FPGA above
\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}