mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-10-30 11:12:29 +00:00
Code Activity

Merge remote-tracking branch 'origin/master' into xc7dsp

Browse source
This commit is contained in:
Eddie Hung 2019-09-18 12:40:21 -07:00
commit f7dbfef792
3 changed files with 44 additions and 15 deletions
Download patch file Download diff file Expand all files Collapse all files

28
tests/various/peepopt.ys
View file

@ -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,31 @@ 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
####################
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
cd gate
select -assert-count 1 t:$shr
select -assert-count 1 t:$mul
select -assert-count 0 t:$shr t:$mul %% t:* %D
####################