mirror of https://github.com/YosysHQ/yosys.git
344 lines
6.5 KiB
Plaintext
344 lines
6.5 KiB
Plaintext
|
|
log -header "Test simple positive case"
|
|||
|
|
log -push
|
|||
|
|
design -reset
|
|||
|
|
read_verilog <<EOF
|
|||
|
|
module top (
|
|||
|
|
input wire [11:0] a,
|
|||
|
|
output wire [11:0] y
|
|||
|
|
);
|
|||
|
|
assign y = (a * 16'd5140) / (257 * 2);
|
|||
|
|
endmodule
|
|||
|
|
EOF
|
|||
|
|
check -assert
|
|||
|
|
equiv_opt -assert peepopt
|
|||
|
|
design -load postopt
|
|||
|
|
select -assert-none t:$div
|
|||
|
|
design -reset
|
|||
|
|
|
|||
|
|
|
|||
|
|
log -pop
|
|||
|
|
log -header "Test negative case where div is kept"
|
|||
|
|
log -push
|
|||
|
|
design -reset
|
|||
|
|
read_verilog <<EOF
|
|||
|
|
module top (
|
|||
|
|
input wire signed [11:0] a,
|
|||
|
|
output wire signed [31:0] y,
|
|||
|
|
output wire probe
|
|||
|
|
);
|
|||
|
|
wire [28:0] tmp = (a * 16'd5140);
|
|||
|
|
assign probe = tmp[28];
|
|||
|
|
|
|||
|
|
assign y = tmp[27:0] / (257 * 2);
|
|||
|
|
endmodule
|
|||
|
|
EOF
|
|||
|
|
check -assert
|
|||
|
|
equiv_opt -assert peepopt
|
|||
|
|
design -load postopt
|
|||
|
|
select -assert-any t:$div
|
|||
|
|
design -reset
|
|||
|
|
|
|||
|
|
|
|||
|
|
log -pop
|
|||
|
|
log -header "Basic pattern transformed: (a * b) / c"
|
|||
|
|
log -push
|
|||
|
|
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
|
|||
|
|
|
|||
|
|
|
|||
|
|
log -pop
|
|||
|
|
log -header "Transformed on symmetry in multiplication"
|
|||
|
|
log -push
|
|||
|
|
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
|
|||
|
|
|
|||
|
|
log -pop
|
|||
|
|
log -header "Transformed on b == c"
|
|||
|
|
log -push
|
|||
|
|
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
|
|||
|
|
|
|||
|
|
|
|||
|
|
log -pop
|
|||
|
|
log -header "b negative, c positive"
|
|||
|
|
log -push
|
|||
|
|
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
|
|||
|
|
|
|||
|
|
|
|||
|
|
log -pop
|
|||
|
|
log -header "b positive, c negative"
|
|||
|
|
log -push
|
|||
|
|
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
|
|||
|
|
|
|||
|
|
|
|||
|
|
log -pop
|
|||
|
|
log -header "No transform when b not divisible by c"
|
|||
|
|
log -push
|
|||
|
|
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
|
|||
|
|
|
|||
|
|
|
|||
|
|
log -pop
|
|||
|
|
log -header "No transform when product has a second fanout"
|
|||
|
|
log -push
|
|||
|
|
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
|
|||
|
|
|
|||
|
|
|
|||
|
|
log -pop
|
|||
|
|
log -header "No transform when divisor is 0"
|
|||
|
|
log -push
|
|||
|
|
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 -assert peepopt
|
|||
|
|
design -load postopt
|
|||
|
|
select -assert-count 1 t:$mul
|
|||
|
|
select -assert-count 1 t:$div
|
|||
|
|
design -reset
|
|||
|
|
|
|||
|
|
|
|||
|
|
log -pop
|
|||
|
|
log -header "No transform when (a*b) output can overflow (divider’s A input signed)"
|
|||
|
|
log -push
|
|||
|
|
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
|
|||
|
|
|
|||
|
|
|
|||
|
|
log -pop
|
|||
|
|
log -header "No transform when (a*b) output can overflow (divider’s A input signed)"
|
|||
|
|
log -push
|
|||
|
|
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
|
|||
|
|
select -assert-count 1 t:$mul
|
|||
|
|
select -assert-count 1 t:$div
|
|||
|
|
design -reset
|
|||
|
|
|
|||
|
|
|
|||
|
|
log -pop
|
|||
|
|
log -header "No transform when (a*b) output can overflow (divider’s A input unsigned)"
|
|||
|
|
log -push
|
|||
|
|
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
|
|||
|
|
|
|||
|
|
log -pop
|
|||
|
|
log -header "No transform when (a*b) output can overflow (divider’s A input unsigned)"
|
|||
|
|
log -push
|
|||
|
|
read_verilog <<EOT
|
|||
|
|
module top(
|
|||
|
|
input [3:0] a,
|
|||
|
|
output [7:0] y,
|
|||
|
|
);
|
|||
|
|
wire [6:0] mul;
|
|||
|
|
assign mul = a * 4'd8;
|
|||
|
|
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
|
|||
|
|
|
|||
|
|
|
|||
|
|
log -pop
|
|||
|
|
log -header "No transform when (a*b) and x/c fitting criteria but not connected (x != a*b)"
|
|||
|
|
log -push
|
|||
|
|
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
|
|||
|
|
|
|||
|
|
log -pop
|
|||
|
|
log -header "No transform when b only divisible by c if b misinterpreted as unsigned"
|
|||
|
|
# b 1001 is -7 but 9 misinterpreted
|
|||
|
|
# c 11 is 3
|
|||
|
|
log -push
|
|||
|
|
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
|
|||
|
|
|
|||
|
|
log -pop
|
|||
|
|
log -header "Transform even if (a*b) result would overflow if divider’s A input signedness is confused & (A input is unsigned)"
|
|||
|
|
log -push
|
|||
|
|
# 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
|