diff --git a/tests/csa_tree/csa_tree_idempotent.ys b/tests/csa_tree/csa_tree_idempotent.ys new file mode 100644 index 000000000..4bc7dc354 --- /dev/null +++ b/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 diff --git a/tests/csa_tree/csa_tree_sub_double_neg.ys b/tests/csa_tree/csa_tree_sub_double_neg.ys new file mode 100644 index 000000000..f3911aee3 --- /dev/null +++ b/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" diff --git a/tests/csa_tree/equiv_sub_double_neg.v b/tests/csa_tree/equiv_sub_double_neg.v new file mode 100644 index 000000000..8d03da23f --- /dev/null +++ b/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 diff --git a/tests/csa_tree/sub_double_neg.v b/tests/csa_tree/sub_double_neg.v new file mode 100644 index 000000000..7172ccd09 --- /dev/null +++ b/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