manual/PRESENTATION_ExOth.tex

   1
   2 \section{Yosys by example -- Beyond Synthesis}
   3
   4 \begin{frame}
   5 \sectionpage
   6 \end{frame}
   7
   8 \begin{frame}{Overview}
   9 This 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}
  26 Yosys can also be used to investigate designs (or netlists created
  27 from other tools).
  28
  29 \begin{itemize}
  30 \item
  31 The selection mechanism (see slides ``Using Selections''), especially patterns such
  32 as {\tt \%ci} and {\tt \%co}, can be used to figure out how parts of the design
  33 are connected.
  34
  35 \item
  36 Commands such as {\tt submod}, {\tt expose}, {\tt splice}, \dots can be used
  37 to transform the design into an equivalent design that is easier to analyse.
  38
  39 \item
  40 Commands such as {\tt eval} and {\tt sat} can be used to investigate the
  41 behavior 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]
  51 read_verilog scrambler.v
  52
  53 hierarchy; proc;;
  54
  55 cd scrambler
  56 submod -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
  78 Eval result: \out = 270369.
  79
  80 > eval -set in 270369 -show out
  81 Eval result: \out = 67634689.
  82
  83 > sat -set out 632435482
  84 Signal 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}
 101 Symbolic Model Checking (SMC) is used to formally prove that a circuit has
 102 (or has not) a given property.
 103
 104 \bigskip
 105 One application is Formal Equivalence Checking: Proving that two circuits
 106 are identical. For example this is a very useful feature when debugging custom
 107 passes in Yosys.
 108
 109 \bigskip
 110 Other applications include checking if a module conforms to interface
 111 standards.
 112
 113 \bigskip
 114 The {\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)}
 118 Remember 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
 130 Lets 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
 136 read_verilog techmap_01.v
 137 hierarchy -top test
 138
 139 # create two version of the design: test_orig and test_mapped
 140 copy test test_orig
 141 rename test test_mapped
 142
 143 # apply the techmap only to test_mapped
 144 techmap -map techmap_01_map.v test_mapped
 145
 146 # create a miter circuit to test equivalence
 147 miter -equiv -make_assert -make_outputs test_orig test_mapped miter
 148 flatten miter
 149
 150 # run equivalence check
 151 sat -verify -prove-asserts -show-inputs -show-outputs miter
 152 \end{lstlisting}
 153
 154 \dots
 155 \begin{lstlisting}[basicstyle=\ttfamily\fontsize{8pt}{10pt}\selectfont]
 156 Solving problem with 945 variables and 2505 clauses..
 157 SAT 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
 163 The following AXI4 Stream Master has a bug. But the bug is not exposed if the
 164 slave keeps {\tt tready} asserted all the time. (Something a test bench might do.)
 165
 166 \medskip
 167 Symbolic Model Checking can be used to expose the bug and find a sequence
 168 of 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]
 181 read_verilog -sv axis_master.v axis_test.v
 182 hierarchy -top axis_test
 183
 184 proc; flatten;;
 185 sat -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]
 191 Solving problem with 159344 variables and 442126 clauses..
 192 SAT 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]
 198 Solving problem with 159144 variables and 441626 clauses..
 199 SAT 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}
 218 Questions?
 219 \end{center}
 220
 221 \bigskip
 222 \bigskip
 223 \begin{center}
 224 \url{https://yosyshq.net/yosys/}
 225 \end{center}
 226 \end{frame}
 227