diff options
Diffstat (limited to 'manual/PRESENTATION_ExOth.tex')
| -rw-r--r-- | manual/PRESENTATION_ExOth.tex | 181 |
1 files changed, 161 insertions, 20 deletions
diff --git a/manual/PRESENTATION_ExOth.tex b/manual/PRESENTATION_ExOth.tex index 13ec3d193..f86dcd7ac 100644 --- a/manual/PRESENTATION_ExOth.tex +++ b/manual/PRESENTATION_ExOth.tex @@ -6,11 +6,10 @@ \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} @@ -23,10 +22,70 @@ This section contains 3 subsections: \subsectionpagesuffix \end{frame} -\subsubsection{TBD} +\begin{frame}{\subsecname} +Yosys can also be used to investigate designs (or netlists created +from other tools). + +\begin{itemize} +\item +The selection mechanism (see slides ``Using Selections''), especially patterns such +as {\tt \%ci} and {\tt \%co}, can be used to figure out how parts of the design +are connected. + +\item +Commands such as {\tt submod}, {\tt expose}, {\tt splice}, \dots can be used +to transform the design into an equivialent design that is easier to analyse. + +\item +Commands such as {\tt eval} and {\tt sat} can be used to investigate the +behavior of the circuit. +\end{itemize} +\end{frame} -\begin{frame}{\subsubsecname} -TBD +\begin{frame}[t, fragile]{Example: Reorganizing a module} +\begin{columns} +\column[t]{4cm} +\lstinputlisting[basicstyle=\ttfamily\fontsize{6pt}{7pt}\selectfont, language=verilog]{PRESENTATION_ExOth/scrambler.v} +\column[t]{7cm} +\begin{lstlisting}[basicstyle=\ttfamily\fontsize{8pt}{10pt}\selectfont, language=ys, frame=single] +read_verilog scrambler.v + +hierarchy; proc;; + +cd scrambler +submod -name xorshift32 \ + xs %c %ci %D %c %ci:+[D] %D \ + %ci*:-$dff xs %co %ci %d +\end{lstlisting} +\end{columns} + +\hfil\includegraphics[width=11cm,trim=0 0cm 0 1.5cm]{PRESENTATION_ExOth/scrambler_p01.pdf} + +\hfil\includegraphics[width=11cm,trim=0 0cm 0 2cm]{PRESENTATION_ExOth/scrambler_p02.pdf} +\end{frame} + +\begin{frame}[t, fragile]{Example: Analysis of circuit behavior} +\begin{lstlisting}[basicstyle=\ttfamily\fontsize{8pt}{10pt}\selectfont, language=ys] +> read_verilog scrambler.v +> hierarchy; proc;; cd scrambler +> submod -name xorshift32 xs %c %ci %D %c %ci:+[D] %D %ci*:-$dff xs %co %ci %d + +> cd xorshift32 +> rename n2 in +> rename n1 out + +> eval -set in 1 -show out +Eval result: \out = 270369. + +> eval -set in 270369 -show out +Eval result: \out = 67634689. + +> sat -set out 632435482 +Signal Name Dec Hex Bin +-------------------- ---------- ---------- ------------------------------------- +\in 745495504 2c6f5bd0 00101100011011110101101111010000 +\out 632435482 25b2331a 00100101101100100011001100011010 +\end{lstlisting} \end{frame} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @@ -38,25 +97,107 @@ TBD \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. + +\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 -\begin{frame}{\subsubsecname} -TBD +\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}} + +\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 -\subsection{Reverse Engineering} +# create two version of the design: test_orig and test_mapped +copy test test_orig +rename test test_mapped -\begin{frame} -\subsectionpage -\subsectionpagesuffix +# 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} + +\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. (Something a test bench might do.) + +\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} -\subsubsection{TBD} +\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 -\begin{frame}{\subsubsecname} -TBD +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} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @@ -65,10 +206,10 @@ TBD \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 |