Edge case tests.

tests/csa_tree/add_1bit_wide_out.v

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

tests/csa_tree/add_multi_const.v

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

tests/csa_tree/add_partial_chain.v

@@ -0,0 +1,9 @@
+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

tests/csa_tree/add_repeated.v

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

tests/csa_tree/csa_tree_1bit_wide_out.ys

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

tests/csa_tree/csa_tree_equiv.ys

@@ -0,0 +1,80 @@
+# Test bit correctness
+read_verilog equiv_narrow.v
+hierarchy -top equiv_add3
+proc; opt_clean
+equiv_opt csa_tree
+design -load postopt
+select -assert-count 1 t:$fa
+select -assert-count 1 t:$add
+design -reset
+log "equiv_add3: ok"
+
+read_verilog equiv_narrow.v
+hierarchy -top equiv_add4
+proc; opt_clean
+equiv_opt csa_tree
+design -load postopt
+select -assert-min 1 t:$fa
+select -assert-count 1 t:$add
+design -reset
+log "equiv_add4: ok"
+
+read_verilog equiv_narrow.v
+hierarchy -top equiv_add5
+proc; opt_clean
+equiv_opt csa_tree
+design -load postopt
+select -assert-min 2 t:$fa
+select -assert-count 1 t:$add
+design -reset
+log "equiv_add5: ok"
+
+read_verilog equiv_narrow.v
+hierarchy -top equiv_add8
+proc; opt_clean
+equiv_opt csa_tree
+design -load postopt
+select -assert-min 1 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
+equiv_opt csa_tree
+design -load postopt
+select -assert-min 1 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
+equiv_opt csa_tree
+design -load postopt
+select -assert-min 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
+equiv_opt csa_tree
+design -load postopt
+select -assert-min 1 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
+equiv_opt csa_tree
+design -load postopt
+select -assert-min 1 t:$fa
+select -assert-count 1 t:$add
+design -reset
+log "equiv_1bit_wide: ok"

tests/csa_tree/csa_tree_multi_const.ys

@@ -0,0 +1,9 @@
+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
+

tests/csa_tree/csa_tree_partial_chain.ys

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

tests/csa_tree/csa_tree_repeated.ys

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

tests/csa_tree/equiv_narrow.v

@@ -0,0 +1,59 @@
+// 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