diff options
author | Clifford Wolf <clifford@clifford.at> | 2014-06-21 16:33:33 +0200 |
---|---|---|
committer | Clifford Wolf <clifford@clifford.at> | 2014-06-21 16:33:33 +0200 |
commit | b18fa95d2f1f4118cdb7c16e3415059bd81e2325 (patch) | |
tree | 68ba5ef340312a0d5f3a63108dddf034e8e6dba6 /manual/PRESENTATION_ExOth.tex | |
parent | 1c85584fe5843a43590de3927fe9bde74a04e72e (diff) |
Progress in presentation
Diffstat (limited to 'manual/PRESENTATION_ExOth.tex')
-rw-r--r-- | manual/PRESENTATION_ExOth.tex | 115 |
1 files changed, 98 insertions, 17 deletions
diff --git a/manual/PRESENTATION_ExOth.tex b/manual/PRESENTATION_ExOth.tex index 64c4af72..3f0749cd 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} @@ -98,25 +97,107 @@ Signal Name Dec Hex Bin \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} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @@ -125,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 |