# Tests for opt_argmax.

log -header "Small masked argmax self-equivalence"
log -push
design -reset
verific -cfg veri_optimize_wide_selector 1
verific -cfg db_infer_wide_muxes_post_elaboration 0
read -sv opt_argmax.sv
verific -import opt_argmax_w8
proc; opt_clean
rename opt_argmax_w8 gold

read -sv opt_argmax.sv
verific -import opt_argmax_w8
proc; opt_clean
select -module opt_argmax_w8
opt_argmax
select -clear
opt_clean
rename opt_argmax_w8 gate

miter -equiv -flatten -make_assert gold gate miter
hierarchy -top miter
proc; opt; memory; opt
sat -prove-asserts -verify
design -reset
log -pop

log -header "Basic masked argmax structural rewrite"
log -push
design -reset
verific -cfg veri_optimize_wide_selector 1
verific -cfg db_infer_wide_muxes_post_elaboration 0
read -sv opt_argmax.sv
verific -import opt_argmax_basic
proc; opt_clean
opt_argmax
opt_clean
select -assert-min 1 w:*argmax*
select -assert-count 16 t:$bmux
select -assert-count 15 t:$lt
select -assert-count 29 t:$mux
select -assert-count 30 t:$and
select -assert-count 29 t:$or
select -assert-count 15 t:$not
select -assert-none c:LessThan_*
design -reset
log -pop

log -header "Flat-bus masked argmax self-equivalence"
log -push
design -reset
verific -cfg veri_optimize_wide_selector 1
verific -cfg db_infer_wide_muxes_post_elaboration 0
read -sv opt_argmax.sv
verific -import opt_argmax_flat
proc; opt_clean
rename opt_argmax_flat gold

read -sv opt_argmax.sv
verific -import opt_argmax_flat
proc; opt_clean
select -module opt_argmax_flat
opt_argmax
select -clear
opt_clean
select -assert-min 1 w:*argmax*
rename opt_argmax_flat gate

miter -equiv -flatten -make_assert gold gate miter
hierarchy -top miter
proc; opt; memory; opt
sat -prove-asserts -verify
design -reset
log -pop

log -header "Identity-index masked argmax self-equivalence"
log -push
design -reset
verific -cfg veri_optimize_wide_selector 1
verific -cfg db_infer_wide_muxes_post_elaboration 0
read -sv opt_argmax.sv
verific -import opt_argmax_identity_w8
proc; opt_clean
rename opt_argmax_identity_w8 gold

read -sv opt_argmax.sv
verific -import opt_argmax_identity_w8
proc; opt_clean
select -module opt_argmax_identity_w8
opt_argmax
select -clear
opt_clean
select -assert-min 1 w:*argmax*
rename opt_argmax_identity_w8 gate

miter -equiv -flatten -make_assert gold gate miter
hierarchy -top miter
proc; opt; memory; opt
sat -prove-asserts -verify
design -reset
log -pop

log -header "Identity-index masked argmax structural rewrite"
log -push
design -reset
verific -cfg veri_optimize_wide_selector 1
verific -cfg db_infer_wide_muxes_post_elaboration 0
read -sv opt_argmax.sv
verific -import opt_argmax_identity_w16
proc; opt_clean
opt_argmax
opt_clean
select -assert-min 1 w:*argmax*
select -assert-none c:*argmax_val*
select -assert-none c:LessThan_*
design -reset
log -pop

log -header "Scaled masked argmax: 8 entries structural"
log -push
design -reset
verific -cfg veri_optimize_wide_selector 1
verific -cfg db_infer_wide_muxes_post_elaboration 0
read -sv opt_argmax.sv
verific -import opt_argmax_w8
proc; opt_clean
opt_argmax
opt_clean
select -assert-min 1 w:*argmax*
design -reset
log -pop

log -header "Scaled masked argmax: 32 entries structural"
log -push
design -reset
verific -cfg veri_optimize_wide_selector 1
verific -cfg db_infer_wide_muxes_post_elaboration 0
read -sv opt_argmax.sv
verific -import opt_argmax_w32
proc; opt_clean
opt_argmax
opt_clean
select -assert-min 1 w:*argmax*
design -reset
log -pop

log -header "Value width edge: 1-bit values"
log -push
design -reset
verific -cfg veri_optimize_wide_selector 1
verific -cfg db_infer_wide_muxes_post_elaboration 0
read -sv opt_argmax.sv
verific -import opt_argmax_value_w1
proc; opt_clean
rename opt_argmax_value_w1 gold

read -sv opt_argmax.sv
verific -import opt_argmax_value_w1
proc; opt_clean
select -module opt_argmax_value_w1
opt_argmax
select -clear
opt_clean
select -assert-min 1 w:*argmax*
rename opt_argmax_value_w1 gate

miter -equiv -flatten -make_assert gold gate miter
hierarchy -top miter
proc; opt; memory; opt
sat -prove-asserts -verify
design -reset
log -pop

log -header "Value width edge: 16-bit values"
log -push
design -reset
verific -cfg veri_optimize_wide_selector 1
verific -cfg db_infer_wide_muxes_post_elaboration 0
read -sv opt_argmax.sv
verific -import opt_argmax_value_w16
proc; opt_clean
rename opt_argmax_value_w16 gold

read -sv opt_argmax.sv
verific -import opt_argmax_value_w16
proc; opt_clean
select -module opt_argmax_value_w16
opt_argmax
select -clear
opt_clean
select -assert-min 1 w:*argmax*
rename opt_argmax_value_w16 gate

miter -equiv -flatten -make_assert gold gate miter
hierarchy -top miter
proc; opt; memory; opt
sat -prove-asserts -verify
design -reset
log -pop

log -header "Same module: two independent argmax regions"
log -push
design -reset
verific -cfg veri_optimize_wide_selector 1
verific -cfg db_infer_wide_muxes_post_elaboration 0
read -sv opt_argmax.sv
verific -import opt_argmax_two_regions
proc; opt_clean
rename opt_argmax_two_regions gold

read -sv opt_argmax.sv
verific -import opt_argmax_two_regions
proc; opt_clean
select -module opt_argmax_two_regions
opt_argmax
select -clear
opt_clean
select -assert-min 2 w:*argmax*
rename opt_argmax_two_regions gate

miter -equiv -flatten -make_assert gold gate miter
hierarchy -top miter
proc; opt; memory; opt
sat -prove-asserts -verify
design -reset
log -pop

log -header "Shared consumer of argmax output remains equivalent"
log -push
design -reset
verific -cfg veri_optimize_wide_selector 1
verific -cfg db_infer_wide_muxes_post_elaboration 0
read -sv opt_argmax.sv
verific -import opt_argmax_shared_consumer
proc; opt_clean
rename opt_argmax_shared_consumer gold

read -sv opt_argmax.sv
verific -import opt_argmax_shared_consumer
proc; opt_clean
select -module opt_argmax_shared_consumer
opt_argmax
select -clear
opt_clean
select -assert-min 1 w:*argmax*
rename opt_argmax_shared_consumer gate

miter -equiv -flatten -make_assert gold gate miter
hierarchy -top miter
proc; opt; memory; opt
sat -prove-asserts -verify
design -reset
log -pop

log -header "Max width leaves argmax unchanged"
log -push
design -reset
verific -cfg veri_optimize_wide_selector 1
verific -cfg db_infer_wide_muxes_post_elaboration 0
read -sv opt_argmax.sv
verific -import opt_argmax_basic
proc; opt_clean
opt_argmax -max_width 8
select -assert-none w:*argmax*
design -reset
log -pop

log -header "Negative: non-power-of-two candidate count"
log -push
design -reset
verific -cfg veri_optimize_wide_selector 1
verific -cfg db_infer_wide_muxes_post_elaboration 0
read -sv opt_argmax.sv
verific -import opt_argmax_w12
proc; opt_clean
opt_argmax
select -assert-none w:*argmax*
design -reset
log -pop

log -header "Negative: mismatched index-map width"
log -push
design -reset
verific -cfg veri_optimize_wide_selector 1
verific -cfg db_infer_wide_muxes_post_elaboration 0
read -sv opt_argmax.sv
verific -import opt_argmax_bad_index_width
proc; opt_clean
opt_argmax
select -assert-none w:*argmax*
design -reset
log -pop

log -header "Negative: strict tie behavior changed"
log -push
design -reset
verific -cfg veri_optimize_wide_selector 1
verific -cfg db_infer_wide_muxes_post_elaboration 0
read -sv opt_argmax.sv
verific -import opt_argmax_tie_high
proc; opt_clean
opt_argmax
select -assert-none w:*argmax*
design -reset
log -pop

log -header "Negative: nonzero all-invalid default"
log -push
design -reset
verific -cfg veri_optimize_wide_selector 1
verific -cfg db_infer_wide_muxes_post_elaboration 0
read -sv opt_argmax.sv
verific -import opt_argmax_nonzero_default
proc; opt_clean
opt_argmax
select -assert-none w:*argmax*
design -reset
log -pop

log -header "Negative: min-selection comparator"
log -push
design -reset
verific -cfg veri_optimize_wide_selector 1
verific -cfg db_infer_wide_muxes_post_elaboration 0
read -sv opt_argmax.sv
verific -import opt_argmax_min
proc; opt_clean
opt_argmax
select -assert-none w:*argmax*
design -reset
log -pop

log -header "Negative: unrelated mux logic unchanged"
log -push
design -reset
verific -cfg veri_optimize_wide_selector 1
verific -cfg db_infer_wide_muxes_post_elaboration 0
read -sv opt_argmax.sv
verific -import opt_argmax_unrelated
proc; opt_clean
select -assert-count 1 t:$mux
opt_argmax
select -assert-none w:*argmax*
select -assert-count 1 t:$mux
design -reset
log -pop

log -header "Negative: bmux-heavy unrelated stress module"
log -push
design -reset
verific -cfg veri_optimize_wide_selector 1
verific -cfg db_infer_wide_muxes_post_elaboration 0
read -sv opt_argmax.sv
verific -import opt_argmax_stress_noop
proc; opt_clean
opt_argmax
select -assert-none w:*argmax*
design -reset
log -pop

log -header "Multi-module: only matching module rewrites"
log -push
design -reset
verific -cfg veri_optimize_wide_selector 1
verific -cfg db_infer_wide_muxes_post_elaboration 0
read -sv opt_argmax.sv
verific -import opt_argmax_multi_match opt_argmax_multi_keep
proc; opt_clean
opt_argmax
opt_clean
select -assert-min 1 opt_argmax_multi_match/w:*argmax*
select -assert-none opt_argmax_multi_keep/w:*argmax*
design -reset
log -pop