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 <> (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 <