diff options
| -rw-r--r-- | manual/PRESENTATION_ExOth.tex | 115 | ||||
| -rw-r--r-- | manual/PRESENTATION_ExOth/Makefile | 10 | ||||
| -rw-r--r-- | manual/PRESENTATION_ExOth/axis_master.v | 27 | ||||
| -rw-r--r-- | manual/PRESENTATION_ExOth/axis_test.v | 27 | ||||
| -rw-r--r-- | manual/PRESENTATION_ExOth/axis_test.ys | 5 | ||||
| -rw-r--r-- | manual/PRESENTATION_ExOth/equiv.ys | 17 | ||||
| -rw-r--r-- | manual/PRESENTATION_ExSyn.tex | 2 | ||||
| -rw-r--r-- | manual/PRESENTATION_ExSyn/Makefile | 2 | ||||
| -rw-r--r-- | manual/PRESENTATION_ExSyn/techmap_01_map.v | 6 |
9 files changed, 188 insertions, 23 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 diff --git a/manual/PRESENTATION_ExOth/Makefile b/manual/PRESENTATION_ExOth/Makefile index a12beada..4864d8d5 100644 --- a/manual/PRESENTATION_ExOth/Makefile +++ b/manual/PRESENTATION_ExOth/Makefile @@ -1,8 +1,16 @@ -all: scrambler_p01.pdf scrambler_p02.pdf +all: scrambler_p01.pdf scrambler_p02.pdf equiv.log axis_test.log scrambler_p01.pdf: scrambler.ys scrambler.v ../../yosys scrambler.ys scrambler_p02.pdf: scrambler_p01.pdf +equiv.log: equiv.ys + ../../yosys -l equiv.log_new equiv.ys + mv equiv.log_new equiv.log + +axis_test.log: axis_test.ys axis_master.v axis_test.v + ../../yosys -l axis_test.log_new axis_test.ys + mv axis_test.log_new axis_test.log + diff --git a/manual/PRESENTATION_ExOth/axis_master.v b/manual/PRESENTATION_ExOth/axis_master.v new file mode 100644 index 00000000..25a1feee --- /dev/null +++ b/manual/PRESENTATION_ExOth/axis_master.v @@ -0,0 +1,27 @@ +module axis_master(aclk, aresetn, tvalid, tready, tdata); + input aclk, aresetn, tready; + output reg tvalid; + output reg [7:0] tdata; + + reg [31:0] state; + always @(posedge aclk) begin + if (!aresetn) begin + state <= 314159265; + tvalid <= 0; + tdata <= 'bx; + end else begin + if (tvalid && tready) + tvalid <= 0; + if (!tvalid || !tready) begin + // ^- should be not inverted! + state = state ^ state << 13; + state = state ^ state >> 7; + state = state ^ state << 17; + if (state[9:8] == 0) begin + tvalid <= 1; + tdata <= state; + end + end + end + end +endmodule diff --git a/manual/PRESENTATION_ExOth/axis_test.v b/manual/PRESENTATION_ExOth/axis_test.v new file mode 100644 index 00000000..0be833f1 --- /dev/null +++ b/manual/PRESENTATION_ExOth/axis_test.v @@ -0,0 +1,27 @@ +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 diff --git a/manual/PRESENTATION_ExOth/axis_test.ys b/manual/PRESENTATION_ExOth/axis_test.ys new file mode 100644 index 00000000..19663ac7 --- /dev/null +++ b/manual/PRESENTATION_ExOth/axis_test.ys @@ -0,0 +1,5 @@ +read_verilog -sv axis_master.v axis_test.v +hierarchy -top axis_test + +proc; flatten;; +sat -falsify -seq 50 -prove-asserts diff --git a/manual/PRESENTATION_ExOth/equiv.ys b/manual/PRESENTATION_ExOth/equiv.ys new file mode 100644 index 00000000..09a4045d --- /dev/null +++ b/manual/PRESENTATION_ExOth/equiv.ys @@ -0,0 +1,17 @@ +# read test design +read_verilog ../PRESENTATION_ExSyn/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 ../PRESENTATION_ExSyn/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 diff --git a/manual/PRESENTATION_ExSyn.tex b/manual/PRESENTATION_ExSyn.tex index 432ce368..d1d8abe4 100644 --- a/manual/PRESENTATION_ExSyn.tex +++ b/manual/PRESENTATION_ExSyn.tex @@ -346,7 +346,7 @@ Finally the {\tt fsm\_map} command can be used to convert the (optimized) {\tt \subsection{The {\tt techmap} command} \begin{frame}[t]{\subsecname} -\vbox to 0cm{\includegraphics[width=12cm,trim=-18cm 0cm 0cm -34cm]{PRESENTATION_ExSyn/techmap_01.pdf}\vss} +\vbox to 0cm{\includegraphics[width=12cm,trim=-15cm 0cm 0cm -20cm]{PRESENTATION_ExSyn/techmap_01.pdf}\vss} \vskip-0.8cm The {\tt techmap} command replaces cells with implementations given as verilog source. For example implementing a 32 bit adder using 16 bit adders: diff --git a/manual/PRESENTATION_ExSyn/Makefile b/manual/PRESENTATION_ExSyn/Makefile index bcff48aa..c34eae3f 100644 --- a/manual/PRESENTATION_ExSyn/Makefile +++ b/manual/PRESENTATION_ExSyn/Makefile @@ -8,7 +8,7 @@ TARGETS += abc_01 all: $(addsuffix .pdf,$(TARGETS)) define make_pdf_template -$(1).pdf: $(1).v $(1).ys +$(1).pdf: $(1)*.v $(1)*.ys ../../yosys -p 'script $(1).ys; show -notitle -prefix $(1) -format pdf' endef diff --git a/manual/PRESENTATION_ExSyn/techmap_01_map.v b/manual/PRESENTATION_ExSyn/techmap_01_map.v index 64c0b87c..4fd86e85 100644 --- a/manual/PRESENTATION_ExSyn/techmap_01_map.v +++ b/manual/PRESENTATION_ExSyn/techmap_01_map.v @@ -13,9 +13,9 @@ output [Y_WIDTH-1:0] Y; generate if ((A_WIDTH == 32) && (B_WIDTH == 32)) begin - wire [15:0] CARRY = |{A[15:0], B[15:0]} && ~|Y[15:0]; - assign Y[15:0] = A[15:0] + B[15:0]; - assign Y[31:16] = A[31:16] + B[31:16] + CARRY; + wire [16:0] S1 = A[15:0] + B[15:0]; + wire [15:0] S2 = A[31:16] + B[31:16] + S1[16]; + assign Y = {S2[15:0], S1[15:0]}; end else wire _TECHMAP_FAIL_ = 1; |