mirror of
				https://github.com/YosysHQ/yosys
				synced 2025-11-04 05:19:11 +00:00 
			
		
		
		
	
		
			
				
	
	
		
			343 lines
		
	
	
	
		
			6.5 KiB
		
	
	
	
		
			Text
		
	
	
	
	
	
			
		
		
	
	
			343 lines
		
	
	
	
		
			6.5 KiB
		
	
	
	
		
			Text
		
	
	
	
	
	
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
 |