mirror of
				https://github.com/YosysHQ/yosys
				synced 2025-10-31 19:52:31 +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
 |