mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2026-03-23 04:49:15 +00:00
Code Activity

Consolidate csa tests.

Browse source
This commit is contained in:
nella 2026-03-18 12:36:31 +01:00
parent 4ce8e7d1df
commit 1c1d782bf8
64 changed files with 641 additions and 704 deletions
Download patch file Download diff file Expand all files Collapse all files

6
tests/csa_tree/abc_bench_add8.v
View file

@ -1,6 +0,0 @@
module abc_bench_add8(
input [7:0] a, b, c, d, e, f, g, h,
output [7:0] y
);
assign y = a + b + c + d + e + f + g + h;
endmodule

9
tests/csa_tree/add_1bit.v
View file

@ -1,9 +0,0 @@
// Edge case for carry shifting
module add_1bit(
input a, b, c,
output [1:0] y
);
assign y = a + b + c;
endmodule

6
tests/csa_tree/add_1bit_wide_out.v
View file

@ -1,6 +0,0 @@
module add_1bit_wide_out(
input a, b, c, d,
output [3:0] y
);
assign y = a + b + c + d;
endmodule

7
tests/csa_tree/add_chain_16.v
View file

@ -1,7 +0,0 @@
module add_chain_16(
input [15:0] a0, a1, a2, a3, a4, a5, a6, a7,
input [15:0] a8, a9, a10, a11, a12, a13, a14, a15,
output [15:0] y
);
assign y = a0 + a1 + a2 + a3 + a4 + a5 + a6 + a7 + a8 + a9 + a10 + a11 + a12 + a13 + a14 + a15;
endmodule

8
tests/csa_tree/add_chain_2_neg.v
View file

@ -1,8 +0,0 @@
// Shouldnt generate csa tree
module add_chain_2(
input [7:0] a, b,
output [7:0] y
);
assign y = a + b;
endmodule

9
tests/csa_tree/add_chain_3.v
View file

@ -1,9 +0,0 @@
// Min chain len
module add_chain_3(
input [7:0] a, b, c,
output [7:0] y
);
assign y = a + b + c;
endmodule

7
tests/csa_tree/add_chain_5.v
View file

@ -1,7 +0,0 @@
module add_chain_5(
input [11:0] a, b, c, d, e,
output [11:0] y
);
assign y = a + b + c + d + e;
endmodule

7
tests/csa_tree/add_chain_8.v
View file

@ -1,7 +0,0 @@
module add_chain_8(
input [15:0] a, b, c, d, e, f, g, h,
output [15:0] y
);
assign y = a + b + c + d + e + f + g + h;
endmodule

10
tests/csa_tree/add_mixed_widths.v
View file

@ -1,10 +0,0 @@
module add_mixed_widths(
input [7:0] a,
input [3:0] b,
input [15:0] c,
input [7:0] d,
output [15:0] y
);
assign y = a + b + c + d;
endmodule

6
tests/csa_tree/add_multi_const.v
View file

@ -1,6 +0,0 @@
module add_multi_const(
input [7:0] x,
output [7:0] y
);
assign y = 8'd1 + 8'd2 + 8'd3 + x;
endmodule

10
tests/csa_tree/add_multi_fanout.v
View file

@ -1,10 +0,0 @@
module add_multi_fanout(
input [7:0] a, b, c,
output [7:0] mid,
output [7:0] y
);
wire [7:0] ab = a + b;
assign mid = ab;
assign y = ab + c;
endmodule

9
tests/csa_tree/add_partial_chain.v
View file

@ -1,9 +0,0 @@
module add_partial_chain(
input [7:0] a, b, c, d, e,
output [7:0] mid,
output [7:0] y
);
wire [7:0] ab = a + b;
assign mid = ab;
assign y = ab + c + d + e;
endmodule

6
tests/csa_tree/add_repeated.v
View file

@ -1,6 +0,0 @@
module add_repeated(
input [7:0] a,
output [7:0] y
);
assign y = a + a + a + a;
endmodule

6
tests/csa_tree/add_signed.v
View file

@ -1,6 +0,0 @@
module add_signed(
input signed [7:0] a, b, c, d,
output signed [9:0] y
);
assign y = a + b + c + d;
endmodule

9
tests/csa_tree/add_two_chains.v
View file

@ -1,9 +0,0 @@
module add_two_chains(
input [7:0] a, b, c, d,
input [7:0] e, f, g, h,
output [7:0] y1,
output [7:0] y2
);
assign y1 = a + b + c + d;
assign y2 = e + f + g + h;
endmodule

6
tests/csa_tree/add_wide_output.v
View file

@ -1,6 +0,0 @@
module add_wide_output(
input [7:0] a, b, c, d,
output [31:0] y
);
assign y = a + b + c + d;
endmodule

7
tests/csa_tree/add_with_const.v
View file

@ -1,7 +0,0 @@
module add_with_const(
input [7:0] a, b, c,
output [7:0] y
);
assign y = a + b + c + 8'd42;
endmodule

8
tests/csa_tree/csa_tree_16input.ys
View file

@ -1,8 +0,0 @@
read_verilog add_chain_16.v
hierarchy -auto-top
proc; opt_clean
csa_tree
stat
select -assert-count 14 t:$fa
select -assert-count 1 t:$add

8
tests/csa_tree/csa_tree_1bit.ys
View file

@ -1,8 +0,0 @@
read_verilog add_1bit.v
hierarchy -auto-top
proc; opt_clean
csa_tree
stat
select -assert-count 1 t:$fa
select -assert-count 1 t:$add

8
tests/csa_tree/csa_tree_1bit_wide_out.ys
View file

@ -1,8 +0,0 @@
read_verilog add_1bit_wide_out.v
hierarchy -auto-top
proc; opt_clean
csa_tree
stat
select -assert-count 2 t:$fa
select -assert-count 1 t:$add

11
tests/csa_tree/csa_tree_2input_neg.ys
View file

@ -1,11 +0,0 @@
# Test csa_tree on 2-operand — should not trigger
read_verilog add_chain_2_neg.v
hierarchy -auto-top
proc; opt_clean
equiv_opt csa_tree
design -load postopt
select -assert-none t:$fa
select -assert-count 1 t:$add

8
tests/csa_tree/csa_tree_3input.ys
View file

@ -1,8 +0,0 @@
read_verilog add_chain_3.v
hierarchy -auto-top
proc; opt_clean
csa_tree
stat
select -assert-count 1 t:$fa
select -assert-count 1 t:$add

8
tests/csa_tree/csa_tree_5input.ys
View file

@ -1,8 +0,0 @@
read_verilog add_chain_5.v
hierarchy -auto-top
proc; opt_clean
csa_tree
stat
select -assert-count 3 t:$fa
select -assert-count 1 t:$add

8
tests/csa_tree/csa_tree_8input.ys
View file

@ -1,8 +0,0 @@
read_verilog add_chain_8.v
hierarchy -auto-top
proc; opt_clean
csa_tree
stat
select -assert-count 6 t:$fa
select -assert-count 1 t:$add

61
tests/csa_tree/csa_tree_add_chains.ys Normal file
View file

@ -0,0 +1,61 @@
read_verilog <<EOT
module add3(
input [7:0] a, b, c,
output [7:0] y
);
assign y = a + b + c;
endmodule
EOT
hierarchy -auto-top
proc
csa_tree
select -assert-count 1 t:$fa
select -assert-count 1 t:$add
design -reset
read_verilog <<EOT
module add5(
input [11:0] a, b, c, d, e,
output [11:0] y
);
assign y = a + b + c + d + e;
endmodule
EOT
hierarchy -auto-top
proc
csa_tree
select -assert-count 3 t:$fa
select -assert-count 1 t:$add
design -reset
read_verilog <<EOT
module add8(
input [15:0] a, b, c, d, e, f, g, h,
output [15:0] y
);
assign y = a + b + c + d + e + f + g + h;
endmodule
EOT
hierarchy -auto-top
proc
csa_tree
select -assert-count 6 t:$fa
select -assert-count 1 t:$add
design -reset
read_verilog <<EOT
module add16(
input [15:0] a0, a1, a2, a3, a4, a5, a6, a7,
input [15:0] a8, a9, a10, a11, a12, a13, a14, a15,
output [15:0] y
);
assign y = a0 + a1 + a2 + a3 + a4 + a5 + a6 + a7
+ a8 + a9 + a10 + a11 + a12 + a13 + a14 + a15;
endmodule
EOT
hierarchy -auto-top
proc
csa_tree
select -assert-count 14 t:$fa
select -assert-count 1 t:$add
design -reset

8
tests/csa_tree/csa_tree_const.ys
View file

@ -1,8 +0,0 @@
read_verilog add_with_const.v
hierarchy -auto-top
proc; opt_clean
csa_tree
stat
select -assert-count 2 t:$fa
select -assert-count 1 t:$add

147
tests/csa_tree/csa_tree_edge_cases.ys Normal file
View file

@ -0,0 +1,147 @@
read_verilog <<EOT
module add_1bit(
input a, b, c,
output [1:0] y
);
assign y = a + b + c;
endmodule
EOT
hierarchy -auto-top
proc
csa_tree
select -assert-count 1 t:$fa
select -assert-count 1 t:$add
design -reset
read_verilog <<EOT
module add_1bit_wide(
input a, b, c, d,
output [3:0] y
);
assign y = a + b + c + d;
endmodule
EOT
hierarchy -auto-top
proc
csa_tree
select -assert-count 2 t:$fa
select -assert-count 1 t:$add
design -reset
read_verilog <<EOT
module add_wide_out(
input [7:0] a, b, c, d,
output [31:0] y
);
assign y = a + b + c + d;
endmodule
EOT
hierarchy -auto-top
proc
csa_tree
select -assert-count 2 t:$fa
select -assert-count 1 t:$add
design -reset
read_verilog <<EOT
module add_mixed(
input [7:0] a,
input [3:0] b,
input [15:0] c,
input [7:0] d,
output [15:0] y
);
assign y = a + b + c + d;
endmodule
EOT
hierarchy -auto-top
proc
csa_tree
select -assert-count 2 t:$fa
select -assert-count 1 t:$add
design -reset
read_verilog <<EOT
module add_signed(
input signed [7:0] a, b, c, d,
output signed [9:0] y
);
assign y = a + b + c + d;
endmodule
EOT
hierarchy -auto-top
proc
csa_tree
select -assert-count 2 t:$fa
select -assert-count 1 t:$add
design -reset
read_verilog <<EOT
module add_repeated(
input [7:0] a,
output [7:0] y
);
assign y = a + a + a + a;
endmodule
EOT
hierarchy -auto-top
proc
csa_tree
select -assert-count 2 t:$fa
select -assert-count 1 t:$add
design -reset
read_verilog <<EOT
module add_const(
input [7:0] a, b, c,
output [7:0] y
);
assign y = a + b + c + 8'd42;
endmodule
EOT
hierarchy -auto-top
proc
csa_tree
select -assert-count 2 t:$fa
select -assert-count 1 t:$add
design -reset
read_verilog <<EOT
module add_two(
input [7:0] a, b, c, d, e, f, g, h,
output [7:0] y1, y2
);
assign y1 = a + b + c + d;
assign y2 = e + f + g + h;
endmodule
EOT
hierarchy -auto-top
proc
csa_tree
select -assert-count 4 t:$fa
select -assert-count 2 t:$add
design -reset
read_verilog <<EOT
module fir_4tap(
input clk,
input [15:0] x, c0, c1, c2, c3,
output reg [31:0] y
);
reg [15:0] x1, x2, x3;
always @(posedge clk) begin
x1 <= x;
x2 <= x1;
x3 <= x2;
end
wire [31:0] sum = x*c0 + x1*c1 + x2*c2 + x3*c3;
always @(posedge clk) y <= sum;
endmodule
EOT
hierarchy -auto-top
proc
csa_tree
select -assert-count 2 t:$fa
select -assert-count 1 t:$add
design -reset

165
tests/csa_tree/csa_tree_equiv.ys
View file

@ -1,81 +1,178 @@
# Equivalence tests using narrow operands
read_verilog equiv_narrow.v
hierarchy -top equiv_add3
proc; opt_clean
read_verilog <<EOT
module equiv_add3(
input [3:0] a, b, c,
output [3:0] y
);
assign y = a + b + c;
endmodule
EOT
hierarchy -auto-top
proc
equiv_opt csa_tree
design -load postopt
select -assert-count 1 t:$fa
select -assert-count 1 t:$add
design -reset
log "equiv_add3"
read_verilog equiv_narrow.v
hierarchy -top equiv_add4
proc; opt_clean
read_verilog <<EOT
module equiv_add4(
input [3:0] a, b, c, d,
output [3:0] y
);
assign y = a + b + c + d;
endmodule
EOT
hierarchy -auto-top
proc
equiv_opt csa_tree
design -load postopt
select -assert-count 2 t:$fa
select -assert-count 1 t:$add
design -reset
log "equiv_add4"
read_verilog equiv_narrow.v
hierarchy -top equiv_add5
proc; opt_clean
read_verilog <<EOT
module equiv_add5(
input [3:0] a, b, c, d, e,
output [3:0] y
);
assign y = a + b + c + d + e;
endmodule
EOT
hierarchy -auto-top
proc
equiv_opt csa_tree
design -load postopt
select -assert-count 3 t:$fa
select -assert-count 1 t:$add
design -reset
log "equiv_add5"
read_verilog equiv_narrow.v
hierarchy -top equiv_add8
proc; opt_clean
read_verilog <<EOT
module equiv_add8(
input [3:0] a, b, c, d, e, f, g, h,
output [3:0] y
);
assign y = a + b + c + d + e + f + g + h;
endmodule
EOT
hierarchy -auto-top
proc
equiv_opt csa_tree
design -load postopt
select -assert-count 6 t:$fa
select -assert-count 1 t:$add
design -reset
log "equiv_add8: ok"
read_verilog equiv_narrow.v
hierarchy -top equiv_signed
proc; opt_clean
read_verilog <<EOT
module equiv_signed(
input signed [3:0] a, b, c, d,
output signed [5:0] y
);
assign y = a + b + c + d;
endmodule
EOT
hierarchy -auto-top
proc
equiv_opt csa_tree
design -load postopt
select -assert-count 2 t:$fa
select -assert-count 1 t:$add
design -reset
log "equiv_signed: ok"
read_verilog equiv_narrow.v
hierarchy -top equiv_mixed_w
proc; opt_clean
read_verilog <<EOT
module equiv_mixed(
input [1:0] a,
input [3:0] b,
input [5:0] c,
output [5:0] y
);
assign y = a + b + c;
endmodule
EOT
hierarchy -auto-top
proc
equiv_opt csa_tree
design -load postopt
select -assert-count 1 t:$fa
select -assert-count 1 t:$add
design -reset
log "equiv_mixed_w: ok"
read_verilog equiv_narrow.v
hierarchy -top equiv_repeated
proc; opt_clean
read_verilog <<EOT
module equiv_sub_mixed(
input [3:0] a, b, c, d,
output [3:0] y
);
assign y = a + b - c + d;
endmodule
EOT
hierarchy -auto-top
proc
equiv_opt csa_tree
design -load postopt
select -assert-count 3 t:$fa
select -assert-count 1 t:$add
design -reset
read_verilog <<EOT
module equiv_sub_all(
input [3:0] a, b, c, d,
output [3:0] y
);
assign y = a - b - c - d;
endmodule
EOT
hierarchy -auto-top
proc
equiv_opt csa_tree
design -load postopt
select -assert-count 3 t:$fa
select -assert-count 1 t:$add
design -reset
read_verilog <<EOT
module equiv_sub_3op(
input [3:0] a, b, c,
output [3:0] y
);
assign y = a - b + c;
endmodule
EOT
hierarchy -auto-top
proc
equiv_opt csa_tree
design -load postopt
select -assert-count 2 t:$fa
select -assert-count 1 t:$add
design -reset
log "equiv_repeated: ok"
read_verilog equiv_narrow.v
hierarchy -top equiv_1bit_wide
proc; opt_clean
read_verilog <<EOT
module equiv_sub_signed(
input signed [3:0] a, b, c, d,
output signed [5:0] y
);
assign y = a + b - c - d;
endmodule
EOT
hierarchy -auto-top
proc
equiv_opt csa_tree
design -load postopt
select -assert-count 3 t:$fa
select -assert-count 1 t:$add
design -reset
read_verilog <<EOT
module equiv_double_neg(
input [3:0] a, b, c,
output [3:0] y
);
wire [3:0] ab = a - b;
assign y = c - ab;
endmodule
EOT
hierarchy -auto-top
proc
equiv_opt csa_tree
design -load postopt
select -assert-count 2 t:$fa
select -assert-count 1 t:$add
design -reset
log "equiv_1bit_wide: ok"

8
tests/csa_tree/csa_tree_fir.ys
View file

@ -1,8 +0,0 @@
read_verilog fir_4tap.v
hierarchy -auto-top
proc; opt_clean
csa_tree
stat
select -assert-count 2 t:$fa
select -assert-count 1 t:$add

14
tests/csa_tree/csa_tree_idempotent.ys
View file

@ -1,15 +1,19 @@
read_verilog add_chain_8.v
read_verilog <<EOT
module add8(
input [15:0] a, b, c, d, e, f, g, h,
output [15:0] y
);
assign y = a + b + c + d + e + f + g + h;
endmodule
EOT
hierarchy -auto-top
proc; opt_clean
proc
csa_tree
stat
select -assert-count 6 t:$fa
select -assert-count 1 t:$add
csa_tree
stat
select -assert-count 6 t:$fa
select -assert-count 1 t:$add
select -assert-none t:$sub

8
tests/csa_tree/csa_tree_mixed_widths.ys
View file

@ -1,8 +0,0 @@
read_verilog add_mixed_widths.v
hierarchy -auto-top
proc; opt_clean
csa_tree
stat
select -assert-count 2 t:$fa
select -assert-count 1 t:$add

9
tests/csa_tree/csa_tree_multi_const.ys
View file

@ -1,9 +0,0 @@
read_verilog add_multi_const.v
hierarchy -auto-top
proc; opt_clean
csa_tree
stat
select -assert-none t:$fa
select -assert-max 1 t:$add

8
tests/csa_tree/csa_tree_multi_fanout.ys
View file

@ -1,8 +0,0 @@
read_verilog add_multi_fanout.v
hierarchy -auto-top
proc; opt_clean
equiv_opt csa_tree
design -load postopt
select -assert-none t:$fa

77
tests/csa_tree/csa_tree_negative.ys Normal file
View file

@ -0,0 +1,77 @@
read_verilog <<EOT
module add2(
input [7:0] a, b,
output [7:0] y
);
assign y = a + b;
endmodule
EOT
hierarchy -auto-top
proc
csa_tree
select -assert-none t:$fa
select -assert-count 1 t:$add
design -reset
read_verilog <<EOT
module add_fanout(
input [7:0] a, b, c,
output [7:0] mid, y
);
wire [7:0] ab = a + b;
assign mid = ab;
assign y = ab + c;
endmodule
EOT
hierarchy -auto-top
proc
csa_tree
select -assert-none t:$fa
design -reset
read_verilog <<EOT
module sub2(
input [7:0] a, b,
output [7:0] y
);
assign y = a - b;
endmodule
EOT
hierarchy -auto-top
proc
csa_tree
select -assert-none t:$fa
select -assert-count 1 t:$sub
design -reset
read_verilog <<EOT
module add_multi_const(
input [7:0] x,
output [7:0] y
);
assign y = 8'd1 + 8'd2 + 8'd3 + x;
endmodule
EOT
hierarchy -auto-top
proc
csa_tree
select -assert-none t:$fa
select -assert-max 1 t:$add
design -reset
read_verilog <<EOT
module add_partial(
input [7:0] a, b, c, d, e,
output [7:0] mid, y
);
wire [7:0] ab = a + b;
assign mid = ab;
assign y = ab + c + d + e;
endmodule
EOT
hierarchy -auto-top
proc
csa_tree
select -assert-count 2 t:$fa
select -assert-count 2 t:$add
design -reset

8
tests/csa_tree/csa_tree_partial_chain.ys
View file

@ -1,8 +0,0 @@
read_verilog add_partial_chain.v
hierarchy -auto-top
proc; opt_clean
csa_tree
stat
select -assert-count 2 t:$fa
select -assert-count 2 t:$add

8
tests/csa_tree/csa_tree_repeated.ys
View file

@ -1,8 +0,0 @@
read_verilog add_repeated.v
hierarchy -auto-top
proc; opt_clean
csa_tree
stat
select -assert-count 2 t:$fa
select -assert-count 1 t:$add

8
tests/csa_tree/csa_tree_signed.ys
View file

@ -1,8 +0,0 @@
read_verilog add_signed.v
hierarchy -auto-top
proc; opt_clean
csa_tree
stat
select -assert-count 2 t:$fa
select -assert-count 1 t:$add

77
tests/csa_tree/csa_tree_sim.ys
View file

@ -1,23 +1,72 @@
read_verilog sim_add4.v
hierarchy -top sim_add4
proc; opt_clean
read_verilog <<EOT
module sim_add4(
input [7:0] a, b, c, d,
output [7:0] y
);
assign y = a + b + c + d;
endmodule
EOT
hierarchy -auto-top
proc
csa_tree
opt_clean
# 1 + 2 + 3 + 4 = 10
sat -set a 1 -set b 2 -set c 3 -set d 4 -prove y 10
# 0 + 0 + 0 + 0 = 0
sat -set a 0 -set b 0 -set c 0 -set d 0 -prove y 0
# 255 + 1 + 0 + 0 = 0
sat -set a 255 -set b 1 -set c 0 -set d 0 -prove y 0
# 100 + 50 + 25 + 25 = 200
sat -set a 100 -set b 50 -set c 25 -set d 25 -prove y 200
# 255 + 255 + 255 + 255 = 252
sat -set a 255 -set b 255 -set c 255 -set d 255 -prove y 252
design -reset
log "ok"
read_verilog <<EOT
module sim_sub_mixed(
input [7:0] a, b, c, d,
output [7:0] y
);
assign y = a + b - c + d;
endmodule
EOT
hierarchy -auto-top
proc
csa_tree
sat -set a 10 -set b 20 -set c 5 -set d 3 -prove y 28
sat -set a 0 -set b 0 -set c 0 -set d 0 -prove y 0
sat -set a 100 -set b 50 -set c 30 -set d 10 -prove y 130
sat -set a 1 -set b 1 -set c 255 -set d 1 -prove y 4
design -reset
read_verilog <<EOT
module sim_sub_all(
input [7:0] a, b, c, d,
output [7:0] y
);
assign y = a - b - c - d;
endmodule
EOT
hierarchy -auto-top
proc
csa_tree
sat -set a 100 -set b 10 -set c 20 -set d 30 -prove y 40
sat -set a 0 -set b 0 -set c 0 -set d 0 -prove y 0
sat -set a 255 -set b 1 -set c 1 -set d 1 -prove y 252
design -reset
read_verilog <<EOT
module sim_double_neg(
input [7:0] a, b, c,
output [7:0] y
);
wire [7:0] ab = a - b;
assign y = c - ab;
endmodule
EOT
hierarchy -auto-top
proc
csa_tree
sat -set a 30 -set b 20 -set c 10 -prove y 0
sat -set a 50 -set b 25 -set c 100 -prove y 75
sat -set a 0 -set b 0 -set c 0 -prove y 0
sat -set a 255 -set b 1 -set c 1 -prove y 3
design -reset

8
tests/csa_tree/csa_tree_sub_2op_neg.ys
View file

@ -1,8 +0,0 @@
read_verilog sub_2op_neg.v
hierarchy -auto-top
proc; opt_clean
csa_tree
stat
select -assert-none t:$fa
select -assert-count 1 t:$sub

10
tests/csa_tree/csa_tree_sub_3op.ys
View file

@ -1,10 +0,0 @@
read_verilog sub_3op.v
hierarchy -auto-top
proc; opt_clean
csa_tree
stat
select -assert-count 2 t:$fa
select -assert-count 1 t:$add
select -assert-count 1 t:$not
select -assert-none t:$sub

10
tests/csa_tree/csa_tree_sub_5op.ys
View file

@ -1,10 +0,0 @@
read_verilog sub_5op.v
hierarchy -auto-top
proc; opt_clean
csa_tree
stat
select -assert-count 4 t:$fa
select -assert-count 1 t:$add
select -assert-count 2 t:$not
select -assert-none t:$sub

10
tests/csa_tree/csa_tree_sub_all.ys
View file

@ -1,10 +0,0 @@
read_verilog sub_all.v
hierarchy -auto-top
proc; opt_clean
csa_tree
stat
select -assert-count 3 t:$fa
select -assert-count 1 t:$add
select -assert-count 3 t:$not
select -assert-none t:$sub

102
tests/csa_tree/csa_tree_sub_chains.ys Normal file
View file

@ -0,0 +1,102 @@
read_verilog <<EOT
module sub_3op(
input [7:0] a, b, c,
output [7:0] y
);
assign y = a - b + c;
endmodule
EOT
hierarchy -auto-top
proc
csa_tree
select -assert-count 2 t:$fa
select -assert-count 1 t:$add
select -assert-count 1 t:$not
select -assert-none t:$sub
design -reset
read_verilog <<EOT
module sub_mixed(
input [7:0] a, b, c, d,
output [7:0] y
);
assign y = a + b - c + d;
endmodule
EOT
hierarchy -auto-top
proc
csa_tree
select -assert-count 3 t:$fa
select -assert-count 1 t:$add
select -assert-count 1 t:$not
select -assert-none t:$sub
design -reset
read_verilog <<EOT
module sub_all(
input [7:0] a, b, c, d,
output [7:0] y
);
assign y = a - b - c - d;
endmodule
EOT
hierarchy -auto-top
proc
csa_tree
select -assert-count 3 t:$fa
select -assert-count 1 t:$add
select -assert-count 3 t:$not
select -assert-none t:$sub
design -reset
read_verilog <<EOT
module sub_5op(
input [11:0] a, b, c, d, e,
output [11:0] y
);
assign y = a - b + c - d + e;
endmodule
EOT
hierarchy -auto-top
proc
csa_tree
select -assert-count 4 t:$fa
select -assert-count 1 t:$add
select -assert-count 2 t:$not
select -assert-none t:$sub
design -reset
read_verilog <<EOT
module sub_signed(
input signed [7:0] a, b, c, d,
output signed [9:0] y
);
assign y = a + b - c - d;
endmodule
EOT
hierarchy -auto-top
proc
csa_tree
select -assert-count 3 t:$fa
select -assert-count 1 t:$add
select -assert-count 2 t:$not
select -assert-none t:$sub
design -reset
read_verilog <<EOT
module sub_double_neg(
input [7:0] a, b, c,
output [7:0] y
);
wire [7:0] ab = a - b;
assign y = c - ab;
endmodule
EOT
hierarchy -auto-top
proc
csa_tree
select -assert-count 2 t:$fa
select -assert-count 1 t:$add
select -assert-count 1 t:$not
select -assert-none t:$sub
design -reset

42
tests/csa_tree/csa_tree_sub_double_neg.ys
View file

@ -1,42 +0,0 @@
read_verilog sub_double_neg.v
hierarchy -auto-top
proc; opt_clean
csa_tree
stat
select -assert-count 2 t:$fa
select -assert-count 1 t:$add
select -assert-count 1 t:$not
select -assert-none t:$sub
design -reset
# equiv_opt on narrow version
read_verilog equiv_sub_double_neg.v
hierarchy -top equiv_sub_double_neg
proc; opt_clean
equiv_opt csa_tree
design -load postopt
select -assert-count 2 t:$fa
select -assert-count 1 t:$add
design -reset
read_verilog sub_double_neg.v
hierarchy -top sub_double_neg
proc; opt_clean
csa_tree
opt_clean
# 10 - (30 - 20) = 0
sat -set a 30 -set b 20 -set c 10 -prove y 0
# 100 - (50 - 25) = 75
sat -set a 50 -set b 25 -set c 100 -prove y 75
# 0 - (0 - 0) = 0
sat -set a 0 -set b 0 -set c 0 -prove y 0
# 1 - (255 - 1) = 3
sat -set a 255 -set b 1 -set c 1 -prove y 3
log "double negation: ok"

39
tests/csa_tree/csa_tree_sub_equiv.ys
View file

@ -1,39 +0,0 @@
read_verilog equiv_sub_narrow.v
hierarchy -top equiv_sub_mixed
proc; opt_clean
equiv_opt csa_tree
design -load postopt
select -assert-count 3 t:$fa
select -assert-count 1 t:$add
design -reset
log "equiv_sub_mixed: ok"
read_verilog equiv_sub_narrow.v
hierarchy -top equiv_sub_all
proc; opt_clean
equiv_opt csa_tree
design -load postopt
select -assert-count 3 t:$fa
select -assert-count 1 t:$add
design -reset
log "equiv_sub_all: ok"
read_verilog equiv_sub_narrow.v
hierarchy -top equiv_sub_3op
proc; opt_clean
equiv_opt csa_tree
design -load postopt
select -assert-count 2 t:$fa
select -assert-count 1 t:$add
design -reset
log "equiv_sub_3op: ok"
read_verilog equiv_sub_narrow.v
hierarchy -top equiv_sub_signed
proc; opt_clean
equiv_opt csa_tree
design -load postopt
select -assert-count 3 t:$fa
select -assert-count 1 t:$add
design -reset
log "equiv_sub_signed: ok"

10
tests/csa_tree/csa_tree_sub_mixed.ys
View file

@ -1,10 +0,0 @@
read_verilog sub_mixed.v
hierarchy -auto-top
proc; opt_clean
csa_tree
stat
select -assert-count 3 t:$fa
select -assert-count 1 t:$add
select -assert-count 1 t:$not
select -assert-none t:$sub

10
tests/csa_tree/csa_tree_sub_signed.ys
View file

@ -1,10 +0,0 @@
read_verilog sub_signed.v
hierarchy -auto-top
proc; opt_clean
csa_tree
stat
select -assert-count 3 t:$fa
select -assert-count 1 t:$add
select -assert-count 2 t:$not
select -assert-none t:$sub

38
tests/csa_tree/csa_tree_sub_sim.ys
View file

@ -1,38 +0,0 @@
read_verilog sub_mixed.v
hierarchy -top sub_mixed
proc; opt_clean
csa_tree
opt_clean
# 10 + 20 - 5 + 3 = 28
sat -set a 10 -set b 20 -set c 5 -set d 3 -prove y 28
# 0 + 0 - 0 + 0 = 0
sat -set a 0 -set b 0 -set c 0 -set d 0 -prove y 0
# 100 + 50 - 30 + 10 = 130
sat -set a 100 -set b 50 -set c 30 -set d 10 -prove y 130
# 1 + 1 - 255 + 1 = 4
sat -set a 1 -set b 1 -set c 255 -set d 1 -prove y 4
log "sub_mixed vectors: ok"
design -reset
read_verilog sub_all.v
hierarchy -top sub_all
proc; opt_clean
csa_tree
opt_clean
# 100 - 10 - 20 - 30 = 40
sat -set a 100 -set b 10 -set c 20 -set d 30 -prove y 40
# 0 - 0 - 0 - 0 = 0
sat -set a 0 -set b 0 -set c 0 -set d 0 -prove y 0
# 255 - 1 - 1 - 1 = 252
sat -set a 255 -set b 1 -set c 1 -set d 1 -prove y 252
log "sub_all vectors: ok"

87
tests/csa_tree/csa_tree_synth.ys
View file

@ -1,59 +1,70 @@
# ABC synthesis comparison: with vs without csa_tree
# Baseline: no csa_tree
read_verilog abc_bench_add8.v
hierarchy -top abc_bench_add8
proc; opt
# Assert against abc synth with and without csa, hopefully prevent regressions
# Baseline
read_verilog <<EOT
module bench(
input [7:0] a, b, c, d, e, f, g, h,
output [7:0] y
);
assign y = a + b + c + d + e + f + g + h;
endmodule
EOT
hierarchy -auto-top
proc
opt
techmap
abc -g AND,OR,XOR
opt_clean
stat
# Baseline is typically 238 gates — assert it's above 235
select -assert-min 236 t:$_AND_ t:$_OR_ t:$_XOR_ %u
design -reset
# With csa_tree
read_verilog abc_bench_add8.v
hierarchy -top abc_bench_add8
proc; opt
read_verilog <<EOT
module bench(
input [7:0] a, b, c, d, e, f, g, h,
output [7:0] y
);
assign y = a + b + c + d + e + f + g + h;
endmodule
EOT
hierarchy -auto-top
proc
opt
csa_tree
techmap
abc -g AND,OR,XOR
opt_clean
stat
# CSA was giving ~232 gates, assert rough equality
select -assert-max 235 t:$_AND_ t:$_OR_ t:$_XOR_ %u
design -reset
# Depth-optimal: baseline
read_verilog abc_bench_add8.v
hierarchy -top abc_bench_add8
proc; opt
# Depth-otimal baseline
read_verilog <<EOT
module bench(
input [7:0] a, b, c, d, e, f, g, h,
output [7:0] y
);
assign y = a + b + c + d + e + f + g + h;
endmodule
EOT
hierarchy -auto-top
proc
opt
techmap
abc -D 1
opt_clean
stat
# Baseline depth-optimal is ~243 cells
select -assert-min 240 t:$_AND_ t:$_NAND_ t:$_OR_ t:$_NOR_ t:$_XOR_ t:$_XNOR_ t:$_NOT_ %u
design -reset
# Depth-optimal: with csa_tree
read_verilog abc_bench_add8.v
hierarchy -top abc_bench_add8
proc; opt
# Depth-optimal with csa_tree
read_verilog <<EOT
module bench(
input [7:0] a, b, c, d, e, f, g, h,
output [7:0] y
);
assign y = a + b + c + d + e + f + g + h;
endmodule
EOT
hierarchy -auto-top
proc
opt
csa_tree
techmap
abc -D 1
opt_clean
stat
# CSA depth-optimal is ~232 cells, must be under baseline
select -assert-max 236 t:$_AND_ t:$_NAND_ t:$_OR_ t:$_NOR_ t:$_XOR_ t:$_XNOR_ t:$_NOT_ %u
log "CSA depth and gate count: ok"
design -reset

8
tests/csa_tree/csa_tree_two_chains.ys
View file

@ -1,8 +0,0 @@
read_verilog add_two_chains.v
hierarchy -auto-top
proc; opt_clean
csa_tree
stat
select -assert-count 4 t:$fa
select -assert-count 2 t:$add

8
tests/csa_tree/csa_tree_wide_output.ys
View file

@ -1,8 +0,0 @@
read_verilog add_wide_output.v
hierarchy -auto-top
proc; opt_clean
csa_tree
stat
select -assert-count 2 t:$fa
select -assert-count 1 t:$add

59
tests/csa_tree/equiv_narrow.v
View file

@ -1,59 +0,0 @@
// Narrow-width test designs for SAT equivalence (4-bit to keep SAT fast)
module equiv_add3(
input [3:0] a, b, c,
output [3:0] y
);
assign y = a + b + c;
endmodule
module equiv_add4(
input [3:0] a, b, c, d,
output [3:0] y
);
assign y = a + b + c + d;
endmodule
module equiv_add5(
input [3:0] a, b, c, d, e,
output [3:0] y
);
assign y = a + b + c + d + e;
endmodule
module equiv_add8(
input [3:0] a, b, c, d, e, f, g, h,
output [3:0] y
);
assign y = a + b + c + d + e + f + g + h;
endmodule
module equiv_signed(
input signed [3:0] a, b, c, d,
output signed [5:0] y
);
assign y = a + b + c + d;
endmodule
module equiv_mixed_w(
input [1:0] a,
input [3:0] b,
input [5:0] c,
output [5:0] y
);
assign y = a + b + c;
endmodule
module equiv_repeated(
input [3:0] a,
output [3:0] y
);
assign y = a + a + a + a;
endmodule
module equiv_1bit_wide(
input a, b, c, d,
output [3:0] y
);
assign y = a + b + c + d;
endmodule

7
tests/csa_tree/equiv_sub_double_neg.v
View file

@ -1,7 +0,0 @@
module equiv_sub_double_neg(
input [3:0] a, b, c,
output [3:0] y
);
wire [3:0] ab = a - b;
assign y = c - ab;
endmodule

27
tests/csa_tree/equiv_sub_narrow.v
View file

@ -1,27 +0,0 @@
module equiv_sub_mixed(
input [3:0] a, b, c, d,
output [3:0] y
);
assign y = a + b - c + d;
endmodule
module equiv_sub_all(
input [3:0] a, b, c, d,
output [3:0] y
);
assign y = a - b - c - d;
endmodule
module equiv_sub_3op(
input [3:0] a, b, c,
output [3:0] y
);
assign y = a - b + c;
endmodule
module equiv_sub_signed(
input signed [3:0] a, b, c, d,
output signed [5:0] y
);
assign y = a + b - c - d;
endmodule

24
tests/csa_tree/fir_4tap.v
View file

@ -1,24 +0,0 @@
module fir_4tap(
input clk,
input [15:0] x,
input [15:0] c0, c1, c2, c3,
output reg [31:0] y
);
reg [15:0] x1, x2, x3;
always @(posedge clk) begin
x1 <= x;
x2 <= x1;
x3 <= x2;
end
wire [31:0] p0 = x * c0;
wire [31:0] p1 = x1 * c1;
wire [31:0] p2 = x2 * c2;
wire [31:0] p3 = x3 * c3;
wire [31:0] sum = p0 + p1 + p2 + p3;
always @(posedge clk)
y <= sum;
endmodule

4
tests/csa_tree/run-test.sh
View file

@ -2,6 +2,6 @@
source ../common-env.sh
set -e
for x in *.ys; do
echo "Running $x.."
../../yosys -ql ${x%.ys}.log $x
echo "Running $x.."
../../yosys -ql ${x%.ys}.log $x
done

6
tests/csa_tree/sim_add4.v
View file

@ -1,6 +0,0 @@
module sim_add4(
input [7:0] a, b, c, d,
output [7:0] y
);
assign y = a + b + c + d;
endmodule

6
tests/csa_tree/sub_2op_neg.v
View file

@ -1,6 +0,0 @@
module sub_2op_neg(
input [7:0] a, b,
output [7:0] y
);
assign y = a - b;
endmodule

6
tests/csa_tree/sub_3op.v
View file

@ -1,6 +0,0 @@
module sub_3op(
input [7:0] a, b, c,
output [7:0] y
);
assign y = a - b + c;
endmodule

6
tests/csa_tree/sub_5op.v
View file

@ -1,6 +0,0 @@
module sub_5op(
input [11:0] a, b, c, d, e,
output [11:0] y
);
assign y = a - b + c - d + e;
endmodule

6
tests/csa_tree/sub_all.v
View file

@ -1,6 +0,0 @@
module sub_all(
input [7:0] a, b, c, d,
output [7:0] y
);
assign y = a - b - c - d;
endmodule

7
tests/csa_tree/sub_double_neg.v
View file

@ -1,7 +0,0 @@
module sub_double_neg(
input [7:0] a, b, c,
output [7:0] y
);
wire [7:0] ab = a - b;
assign y = c - ab;
endmodule

6
tests/csa_tree/sub_mixed.v
View file

@ -1,6 +0,0 @@
module sub_mixed(
input [7:0] a, b, c, d,
output [7:0] y
);
assign y = a + b - c + d;
endmodule

6
tests/csa_tree/sub_signed.v
View file

@ -1,6 +0,0 @@
module sub_signed(
input signed [7:0] a, b, c, d,
output signed [9:0] y
);
assign y = a + b - c - d;
endmodule