Add counter-example from @cliffordwolf

This commit is contained in:
Eddie Hung 2019-09-13 16:41:10 -07:00
parent 14d72c39c3
commit a2eee9ebef
1 changed files with 24 additions and 0 deletions

View File

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