mirror of https://github.com/YosysHQ/yosys.git
50 lines
961 B
Plaintext
50 lines
961 B
Plaintext
log -header "Test simple positive case"
|
|
log -push
|
|
design -reset
|
|
read_verilog <<EOF
|
|
module top (
|
|
input wire [31:0] a,
|
|
output wire [63:0] y
|
|
);
|
|
assign y = (a * 5140) / (257 * 2);
|
|
endmodule
|
|
EOF
|
|
check -assert
|
|
copy top orig
|
|
cd top
|
|
peepopt
|
|
select -assert-none t:$div
|
|
clean -purge
|
|
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 -header "Test negative case where div is kept"
|
|
log -push
|
|
design -reset
|
|
read_verilog <<EOF
|
|
module top (
|
|
input wire signed [31:0] a,
|
|
output wire signed [63:0] y,
|
|
output wire probe
|
|
);
|
|
wire [44:0] tmp = (a * 5140);
|
|
assign probe = tmp[44];
|
|
|
|
assign y = tmp[43:0] / (257 * 2);
|
|
endmodule
|
|
EOF
|
|
check -assert
|
|
copy top orig
|
|
cd top
|
|
peepopt
|
|
select -assert-any t:$div
|
|
clean -purge
|
|
cd
|
|
miter -equiv -flatten -make_assert -make_outputs -ignore_gold_x top orig miter
|
|
sat -verify -prove-asserts -show-ports -enable_undef miter
|
|
|
|
|