summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorClifford Wolf <clifford@clifford.at>2014-06-21 16:33:33 +0200
committerClifford Wolf <clifford@clifford.at>2014-06-21 16:33:33 +0200
commitb18fa95d2f1f4118cdb7c16e3415059bd81e2325 (patch)
tree68ba5ef340312a0d5f3a63108dddf034e8e6dba6
parent1c85584fe5843a43590de3927fe9bde74a04e72e (diff)
Progress in presentation
-rw-r--r--manual/PRESENTATION_ExOth.tex115
-rw-r--r--manual/PRESENTATION_ExOth/Makefile10
-rw-r--r--manual/PRESENTATION_ExOth/axis_master.v27
-rw-r--r--manual/PRESENTATION_ExOth/axis_test.v27
-rw-r--r--manual/PRESENTATION_ExOth/axis_test.ys5
-rw-r--r--manual/PRESENTATION_ExOth/equiv.ys17
-rw-r--r--manual/PRESENTATION_ExSyn.tex2
-rw-r--r--manual/PRESENTATION_ExSyn/Makefile2
-rw-r--r--manual/PRESENTATION_ExSyn/techmap_01_map.v6
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;