# =============================================================================
# Test 1: SAT equivalence — VPS byte-write vs case-statement reference
# Proves opt_vps produces a logically equivalent circuit to hand-written
# case statements for a 32-bit register with 4 byte lanes.
# =============================================================================
log -header "SAT equivalence: byte-write VPS vs case-statement ref"
log -push
design -reset
verific -cfg veri_optimize_wide_selector 1
verific -cfg db_infer_wide_muxes_post_elaboration 0

read -sv opt_vps_byte_write.sv
verific -import opt_vps_byte_write
proc; opt_clean
opt_vps; opt_clean
rename opt_vps_byte_write gate

read -sv opt_vps_byte_write_ref.sv
verific -import opt_vps_byte_write
proc; opt_clean
rename opt_vps_byte_write gold

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

# =============================================================================
# Test 2: SAT self-equivalence — byte-write before vs after opt_vps
# Proves opt_vps does not change the functional behavior.
# =============================================================================
log -header "SAT self-equivalence: byte-write before vs after opt_vps"
log -push
design -reset
verific -cfg veri_optimize_wide_selector 1
verific -cfg db_infer_wide_muxes_post_elaboration 0

read -sv opt_vps_byte_write.sv
verific -import opt_vps_byte_write
proc; opt_clean
rename opt_vps_byte_write gold

read -sv opt_vps_byte_write.sv
verific -import opt_vps_byte_write
proc; opt_clean
opt_vps; opt_clean
rename opt_vps_byte_write gate

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

# =============================================================================
# Test 3: SAT self-equivalence — wide (128-bit, 16-bit lanes)
# Ensures opt_vps is correct on a larger design with 8 lanes.
# =============================================================================
log -header "SAT self-equivalence: wide 128-bit VPS"
log -push
design -reset
verific -cfg veri_optimize_wide_selector 1
verific -cfg db_infer_wide_muxes_post_elaboration 0

read -sv opt_vps_wide.sv
verific -import opt_vps_wide
proc; opt_clean
rename opt_vps_wide gold

read -sv opt_vps_wide.sv
verific -import opt_vps_wide
proc; opt_clean
opt_vps; opt_clean
rename opt_vps_wide gate

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

# =============================================================================
# Test 4: Cell count verification — byte-write
# After opt_vps, all $pmux and $reduce_or cells should be eliminated and
# replaced with per-lane $eq/$and/$mux cells.
# =============================================================================
log -header "Cell counts: byte-write post-opt_vps"
log -push
design -reset
verific -cfg veri_optimize_wide_selector 1
verific -cfg db_infer_wide_muxes_post_elaboration 0

read -sv opt_vps_byte_write.sv
verific -import opt_vps_byte_write
proc; opt_clean
opt_vps; opt_clean

select -assert-none t:$pmux
select -assert-none t:$reduce_or
select -assert-count 4 t:$eq
select -assert-count 4 t:$and
select -assert-count 4 t:$mux
select -assert-count 1 t:$dff
design -reset
log -pop

# =============================================================================
# Test 5: Cell count verification — wide
# Same as above but for the wider 128-bit / 8-lane case.
# =============================================================================
log -header "Cell counts: wide post-opt_vps"
log -push
design -reset
verific -cfg veri_optimize_wide_selector 1
verific -cfg db_infer_wide_muxes_post_elaboration 0

read -sv opt_vps_wide.sv
verific -import opt_vps_wide
proc; opt_clean
opt_vps; opt_clean

select -assert-none t:$pmux
select -assert-none t:$reduce_or
select -assert-count 1 t:$dff
design -reset
log -pop

# =============================================================================
# Test 6: Negative case — no VPS pattern
# A simple mux-based register should not trigger opt_vps.
# =============================================================================
log -header "Negative: non-VPS design unchanged"
log -push
design -reset
verific -cfg veri_optimize_wide_selector 1
verific -cfg db_infer_wide_muxes_post_elaboration 0

read -sv opt_vps_no_match.sv
verific -import opt_vps_no_match
proc; opt_clean

stat
opt_vps
stat

select -assert-none t:$pmux
select -assert-none t:$eq w:*vps*
select -assert-count 1 t:$mux
select -assert-count 1 t:$dff
design -reset
log -pop