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

8 files changed, 453 insertions, 2 deletions

diff --git a/tests/simple_abc9/abc.box b/tests/simple_abc9/abc.box
new file mode 100644
index 000000000..a8801d807
--- /dev/null
+++ b/tests/simple_abc9/abc.box
@@ -0,0 +1,2 @@
+MUXF8 1 0 3 1
+1 1 1
diff --git a/tests/simple_abc9/abc9.v b/tests/simple_abc9/abc9.v
index f37d975ff..2752ff8cc 100644
--- a/tests/simple_abc9/abc9.v
+++ b/tests/simple_abc9/abc9.v
@@ -142,3 +142,111 @@ assign b = ~a;
 (* keep *) reg d;
 always @* d <= &c;
 endmodule
+
+// Citation: https://github.com/alexforencich/verilog-ethernet
+module abc9_test021(clk, rst, s_eth_hdr_valid, s_eth_hdr_ready, s_eth_dest_mac, s_eth_src_mac, s_eth_type, s_eth_payload_axis_tdata, s_eth_payload_axis_tkeep, s_eth_payload_axis_tvalid, s_eth_payload_axis_tready, s_eth_payload_axis_tlast, s_eth_payload_axis_tid, s_eth_payload_axis_tdest, s_eth_payload_axis_tuser, m_eth_hdr_valid, m_eth_hdr_ready, m_eth_dest_mac, m_eth_src_mac, m_eth_type, m_eth_payload_axis_tdata, m_eth_payload_axis_tkeep, m_eth_payload_axis_tvalid, m_eth_payload_axis_tready, m_eth_payload_axis_tlast, m_eth_payload_axis_tid, m_eth_payload_axis_tdest, m_eth_payload_axis_tuser);
+  input clk;
+  output [47:0] m_eth_dest_mac;
+  input m_eth_hdr_ready;
+  output m_eth_hdr_valid;
+  output [7:0] m_eth_payload_axis_tdata;
+  output [7:0] m_eth_payload_axis_tdest;
+  output [7:0] m_eth_payload_axis_tid;
+  output m_eth_payload_axis_tkeep;
+  output m_eth_payload_axis_tlast;
+  input m_eth_payload_axis_tready;
+  output m_eth_payload_axis_tuser;
+  output m_eth_payload_axis_tvalid;
+  output [47:0] m_eth_src_mac;
+  output [15:0] m_eth_type;
+  input rst;
+  input [191:0] s_eth_dest_mac;
+  output [3:0] s_eth_hdr_ready;
+  input [3:0] s_eth_hdr_valid;
+  input [31:0] s_eth_payload_axis_tdata;
+  input [31:0] s_eth_payload_axis_tdest;
+  input [31:0] s_eth_payload_axis_tid;
+  input [3:0] s_eth_payload_axis_tkeep;
+  input [3:0] s_eth_payload_axis_tlast;
+  output [3:0] s_eth_payload_axis_tready;
+  input [3:0] s_eth_payload_axis_tuser;
+  input [3:0] s_eth_payload_axis_tvalid;
+  input [191:0] s_eth_src_mac;
+  input [63:0] s_eth_type;
+  (* keep *)
+  wire [0:0] grant, request;
+  wire a;
+  not u0 (
+    a,
+    grant[0]
+  );
+  and u1  (
+    request[0],
+    s_eth_hdr_valid[0],
+    a
+  );
+  (* keep *)
+  MUXF8 u2  (
+    .I0(1'bx),
+    .I1(1'bx),
+    .O(o),
+    .S(1'bx)
+  );
+  arbiter  arb_inst (
+    .acknowledge(acknowledge),
+    .clk(clk),
+    .grant(grant),
+    .grant_encoded(grant_encoded),
+    .grant_valid(grant_valid),
+    .request(request),
+    .rst(rst)
+  );
+endmodule
+
+module arbiter (clk, rst, request, acknowledge, grant, grant_valid, grant_encoded);
+  input [3:0] acknowledge;
+  input clk;
+  output [3:0] grant;
+  output [1:0] grant_encoded;
+  output grant_valid;
+  input [3:0] request;
+  input rst;
+endmodule
+
+(* abc_box_id=1 *)
+module MUXF8(input I0, I1, S, output O);
+endmodule
+
+// Citation: https://github.com/alexforencich/verilog-ethernet
+// TODO: yosys -p "synth_xilinx -abc9 -top abc9_test022" abc9.v -q
+// returns before b4321a31
+//   Warning: Wire abc9_test022.\m_eth_payload_axis_tkeep [7] is used but has no
+//   driver.
+//   Warning: Wire abc9_test022.\m_eth_payload_axis_tkeep [3] is used but has no
+//   driver.
+module abc9_test022
+(
+    input  wire        clk,
+    input  wire        i,
+    output wire [7:0]  m_eth_payload_axis_tkeep
+);
+    reg [7:0]  m_eth_payload_axis_tkeep_reg = 8'd0;
+    assign m_eth_payload_axis_tkeep = m_eth_payload_axis_tkeep_reg;
+    always @(posedge clk)
+        m_eth_payload_axis_tkeep_reg <= i ? 8'hff : 8'h0f;
+endmodule
+
+// Citation: https://github.com/riscv/riscv-bitmanip
+// TODO: yosys -p "synth_xilinx -abc9 -top abc9_test023" abc9.v -q
+// returns before 14233843
+//   Warning: Wire abc9_test023.\dout [1] is used but has no driver.
+module abc9_test023 #(
+	parameter integer N = 2,
+	parameter integer M = 2
+) (
+	input [7:0] din,
+	output [M-1:0] dout
+);
+	wire [2*M-1:0] mask = {M{1'b1}};
+	assign dout = (mask << din[N-1:0]) >> M;
+endmodule
diff --git a/tests/simple_abc9/run-test.sh b/tests/simple_abc9/run-test.sh
index 97f284378..4935d41ad 100755
--- a/tests/simple_abc9/run-test.sh
+++ b/tests/simple_abc9/run-test.sh
@@ -19,4 +19,4 @@ fi
 
 cp ../simple/*.v .
 DOLLAR='?'
-exec ${MAKE:-make} -f ../tools/autotest.mk $seed *.v EXTRA_FLAGS="-p 'hierarchy; synth -run coarse; techmap; opt -full; abc9 -lut 4; stat; check -assert; select -assert-none t:${DOLLAR}_NOT_ t:${DOLLAR}_AND_ %%'"
+exec ${MAKE:-make} -f ../tools/autotest.mk $seed *.v EXTRA_FLAGS="-p 'hierarchy; synth -run coarse; opt -full; techmap; abc9 -lut 4 -box ../abc.box; stat; check -assert; select -assert-none t:${DOLLAR}_NOT_ t:${DOLLAR}_AND_ %%'"
diff --git a/tests/tools/autotest.sh b/tests/tools/autotest.sh
index c394b9817..23964a751 100755
--- a/tests/tools/autotest.sh
+++ b/tests/tools/autotest.sh
@@ -143,6 +143,7 @@ do
 		fn=$(basename $fn)
 		bn=$(basename $bn)
 
+		rm -f ${bn}_ref.fir
 		if [[ "$ext" == "v" ]]; then
 			egrep -v '^\s*`timescale' ../$fn > ${bn}_ref.${ext}
 		elif [[ "$ext" == "aig" ]] || [[ "$ext" == "aag" ]]; then
@@ -150,7 +151,6 @@ do
 		else
 			cp ../${fn} ${bn}_ref.${ext}
 		fi
-		rm -f ${bn}_ref.fir
 
 		if [ ! -f ../${bn}_tb.v ]; then
 			"$toolsdir"/../../yosys -f "$frontend $include_opts" -b "test_autotb $autotb_opts" -o ${bn}_tb.v ${bn}_ref.v
diff --git a/tests/various/muxpack.v b/tests/various/muxpack.v
new file mode 100644
index 000000000..f1bd5ea8e
--- /dev/null
+++ b/tests/various/muxpack.v
@@ -0,0 +1,138 @@
+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
diff --git a/tests/various/muxpack.ys b/tests/various/muxpack.ys
new file mode 100644
index 000000000..9ea743b9f
--- /dev/null
+++ b/tests/various/muxpack.ys
@@ -0,0 +1,150 @@
+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
+
+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
diff --git a/tests/various/shregmap.v b/tests/various/shregmap.v
new file mode 100644
index 000000000..56e05c2c0
--- /dev/null
+++ b/tests/various/shregmap.v
@@ -0,0 +1,22 @@
+module shregmap_test(input i, clk, output [1:0] q);
+reg head = 1'b0;
+reg [3:0] shift1 = 4'b0000;
+reg [3:0] shift2 = 4'b0000;
+
+always @(posedge clk) begin
+    head <= i;
+    shift1 <= {shift1[2:0], head};
+    shift2 <= {shift2[2:0], head};
+end
+
+assign q = {shift2[3], shift1[3]};
+endmodule
+
+module $__SHREG_DFF_P_(input C, D, output Q);
+parameter DEPTH = 1;
+parameter [DEPTH-1:0] INIT = {DEPTH{1'b0}};
+reg [DEPTH-1:0] r = INIT;
+always @(posedge C) 
+    r <= { r[DEPTH-2:0], D };
+assign Q = r[DEPTH-1];
+endmodule
diff --git a/tests/various/shregmap.ys b/tests/various/shregmap.ys
new file mode 100644
index 000000000..ca7f47015
--- /dev/null
+++ b/tests/various/shregmap.ys
@@ -0,0 +1,31 @@
+read_verilog shregmap.v
+design -copy-to model $__SHREG_DFF_P_
+hierarchy -top shregmap_test
+prep
+design -save gold
+
+techmap
+shregmap -init
+
+opt
+
+stat
+# show -width
+select -assert-count 1 t:$_DFF_P_
+select -assert-count 2 t:$__SHREG_DFF_P_
+
+design -stash gate
+
+design -import gold -as gold
+design -import gate -as gate
+design -copy-from model -as $__SHREG_DFF_P_ \$__SHREG_DFF_P_
+prep
+
+miter -equiv -flatten -make_assert -make_outputs gold gate miter
+sat -verify -prove-asserts -show-ports -seq 5 miter
+
+design -load gold
+stat
+
+design -load gate
+stat