1
2\section{Yosys by example -- Beyond Synthesis}
3
4\begin{frame}
5\sectionpage
6\end{frame}
7
8\begin{frame}{Overview}
9This section contains 2 subsections:
10\begin{itemize}
11\item Interactive Design Investigation
12\item Symbolic Model Checking
13\end{itemize}
14\end{frame}
15
16%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
17
18\subsection{Interactive Design Investigation}
19
20\begin{frame}
21\subsectionpage
22\subsectionpagesuffix
23\end{frame}
24
25\begin{frame}{\subsecname}
26Yosys can also be used to investigate designs (or netlists created
27from other tools).
28
29\begin{itemize}
30\item
31The selection mechanism (see slides ``Using Selections''), especially patterns such
32as {\tt \%ci} and {\tt \%co}, can be used to figure out how parts of the design
33are connected.
34
35\item
36Commands such as {\tt submod}, {\tt expose}, {\tt splice}, \dots can be used
37to transform the design into an equivalent design that is easier to analyse.
38
39\item
40Commands such as {\tt eval} and {\tt sat} can be used to investigate the
41behavior of the circuit.
42\end{itemize}
43\end{frame}
44
45\begin{frame}[t, fragile]{Example: Reorganizing a module}
46\begin{columns}
47\column[t]{4cm}
48\lstinputlisting[basicstyle=\ttfamily\fontsize{6pt}{7pt}\selectfont, language=verilog]{PRESENTATION_ExOth/scrambler.v}
49\column[t]{7cm}
50\begin{lstlisting}[basicstyle=\ttfamily\fontsize{8pt}{10pt}\selectfont, language=ys, frame=single]
51read_verilog scrambler.v
52
53hierarchy; proc;;
54
55cd scrambler
56submod -name xorshift32 \
57           xs %c %ci %D %c %ci:+[D] %D \
58           %ci*:-$dff xs %co %ci %d
59\end{lstlisting}
60\end{columns}
61
62\hfil\includegraphics[width=11cm,trim=0 0cm 0 1.5cm]{PRESENTATION_ExOth/scrambler_p01.pdf}
63
64\hfil\includegraphics[width=11cm,trim=0 0cm 0 2cm]{PRESENTATION_ExOth/scrambler_p02.pdf}
65\end{frame}
66
67\begin{frame}[t, fragile]{Example: Analysis of circuit behavior}
68\begin{lstlisting}[basicstyle=\ttfamily\fontsize{8pt}{10pt}\selectfont, language=ys]
69> read_verilog scrambler.v
70> hierarchy; proc;; cd scrambler
71> submod -name xorshift32 xs %c %ci %D %c %ci:+[D] %D %ci*:-$dff xs %co %ci %d
72
73> cd xorshift32
74> rename n2 in
75> rename n1 out
76
77> eval -set in 1 -show out
78Eval result: \out = 270369.
79
80> eval -set in 270369 -show out
81Eval result: \out = 67634689.
82
83> sat -set out 632435482
84Signal Name                 Dec        Hex                                   Bin
85-------------------- ---------- ---------- -------------------------------------
86\in                   745495504   2c6f5bd0      00101100011011110101101111010000
87\out                  632435482   25b2331a      00100101101100100011001100011010
88\end{lstlisting}
89\end{frame}
90
91%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
92
93\subsection{Symbolic Model Checking}
94
95\begin{frame}
96\subsectionpage
97\subsectionpagesuffix
98\end{frame}
99
100\begin{frame}{\subsecname}
101Symbolic Model Checking (SMC) is used to formally prove that a circuit has
102(or has not) a given property.
103
104\bigskip
105One application is Formal Equivalence Checking: Proving that two circuits
106are identical. For example this is a very useful feature when debugging custom
107passes in Yosys.
108
109\bigskip
110Other applications include checking if a module conforms to interface
111standards.
112
113\bigskip
114The {\tt sat} command in Yosys can be used to perform Symbolic Model Checking.
115\end{frame}
116
117\begin{frame}[t]{Example: Formal Equivalence Checking (1/2)}
118Remember the following example?
119\vskip1em
120
121\vbox to 0cm{
122\vskip-0.3cm
123\lstinputlisting[basicstyle=\ttfamily\fontsize{6pt}{7pt}\selectfont, language=verilog]{PRESENTATION_ExSyn/techmap_01_map.v}
124}\vbox to 0cm{
125\vskip-0.5cm
126\lstinputlisting[xleftmargin=5cm, basicstyle=\ttfamily\fontsize{8pt}{10pt}\selectfont, frame=single, language=verilog]{PRESENTATION_ExSyn/techmap_01.v}
127\lstinputlisting[xleftmargin=5cm, basicstyle=\ttfamily\fontsize{8pt}{10pt}\selectfont, language=ys, frame=single]{PRESENTATION_ExSyn/techmap_01.ys}}
128
129\vskip5cm\hskip5cm
130Lets see if it is correct..
131\end{frame}
132
133\begin{frame}[t, fragile]{Example: Formal Equivalence Checking (2/2)}
134\begin{lstlisting}[basicstyle=\ttfamily\fontsize{8pt}{10pt}\selectfont, language=ys, frame=single]
135# read test design
136read_verilog techmap_01.v
137hierarchy -top test
138
139# create two version of the design: test_orig and test_mapped
140copy test test_orig
141rename test test_mapped
142
143# apply the techmap only to test_mapped
144techmap -map techmap_01_map.v test_mapped
145
146# create a miter circuit to test equivalence
147miter -equiv -make_assert -make_outputs test_orig test_mapped miter
148flatten miter
149
150# run equivalence check
151sat -verify -prove-asserts -show-inputs -show-outputs miter
152\end{lstlisting}
153
154\dots
155\begin{lstlisting}[basicstyle=\ttfamily\fontsize{8pt}{10pt}\selectfont]
156Solving problem with 945 variables and 2505 clauses..
157SAT proof finished - no model found: SUCCESS!
158\end{lstlisting}
159\end{frame}
160
161\begin{frame}[t, fragile]{Example: Symbolic Model Checking (1/2)}
162\small
163The following AXI4 Stream Master has a bug. But the bug is not exposed if the
164slave keeps {\tt tready} asserted all the time. (Something a test bench might do.)
165
166\medskip
167Symbolic Model Checking can be used to expose the bug and find a sequence
168of values for {\tt tready} that yield the incorrect behavior.
169
170\vskip-1em
171\begin{columns}
172\column[t]{5cm}
173\lstinputlisting[basicstyle=\ttfamily\fontsize{5pt}{6pt}\selectfont, language=verilog]{PRESENTATION_ExOth/axis_master.v}
174\column[t]{5cm}
175\lstinputlisting[basicstyle=\ttfamily\fontsize{5pt}{6pt}\selectfont, language=verilog]{PRESENTATION_ExOth/axis_test.v}
176\end{columns}
177\end{frame}
178
179\begin{frame}[t, fragile]{Example: Symbolic Model Checking (2/2)}
180\begin{lstlisting}[basicstyle=\ttfamily\fontsize{8pt}{10pt}\selectfont, language=ys, frame=single]
181read_verilog -sv axis_master.v axis_test.v
182hierarchy -top axis_test
183
184proc; flatten;;
185sat -seq 50 -prove-asserts
186\end{lstlisting}
187
188\bigskip
189\dots with unmodified {\tt axis\_master.v}:
190\begin{lstlisting}[basicstyle=\ttfamily\fontsize{8pt}{10pt}\selectfont]
191Solving problem with 159344 variables and 442126 clauses..
192SAT proof finished - model found: FAIL!
193\end{lstlisting}
194
195\bigskip
196\dots with fixed {\tt axis\_master.v}:
197\begin{lstlisting}[basicstyle=\ttfamily\fontsize{8pt}{10pt}\selectfont]
198Solving problem with 159144 variables and 441626 clauses..
199SAT proof finished - no model found: SUCCESS!
200\end{lstlisting}
201\end{frame}
202
203%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
204
205\subsection{Summary}
206
207\begin{frame}{\subsecname}
208\begin{itemize}
209\item Yosys provides useful features beyond synthesis.
210\item The commands {\tt sat} and {\tt eval} can be used to analyse the behavior of a circuit.
211\item The {\tt sat} command can also be used for symbolic model checking.
212\item This can be useful for debugging and testing designs and Yosys extensions alike.
213\end{itemize}
214
215\bigskip
216\bigskip
217\begin{center}
218Questions?
219\end{center}
220
221\bigskip
222\bigskip
223\begin{center}
224\url{https://yosyshq.net/yosys/}
225\end{center}
226\end{frame}
227
228