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

5 files changed, 298 insertions, 1 deletions

diff --git a/tests/simple/generate.v b/tests/simple/generate.v
index 3c55682cb..0e353ad9b 100644
--- a/tests/simple/generate.v
+++ b/tests/simple/generate.v
@@ -148,3 +148,14 @@ generate
 endgenerate
 assign out = steps[WIDTH].outer[0].val;
 endmodule
+
+// ------------------------------------------
+
+module gen_test6(output [3:0] o);
+generate
+    genvar i;
+    for (i = 3; i >= 0; i = i-1) begin
+        assign o[i] = 1'b0;
+    end
+endgenerate
+endmodule
diff --git a/tests/various/muxcover.ys b/tests/various/muxcover.ys
index 7ac460f13..8ef619b46 100644
--- a/tests/various/muxcover.ys
+++ b/tests/various/muxcover.ys
@@ -13,7 +13,7 @@ read_verilog -formal <<EOT
 EOT
 
 
-## Examle usage for "pmuxtree" and "muxcover"
+## Example usage for "pmuxtree" and "muxcover"
 
 proc
 pmuxtree
@@ -49,3 +49,142 @@ hierarchy -top equiv
 equiv_simple -undef
 equiv_status -assert
 
+## Partial matching MUX4
+
+design -reset
+read_verilog -formal <<EOT
+module mux_if_bal_3_1 #(parameter N=3, parameter W=1) (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] == 1'b0)
+     if (s[1] == 1'b0)
+      o <= i[0*W+:W];
+     else
+      o <= i[1*W+:W];
+    else
+     if (s[1] == 1'b0)
+      o <= i[2*W+:W];
+end
+endmodule
+EOT
+prep
+design -save gold
+
+techmap
+muxcover -mux4=150
+select -assert-count 0 t:$_MUX_
+select -assert-count 1 t:$_MUX4_
+select -assert-count 0 t:$_MUX8_
+select -assert-count 0 t:$_MUX16_
+techmap -map +/simcells.v t:$_MUX4_
+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
+
+## Partial matching MUX8
+
+design -reset
+read_verilog -formal <<EOT
+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 @* begin
+    o <= {{W{{1'bx}}}};
+    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];
+end
+endmodule
+EOT
+prep
+design -save gold
+
+techmap
+muxcover -mux4=150 -mux8=200
+clean
+opt_expr -mux_bool
+select -assert-count 0 t:$_MUX_
+select -assert-count 0 t:$_MUX4_
+select -assert-count 1 t:$_MUX8_
+select -assert-count 0 t:$_MUX16_
+techmap -map +/simcells.v t:$_MUX8_
+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
+
+## Partial matching MUX16
+
+design -reset
+read_verilog -formal <<EOT
+module mux_if_bal_9_1 #(parameter N=9, parameter W=1) (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] == 1'b0)
+     if (s[1] == 1'b0)
+      if (s[2] == 1'b0)
+       if (s[3] == 1'b0)
+        o <= i[0*W+:W];
+       else
+        o <= i[1*W+:W];
+      else
+       if (s[3] == 1'b0)
+        o <= i[2*W+:W];
+       else
+        o <= i[3*W+:W];
+     else
+      if (s[2] == 1'b0)
+       if (s[3] == 1'b0)
+        o <= i[4*W+:W];
+       else
+        o <= i[5*W+:W];
+      else
+       if (s[3] == 1'b0)
+        o <= i[6*W+:W];
+       else
+        o <= i[7*W+:W];
+    else
+     if (s[1] == 1'b0)
+      if (s[2] == 1'b0)
+       if (s[3] == 1'b0)
+        o <= i[8*W+:W];
+end
+endmodule
+EOT
+prep
+design -save gold
+
+techmap
+muxcover -mux4=150 -mux8=200 -mux16=250
+clean
+opt_expr -mux_bool
+select -assert-count 0 t:$_MUX_
+select -assert-count 0 t:$_MUX4_
+select -assert-count 0 t:$_MUX8_
+select -assert-count 1 t:$_MUX16_
+techmap -map +/simcells.v t:$_MUX16_
+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..604c2c976
--- /dev/null
+++ b/tests/various/shregmap.v
@@ -0,0 +1,48 @@
+module shregmap_static_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
+
+module shregmap_variable_test(input i, clk, input [1:0] l1, l2, 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[l2], shift1[l1]};
+endmodule
+
+module $__XILINX_SHREG_(input C, D, input [1:0] L, output Q);
+parameter CLKPOL = 1;
+parameter ENPOL = 1;
+parameter DEPTH = 1;
+parameter [DEPTH-1:0] INIT = {DEPTH{1'b0}};
+reg [DEPTH-1:0] r = INIT;
+wire clk = C ^ CLKPOL;
+always @(posedge C)
+    r <= { r[DEPTH-2:0], D };
+assign Q = r[L];
+endmodule
diff --git a/tests/various/shregmap.ys b/tests/various/shregmap.ys
new file mode 100644
index 000000000..d644a88aa
--- /dev/null
+++ b/tests/various/shregmap.ys
@@ -0,0 +1,66 @@
+read_verilog shregmap.v
+design -save read
+
+design -copy-to model $__SHREG_DFF_P_
+hierarchy -top shregmap_static_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
+
+##########
+
+design -load read
+design -copy-to model $__XILINX_SHREG_
+hierarchy -top shregmap_variable_test
+prep
+design -save gold
+
+simplemap t:$dff t:$dffe
+shregmap -tech xilinx
+
+stat
+# show -width
+write_verilog -noexpr -norename
+select -assert-count 1 t:$_DFF_P_
+select -assert-count 2 t:$__XILINX_SHREG_
+
+design -stash gate
+
+design -import gold -as gold
+design -import gate -as gate
+design -copy-from model -as $__XILINX_SHREG_ \$__XILINX_SHREG_
+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
diff --git a/tests/various/signext.ys b/tests/various/signext.ys
new file mode 100644
index 000000000..0c8d671e7
--- /dev/null
+++ b/tests/various/signext.ys
@@ -0,0 +1,33 @@
+
+read_verilog -formal <<EOT
+module gate(input clk, output [32:0] o, p, q, r, s, t, u);
+assign o = 'bx;
+assign p = 1'bx;
+assign q = 'bz;
+assign r = 1'bz;
+assign s = 1'b0;
+assign t = 'b1;
+assign u = -'sb1;
+endmodule
+EOT
+
+proc
+
+## Equivalence checking
+
+read_verilog -formal <<EOT
+module gold(input clk, output [32:0] o, p, q, r, s, t, u);
+assign o = {33{1'bx}};
+assign p = {{32{1'b0}}, 1'bx};
+assign q = {33{1'bz}};
+assign r = {{32{1'b0}}, 1'bz};
+assign s = {33{1'b0}};
+assign t = {{32{1'b0}}, 1'b1};
+assign u = {33{1'b1}};
+endmodule
+EOT
+
+proc
+
+miter -equiv -flatten -make_assert -make_outputs gold gate miter
+sat -verify -prove-asserts -show-ports -enable_undef miter