Merge remote-tracking branch 'origin/master' into xaig

5 files changed, 577 insertions, 1 deletions

diff --git a/tests/memories/issue00335.v b/tests/memories/issue00335.v
new file mode 100644
index 000000000..f3b6e5dfe
--- /dev/null
+++ b/tests/memories/issue00335.v
@@ -0,0 +1,28 @@
+// expect-wr-ports 1
+// expect-rd-ports 1
+// expect-rd-clk \clk
+
+module ram2 (input clk,
+             input             sel,
+             input             we, 
+             input [SIZE-1:0]  adr, 
+             input [63:0]      dat_i, 
+             output reg [63:0] dat_o);
+   parameter  SIZE = 5; // Address size
+
+   reg [63:0] mem [0:(1 << SIZE)-1];
+   integer    i;
+
+   initial begin
+      for (i = 0; i < (1<<SIZE) - 1; i = i + 1)
+        mem[i] <= 0;
+   end
+   
+   always @(posedge clk)
+     if (sel) begin
+       if (~we)
+         dat_o <= mem[adr];
+       else
+         mem[adr] <= dat_i;
+     end
+endmodule
diff --git a/tests/memories/issue00710.v b/tests/memories/issue00710.v
new file mode 100644
index 000000000..7a5fad1c2
--- /dev/null
+++ b/tests/memories/issue00710.v
@@ -0,0 +1,17 @@
+// expect-wr-ports 1
+// expect-rd-ports 1
+// expect-rd-clk \clk
+
+module top(input clk, input we, re, reset, input [7:0] addr, wdata, output reg [7:0] rdata);
+
+reg [7:0] bram[0:255];
+(* keep *) reg dummy;
+
+always @(posedge clk)
+	if (reset)
+		dummy <= 1'b0;
+	else if (re)
+		rdata <= bram[addr];
+	else if (we)
+		bram[addr] <= wdata;
+endmodule
diff --git a/tests/memories/run-test.sh b/tests/memories/run-test.sh
index 734a96682..d0537bb98 100755
--- a/tests/memories/run-test.sh
+++ b/tests/memories/run-test.sh
@@ -14,7 +14,7 @@ shift "$((OPTIND-1))"
 
 bash ../tools/autotest.sh $seed -G *.v
 
-for f in `egrep -l 'expect-(wr|rd)-ports' *.v`; do
+for f in `egrep -l 'expect-(wr-ports|rd-ports|rd-clk)' *.v`; do
 	echo -n "Testing expectations for $f .."
 	../../yosys -qp "proc; opt; memory -nomap;; dump -outfile ${f%.v}.dmp t:\$mem" $f
 	if grep -q expect-wr-ports $f; then
@@ -25,6 +25,10 @@ for f in `egrep -l 'expect-(wr|rd)-ports' *.v`; do
 		grep -q "parameter \\\\RD_PORTS $(gawk '/expect-rd-ports/ { print $3; }' $f)\$" ${f%.v}.dmp ||
 				{ echo " ERROR: Unexpected number of read ports."; false; }
 	fi
+	if grep -q expect-rd-clk $f; then
+		grep -q "connect \\\\RD_CLK \\$(gawk '/expect-rd-clk/ { print $3; }' $f)\$" ${f%.v}.dmp ||
+				{ echo " ERROR: Unexpected read clock."; false; }
+	fi
 	echo " ok."
 done
 
diff --git a/tests/various/muxpack.v b/tests/various/muxpack.v
new file mode 100644
index 000000000..33ece1f16
--- /dev/null
+++ b/tests/various/muxpack.v
@@ -0,0 +1,259 @@
+module mux_if_unbal_4_1 #(parameter N=4, parameter W=1) (input [N*W-1:0] i, input [$clog2(N)-1:0] s, output reg [W-1:0] o);
+always @*
+    if (s == 0) o <= i[0*W+:W];
+    else if (s == 1) o <= i[1*W+:W];
+    else if (s == 2) o <= i[2*W+:W];
+    else if (s == 3) o <= i[3*W+:W];
+    else o <= {W{1'bx}};
+endmodule
+
+module mux_if_unbal_5_3 #(parameter N=5, parameter W=3) (input [N*W-1:0] i, input [$clog2(N)-1:0] s, output reg [W-1:0] o);
+always @* begin
+    o <= {W{1'bx}};
+    if (s == 0) o <= i[0*W+:W];
+    if (s == 1) o <= i[1*W+:W];
+    if (s == 2) o <= i[2*W+:W];
+    if (s == 3) o <= i[3*W+:W];
+    if (s == 4) o <= i[4*W+:W];
+end
+endmodule
+
+module mux_if_unbal_5_3_invert #(parameter N=5, parameter W=3) (input [N*W-1:0] i, input [$clog2(N)-1:0] s, output reg [W-1:0] o);
+always @*
+    if (s != 0) 
+	   	if (s != 1) 
+			if (s != 2)
+				if (s != 3)
+					if (s != 4) o <= i[4*W+:W];
+					else o <= i[0*W+:W];
+				else o <= i[3*W+:W];
+			else o <= i[2*W+:W];
+		else o <= i[1*W+:W];
+    else o <= {W{1'bx}};
+endmodule
+
+module mux_if_unbal_5_3_width_mismatch #(parameter N=5, parameter W=3) (input [N*W-1:0] i, input [$clog2(N)-1:0] s, output reg [W-1:0] o);
+always @* begin
+    o <= {W{1'bx}};
+    if (s == 0) o <= i[0*W+:W];
+    if (s == 1) o <= i[1*W+:W];
+    if (s == 2) o[W-2:0] <= i[2*W+:W-1];
+    if (s == 3) o <= i[3*W+:W];
+    if (s == 4) o <= i[4*W+:W];
+end
+endmodule
+
+module mux_if_unbal_4_1_missing #(parameter N=5, parameter W=3) (input [N*W-1:0] i, input [$clog2(N)-1:0] s, output reg [W-1:0] o);
+always @* begin
+    if (s == 0) o <= i[0*W+:W];
+//    else if (s == 1) o <= i[1*W+:W];
+//    else if (s == 2) o <= i[2*W+:W];
+    else if (s == 3) o <= i[3*W+:W];
+    else o <= {W{1'bx}};
+end
+endmodule
+
+module mux_if_unbal_5_3_order #(parameter N=5, parameter W=3) (input [N*W-1:0] i, input [$clog2(N)-1:0] s, output reg [W-1:0] o);
+always @* begin
+    o <= {W{1'bx}};
+    if (s == 3) o <= i[3*W+:W];
+    if (s == 2) o <= i[2*W+:W];
+    if (s == 1) o <= i[1*W+:W];
+    if (s == 4) o <= i[4*W+:W];
+    if (s == 0) o <= i[0*W+:W];
+end
+endmodule
+
+module mux_if_unbal_4_1_nonexcl #(parameter N=4, parameter W=1) (input [N*W-1:0] i, input [$clog2(N)-1:0] s, output reg [W-1:0] o);
+always @*
+    if (s == 0) o <= i[0*W+:W];
+    else if (s == 1) o <= i[1*W+:W];
+    else if (s == 2) o <= i[2*W+:W];
+    else if (s == 3) o <= i[3*W+:W];
+	else if (s == 0) o <= {W{1'b0}};
+    else o <= {W{1'bx}};
+endmodule
+
+module mux_if_unbal_5_3_nonexcl #(parameter N=5, parameter W=3) (input [N*W-1:0] i, input [$clog2(N)-1:0] s, output reg [W-1:0] o);
+always @* begin
+    o <= {W{1'bx}};
+    if (s == 0) o <= i[0*W+:W];
+    if (s == 1) o <= i[1*W+:W];
+    if (s == 2) o <= i[2*W+:W];
+    if (s == 3) o <= i[3*W+:W];
+    if (s == 4) o <= i[4*W+:W];
+	if (s == 0) o <= i[2*W+:W];
+end
+endmodule
+
+module mux_case_unbal_8_7#(parameter N=8, parameter W=7) (input [N*W-1:0] i, input [$clog2(N)-1:0] s, output reg [W-1:0] o);
+always @* begin
+    o <= {W{1'bx}};
+    case (s)
+    0: o <= i[0*W+:W];
+    default:
+        case (s)
+        1: o <= i[1*W+:W];
+        2: o <= i[2*W+:W];
+        default:
+            case (s)
+            3: o <= i[3*W+:W];
+            4: o <= i[4*W+:W];
+            5: o <= i[5*W+:W];
+            default:
+                case (s)
+                    6: o <= i[6*W+:W];
+                    default: o <= i[7*W+:W];
+                endcase
+            endcase
+        endcase
+    endcase
+end
+endmodule
+
+module mux_if_bal_8_2 #(parameter N=8, parameter W=2) (input [N*W-1:0] i, input [$clog2(N)-1:0] s, output reg [W-1:0] o);
+always @*
+    if (s[0] == 1'b0)
+     if (s[1] == 1'b0)
+      if (s[2] == 1'b0)
+       o <= i[0*W+:W];
+      else
+       o <= i[1*W+:W];
+     else
+      if (s[2] == 1'b0)
+       o <= i[2*W+:W];
+      else
+       o <= i[3*W+:W];
+    else
+     if (s[1] == 1'b0)
+      if (s[2] == 1'b0)
+       o <= i[4*W+:W];
+      else
+       o <= i[5*W+:W];
+     else
+      if (s[2] == 1'b0)
+       o <= i[6*W+:W];
+      else
+       o <= i[7*W+:W];
+endmodule
+
+module mux_if_bal_5_1 #(parameter N=5, parameter W=1) (input [N*W-1:0] i, input [$clog2(N)-1:0] s, output reg [W-1:0] o);
+always @*
+    if (s[0] == 1'b0)
+     if (s[1] == 1'b0)
+      if (s[2] == 1'b0)
+       o <= i[0*W+:W];
+      else
+       o <= i[1*W+:W];
+     else
+      if (s[2] == 1'b0)
+       o <= i[2*W+:W];
+      else
+       o <= i[3*W+:W];
+    else
+     o <= i[4*W+:W];
+endmodule
+
+module cliffordwolf_nonexclusive_select (
+        input wire x, y, z,
+        input wire a, b, c, d,
+        output reg o
+);
+        always @* begin
+                o = a;
+                if (x) o = b;
+                if (y) o = c;
+                if (z) o = d;
+        end
+endmodule
+
+module cliffordwolf_freduce (
+        input wire [1:0] s,
+        input wire a, b, c, d,
+        output reg [3:0] o
+);
+        always @* begin
+                o = {4{a}};
+                if (s == 0) o = {3{b}};
+                if (s == 1) o = {2{c}};
+                if (s == 2) o = d;
+        end
+endmodule
+
+module case_nonexclusive_select (
+        input wire [1:0] x, y,
+        input wire a, b, c, d, e,
+        output reg o
+);
+        always @* begin
+            case (x)
+                0: o = b;
+                2: o = b;
+                1: o = c;
+                default: begin
+                    o = a;
+                    if (y == 0) o = d;
+                    if (y == 1) o = e;
+                end
+        endcase
+        end
+endmodule
+
+module case_nonoverlap (
+        input wire [2:0] x,
+        input wire a, b, c, d, e,
+        output reg o
+);
+        always @* begin
+            case (x)
+                0, 2: o = b; // Creates $reduce_or
+                1: o = c;
+                default:
+                    case (x)
+                        3: o = d; 4: o = d; // Creates $reduce_or
+                        5: o = e;
+                        default: o = 1'b0;
+                    endcase
+        endcase
+        end
+endmodule
+
+module case_overlap (
+        input wire [2:0] x,
+        input wire a, b, c, d, e,
+        output reg o
+);
+        always @* begin
+            case (x)
+                0, 2: o = b; // Creates $reduce_or
+                1: o = c;
+                default:
+                    case (x)
+                        0: o = 1'b1; // OVERLAP!
+                        3, 4: o = d; // Creates $reduce_or
+                        5: o = e;
+                        default: o = 1'b0;
+                    endcase
+        endcase
+        end
+endmodule
+
+module case_overlap2 (
+        input wire [2:0] x,
+        input wire a, b, c, d, e,
+        output reg o
+);
+        always @* begin
+            case (x)
+                0: o = b; 2: o = b; // Creates $reduce_or
+                1: o = c;
+                default:
+                    case (x)
+                        0: o = d; 2: o = d; // Creates $reduce_or
+                        3: o = d; 4: o = d; // Creates $reduce_or
+                        5: o = e;
+                        default: o = 1'b0;
+                    endcase
+        endcase
+        end
+endmodule
diff --git a/tests/various/muxpack.ys b/tests/various/muxpack.ys
new file mode 100644
index 000000000..af23fcec8
--- /dev/null
+++ b/tests/various/muxpack.ys
@@ -0,0 +1,268 @@
+read_verilog muxpack.v
+design -save read
+
+hierarchy -top mux_if_unbal_4_1
+prep
+design -save gold
+muxpack
+opt
+stat
+select -assert-count 0 t:$mux
+select -assert-count 1 t:$pmux
+design -stash gate
+design -import gold -as gold
+design -import gate -as gate
+miter -equiv -flatten -make_assert -make_outputs gold gate miter
+sat -verify -prove-asserts -show-ports miter
+
+design -load read
+hierarchy -top mux_if_unbal_5_3
+prep
+design -save gold
+muxpack
+opt
+stat
+select -assert-count 0 t:$mux
+select -assert-count 1 t:$pmux
+design -stash gate
+design -import gold -as gold
+design -import gate -as gate
+miter -equiv -flatten -make_assert -make_outputs gold gate miter
+sat -verify -prove-asserts -show-ports miter
+
+# TODO: Currently ExclusiveDatabase only analyses $eq cells
+#design -load read
+#hierarchy -top mux_if_unbal_5_3_invert
+#prep
+#design -save gold
+#muxpack
+#opt
+#stat
+#select -assert-count 0 t:$mux
+#select -assert-count 1 t:$pmux
+#design -stash gate
+#design -import gold -as gold
+#design -import gate -as gate
+#miter -equiv -flatten -make_assert -make_outputs gold gate miter
+#sat -verify -prove-asserts -show-ports miter
+
+design -load read
+hierarchy -top mux_if_unbal_5_3_width_mismatch
+prep
+design -save gold
+muxpack
+opt
+stat
+select -assert-count 0 t:$mux
+select -assert-count 2 t:$pmux
+design -stash gate
+design -import gold -as gold
+design -import gate -as gate
+miter -equiv -flatten -make_assert -make_outputs gold gate miter
+sat -verify -prove-asserts -show-ports miter
+
+design -load read
+hierarchy -top mux_if_unbal_4_1_missing
+prep
+design -save gold
+muxpack
+opt
+stat
+select -assert-count 0 t:$mux
+select -assert-count 1 t:$pmux
+design -stash gate
+design -import gold -as gold
+design -import gate -as gate
+miter -equiv -flatten -make_assert -make_outputs gold gate miter
+sat -verify -prove-asserts -show-ports miter
+
+design -load read
+hierarchy -top mux_if_unbal_5_3_order
+prep
+design -save gold
+muxpack
+opt
+stat
+select -assert-count 0 t:$mux
+select -assert-count 1 t:$pmux
+design -stash gate
+design -import gold -as gold
+design -import gate -as gate
+miter -equiv -flatten -make_assert -make_outputs gold gate miter
+sat -verify -prove-asserts -show-ports miter
+
+design -load read
+hierarchy -top mux_if_unbal_4_1_nonexcl
+prep
+design -save gold
+muxpack
+opt
+stat
+select -assert-count 0 t:$mux
+select -assert-count 1 t:$pmux
+design -stash gate
+design -import gold -as gold
+design -import gate -as gate
+miter -equiv -flatten -make_assert -make_outputs gold gate miter
+sat -verify -prove-asserts -show-ports miter
+
+design -load read
+hierarchy -top mux_if_unbal_5_3_nonexcl
+prep
+design -save gold
+muxpack
+opt
+stat
+select -assert-count 0 t:$mux
+select -assert-count 1 t:$pmux
+design -stash gate
+design -import gold -as gold
+design -import gate -as gate
+miter -equiv -flatten -make_assert -make_outputs gold gate miter
+sat -verify -prove-asserts -show-ports miter
+
+design -load read
+hierarchy -top mux_case_unbal_8_7
+prep
+design -save gold
+muxpack
+opt
+stat
+select -assert-count 0 t:$mux
+select -assert-count 1 t:$pmux
+design -stash gate
+design -import gold -as gold
+design -import gate -as gate
+miter -equiv -flatten -make_assert -make_outputs gold gate miter
+sat -verify -prove-asserts -show-ports miter
+
+design -load read
+hierarchy -top mux_if_bal_8_2
+prep
+design -save gold
+muxpack
+opt
+stat
+select -assert-count 7 t:$mux
+select -assert-count 0 t:$pmux
+design -stash gate
+design -import gold -as gold
+design -import gate -as gate
+miter -equiv -flatten -make_assert -make_outputs gold gate miter
+sat -verify -prove-asserts -show-ports miter
+
+design -load read
+hierarchy -top mux_if_bal_5_1
+prep
+design -save gold
+muxpack
+opt
+stat
+select -assert-count 4 t:$mux
+select -assert-count 0 t:$pmux
+design -stash gate
+design -import gold -as gold
+design -import gate -as gate
+miter -equiv -flatten -make_assert -make_outputs gold gate miter
+sat -verify -prove-asserts -show-ports miter
+
+design -load read
+hierarchy -top cliffordwolf_nonexclusive_select
+prep
+design -save gold
+muxpack
+opt
+stat
+select -assert-count 3 t:$mux
+select -assert-count 0 t:$pmux
+design -stash gate
+design -import gold -as gold
+design -import gate -as gate
+miter -equiv -flatten -make_assert -make_outputs gold gate miter
+sat -verify -prove-asserts -show-ports miter
+
+#design -load read
+#hierarchy -top cliffordwolf_freduce
+#prep
+#design -save gold
+#proc; opt; freduce; opt
+#show
+#muxpack
+#opt
+#stat
+#select -assert-count 0 t:$mux
+#select -assert-count 1 t:$pmux
+#design -stash gate
+#design -import gold -as gold
+#design -import gate -as gate
+#miter -equiv -flatten -make_assert -make_outputs gold gate miter
+#sat -verify -prove-asserts -show-ports miter
+
+design -load read
+hierarchy -top case_nonexclusive_select
+prep
+design -save gold
+muxpack
+opt
+stat
+select -assert-count 0 t:$mux
+select -assert-count 2 t:$pmux
+design -stash gate
+design -import gold -as gold
+design -import gate -as gate
+miter -equiv -flatten -make_assert -make_outputs gold gate miter
+sat -verify -prove-asserts -show-ports miter
+
+design -load read
+hierarchy -top case_nonoverlap
+#prep # Do not prep otherwise $pmux's overlapping entry will get removed
+proc
+design -save gold
+opt -fast -mux_undef
+select -assert-count 2 t:$pmux
+muxpack
+opt
+stat
+select -assert-count 0 t:$mux
+select -assert-count 1 t:$pmux
+design -stash gate
+design -import gold -as gold
+design -import gate -as gate
+miter -equiv -flatten -make_assert -make_outputs gold gate miter
+sat -verify -prove-asserts -show-ports miter
+
+design -load read
+hierarchy -top case_overlap
+#prep # Do not prep otherwise $pmux's overlapping entry will get removed
+proc
+design -save gold
+opt -fast -mux_undef
+select -assert-count 2 t:$pmux
+muxpack
+opt
+stat
+select -assert-count 0 t:$mux
+select -assert-count 2 t:$pmux
+design -stash gate
+design -import gold -as gold
+design -import gate -as gate
+miter -equiv -flatten -make_assert -make_outputs gold gate miter
+sat -verify -prove-asserts -show-ports miter
+
+design -load read
+hierarchy -top case_overlap2
+#prep # Do not prep otherwise $pmux's overlapping entry will get removed
+proc
+design -save gold
+opt -fast -mux_undef
+select -assert-count 2 t:$pmux
+muxpack
+opt
+stat
+select -assert-count 0 t:$mux
+select -assert-count 2 t:$pmux
+design -stash gate
+design -import gold -as gold
+design -import gate -as gate
+miter -equiv -flatten -make_assert -make_outputs gold gate miter
+sat -verify -prove-asserts -show-ports miter