riscv
/
yosys
mirror of https://github.com/YosysHQ/yosys.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity

Merge pull request #8 from alainmarcel/new_peepopts 

Back to equiv_opt for multdiv tests
This commit is contained in:
alaindargelas 2024-12-18 20:22:58 -08:00 committed by GitHub
parent 1c774f41ee 24c012aa6d
commit 32406ea1e3
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
1 changed files with 13 additions and 23 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

34
tests/peepopt/multdiv_c.ys
View File

@ -3,21 +3,17 @@ log -push
design -reset design -reset
read_verilog <<EOF read_verilog <<EOF
module top ( module top (
input wire [31:0] a, input wire [11:0] a,
output wire [63:0] y output wire [31:0] y
); );
assign y = (a * 5140) / (257 * 2); assign y = (a * 16'd5140) / (257 * 2);
endmodule endmodule
EOF EOF
check -assert check -assert
copy top orig equiv_opt -assert peepopt
cd top design -load postopt
peepopt
select -assert-none t:$div select -assert-none t:$div
clean -purge design -reset
cd
miter -equiv -flatten -make_assert -make_outputs -ignore_gold_x top orig miter
sat -verify -prove-asserts -show-ports -enable_undef miter
log -pop log -pop
@ -26,24 +22,18 @@ log -push
design -reset design -reset
read_verilog <<EOF read_verilog <<EOF
module top ( module top (
input wire signed [31:0] a, input wire signed [11:0] a,
output wire signed [63:0] y, output wire signed [31:0] y,
output wire probe output wire probe
); );
wire [44:0] tmp = (a * 5140); wire [44:0] tmp = (a * 16'd5140);
assign probe = tmp[44]; assign probe = tmp[44];
assign y = tmp[43:0] / (257 * 2); assign y = tmp[43:0] / (257 * 2);
endmodule endmodule
EOF EOF
check -assert check -assert
copy top orig equiv_opt -assert peepopt
cd top design -load postopt
peepopt
select -assert-any t:$div select -assert-any t:$div
clean -purge design -reset
cd
miter -equiv -flatten -make_assert -make_outputs -ignore_gold_x top orig miter
sat -verify -prove-asserts -show-ports -enable_undef miter