mirror of
				https://github.com/YosysHQ/yosys
				synced 2025-11-04 05:19:11 +00:00 
			
		
		
		
	Revert "Wrap SB_LUT+SB_CARRY into $__ICE40_CARRY_WRAPPER"
This commit is contained in:
		
							parent
							
								
									f54bf1631f
								
							
						
					
					
						commit
						f9020ce2b3
					
				
					 20 changed files with 181 additions and 181 deletions
				
			
		
							
								
								
									
										148
									
								
								tests/various/opt_expr.ys
									
										
									
									
									
										Normal file
									
								
							
							
						
						
									
										148
									
								
								tests/various/opt_expr.ys
									
										
									
									
									
										Normal file
									
								
							| 
						 | 
				
			
			@ -0,0 +1,148 @@
 | 
			
		|||
 | 
			
		||||
read_verilog <<EOT
 | 
			
		||||
module opt_expr_add_test(input [3:0] i, input [7:0] j, output [8:0] o);
 | 
			
		||||
    assign o = (i << 4) + j;
 | 
			
		||||
endmodule
 | 
			
		||||
EOT
 | 
			
		||||
 | 
			
		||||
hierarchy -auto-top
 | 
			
		||||
proc
 | 
			
		||||
design -save gold
 | 
			
		||||
 | 
			
		||||
opt_expr -fine
 | 
			
		||||
wreduce
 | 
			
		||||
 | 
			
		||||
select -assert-count 1 t:$add r:A_WIDTH=4 r:B_WIDTH=4 r:Y_WIDTH=5 %i %i %i
 | 
			
		||||
 | 
			
		||||
design -stash gate
 | 
			
		||||
 | 
			
		||||
design -import gold -as gold
 | 
			
		||||
design -import gate -as gate
 | 
			
		||||
 | 
			
		||||
miter -equiv -flatten -make_assert -make_outputs gold gate miter
 | 
			
		||||
sat -verify -prove-asserts -show-ports miter
 | 
			
		||||
 | 
			
		||||
##########
 | 
			
		||||
 | 
			
		||||
read_verilog <<EOT
 | 
			
		||||
module opt_expr_add_signed_test(input signed [3:0] i, input signed [7:0] j, output signed [8:0] o);
 | 
			
		||||
    assign o = (i << 4) + j;
 | 
			
		||||
endmodule
 | 
			
		||||
EOT
 | 
			
		||||
 | 
			
		||||
hierarchy -auto-top
 | 
			
		||||
proc
 | 
			
		||||
design -save gold
 | 
			
		||||
 | 
			
		||||
opt_expr -fine
 | 
			
		||||
wreduce
 | 
			
		||||
 | 
			
		||||
select -assert-count 1 t:$add r:A_WIDTH=4 r:B_WIDTH=4 r:Y_WIDTH=5 %i %i %i
 | 
			
		||||
 | 
			
		||||
design -stash gate
 | 
			
		||||
 | 
			
		||||
design -import gold -as gold
 | 
			
		||||
design -import gate -as gate
 | 
			
		||||
 | 
			
		||||
miter -equiv -flatten -make_assert -make_outputs gold gate miter
 | 
			
		||||
sat -verify -prove-asserts -show-ports miter
 | 
			
		||||
 | 
			
		||||
##########
 | 
			
		||||
 | 
			
		||||
read_verilog <<EOT
 | 
			
		||||
module opt_expr_sub_test1(input [3:0] i, input [7:0] j, output [8:0] o);
 | 
			
		||||
    assign o = j - (i << 4);
 | 
			
		||||
endmodule
 | 
			
		||||
EOT
 | 
			
		||||
 | 
			
		||||
hierarchy -auto-top
 | 
			
		||||
proc
 | 
			
		||||
design -save gold
 | 
			
		||||
 | 
			
		||||
opt_expr -fine
 | 
			
		||||
wreduce
 | 
			
		||||
 | 
			
		||||
select -assert-count 1 t:$sub r:A_WIDTH=4 r:B_WIDTH=4 r:Y_WIDTH=5 %i %i %i
 | 
			
		||||
 | 
			
		||||
design -stash gate
 | 
			
		||||
 | 
			
		||||
design -import gold -as gold
 | 
			
		||||
design -import gate -as gate
 | 
			
		||||
 | 
			
		||||
miter -equiv -flatten -make_assert -make_outputs gold gate miter
 | 
			
		||||
sat -verify -prove-asserts -show-ports miter
 | 
			
		||||
 | 
			
		||||
##########
 | 
			
		||||
 | 
			
		||||
read_verilog <<EOT
 | 
			
		||||
module opt_expr_sub_signed_test1(input signed [3:0] i, input signed [7:0] j, output signed [8:0] o);
 | 
			
		||||
    assign o = j - (i << 4);
 | 
			
		||||
endmodule
 | 
			
		||||
EOT
 | 
			
		||||
 | 
			
		||||
hierarchy -auto-top
 | 
			
		||||
proc
 | 
			
		||||
design -save gold
 | 
			
		||||
 | 
			
		||||
opt_expr -fine
 | 
			
		||||
wreduce
 | 
			
		||||
 | 
			
		||||
select -assert-count 1 t:$sub r:A_WIDTH=4 r:B_WIDTH=4 r:Y_WIDTH=5 %i %i %i
 | 
			
		||||
 | 
			
		||||
design -stash gate
 | 
			
		||||
 | 
			
		||||
design -import gold -as gold
 | 
			
		||||
design -import gate -as gate
 | 
			
		||||
 | 
			
		||||
miter -equiv -flatten -make_assert -make_outputs gold gate miter
 | 
			
		||||
sat -verify -prove-asserts -show-ports miter
 | 
			
		||||
 | 
			
		||||
##########
 | 
			
		||||
 | 
			
		||||
read_verilog <<EOT
 | 
			
		||||
module opt_expr_sub_test2(input [3:0] i, input [7:0] j, output [8:0] o);
 | 
			
		||||
    assign o = (i << 4) - j;
 | 
			
		||||
endmodule
 | 
			
		||||
EOT
 | 
			
		||||
 | 
			
		||||
hierarchy -auto-top
 | 
			
		||||
proc
 | 
			
		||||
design -save gold
 | 
			
		||||
 | 
			
		||||
opt_expr -fine
 | 
			
		||||
wreduce
 | 
			
		||||
 | 
			
		||||
select -assert-count 1 t:$sub r:A_WIDTH=8 r:B_WIDTH=8 r:Y_WIDTH=9 %i %i %i
 | 
			
		||||
 | 
			
		||||
design -stash gate
 | 
			
		||||
 | 
			
		||||
design -import gold -as gold
 | 
			
		||||
design -import gate -as gate
 | 
			
		||||
 | 
			
		||||
miter -equiv -flatten -make_assert -make_outputs gold gate miter
 | 
			
		||||
sat -verify -prove-asserts -show-ports miter
 | 
			
		||||
 | 
			
		||||
##########
 | 
			
		||||
 | 
			
		||||
read_verilog <<EOT
 | 
			
		||||
module opt_expr_sub_test4(input [3:0] i, output [8:0] o);
 | 
			
		||||
    assign o = 5'b00010 - i;
 | 
			
		||||
endmodule
 | 
			
		||||
EOT
 | 
			
		||||
 | 
			
		||||
hierarchy -auto-top
 | 
			
		||||
proc
 | 
			
		||||
design -save gold
 | 
			
		||||
 | 
			
		||||
opt_expr -fine
 | 
			
		||||
wreduce
 | 
			
		||||
 | 
			
		||||
select -assert-count 1 t:$sub r:A_WIDTH=2 r:B_WIDTH=4 r:Y_WIDTH=5 %i %i %i
 | 
			
		||||
 | 
			
		||||
design -stash gate
 | 
			
		||||
 | 
			
		||||
design -import gold -as gold
 | 
			
		||||
design -import gate -as gate
 | 
			
		||||
 | 
			
		||||
miter -equiv -flatten -make_assert -make_outputs gold gate miter
 | 
			
		||||
sat -verify -prove-asserts -show-ports miter
 | 
			
		||||
							
								
								
									
										50
									
								
								tests/various/opt_rmdff.v
									
										
									
									
									
										Normal file
									
								
							
							
						
						
									
										50
									
								
								tests/various/opt_rmdff.v
									
										
									
									
									
										Normal file
									
								
							| 
						 | 
				
			
			@ -0,0 +1,50 @@
 | 
			
		|||
module opt_rmdff_test (input C, input D, input E, output [29:0] Q);
 | 
			
		||||
\$dffe #(.WIDTH(1), .CLK_POLARITY(1), .EN_POLARITY(1)) remove0 (.CLK(C), .D(D), .EN(1'b0), .Q(Q[0])); // EN is never active
 | 
			
		||||
(* init = "1'b1" *) wire Q1; assign Q[1] = Q1;
 | 
			
		||||
\$dffe #(.WIDTH(1), .CLK_POLARITY(1), .EN_POLARITY(1)) remove1 (.CLK(C), .D(D), .EN(1'b0), .Q(Q1)); // EN is never active
 | 
			
		||||
\$dffe #(.WIDTH(1), .CLK_POLARITY(1), .EN_POLARITY(1)) remove2 (.CLK(C), .D(D), .EN(1'bx), .Q(Q[2])); // EN is don't care
 | 
			
		||||
\$dffe #(.WIDTH(1), .CLK_POLARITY(1), .EN_POLARITY(1)) keep3 (.CLK(C), .D(D), .EN(1'b1), .Q(Q[3])); // EN is always active
 | 
			
		||||
(* init = "1'b0" *) wire Q4; assign Q[4] = Q4;
 | 
			
		||||
\$dffe #(.WIDTH(1), .CLK_POLARITY(0), .EN_POLARITY(1)) keep4 (.CLK(C), .D(D), .EN(1'b1), .Q(Q4)); // EN is always active
 | 
			
		||||
\$dffe #(.WIDTH(1), .CLK_POLARITY(1), .EN_POLARITY(0)) remove5 (.CLK(C), .D(D), .EN(1'b1), .Q(Q[5])); // EN is never active
 | 
			
		||||
\$dffe #(.WIDTH(1), .CLK_POLARITY(1), .EN_POLARITY(0)) remove6 (.CLK(C), .D(D), .EN(1'bx), .Q(Q[6])); // EN is don't care
 | 
			
		||||
(* init = "1'b0" *) wire Q7; assign Q[7] = Q7;
 | 
			
		||||
\$dffe #(.WIDTH(1), .CLK_POLARITY(0), .EN_POLARITY(0)) keep7 (.CLK(C), .D(D), .EN(E), .Q(Q7)); // EN is non constant
 | 
			
		||||
 | 
			
		||||
\$_DFFE_PP_ remove8 (.C(C), .D(D), .E(1'b0), .Q(Q[8])); // EN is never active
 | 
			
		||||
(* init = "1'b1" *) wire Q9; assign Q[9] = Q9;
 | 
			
		||||
\$_DFFE_PP_ remove9 (.C(C), .D(D), .E(1'b0), .Q(Q9)); // EN is never active
 | 
			
		||||
\$_DFFE_PP_ remove10 (.C(C), .D(D), .E(1'bx), .Q(Q[10])); // EN is don't care
 | 
			
		||||
\$_DFFE_PP_ keep11 (.C(C), .D(D), .E(1'b1), .Q(Q[11])); // EN is always active
 | 
			
		||||
(* init = "1'b0" *) wire Q12; assign Q[12] = Q12;
 | 
			
		||||
\$_DFFE_PP_ keep12 (.C(C), .D(D), .E(1'b1), .Q(Q12)); // EN is always active
 | 
			
		||||
 | 
			
		||||
\$_DFFE_NN_ remove13 (.C(C), .D(D), .E(1'b1), .Q(Q[13])); // EN is never active
 | 
			
		||||
(* init = "1'b1" *) wire Q14; assign Q[14] = Q14;
 | 
			
		||||
\$_DFFE_NN_ remove14 (.C(C), .D(D), .E(1'b1), .Q(Q14)); // EN is never active
 | 
			
		||||
\$_DFFE_NN_ remove15 (.C(C), .D(D), .E(1'bx), .Q(Q[15])); // EN is don't care
 | 
			
		||||
\$_DFFE_NN_ keep16 (.C(C), .D(D), .E(1'b0), .Q(Q[16])); // EN is always active
 | 
			
		||||
(* init = "1'b0" *) wire Q17; assign Q[17] = Q17;
 | 
			
		||||
\$_DFFE_NN_ keep17 (.C(C), .D(D), .E(1'b0), .Q(Q17)); // EN is always active
 | 
			
		||||
 | 
			
		||||
\$dffe #(.WIDTH(1), .CLK_POLARITY(1), .EN_POLARITY(1)) remove18 (.CLK(1'b0), .D(D), .EN(E), .Q(Q[18])); // CLK is constant
 | 
			
		||||
(* init = "1'b1" *) wire Q19; assign Q[19] = Q19;
 | 
			
		||||
\$dffe #(.WIDTH(1), .CLK_POLARITY(1), .EN_POLARITY(1)) remove19 (.CLK(1'b1), .D(D), .EN(E), .Q(Q19)); // CLK is constant
 | 
			
		||||
\$dffe #(.WIDTH(1), .CLK_POLARITY(1), .EN_POLARITY(1)) remove20 (.CLK(C), .D(1'bx), .EN(E), .Q(Q[20])); // D is undriven, Q has no initial value
 | 
			
		||||
(* init = "1'b0" *) wire Q21; assign Q[21] = Q21;
 | 
			
		||||
\$dffe #(.WIDTH(1), .CLK_POLARITY(1), .EN_POLARITY(1)) keep21 (.CLK(C), .D(1'bx), .EN(E), .Q(Q21)); // D is undriven, Q has initial value
 | 
			
		||||
//\$dffe #(.WIDTH(1), .CLK_POLARITY(0), .EN_POLARITY(1)) remove22 (.CLK(C), .D(1'b0), .EN(1'b1), .Q(Q[22])); // D is constant, no initial Q value, EN is always active
 | 
			
		||||
//                                                                                                           // (TODO, Q starts with 1'bx and becomes 1'b0)
 | 
			
		||||
(* init = "1'b0" *) wire Q23; assign Q[23] = Q23;
 | 
			
		||||
\$dffe #(.WIDTH(1), .CLK_POLARITY(1), .EN_POLARITY(1)) noenable23 (.CLK(C), .D(1'b0), .EN(1'b1), .Q(Q23)); // D is constant, initial Q value same as D, EN is always active
 | 
			
		||||
(* init = "1'b1" *) wire Q24; assign Q[24] = Q24;
 | 
			
		||||
\$dffe #(.WIDTH(1), .CLK_POLARITY(1), .EN_POLARITY(0)) keep24 (.CLK(C), .D(1'b0), .EN(1'b0), .Q(Q24)); // D is constant, initial Q value NOT same as D, EN is always active
 | 
			
		||||
(* init = "1'b1" *) wire Q25; assign Q[25] = Q25;
 | 
			
		||||
\$dffe #(.WIDTH(1), .CLK_POLARITY(1), .EN_POLARITY(0)) remove25 (.CLK(C), .D(1'b0), .EN(1'b1), .Q(Q25)); // D is constant, EN is never active
 | 
			
		||||
\$dffe #(.WIDTH(1), .CLK_POLARITY(1), .EN_POLARITY(1)) remove26 (.CLK(C), .D(Q[26]), .EN(1'b1), .Q(Q[26])); // D is Q, EN is always active
 | 
			
		||||
\$dffe #(.WIDTH(1), .CLK_POLARITY(1), .EN_POLARITY(0)) remove27 (.CLK(C), .D(Q[27]), .EN(1'b1), .Q(Q[27])); // D is Q, EN is never active, but no initial value
 | 
			
		||||
\$dffe #(.WIDTH(1), .CLK_POLARITY(1), .EN_POLARITY(0)) remove28 (.CLK(C), .D(Q[28]), .EN(E), .Q(Q[28])); // EN is nonconst, but no initial value
 | 
			
		||||
(* init = "1'b1" *) wire Q29; assign Q[29] = Q29;
 | 
			
		||||
\$dffe #(.WIDTH(1), .CLK_POLARITY(1), .EN_POLARITY(1)) keep29 (.CLK(C), .D(Q[29]), .EN(1'b1), .Q(Q29)); // EN is always active, but with initial value
 | 
			
		||||
 | 
			
		||||
endmodule
 | 
			
		||||
							
								
								
									
										26
									
								
								tests/various/opt_rmdff.ys
									
										
									
									
									
										Normal file
									
								
							
							
						
						
									
										26
									
								
								tests/various/opt_rmdff.ys
									
										
									
									
									
										Normal file
									
								
							| 
						 | 
				
			
			@ -0,0 +1,26 @@
 | 
			
		|||
read_verilog -icells opt_rmdff.v
 | 
			
		||||
prep
 | 
			
		||||
design -stash gold
 | 
			
		||||
read_verilog -icells opt_rmdff.v
 | 
			
		||||
proc
 | 
			
		||||
opt_rmdff
 | 
			
		||||
 | 
			
		||||
select -assert-count 0 c:remove*
 | 
			
		||||
select -assert-min 7 c:keep*
 | 
			
		||||
select -assert-count 0  t:$dffe 7:$_DFFE_* %u c:noenable* %i
 | 
			
		||||
 | 
			
		||||
design -stash gate
 | 
			
		||||
 | 
			
		||||
design -import gold -as gold
 | 
			
		||||
design -import gate -as gate
 | 
			
		||||
 | 
			
		||||
equiv_make gold gate equiv
 | 
			
		||||
hierarchy -top equiv
 | 
			
		||||
equiv_simple -undef
 | 
			
		||||
equiv_status -assert
 | 
			
		||||
 | 
			
		||||
design -load gold
 | 
			
		||||
stat
 | 
			
		||||
 | 
			
		||||
design -load gate
 | 
			
		||||
stat
 | 
			
		||||
| 
						 | 
				
			
			@ -36,6 +36,7 @@ design -save gold
 | 
			
		|||
opt_expr
 | 
			
		||||
wreduce
 | 
			
		||||
 | 
			
		||||
dump
 | 
			
		||||
select -assert-count 1 t:$sub r:A_WIDTH=4 r:B_WIDTH=4 r:Y_WIDTH=5 %i %i %i
 | 
			
		||||
 | 
			
		||||
design -stash gate
 | 
			
		||||
| 
						 | 
				
			
			@ -45,35 +46,3 @@ design -import gate -as gate
 | 
			
		|||
 | 
			
		||||
miter -equiv -flatten -make_assert -make_outputs gold gate miter
 | 
			
		||||
sat -verify -prove-asserts -show-ports miter
 | 
			
		||||
 | 
			
		||||
##########
 | 
			
		||||
 | 
			
		||||
# Testcase from: https://github.com/YosysHQ/yosys/commit/25680f6a078bb32f157bd580705656496717bafb
 | 
			
		||||
design -reset
 | 
			
		||||
read_verilog <<EOT
 | 
			
		||||
module top(
 | 
			
		||||
    input clk,
 | 
			
		||||
    input rst,
 | 
			
		||||
    input [2:0] a,
 | 
			
		||||
    output [1:0] b
 | 
			
		||||
);
 | 
			
		||||
    reg [2:0] b_reg;
 | 
			
		||||
    initial begin
 | 
			
		||||
        b_reg <= 3'b0;
 | 
			
		||||
    end
 | 
			
		||||
 | 
			
		||||
    assign b = b_reg[1:0];
 | 
			
		||||
    always @(posedge clk or posedge rst) begin
 | 
			
		||||
        if(rst) begin
 | 
			
		||||
            b_reg <= 3'b0;
 | 
			
		||||
        end else begin
 | 
			
		||||
            b_reg <= a;
 | 
			
		||||
        end
 | 
			
		||||
    end
 | 
			
		||||
endmodule
 | 
			
		||||
EOT
 | 
			
		||||
 | 
			
		||||
proc
 | 
			
		||||
wreduce
 | 
			
		||||
 | 
			
		||||
select -assert-count 1 t:$adff r:ARST_VALUE=2'b00 %i
 | 
			
		||||
| 
						 | 
				
			
			
 | 
			
		|||
		Loading…
	
	Add table
		Add a link
		
	
		Reference in a new issue