From ef0681ea4ca0b34689cbf14d5a4478e2785600d9 Mon Sep 17 00:00:00 2001
From: Eddie Hung <eddie@fpgeh.com>
Date: Thu, 5 Sep 2019 08:43:22 -0700
Subject: simple/peepopt.v tests to various/peepopt.ys with equiv_opt & select

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

(limited to 'tests/various')

diff --git a/tests/various/peepopt.ys b/tests/various/peepopt.ys
new file mode 100644
index 000000000..91db22423
--- /dev/null
+++ b/tests/various/peepopt.ys
@@ -0,0 +1,63 @@
+read_verilog <<EOT
+module peepopt_shiftmul_0 #(parameter N=3, parameter W=3) (input [N*W-1:0] i, input [$clog2(N)-1:0] s, output [W-1:0] o);
+assign o = i[s*W+:W];
+endmodule
+EOT
+
+prep -nokeepdc
+equiv_opt peepopt
+design -load postopt
+clean
+select -assert-count 1 t:$shiftx
+select -assert-count 0 t:$shiftx t:* %D
+
+####################
+
+design -reset
+read_verilog <<EOT
+module peepopt_shiftmul_1 (output [7:0] y, input [2:0] w);
+assign y = 1'b1 >> (w * (3'b110));
+endmodule
+EOT
+
+prep -nokeepdc
+equiv_opt peepopt
+design -load postopt
+clean
+select -assert-count 1 t:$shr
+select -assert-count 1 t:$mul
+select -assert-count 0 t:$shr t:$mul %% t:* %D
+
+####################
+
+design -reset
+read_verilog <<EOT
+module peepopt_muldiv_0(input [1:0] i, output [1:0] o);
+wire [3:0] t;
+assign t = i * 3;
+assign o = t / 3;
+endmodule
+EOT
+
+prep -nokeepdc
+equiv_opt peepopt
+design -load postopt
+clean
+select -assert-count 0 t:*
+
+####################
+
+design -reset
+read_verilog <<EOT
+module peepopt_dffmuxext_signed(input clk, ce, input signed [1:0] i, output reg signed [3:0] o);
+    always @(posedge clk) if (ce) o <= i;
+endmodule
+EOT
+
+prep -nokeepdc
+equiv_opt peepopt
+design -load postopt
+clean
+select -assert-count 1 t:$dff r:WIDTH=2 %i
+select -assert-count 1 t:$mux r:WIDTH=2 %i
+select -assert-count 0 t:$dff t:$mux %% t:* %D
-- 
cgit v1.2.3


From 51b559af2cc60226d85880efc3705f0860ffaed6 Mon Sep 17 00:00:00 2001
From: Eddie Hung <eddie@fpgeh.com>
Date: Fri, 6 Sep 2019 22:48:04 -0700
Subject: Usee equiv_opt -assert

---
 tests/various/peepopt.ys | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'tests/various')

diff --git a/tests/various/peepopt.ys b/tests/various/peepopt.ys
index 91db22423..a476133a2 100644
--- a/tests/various/peepopt.ys
+++ b/tests/various/peepopt.ys
@@ -5,7 +5,7 @@ endmodule
 EOT
 
 prep -nokeepdc
-equiv_opt peepopt
+equiv_opt -assert peepopt
 design -load postopt
 clean
 select -assert-count 1 t:$shiftx
@@ -21,7 +21,7 @@ endmodule
 EOT
 
 prep -nokeepdc
-equiv_opt peepopt
+equiv_opt -assert peepopt
 design -load postopt
 clean
 select -assert-count 1 t:$shr
@@ -40,7 +40,7 @@ endmodule
 EOT
 
 prep -nokeepdc
-equiv_opt peepopt
+equiv_opt -assert peepopt
 design -load postopt
 clean
 select -assert-count 0 t:*
-- 
cgit v1.2.3


From e2c2d784c8217e4bcf29fb6b156b6a8285036b80 Mon Sep 17 00:00:00 2001
From: Eddie Hung <eddie@fpgeh.com>
Date: Fri, 6 Sep 2019 22:48:23 -0700
Subject: Make one check $shift(x)? only; change testcase to be 8b

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

(limited to 'tests/various')

diff --git a/tests/various/peepopt.ys b/tests/various/peepopt.ys
index a476133a2..dcf3cacbd 100644
--- a/tests/various/peepopt.ys
+++ b/tests/various/peepopt.ys
@@ -16,7 +16,7 @@ select -assert-count 0 t:$shiftx t:* %D
 design -reset
 read_verilog <<EOT
 module peepopt_shiftmul_1 (output [7:0] y, input [2:0] w);
-assign y = 1'b1 >> (w * (3'b110));
+assign y = 1'b1 >> (w * (8'b110));
 endmodule
 EOT
 
@@ -25,7 +25,7 @@ equiv_opt -assert peepopt
 design -load postopt
 clean
 select -assert-count 1 t:$shr
-select -assert-count 1 t:$mul
+select -assert-count 0 t:$mul
 select -assert-count 0 t:$shr t:$mul %% t:* %D
 
 ####################
-- 
cgit v1.2.3


From 97e1520b13231c8170cec73774eee7a22c5dc065 Mon Sep 17 00:00:00 2001
From: Eddie Hung <eddie@fpgeh.com>
Date: Fri, 6 Sep 2019 22:50:03 -0700
Subject: Missing equiv_opt -assert

---
 tests/various/peepopt.ys | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tests/various')

diff --git a/tests/various/peepopt.ys b/tests/various/peepopt.ys
index dcf3cacbd..33555264d 100644
--- a/tests/various/peepopt.ys
+++ b/tests/various/peepopt.ys
@@ -55,7 +55,7 @@ endmodule
 EOT
 
 prep -nokeepdc
-equiv_opt peepopt
+equiv_opt -assert peepopt
 design -load postopt
 clean
 select -assert-count 1 t:$dff r:WIDTH=2 %i
-- 
cgit v1.2.3


From 580faae8ad608981ef6ef6a99ca6b771dc0368ae Mon Sep 17 00:00:00 2001
From: Eddie Hung <eddie@fpgeh.com>
Date: Wed, 11 Sep 2019 00:07:17 -0700
Subject: Add unsigned case

---
 tests/various/peepopt.ys | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)

(limited to 'tests/various')

diff --git a/tests/various/peepopt.ys b/tests/various/peepopt.ys
index 33555264d..e930015a4 100644
--- a/tests/various/peepopt.ys
+++ b/tests/various/peepopt.ys
@@ -47,6 +47,23 @@ select -assert-count 0 t:*
 
 ####################
 
+design -reset
+read_verilog <<EOT
+module peepopt_dffmuxext_unsigned(input clk, ce, input [1:0] i, output reg [3:0] o);
+    always @(posedge clk) if (ce) o <= i;
+endmodule
+EOT
+
+prep -nokeepdc
+equiv_opt -assert peepopt
+design -load postopt
+clean
+select -assert-count 1 t:$dff r:WIDTH=2 %i
+select -assert-count 1 t:$mux r:WIDTH=2 %i
+select -assert-count 0 t:$dff t:$mux %% t:* %D
+
+####################
+
 design -reset
 read_verilog <<EOT
 module peepopt_dffmuxext_signed(input clk, ce, input signed [1:0] i, output reg signed [3:0] o);
-- 
cgit v1.2.3


From 3a8582081e1eda7e4a41ec1ec7292e7d247559da Mon Sep 17 00:00:00 2001
From: Eddie Hung <eddie@fpgeh.com>
Date: Wed, 11 Sep 2019 00:14:06 -0700
Subject: proc instead of prep

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

(limited to 'tests/various')

diff --git a/tests/various/peepopt.ys b/tests/various/peepopt.ys
index e930015a4..2a660d5c9 100644
--- a/tests/various/peepopt.ys
+++ b/tests/various/peepopt.ys
@@ -54,7 +54,7 @@ module peepopt_dffmuxext_unsigned(input clk, ce, input [1:0] i, output reg [3:0]
 endmodule
 EOT
 
-prep -nokeepdc
+proc
 equiv_opt -assert peepopt
 design -load postopt
 clean
@@ -71,7 +71,7 @@ module peepopt_dffmuxext_signed(input clk, ce, input signed [1:0] i, output reg
 endmodule
 EOT
 
-prep -nokeepdc
+proc
 equiv_opt -assert peepopt
 design -load postopt
 clean
-- 
cgit v1.2.3


From f46ef47893b4d2cb01fc5914fe0ee89d206f686f Mon Sep 17 00:00:00 2001
From: Eddie Hung <eddie@fpgeh.com>
Date: Wed, 11 Sep 2019 13:22:41 -0700
Subject: Add more tests

---
 tests/various/peepopt.ys | 32 ++++++++++++++++++++++++++++++++
 1 file changed, 32 insertions(+)

(limited to 'tests/various')

diff --git a/tests/various/peepopt.ys b/tests/various/peepopt.ys
index 2a660d5c9..8dce679ff 100644
--- a/tests/various/peepopt.ys
+++ b/tests/various/peepopt.ys
@@ -78,3 +78,35 @@ clean
 select -assert-count 1 t:$dff r:WIDTH=2 %i
 select -assert-count 1 t:$mux r:WIDTH=2 %i
 select -assert-count 0 t:$dff t:$mux %% t:* %D
+
+###################
+
+design -reset
+read_verilog <<EOT
+module peepopt_dffmuxext_const(input clk, ce, input [1:0] i, output reg [5:0] o);
+    always @(posedge clk) if (ce) o <= {1'b0, i[1], 2'b1x, i[0], 1'bz};
+endmodule
+EOT
+
+proc
+equiv_opt -assert peepopt
+design -load postopt
+select -assert-count 1 t:$dff r:WIDTH=2 %i
+select -assert-count 1 t:$mux r:WIDTH=2 %i
+select -assert-count 0 t:$dff t:$mux %% t:* %D
+
+###################
+
+design -reset
+read_verilog <<EOT
+module peepopt_dffmuxext_const_init(input clk, ce, input [1:0] i, (* init=6'b0x00x1 *) output reg [5:0] o);
+    always @(posedge clk) if (ce) o <= {1'b0, i[1], 2'b1x, i[0], 1'bz};
+endmodule
+EOT
+
+proc
+equiv_opt -assert peepopt
+design -load postopt
+select -assert-count 1 t:$dff r:WIDTH=5 %i
+select -assert-count 1 t:$mux r:WIDTH=5 %i
+select -assert-count 0 t:$dff t:$mux %% t:* %D
-- 
cgit v1.2.3


From bdb5e0f29c3e913fb4e701317105363064b9a7d3 Mon Sep 17 00:00:00 2001
From: Eddie Hung <eddie@fpgeh.com>
Date: Wed, 11 Sep 2019 13:36:37 -0700
Subject: Cope with presence of reset muxes too

---
 tests/various/peepopt.ys | 39 +++++++++++++++++++++++++++++++++++++++
 1 file changed, 39 insertions(+)

(limited to 'tests/various')

diff --git a/tests/various/peepopt.ys b/tests/various/peepopt.ys
index 8dce679ff..886c8cd9d 100644
--- a/tests/various/peepopt.ys
+++ b/tests/various/peepopt.ys
@@ -110,3 +110,42 @@ design -load postopt
 select -assert-count 1 t:$dff r:WIDTH=5 %i
 select -assert-count 1 t:$mux r:WIDTH=5 %i
 select -assert-count 0 t:$dff t:$mux %% t:* %D
+
+####################
+
+design -reset
+read_verilog <<EOT
+module peepopt_dffmuxext_unsigned_rst(input clk, ce, rst, input [1:0] i, output reg [3:0] o);
+    always @(posedge clk) if (rst) o <= 0; else if (ce) o <= i;
+endmodule
+EOT
+
+proc
+equiv_opt -assert peepopt
+design -load postopt
+wreduce
+select -assert-count 1 t:$dff r:WIDTH=2 %i
+select -assert-count 2 t:$mux
+select -assert-count 2 t:$mux r:WIDTH=2 %i
+select -assert-count 0 t:$dff t:$mux %% t:* %D
+
+####################
+
+design -reset
+read_verilog <<EOT
+module peepopt_dffmuxext_signed_rst(input clk, ce, rstn, input signed [1:0] i, output reg signed [3:0] o);
+    always @(posedge clk) begin
+        if (ce) o <= i;
+        if (!rstn) o <= 4'b1111;
+    end
+endmodule
+EOT
+
+proc
+equiv_opt -assert peepopt
+design -load postopt
+wreduce
+select -assert-count 1 t:$dff r:WIDTH=2 %i
+select -assert-count 2 t:$mux
+select -assert-count 2 t:$mux r:WIDTH=2 %i
+select -assert-count 0 t:$logic_not t:$dff t:$mux %% t:* %D
-- 
cgit v1.2.3


From 14d72c39c385bba3005085815a0d66989a437eff Mon Sep 17 00:00:00 2001
From: Eddie Hung <eddie@fpgeh.com>
Date: Fri, 13 Sep 2019 16:33:18 -0700
Subject: Revert "Make one check $shift(x)? only; change testcase to be 8b"

This reverts commit e2c2d784c8217e4bcf29fb6b156b6a8285036b80.
---
 tests/various/peepopt.ys | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'tests/various')

diff --git a/tests/various/peepopt.ys b/tests/various/peepopt.ys
index 886c8cd9d..abee9cc0a 100644
--- a/tests/various/peepopt.ys
+++ b/tests/various/peepopt.ys
@@ -16,7 +16,7 @@ select -assert-count 0 t:$shiftx t:* %D
 design -reset
 read_verilog <<EOT
 module peepopt_shiftmul_1 (output [7:0] y, input [2:0] w);
-assign y = 1'b1 >> (w * (8'b110));
+assign y = 1'b1 >> (w * (3'b110));
 endmodule
 EOT
 
@@ -25,7 +25,7 @@ equiv_opt -assert peepopt
 design -load postopt
 clean
 select -assert-count 1 t:$shr
-select -assert-count 0 t:$mul
+select -assert-count 1 t:$mul
 select -assert-count 0 t:$shr t:$mul %% t:* %D
 
 ####################
-- 
cgit v1.2.3


From a2eee9ebefc6e8089c815b4355bc64d1ac3396b5 Mon Sep 17 00:00:00 2001
From: Eddie Hung <eddie@fpgeh.com>
Date: Fri, 13 Sep 2019 16:41:10 -0700
Subject: Add counter-example from @cliffordwolf

---
 tests/various/peepopt.ys | 24 ++++++++++++++++++++++++
 1 file changed, 24 insertions(+)

(limited to 'tests/various')

diff --git a/tests/various/peepopt.ys b/tests/various/peepopt.ys
index abee9cc0a..7c1c3b5bc 100644
--- a/tests/various/peepopt.ys
+++ b/tests/various/peepopt.ys
@@ -30,6 +30,30 @@ select -assert-count 0 t:$shr t:$mul %% t:* %D
 
 ####################
 
+design -reset
+read_verilog <<EOT
+module peepopt_shiftmul_2 (input [11:0] D, input [1:0] S, output [11:0] Y);
+	assign Y = D >> (S*3);
+endmodule
+EOT
+
+prep
+design -save gold
+peepopt
+design -stash gate
+
+design -import gold -as gold peepopt_shiftmul_2
+design -import gate -as gate peepopt_shiftmul_2
+
+miter -equiv -make_assert -make_outputs -ignore_gold_x -flatten gold gate miter
+sat -show-public -enable_undef -prove-asserts miter
+select -assert-count 1 t:$shr
+select -assert-count 1 t:$mul
+select -assert-count 0 t:$shr t:$mul %% t:* %D
+exit
+
+####################
+
 design -reset
 read_verilog <<EOT
 module peepopt_muldiv_0(input [1:0] i, output [1:0] o);
-- 
cgit v1.2.3


From f492567c872c1f6bc864fe0a3d86021558f8101e Mon Sep 17 00:00:00 2001
From: Eddie Hung <eddie@fpgeh.com>
Date: Fri, 13 Sep 2019 18:19:07 -0700
Subject: Oops

---
 tests/various/peepopt.ys | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tests/various')

diff --git a/tests/various/peepopt.ys b/tests/various/peepopt.ys
index 7c1c3b5bc..6bca62e2b 100644
--- a/tests/various/peepopt.ys
+++ b/tests/various/peepopt.ys
@@ -47,10 +47,10 @@ design -import gate -as gate peepopt_shiftmul_2
 
 miter -equiv -make_assert -make_outputs -ignore_gold_x -flatten gold gate miter
 sat -show-public -enable_undef -prove-asserts miter
+cd gate
 select -assert-count 1 t:$shr
 select -assert-count 1 t:$mul
 select -assert-count 0 t:$shr t:$mul %% t:* %D
-exit
 
 ####################
 
-- 
cgit v1.2.3