From 4ce8e7d1df4b261d133ac835b698526debf8a52c Mon Sep 17 00:00:00 2001 From: nella Date: Mon, 16 Mar 2026 16:23:42 +0100 Subject: [PATCH] Tighten csa tests. --- tests/csa_tree/csa_tree_16input.ys | 2 +- tests/csa_tree/csa_tree_1bit.ys | 4 +--- tests/csa_tree/csa_tree_1bit_wide_out.ys | 2 +- tests/csa_tree/csa_tree_3input.ys | 7 ++----- tests/csa_tree/csa_tree_5input.ys | 9 +++------ tests/csa_tree/csa_tree_8input.ys | 3 +-- tests/csa_tree/csa_tree_const.ys | 7 +++---- tests/csa_tree/csa_tree_equiv.ys | 22 +++++++++++----------- tests/csa_tree/csa_tree_fir.ys | 8 ++++---- tests/csa_tree/csa_tree_idempotent.ys | 6 ++---- tests/csa_tree/csa_tree_mixed_widths.ys | 7 +++---- tests/csa_tree/csa_tree_partial_chain.ys | 4 ++-- tests/csa_tree/csa_tree_repeated.ys | 2 +- tests/csa_tree/csa_tree_signed.ys | 7 +++---- tests/csa_tree/csa_tree_sub_3op.ys | 5 ++--- tests/csa_tree/csa_tree_sub_5op.ys | 3 ++- tests/csa_tree/csa_tree_sub_all.ys | 3 ++- tests/csa_tree/csa_tree_sub_double_neg.ys | 14 ++++++-------- tests/csa_tree/csa_tree_sub_equiv.ys | 10 ++++------ tests/csa_tree/csa_tree_sub_mixed.ys | 5 ++--- tests/csa_tree/csa_tree_sub_signed.ys | 3 ++- tests/csa_tree/csa_tree_two_chains.ys | 8 ++++---- tests/csa_tree/csa_tree_wide_output.ys | 8 ++++---- 23 files changed, 66 insertions(+), 83 deletions(-) diff --git a/tests/csa_tree/csa_tree_16input.ys b/tests/csa_tree/csa_tree_16input.ys index 230d5f845..46f51d44c 100644 --- a/tests/csa_tree/csa_tree_16input.ys +++ b/tests/csa_tree/csa_tree_16input.ys @@ -4,5 +4,5 @@ proc; opt_clean csa_tree stat -select -assert-min 5 t:$fa +select -assert-count 14 t:$fa select -assert-count 1 t:$add diff --git a/tests/csa_tree/csa_tree_1bit.ys b/tests/csa_tree/csa_tree_1bit.ys index 4245f3d24..4c1f7745a 100644 --- a/tests/csa_tree/csa_tree_1bit.ys +++ b/tests/csa_tree/csa_tree_1bit.ys @@ -1,10 +1,8 @@ -# Test csa_tree with single-bit operands — carry shift edge case - read_verilog add_1bit.v hierarchy -auto-top proc; opt_clean csa_tree stat -select -assert-min 1 t:$fa +select -assert-count 1 t:$fa select -assert-count 1 t:$add diff --git a/tests/csa_tree/csa_tree_1bit_wide_out.ys b/tests/csa_tree/csa_tree_1bit_wide_out.ys index 5e2605340..675fbc0a3 100644 --- a/tests/csa_tree/csa_tree_1bit_wide_out.ys +++ b/tests/csa_tree/csa_tree_1bit_wide_out.ys @@ -4,5 +4,5 @@ proc; opt_clean csa_tree stat -select -assert-min 1 t:$fa +select -assert-count 2 t:$fa select -assert-count 1 t:$add diff --git a/tests/csa_tree/csa_tree_3input.ys b/tests/csa_tree/csa_tree_3input.ys index 68ff2ff2e..9e7c9aaf2 100644 --- a/tests/csa_tree/csa_tree_3input.ys +++ b/tests/csa_tree/csa_tree_3input.ys @@ -1,11 +1,8 @@ -# Test csa_tree on 3-operand chain — minimal trigger case - read_verilog add_chain_3.v hierarchy -auto-top proc; opt_clean -equiv_opt csa_tree -design -load postopt +csa_tree +stat select -assert-count 1 t:$fa select -assert-count 1 t:$add - diff --git a/tests/csa_tree/csa_tree_5input.ys b/tests/csa_tree/csa_tree_5input.ys index dadea092f..ef26e21ce 100644 --- a/tests/csa_tree/csa_tree_5input.ys +++ b/tests/csa_tree/csa_tree_5input.ys @@ -1,11 +1,8 @@ -# Test csa_tree with 5 operands — tree with remainders - read_verilog add_chain_5.v hierarchy -auto-top proc; opt_clean -equiv_opt csa_tree -design -load postopt +csa_tree +stat -select -assert-min 2 t:$fa +select -assert-count 3 t:$fa select -assert-count 1 t:$add - diff --git a/tests/csa_tree/csa_tree_8input.ys b/tests/csa_tree/csa_tree_8input.ys index 23d2d698a..fc5148edf 100644 --- a/tests/csa_tree/csa_tree_8input.ys +++ b/tests/csa_tree/csa_tree_8input.ys @@ -4,6 +4,5 @@ proc; opt_clean csa_tree stat -select -assert-min 1 t:$fa +select -assert-count 6 t:$fa select -assert-count 1 t:$add - diff --git a/tests/csa_tree/csa_tree_const.ys b/tests/csa_tree/csa_tree_const.ys index 75d0bc1d7..be53bba11 100644 --- a/tests/csa_tree/csa_tree_const.ys +++ b/tests/csa_tree/csa_tree_const.ys @@ -1,9 +1,8 @@ read_verilog add_with_const.v hierarchy -auto-top proc; opt_clean -equiv_opt csa_tree -design -load postopt +csa_tree +stat -select -assert-min 1 t:$fa +select -assert-count 2 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 index ac976e1b3..360b9d30e 100644 --- a/tests/csa_tree/csa_tree_equiv.ys +++ b/tests/csa_tree/csa_tree_equiv.ys @@ -1,4 +1,4 @@ -# Test bit correctness +# Equivalence tests using narrow operands read_verilog equiv_narrow.v hierarchy -top equiv_add3 @@ -8,34 +8,34 @@ design -load postopt select -assert-count 1 t:$fa select -assert-count 1 t:$add design -reset -log "equiv_add3: ok" +log "equiv_add3" 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 2 t:$fa select -assert-count 1 t:$add design -reset -log "equiv_add4: ok" +log "equiv_add4" 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 3 t:$fa select -assert-count 1 t:$add design -reset -log "equiv_add5: ok" +log "equiv_add5" 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 6 t:$fa select -assert-count 1 t:$add design -reset log "equiv_add8: ok" @@ -45,7 +45,7 @@ hierarchy -top equiv_signed proc; opt_clean equiv_opt csa_tree design -load postopt -select -assert-min 1 t:$fa +select -assert-count 2 t:$fa select -assert-count 1 t:$add design -reset log "equiv_signed: ok" @@ -55,7 +55,7 @@ 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:$fa select -assert-count 1 t:$add design -reset log "equiv_mixed_w: ok" @@ -65,7 +65,7 @@ hierarchy -top equiv_repeated proc; opt_clean equiv_opt csa_tree design -load postopt -select -assert-min 1 t:$fa +select -assert-count 2 t:$fa select -assert-count 1 t:$add design -reset log "equiv_repeated: ok" @@ -75,7 +75,7 @@ hierarchy -top equiv_1bit_wide proc; opt_clean equiv_opt csa_tree design -load postopt -select -assert-min 1 t:$fa +select -assert-count 2 t:$fa select -assert-count 1 t:$add design -reset log "equiv_1bit_wide: ok" diff --git a/tests/csa_tree/csa_tree_fir.ys b/tests/csa_tree/csa_tree_fir.ys index 59aac98b0..89d60af03 100644 --- a/tests/csa_tree/csa_tree_fir.ys +++ b/tests/csa_tree/csa_tree_fir.ys @@ -1,8 +1,8 @@ read_verilog fir_4tap.v hierarchy -auto-top proc; opt_clean -equiv_opt -async2sync csa_tree -design -load postopt - -select -assert-min 1 t:$fa +csa_tree +stat +select -assert-count 2 t:$fa +select -assert-count 1 t:$add diff --git a/tests/csa_tree/csa_tree_idempotent.ys b/tests/csa_tree/csa_tree_idempotent.ys index 4bc7dc354..138edb4ae 100644 --- a/tests/csa_tree/csa_tree_idempotent.ys +++ b/tests/csa_tree/csa_tree_idempotent.ys @@ -1,17 +1,15 @@ -# 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 6 t:$fa select -assert-count 1 t:$add csa_tree stat -select -assert-min 1 t:$fa +select -assert-count 6 t:$fa select -assert-count 1 t:$add select -assert-none t:$sub diff --git a/tests/csa_tree/csa_tree_mixed_widths.ys b/tests/csa_tree/csa_tree_mixed_widths.ys index 1cecae201..e324c17ca 100644 --- a/tests/csa_tree/csa_tree_mixed_widths.ys +++ b/tests/csa_tree/csa_tree_mixed_widths.ys @@ -1,9 +1,8 @@ read_verilog add_mixed_widths.v hierarchy -auto-top proc; opt_clean -equiv_opt csa_tree -design -load postopt +csa_tree +stat -select -assert-min 1 t:$fa +select -assert-count 2 t:$fa select -assert-count 1 t:$add - diff --git a/tests/csa_tree/csa_tree_partial_chain.ys b/tests/csa_tree/csa_tree_partial_chain.ys index 3852c4f9d..ba857292e 100644 --- a/tests/csa_tree/csa_tree_partial_chain.ys +++ b/tests/csa_tree/csa_tree_partial_chain.ys @@ -4,5 +4,5 @@ proc; opt_clean csa_tree stat -select -assert-min 1 t:$fa -select -assert-min 2 t:$add +select -assert-count 2 t:$fa +select -assert-count 2 t:$add diff --git a/tests/csa_tree/csa_tree_repeated.ys b/tests/csa_tree/csa_tree_repeated.ys index 7e1c2ec51..b4581d2b4 100644 --- a/tests/csa_tree/csa_tree_repeated.ys +++ b/tests/csa_tree/csa_tree_repeated.ys @@ -4,5 +4,5 @@ proc; opt_clean csa_tree stat -select -assert-min 1 t:$fa +select -assert-count 2 t:$fa select -assert-count 1 t:$add diff --git a/tests/csa_tree/csa_tree_signed.ys b/tests/csa_tree/csa_tree_signed.ys index 7e29cc123..1093f7330 100644 --- a/tests/csa_tree/csa_tree_signed.ys +++ b/tests/csa_tree/csa_tree_signed.ys @@ -1,9 +1,8 @@ read_verilog add_signed.v hierarchy -auto-top proc; opt_clean -equiv_opt csa_tree -design -load postopt +csa_tree +stat -select -assert-min 1 t:$fa +select -assert-count 2 t:$fa select -assert-count 1 t:$add - diff --git a/tests/csa_tree/csa_tree_sub_3op.ys b/tests/csa_tree/csa_tree_sub_3op.ys index 70801d30c..536f65bd7 100644 --- a/tests/csa_tree/csa_tree_sub_3op.ys +++ b/tests/csa_tree/csa_tree_sub_3op.ys @@ -1,11 +1,10 @@ -# Test minimal sub chain - read_verilog sub_3op.v hierarchy -auto-top proc; opt_clean csa_tree stat -select -assert-min 1 t:$fa +select -assert-count 2 t:$fa select -assert-count 1 t:$add +select -assert-count 1 t:$not select -assert-none t:$sub diff --git a/tests/csa_tree/csa_tree_sub_5op.ys b/tests/csa_tree/csa_tree_sub_5op.ys index 62c4a80ff..b40c97084 100644 --- a/tests/csa_tree/csa_tree_sub_5op.ys +++ b/tests/csa_tree/csa_tree_sub_5op.ys @@ -4,6 +4,7 @@ proc; opt_clean csa_tree stat -select -assert-min 2 t:$fa +select -assert-count 4 t:$fa select -assert-count 1 t:$add +select -assert-count 2 t:$not select -assert-none t:$sub diff --git a/tests/csa_tree/csa_tree_sub_all.ys b/tests/csa_tree/csa_tree_sub_all.ys index 8e47bb0db..ba0503462 100644 --- a/tests/csa_tree/csa_tree_sub_all.ys +++ b/tests/csa_tree/csa_tree_sub_all.ys @@ -4,6 +4,7 @@ proc; opt_clean csa_tree stat -select -assert-min 1 t:$fa +select -assert-count 3 t:$fa select -assert-count 1 t:$add +select -assert-count 3 t:$not select -assert-none t:$sub diff --git a/tests/csa_tree/csa_tree_sub_double_neg.ys b/tests/csa_tree/csa_tree_sub_double_neg.ys index f3911aee3..b3a524abb 100644 --- a/tests/csa_tree/csa_tree_sub_double_neg.ys +++ b/tests/csa_tree/csa_tree_sub_double_neg.ys @@ -1,13 +1,12 @@ -# 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 2 t:$fa select -assert-count 1 t:$add +select -assert-count 1 t:$not select -assert-none t:$sub design -reset @@ -18,27 +17,26 @@ 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 2 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 +# 10 - (30 - 20) = 0 sat -set a 30 -set b 20 -set c 10 -prove y 0 -# 100 - (50 - 25) = 100 - 25 = 75 +# 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) = 1 - 254 = 3 +# 1 - (255 - 1) = 3 sat -set a 255 -set b 1 -set c 1 -prove y 3 log "double negation: ok" diff --git a/tests/csa_tree/csa_tree_sub_equiv.ys b/tests/csa_tree/csa_tree_sub_equiv.ys index b1be6bebe..7138b010c 100644 --- a/tests/csa_tree/csa_tree_sub_equiv.ys +++ b/tests/csa_tree/csa_tree_sub_equiv.ys @@ -1,11 +1,9 @@ -# Test equiv_opt on narrow sub designs - read_verilog equiv_sub_narrow.v hierarchy -top equiv_sub_mixed proc; opt_clean equiv_opt csa_tree design -load postopt -select -assert-min 1 t:$fa +select -assert-count 3 t:$fa select -assert-count 1 t:$add design -reset log "equiv_sub_mixed: ok" @@ -15,7 +13,7 @@ hierarchy -top equiv_sub_all proc; opt_clean equiv_opt csa_tree design -load postopt -select -assert-min 1 t:$fa +select -assert-count 3 t:$fa select -assert-count 1 t:$add design -reset log "equiv_sub_all: ok" @@ -25,7 +23,7 @@ hierarchy -top equiv_sub_3op proc; opt_clean equiv_opt csa_tree design -load postopt -select -assert-min 1 t:$fa +select -assert-count 2 t:$fa select -assert-count 1 t:$add design -reset log "equiv_sub_3op: ok" @@ -35,7 +33,7 @@ hierarchy -top equiv_sub_signed proc; opt_clean equiv_opt csa_tree design -load postopt -select -assert-min 1 t:$fa +select -assert-count 3 t:$fa select -assert-count 1 t:$add design -reset log "equiv_sub_signed: ok" diff --git a/tests/csa_tree/csa_tree_sub_mixed.ys b/tests/csa_tree/csa_tree_sub_mixed.ys index 8fea5f0d2..92e0e1a0d 100644 --- a/tests/csa_tree/csa_tree_sub_mixed.ys +++ b/tests/csa_tree/csa_tree_sub_mixed.ys @@ -1,11 +1,10 @@ -# Test mixed csa chain - read_verilog sub_mixed.v hierarchy -auto-top proc; opt_clean csa_tree stat -select -assert-min 1 t:$fa +select -assert-count 3 t:$fa select -assert-count 1 t:$add +select -assert-count 1 t:$not select -assert-none t:$sub diff --git a/tests/csa_tree/csa_tree_sub_signed.ys b/tests/csa_tree/csa_tree_sub_signed.ys index 78caf5a2e..ad3b0cfb4 100644 --- a/tests/csa_tree/csa_tree_sub_signed.ys +++ b/tests/csa_tree/csa_tree_sub_signed.ys @@ -4,6 +4,7 @@ proc; opt_clean csa_tree stat -select -assert-min 1 t:$fa +select -assert-count 3 t:$fa select -assert-count 1 t:$add +select -assert-count 2 t:$not select -assert-none t:$sub diff --git a/tests/csa_tree/csa_tree_two_chains.ys b/tests/csa_tree/csa_tree_two_chains.ys index bc852071b..42d5c87b9 100644 --- a/tests/csa_tree/csa_tree_two_chains.ys +++ b/tests/csa_tree/csa_tree_two_chains.ys @@ -1,8 +1,8 @@ read_verilog add_two_chains.v hierarchy -auto-top proc; opt_clean -equiv_opt csa_tree -design -load postopt +csa_tree +stat -select -assert-min 2 t:$fa -select -assert-count 2 t:$add \ No newline at end of file +select -assert-count 4 t:$fa +select -assert-count 2 t:$add diff --git a/tests/csa_tree/csa_tree_wide_output.ys b/tests/csa_tree/csa_tree_wide_output.ys index 82003ff63..ccb160f5c 100644 --- a/tests/csa_tree/csa_tree_wide_output.ys +++ b/tests/csa_tree/csa_tree_wide_output.ys @@ -1,8 +1,8 @@ read_verilog add_wide_output.v hierarchy -auto-top proc; opt_clean -equiv_opt csa_tree -design -load postopt +csa_tree +stat -select -assert-min 1 t:$fa -select -assert-count 1 t:$add \ No newline at end of file +select -assert-count 2 t:$fa +select -assert-count 1 t:$add