Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add muldiv_c and muxadd peepopts #4740

Open
wants to merge 68 commits into
base: main
Choose a base branch
from
Open
Changes from 1 commit
Commits
Show all changes
68 commits
Select commit Hold shift + click to select a range
9943b18
Add `muldiv_c` and `muxadd` peepopts
akashlevy Nov 13, 2024
9f84a92
Update passes/pmgen/peepopt_muxadd.pmg
akashlevy Nov 17, 2024
a3cc228
Update passes/pmgen/peepopt_muxadd.pmg
akashlevy Nov 17, 2024
ee18e1f
Preliminary fixes, not done
akashlevy Nov 17, 2024
0ddb3d7
Merge branch 'YosysHQ:main' into new_peepopts
akashlevy Dec 17, 2024
2375879
Update peepopt_muldiv_c.pmg
akashlevy Dec 17, 2024
0e15edd
Add muxadd peepopt tests
povik Dec 17, 2024
3b73888
Compiles and transforms correctly, fails equiv
Dec 17, 2024
8a6c100
Clean after opt
Dec 17, 2024
cfadf28
Merge pull request #1 from alainmarcel/new_peepopts
akashlevy Dec 17, 2024
b4fa7dc
Update peepopt_muxadd.pmg
akashlevy Dec 17, 2024
f9ae66d
Update peepopt_muldiv_c.pmg
akashlevy Dec 17, 2024
2979232
Fix code review issue
Dec 18, 2024
6c5d7cc
Merge pull request #2 from alainmarcel/new_peepopts
akashlevy Dec 18, 2024
5212ad7
Passing equiv for simplest muxadd case, prevent multiple match/rewiri…
Dec 18, 2024
8e78720
peepopt_muldiv_c: add test
widlarizer Dec 18, 2024
d81bda8
Merge pull request #3 from alainmarcel/new_peepopts
akashlevy Dec 18, 2024
ff5237f
Switch formal proof to use miter/sat
Dec 18, 2024
029c255
Merge pull request #4 from alainmarcel/new_peepopts
akashlevy Dec 18, 2024
7b70ba4
Convert to miter/sat
Dec 18, 2024
ceb5d2a
Merge pull request #5 from alainmarcel/new_peepopts
alaindargelas Dec 18, 2024
0f8356d
Code review fix, bail out on integers above 64 bits
Dec 18, 2024
50c93f7
Merge pull request #6 from alainmarcel/new_peepopts
alaindargelas Dec 18, 2024
53cf38c
Leave comment about signage assumption
Dec 18, 2024
d98b224
Merge pull request #7 from alainmarcel/new_peepopts
alaindargelas Dec 18, 2024
1c774f4
peepopt_muldiv_c: remove write_verilog from test
widlarizer Dec 18, 2024
6db406f
Back to equiv_opt for multdiv tests
Dec 19, 2024
24c012a
Back to equiv_opt for multdiv tests
Dec 19, 2024
32406ea
Merge pull request #8 from alainmarcel/new_peepopts
alaindargelas Dec 19, 2024
cd9e45d
Check for overflow, remove obsolete code, fix test
Dec 19, 2024
1ad1a0a
Merge pull request #9 from alainmarcel/new_peepopts
alaindargelas Dec 19, 2024
fc47616
Remove redundant code
Dec 19, 2024
eb4e147
Merge branch 'new_peepopts' of github.com:alainmarcel/yosys_akash int…
Dec 19, 2024
7270cd3
Merge pull request #10 from alainmarcel/new_peepopts
alaindargelas Dec 19, 2024
45500f4
A or B width extend
Dec 19, 2024
bb49acd
Merge pull request #11 from alainmarcel/new_peepopts
alaindargelas Dec 19, 2024
325b0e3
peepopt_multdiv_c: add forgotten -assert
widlarizer Dec 19, 2024
e8e806f
Consolidate tests
Dec 19, 2024
b63ef81
Merge pull request #12 from alainmarcel/new_peepopts
alaindargelas Dec 19, 2024
b525a02
Move helper code to peepopt.cc, check offset
Dec 19, 2024
5b97274
Merge pull request #13 from alainmarcel/new_peepopts
alaindargelas Dec 19, 2024
8b08f81
compress constant ratio
Dec 19, 2024
8687e5f
compress constant ratio
Dec 19, 2024
43f4181
Merge pull request #14 from alainmarcel/new_peepopts
alaindargelas Dec 19, 2024
72aef58
muxadd pass basic equiv_opt
Dec 19, 2024
a1db286
Merge pull request #15 from alainmarcel/new_peepopts
alaindargelas Dec 19, 2024
456773e
log test header for debug
Dec 20, 2024
87b8419
Merge pull request #16 from alainmarcel/new_peepopts
alaindargelas Dec 20, 2024
4d984d5
Fix symmetry test
Dec 20, 2024
a2bc9b2
Merge pull request #17 from alainmarcel/new_peepopts
alaindargelas Dec 20, 2024
4a28e0d
Pass all muldiv tests
Dec 20, 2024
a7fcda9
Merge branch 'new_peepopts' of github.com:alainmarcel/yosys_akash int…
Dec 20, 2024
48a971c
Merge pull request #18 from alainmarcel/new_peepopts
alaindargelas Dec 20, 2024
b6d079b
Overflow test fix
Dec 20, 2024
b1930e9
Overflow test fix
Dec 20, 2024
a497be5
Merge pull request #19 from alainmarcel/new_peepopts
alaindargelas Dec 20, 2024
7ce0460
All tests pass
Dec 20, 2024
095bf92
All tests pass
Dec 20, 2024
cd503d4
All tests pass
Dec 20, 2024
a731570
Merge pull request #20 from alainmarcel/new_peepopts
alaindargelas Dec 20, 2024
e0534a2
Merge remote-tracking branch 'upstream/main' into new_peepopts
akashlevy Dec 20, 2024
39ff442
Small muxadd comments
akashlevy Dec 20, 2024
832c877
Smallfixes
akashlevy Dec 20, 2024
b9c3666
GetSize, fix int sizing thing, add .gitignore
akashlevy Dec 20, 2024
11e4446
Fix nanoxplore meminit test
Dec 21, 2024
9450dc1
Merge pull request #21 from alainmarcel/new_peepopts
alaindargelas Dec 21, 2024
41a7c72
muxadd breaks Quicklogic dsp inference, make it optional
Dec 21, 2024
0b32e09
Merge pull request #22 from alainmarcel/new_peepopts
alaindargelas Dec 21, 2024
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
258 changes: 258 additions & 0 deletions tests/peepopt/muldiv_c.ys
Original file line number Diff line number Diff line change
@@ -0,0 +1,258 @@
# Basic pattern transformed: (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'sd6;
assign y = mul / 8'sd3;
endmodule
EOT
equiv_opt -assert peepopt
akashlevy marked this conversation as resolved.
Show resolved Hide resolved
design -load postopt
select -assert-count 1 t:$mul
select -assert-count 0 t:$div
design -reset

# Transformed on symmetry in multiplication
read_verilog <<EOT
module top(
input signed [3:0] a,
output signed [7:0] y,
);
wire signed [7:0] mul;
assign mul = 4'sd6 * a;
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

# Transformed on 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'sd6;
assign y = mul / 8'sd6;
endmodule
EOT
equiv_opt -assert peepopt
design -load postopt
select -assert-count 1 t:$mul
select -assert-count 0 t:$div
design -reset

# b negative, c positive
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 / 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

# b positive, c negative
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 / -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

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

# 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
widlarizer marked this conversation as resolved.
Show resolved Hide resolved
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
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
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Remove debugging statement

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

oops, I checked I didn't leave any show or dump but not 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 b misinterpreted as unsigned
# b 1001 is -7 but 9 misinterpreted
# c 11 is 3
read_verilog <<EOT
module top(
input signed [3:0] a,
output signed [7:0] y,
);
wire signed [7:0] mul;
assign mul = a * 4'sb1001;
assign y = mul / 8'sb11;
endmodule
EOT
equiv_opt -assert peepopt
design -load postopt
select -assert-count 1 t:$mul
select -assert-count 1 t:$div
design -reset

# Transform even if:
# (a*b) result would overflow if divider’s A input signedness is confused
# (A input is unsigned)
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
Loading