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