yosys/tests/csa_tree/csa_tree_equiv.ys

# Equivalence tests using narrow operands

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"

read_verilog equiv_narrow.v
hierarchy -top equiv_add4
proc; opt_clean
equiv_opt csa_tree
design -load postopt
select -assert-count 2 t:$fa
select -assert-count 1 t:$add
design -reset
log "equiv_add4"

read_verilog equiv_narrow.v
hierarchy -top equiv_add5
proc; opt_clean
equiv_opt csa_tree
design -load postopt
select -assert-count 3 t:$fa
select -assert-count 1 t:$add
design -reset
log "equiv_add5"

read_verilog equiv_narrow.v
hierarchy -top equiv_add8
proc; opt_clean
equiv_opt csa_tree
design -load postopt
select -assert-count 6 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-count 2 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-count 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-count 2 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-count 2 t:$fa
select -assert-count 1 t:$add
design -reset
log "equiv_1bit_wide: ok"