228 lines
6.8 KiB
TeX
228 lines
6.8 KiB
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}
|
|
|