Progress in presentation

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.
 
-\begin{frame}{\subsubsecname}
+\bigskip
-TBD
+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
 
-\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}
+\vskip5cm\hskip5cm
-\subsectionpage
+Lets see if it is correct..
-\subsectionpagesuffix
 \end{frame}
 
-\subsubsection{TBD}
+\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
 
-\begin{frame}{\subsubsecname}
+# create two version of the design: test_orig and test_mapped
-TBD
+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}
+
+\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.)
+
+\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 Yosys provides useful features beyond synthesis.
-\item TBD
+\item The commands {\tt sat} and {\tt eval} can be used to analyse the behavior of a circuit.
-\item TBD
+\item The {\tt sat} command can also be used for symbolic model checking.
-\item TBD
+\item This can be useful for debugging and testing designs and Yosys extensions alike.
 \end{itemize}
 
 \bigskip

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
+

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

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

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

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

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:

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
 

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];
+      wire [16:0] S1 = A[15:0] + B[15:0];
-      assign Y[15:0] = A[15:0] + B[15:0];
+      wire [15:0] S2 = A[31:16] + B[31:16] + S1[16];
-      assign Y[31:16] = A[31:16] + B[31:16] + CARRY;
+      assign Y = {S2[15:0], S1[15:0]};
     end
   else
     wire _TECHMAP_FAIL_ = 1;