From: Eddie Hung <eddie@fpgeh.com>
Date: Fri, 13 Sep 2019 23:41:10 +0000 (-0700)
Subject: Add counter-example from @cliffordwolf
X-Git-Tag: working-ls180~1058^2~1
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a2eee9ebefc6e8089c815b4355bc64d1ac3396b5;p=yosys.git

Add counter-example from @cliffordwolf
---

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