2 \section{Yosys by example -- Beyond Synthesis
}
8 \begin{frame
}{Overview
}
9 This section contains
2 subsections:
11 \item Interactive Design Investigation
12 \item Symbolic Model Checking
16 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
18 \subsection{Interactive Design Investigation
}
25 \begin{frame
}{\subsecname}
26 Yosys can also be used to investigate designs (or netlists created
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
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.
40 Commands such as
{\tt eval
} and
{\tt sat
} can be used to investigate the
41 behavior of the circuit.
45 \begin{frame
}[t, fragile
]{Example: Reorganizing a module
}
48 \lstinputlisting[basicstyle=
\ttfamily\fontsize{6pt
}{7pt
}\selectfont, language=verilog
]{PRESENTATION_ExOth/scrambler.v
}
50 \begin{lstlisting
}[basicstyle=
\ttfamily\fontsize{8pt
}{10pt
}\selectfont, language=ys, frame=single
]
51 read_verilog scrambler.v
56 submod -name xorshift32 \
57 xs
%c %ci %D %c %ci:+[D] %D \
58 %ci*:-$dff xs %co %ci %d
62 \hfil\includegraphics[width=
11cm,trim=
0 0cm
0 1.5cm
]{PRESENTATION_ExOth/scrambler_p01.pdf
}
64 \hfil\includegraphics[width=
11cm,trim=
0 0cm
0 2cm
]{PRESENTATION_ExOth/scrambler_p02.pdf
}
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
77 > eval -set in
1 -show out
78 Eval result:
\out =
270369.
80 > eval -set in
270369 -show out
81 Eval result:
\out =
67634689.
83 > sat -set out
632435482
84 Signal Name Dec Hex Bin
85 -------------------- ---------- ---------- -------------------------------------
86 \in 745495504 2c6f5bd0
00101100011011110101101111010000
87 \out 632435482 25b2331a
00100101101100100011001100011010
91 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
93 \subsection{Symbolic Model Checking
}
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.
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
110 Other applications include checking if a module conforms to interface
114 The
{\tt sat
} command in Yosys can be used to perform Symbolic Model Checking.
117 \begin{frame
}[t
]{Example: Formal Equivalence Checking (
1/
2)
}
118 Remember the following example?
123 \lstinputlisting[basicstyle=
\ttfamily\fontsize{6pt
}{7pt
}\selectfont, language=verilog
]{PRESENTATION_ExSyn/techmap_01_map.v
}
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
}}
130 Lets see if it is correct..
133 \begin{frame
}[t, fragile
]{Example: Formal Equivalence Checking (
2/
2)
}
134 \begin{lstlisting
}[basicstyle=
\ttfamily\fontsize{8pt
}{10pt
}\selectfont, language=ys, frame=single
]
136 read_verilog techmap_01.v
139 # create two version of the design: test_orig and test_mapped
141 rename test test_mapped
143 # apply the techmap only to test_mapped
144 techmap -map techmap_01_map.v test_mapped
146 # create a miter circuit to test equivalence
147 miter -equiv -make_assert -make_outputs test_orig test_mapped miter
150 # run equivalence check
151 sat -verify -prove-asserts -show-inputs -show-outputs miter
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!
161 \begin{frame
}[t, fragile
]{Example: Symbolic Model Checking (
1/
2)
}
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.)
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.
173 \lstinputlisting[basicstyle=
\ttfamily\fontsize{5pt
}{6pt
}\selectfont, language=verilog
]{PRESENTATION_ExOth/axis_master.v
}
175 \lstinputlisting[basicstyle=
\ttfamily\fontsize{5pt
}{6pt
}\selectfont, language=verilog
]{PRESENTATION_ExOth/axis_test.v
}
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
185 sat -seq
50 -prove-asserts
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!
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!
203 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
207 \begin{frame
}{\subsecname}
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.
224 \url{http://www.clifford.at/yosys/
}