From b6ea0bb4ccafa1da9a01e89319dcdf59f47e3bbf Mon Sep 17 00:00:00 2001 From: nella Date: Fri, 13 Mar 2026 12:33:26 +0100 Subject: [PATCH] Edge case tests. --- tests/csa_tree/add_1bit_wide_out.v | 6 ++ tests/csa_tree/add_multi_const.v | 6 ++ tests/csa_tree/add_partial_chain.v | 9 +++ tests/csa_tree/add_repeated.v | 6 ++ tests/csa_tree/csa_tree_1bit_wide_out.ys | 8 +++ tests/csa_tree/csa_tree_equiv.ys | 80 ++++++++++++++++++++++++ tests/csa_tree/csa_tree_multi_const.ys | 9 +++ tests/csa_tree/csa_tree_partial_chain.ys | 8 +++ tests/csa_tree/csa_tree_repeated.ys | 8 +++ tests/csa_tree/equiv_narrow.v | 59 +++++++++++++++++ 10 files changed, 199 insertions(+) create mode 100644 tests/csa_tree/add_1bit_wide_out.v create mode 100644 tests/csa_tree/add_multi_const.v create mode 100644 tests/csa_tree/add_partial_chain.v create mode 100644 tests/csa_tree/add_repeated.v create mode 100644 tests/csa_tree/csa_tree_1bit_wide_out.ys create mode 100644 tests/csa_tree/csa_tree_equiv.ys create mode 100644 tests/csa_tree/csa_tree_multi_const.ys create mode 100644 tests/csa_tree/csa_tree_partial_chain.ys create mode 100644 tests/csa_tree/csa_tree_repeated.ys create mode 100644 tests/csa_tree/equiv_narrow.v diff --git a/tests/csa_tree/add_1bit_wide_out.v b/tests/csa_tree/add_1bit_wide_out.v new file mode 100644 index 000000000..e1a6ceb51 --- /dev/null +++ b/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 diff --git a/tests/csa_tree/add_multi_const.v b/tests/csa_tree/add_multi_const.v new file mode 100644 index 000000000..7da78f9de --- /dev/null +++ b/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 diff --git a/tests/csa_tree/add_partial_chain.v b/tests/csa_tree/add_partial_chain.v new file mode 100644 index 000000000..a4f20cfa4 --- /dev/null +++ b/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 diff --git a/tests/csa_tree/add_repeated.v b/tests/csa_tree/add_repeated.v new file mode 100644 index 000000000..e3337097b --- /dev/null +++ b/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 diff --git a/tests/csa_tree/csa_tree_1bit_wide_out.ys b/tests/csa_tree/csa_tree_1bit_wide_out.ys new file mode 100644 index 000000000..5e2605340 --- /dev/null +++ b/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 diff --git a/tests/csa_tree/csa_tree_equiv.ys b/tests/csa_tree/csa_tree_equiv.ys new file mode 100644 index 000000000..9c5b4ab44 --- /dev/null +++ b/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" diff --git a/tests/csa_tree/csa_tree_multi_const.ys b/tests/csa_tree/csa_tree_multi_const.ys new file mode 100644 index 000000000..a68b60e33 --- /dev/null +++ b/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 + diff --git a/tests/csa_tree/csa_tree_partial_chain.ys b/tests/csa_tree/csa_tree_partial_chain.ys new file mode 100644 index 000000000..3852c4f9d --- /dev/null +++ b/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 diff --git a/tests/csa_tree/csa_tree_repeated.ys b/tests/csa_tree/csa_tree_repeated.ys new file mode 100644 index 000000000..7e1c2ec51 --- /dev/null +++ b/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 diff --git a/tests/csa_tree/equiv_narrow.v b/tests/csa_tree/equiv_narrow.v new file mode 100644 index 000000000..f4f7ef279 --- /dev/null +++ b/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