# 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"