Add more robsutness tests.

tests/csa_tree/csa_tree_idempotent.ys

@@ -0,0 +1,17 @@
+# Running csa_tree twice, verify nothing changes on second run
+
+read_verilog add_chain_8.v
+hierarchy -auto-top
+proc; opt_clean
+
+csa_tree
+stat
+select -assert-min 1 t:$fa
+select -assert-count 1 t:$add
+
+csa_tree
+stat
+
+select -assert-min 1 t:$fa
+select -assert-count 1 t:$add
+select -assert-none t:$sub

tests/csa_tree/csa_tree_sub_double_neg.ys

@@ -0,0 +1,44 @@
+# Test double negation
+
+read_verilog sub_double_neg.v
+hierarchy -auto-top
+proc; opt_clean
+csa_tree
+stat
+
+select -assert-min 1 t:$fa
+select -assert-count 1 t:$add
+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-min 1 t:$fa
+select -assert-count 1 t:$add
+design -reset
+
+# sat-prove on full width
+read_verilog sub_double_neg.v
+hierarchy -top sub_double_neg
+proc; opt_clean
+csa_tree
+opt_clean
+
+# 10 - (30 - 20) = 10 - 10 = 0
+sat -set a 30 -set b 20 -set c 10 -prove y 0
+
+# 100 - (50 - 25) = 100 - 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) = 1 - 254 = 3
+sat -set a 255 -set b 1 -set c 1 -prove y 3
+
+log "double negation: ok"

tests/csa_tree/equiv_sub_double_neg.v

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

tests/csa_tree/sub_double_neg.v

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