\end{frame}
\begin{frame}{Overview}
-This section contains 3 subsections:
+This section contains 2 subsections:
\begin{itemize}
\item Interactive Design Investigation
\item Symbolic Model Checking
-\item Reverse Engineering
\end{itemize}
\end{frame}
\subsectionpagesuffix
\end{frame}
-\subsubsection{TBD}
+\begin{frame}{\subsecname}
+Symbolic Model Checking (SMC) is used to formally prove that a circuit has
+(or has not) a given property.
+
+\bigskip
+One appliction 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.
-\begin{frame}{\subsubsecname}
-TBD
+\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
-\subsection{Reverse Engineering}
+\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}}
-\begin{frame}
-\subsectionpage
-\subsectionpagesuffix
+\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 equivialence
+miter -equiv -make_assert -make_outputs test_orig test_mapped miter
+flatten miter
+
+# run equivialence 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}
-\subsubsection{TBD}
+\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. (Somtheing a test bench might do.)
-\begin{frame}{\subsubsecname}
-TBD
+\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}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}{\subsecname}
\begin{itemize}
-\item TBD
-\item TBD
-\item TBD
-\item TBD
+\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
--- /dev/null
+module axis_test(aclk, tready);
+ input aclk, tready;
+ wire aresetn, tvalid;
+ wire [7:0] tdata;
+
+ integer counter = 0;
+ reg aresetn = 0;
+
+ axis_master uut (aclk, aresetn, tvalid, tready, tdata);
+
+ always @(posedge aclk) begin
+ if (aresetn && tready && tvalid) begin
+ if (counter == 0) assert(tdata == 19);
+ if (counter == 1) assert(tdata == 99);
+ if (counter == 2) assert(tdata == 1);
+ if (counter == 3) assert(tdata == 244);
+ if (counter == 4) assert(tdata == 133);
+ if (counter == 5) assert(tdata == 209);
+ if (counter == 6) assert(tdata == 241);
+ if (counter == 7) assert(tdata == 137);
+ if (counter == 8) assert(tdata == 176);
+ if (counter == 9) assert(tdata == 6);
+ counter <= counter + 1;
+ end
+ aresetn <= 1;
+ end
+endmodule
projects / yosys.git / commitdiff