8 files changed, 130 insertions, 0 deletions
diff --git a/manual/PRESENTATION_ExOth/.gitignore b/manual/PRESENTATION_ExOth/.gitignore
new file mode 100644
index 000000000..cf658897d
--- /dev/null
+++ b/manual/PRESENTATION_ExOth/.gitignore
@@ -0,0 +1 @@
+*.dot
diff --git a/manual/PRESENTATION_ExOth/Makefile b/manual/PRESENTATION_ExOth/Makefile
new file mode 100644
index 000000000..4864d8d52
--- /dev/null
+++ b/manual/PRESENTATION_ExOth/Makefile
@@ -0,0 +1,16 @@
+
+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 000000000..25a1feee4
--- /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 000000000..0be833f16
--- /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 000000000..19663ac77
--- /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 000000000..09a4045db
--- /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_ExOth/scrambler.v b/manual/PRESENTATION_ExOth/scrambler.v
new file mode 100644
index 000000000..d4c1fa2bb
--- /dev/null
+++ b/manual/PRESENTATION_ExOth/scrambler.v
@@ -0,0 +1,14 @@
+module scrambler(
+        input clk, rst, in_bit,
+        output reg out_bit
+);
+    reg [31:0] xs;
+    always @(posedge clk) begin
+    	if (rst)
+	    xs = 1;
+        xs = xs ^ (xs << 13);
+        xs = xs ^ (xs >> 17);
+        xs = xs ^ (xs << 5);
+        out_bit <= in_bit ^ xs[0];
+    end
+endmodule
diff --git a/manual/PRESENTATION_ExOth/scrambler.ys b/manual/PRESENTATION_ExOth/scrambler.ys
new file mode 100644
index 000000000..2ef14c56e
--- /dev/null
+++ b/manual/PRESENTATION_ExOth/scrambler.ys
@@ -0,0 +1,23 @@
+
+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 ..
+
+show -prefix scrambler_p01 -format pdf -notitle scrambler
+show -prefix scrambler_p02 -format pdf -notitle xorshift32
+
+echo on
+
+cd xorshift32
+rename n2 in
+rename n1 out
+
+eval -set in 1 -show out
+eval -set in 270369 -show out
+
+sat -set out 632435482
+