From 45c2a5f87694a83e0cf96477ede02567a93b32a8 Mon Sep 17 00:00:00 2001
From: Eddie Hung <eddie@fpgeh.com>
Date: Wed, 12 Jun 2019 08:34:06 -0700
Subject: Add shregmap -tech xilinx test

---
 tests/various/shregmap.v  | 28 +++++++++++++++++++++++++++-
 tests/various/shregmap.ys | 37 ++++++++++++++++++++++++++++++++++++-
 2 files changed, 63 insertions(+), 2 deletions(-)

(limited to 'tests')

diff --git a/tests/various/shregmap.v b/tests/various/shregmap.v
index 56e05c2c0..604c2c976 100644
--- a/tests/various/shregmap.v
+++ b/tests/various/shregmap.v
@@ -1,4 +1,4 @@
-module shregmap_test(input i, clk, output [1:0] q);
+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;
@@ -20,3 +20,29 @@ 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
index ca7f47015..d644a88aa 100644
--- a/tests/various/shregmap.ys
+++ b/tests/various/shregmap.ys
@@ -1,6 +1,8 @@
 read_verilog shregmap.v
+design -save read
+
 design -copy-to model $__SHREG_DFF_P_
-hierarchy -top shregmap_test
+hierarchy -top shregmap_static_test
 prep
 design -save gold
 
@@ -29,3 +31,36 @@ 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
-- 
cgit v1.2.3


From b98276fa61be7a1c589d6dac661d31982cfab16b Mon Sep 17 00:00:00 2001
From: Eddie Hung <eddie@fpgeh.com>
Date: Thu, 20 Jun 2019 10:10:43 -0700
Subject: Add test

---
 tests/various/signext.ys | 24 ++++++++++++++++++++++++
 1 file changed, 24 insertions(+)
 create mode 100644 tests/various/signext.ys

(limited to 'tests')

diff --git a/tests/various/signext.ys b/tests/various/signext.ys
new file mode 100644
index 000000000..26dab13a6
--- /dev/null
+++ b/tests/various/signext.ys
@@ -0,0 +1,24 @@
+
+read_verilog -formal <<EOT
+module gate(input clk, output [1:0] o);
+assign o = 1'bx;
+endmodule
+EOT
+
+
+## Example usage for "pmuxtree" and "muxcover"
+
+proc
+
+## Equivalence checking
+
+read_verilog -formal <<EOT
+module gold(input clk, output [1:0] o);
+assign o = 2'bxx;
+endmodule
+EOT
+
+proc
+
+miter -equiv -flatten -make_assert -make_outputs gold gate miter
+sat -verify -prove-asserts -show-ports -enable_undef miter
-- 
cgit v1.2.3


From b77322034c9234a8c24c6f53ed028fe29737b6b4 Mon Sep 17 00:00:00 2001
From: Eddie Hung <eddie@fpgeh.com>
Date: Thu, 20 Jun 2019 10:15:04 -0700
Subject: Remove leftover comment

---
 tests/various/signext.ys | 3 ---
 1 file changed, 3 deletions(-)

(limited to 'tests')

diff --git a/tests/various/signext.ys b/tests/various/signext.ys
index 26dab13a6..ae44a0e06 100644
--- a/tests/various/signext.ys
+++ b/tests/various/signext.ys
@@ -5,9 +5,6 @@ assign o = 1'bx;
 endmodule
 EOT
 
-
-## Example usage for "pmuxtree" and "muxcover"
-
 proc
 
 ## Equivalence checking
-- 
cgit v1.2.3


From d0bbf9e4d4a508179b55a0cc7793d984f3318f7c Mon Sep 17 00:00:00 2001
From: Eddie Hung <eddie@fpgeh.com>
Date: Thu, 20 Jun 2019 12:43:59 -0700
Subject: Extend sign extension tests

---
 tests/various/signext.ys | 20 ++++++++++++++++----
 1 file changed, 16 insertions(+), 4 deletions(-)

(limited to 'tests')

diff --git a/tests/various/signext.ys b/tests/various/signext.ys
index ae44a0e06..0c8d671e7 100644
--- a/tests/various/signext.ys
+++ b/tests/various/signext.ys
@@ -1,7 +1,13 @@
 
 read_verilog -formal <<EOT
-module gate(input clk, output [1:0] o);
-assign o = 1'bx;
+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
 
@@ -10,8 +16,14 @@ proc
 ## Equivalence checking
 
 read_verilog -formal <<EOT
-module gold(input clk, output [1:0] o);
-assign o = 2'bxx;
+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
 
-- 
cgit v1.2.3


From c20adc52638b0f3ba3b1c39e5286ae92e901005d Mon Sep 17 00:00:00 2001
From: Eddie Hung <eddie@fpgeh.com>
Date: Thu, 20 Jun 2019 16:07:22 -0700
Subject: Add test

---
 tests/simple/generate.v | 11 +++++++++++
 1 file changed, 11 insertions(+)

(limited to 'tests')

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
-- 
cgit v1.2.3


From 75375a3fbce622b5c4cb6f4464379bb0e66a1107 Mon Sep 17 00:00:00 2001
From: Eddie Hung <eddie@fpgeh.com>
Date: Wed, 19 Jun 2019 10:07:34 -0700
Subject: Add test

---
 tests/various/muxcover.ys | 137 +++++++++++++++++++++++++++++++++++++++++++++-
 1 file changed, 136 insertions(+), 1 deletion(-)

(limited to 'tests')

diff --git a/tests/various/muxcover.ys b/tests/various/muxcover.ys
index 7ac460f13..d55a35b8c 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,138 @@ 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
+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
+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
+
-- 
cgit v1.2.3


From 844c42cef8c7c04fa67653f998ccab0e90532d28 Mon Sep 17 00:00:00 2001
From: Eddie Hung <eddie@fpgeh.com>
Date: Wed, 19 Jun 2019 10:15:41 -0700
Subject: Missing a `clean` and `opt_expr -mux_bool` in test

---
 tests/various/muxcover.ys | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'tests')

diff --git a/tests/various/muxcover.ys b/tests/various/muxcover.ys
index d55a35b8c..8ef619b46 100644
--- a/tests/various/muxcover.ys
+++ b/tests/various/muxcover.ys
@@ -115,6 +115,8 @@ 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_
@@ -171,6 +173,8 @@ 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_
-- 
cgit v1.2.3