forked from YosysHQ/yosys
-
Notifications
You must be signed in to change notification settings - Fork 0
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
peepopt: continue tests, mixed success
- Loading branch information
1 parent
7dad9b3
commit 1f9425f
Showing
1 changed file
with
199 additions
and
2 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,11 +1,208 @@ | ||
# basic pattern: (a * b) / c | ||
read_verilog <<EOT | ||
module top( | ||
input signed [3:0] a, | ||
output signed [7:0] y, | ||
); | ||
wire signed [7:0] mul; | ||
assign mul = a * 4'sd4; | ||
assign mul = a * 4'sd6; | ||
assign y = mul / 8'sd3; | ||
endmodule | ||
EOT | ||
equiv_opt -assert peepopt | ||
design -load postopt | ||
select -assert-count 1 t:$mul | ||
select -assert-count 0 t:$div | ||
design -reset | ||
|
||
read_verilog <<EOT | ||
module top( | ||
input [3:0] a, | ||
output [7:0] y, | ||
); | ||
wire [7:0] mul; | ||
assign mul = a * 4'd6; | ||
assign y = mul / 8'd3; | ||
endmodule | ||
EOT | ||
equiv_opt -assert peepopt | ||
design -load postopt | ||
select -assert-count 1 t:$mul | ||
select -assert-count 0 t:$div | ||
design -reset | ||
|
||
# No transform when b not divisible by c | ||
read_verilog <<EOT | ||
module top( | ||
input signed [3:0] a, | ||
output signed [7:0] y, | ||
); | ||
wire signed [7:0] mul; | ||
assign mul = a * 4'sd3; | ||
assign y = mul / 8'sd2; | ||
endmodule | ||
EOT | ||
equiv_opt peepopt | ||
equiv_opt -assert peepopt | ||
design -load postopt | ||
select -assert-count 1 t:$mul | ||
select -assert-count 1 t:$div | ||
design -reset | ||
|
||
# No transform when product has a second fanout | ||
read_verilog <<EOT | ||
module top( | ||
input signed [3:0] a, | ||
output signed [7:0] y, | ||
output signed [7:0] z, | ||
); | ||
wire signed [7:0] mul; | ||
assign mul = a * 4'sd6; | ||
assign y = mul / 8'sd3; | ||
assign z = mul; | ||
endmodule | ||
EOT | ||
equiv_opt -assert peepopt | ||
design -load postopt | ||
select -assert-count 1 t:$mul | ||
select -assert-count 1 t:$div | ||
design -reset | ||
|
||
# SIGFPE! | ||
# No transform when divisor is 0 | ||
# read_verilog <<EOT | ||
# module top( | ||
# input signed [3:0] a, | ||
# output signed [7:0] y, | ||
# ); | ||
# wire signed [7:0] mul; | ||
# assign mul = a * 4'sd4; | ||
# assign y = mul / 8'sd0; | ||
# endmodule | ||
# EOT | ||
# equiv_opt peepopt | ||
# design -load postopt | ||
# select -assert-count 1 t:$mul | ||
# select -assert-count 1 t:$div | ||
# design -reset | ||
|
||
# No transform when (a*b) output can overflow (divider’s A input signed) | ||
# read_verilog <<EOT | ||
# module top( | ||
# input signed [3:0] a, | ||
# output signed [7:0] y, | ||
# ); | ||
# wire signed [5:0] mul; | ||
# assign mul = a * 4'sd6; | ||
# assign y = mul / 8'sd3; | ||
# endmodule | ||
# EOT | ||
# equiv_opt -assert peepopt | ||
# design -load postopt | ||
# write_verilog | ||
# select -assert-count 1 t:$mul | ||
# select -assert-count 1 t:$div | ||
# design -reset | ||
# read_verilog <<EOT | ||
# module top( | ||
# input signed [3:0] a, | ||
# output signed [7:0] y, | ||
# ); | ||
# wire signed [6:0] mul; | ||
# assign mul = a * 4'sd6; | ||
# assign y = mul / 8'sd3; | ||
# endmodule | ||
# EOT | ||
# equiv_opt -assert peepopt | ||
# design -load postopt | ||
# write_verilog | ||
# select -assert-count 1 t:$mul | ||
# select -assert-count 1 t:$div | ||
# design -reset | ||
|
||
# No transform when (a*b) output can overflow (divider’s A input unsigned) | ||
# read_verilog <<EOT | ||
# module top( | ||
# input [3:0] a, | ||
# output [7:0] y, | ||
# ); | ||
# wire [4:0] mul; | ||
# assign mul = a * 4'd4; | ||
# assign y = mul / 8'd2; | ||
# endmodule | ||
# EOT | ||
# equiv_opt -assert peepopt | ||
# design -load postopt | ||
# select -assert-count 1 t:$mul | ||
# select -assert-count 1 t:$div | ||
# design -reset | ||
# read_verilog <<EOT | ||
# module top( | ||
# input [3:0] a, | ||
# output [7:0] y, | ||
# ); | ||
# wire [6:0] mul; | ||
# assign mul = a * 4'd4; | ||
# assign y = mul / 8'd2; | ||
# endmodule | ||
# EOT | ||
# equiv_opt -assert peepopt | ||
# design -load postopt | ||
# select -assert-count 1 t:$mul | ||
# select -assert-count 1 t:$div | ||
# design -reset | ||
|
||
# No transform when (a*b) and x/c fitting criteria but not connected (x != a*b) | ||
# read_verilog <<EOT | ||
# module top( | ||
# input signed [3:0] a, | ||
# input signed [7:0] b, | ||
# output signed [7:0] y, | ||
# output signed [7:0] z, | ||
# ); | ||
# assign y = a * 4'sd6; | ||
# assign z = b / 8'sd3; | ||
# endmodule | ||
# EOT | ||
# equiv_opt -assert peepopt | ||
# design -load postopt | ||
# select -assert-count 1 t:$mul | ||
# select -assert-count 1 t:$div | ||
# design -reset | ||
|
||
# No transform when b only divisible by c if c misinterpreted as unsigned | ||
read_verilog <<EOT | ||
module top( | ||
input signed [3:0] a, | ||
output signed [7:0] y, | ||
); | ||
wire signed [7:0] mul; | ||
assign mul = a * 4'sd6; | ||
assign y = mul / 3'sb110; | ||
endmodule | ||
EOT | ||
equiv_opt -assert peepopt | ||
# design -load postopt | ||
# show | ||
# select -assert-count 1 t:$mul | ||
# select -assert-count 1 t:$div | ||
# design -reset | ||
|
||
# No transform when b only divisible by c if b misinterpreted as unsigned | ||
# read_verilog <<EOT | ||
# module top( | ||
# input signed [3:0] a, | ||
# output signed [7:0] y, | ||
# ); | ||
# wire signed [7:0] mul; | ||
# assign mul = a * -4'sd8; | ||
# assign y = mul / 8'sd2; | ||
# endmodule | ||
# EOT | ||
# dump | ||
# peepopt | ||
# show | ||
# equiv_opt -assert peepopt | ||
# design -load postopt | ||
# select -assert-count 1 t:$mul | ||
# select -assert-count 1 t:$div | ||
# design -reset |