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')

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')

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')

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