# run_lec.tcl — Logic Equivalence Checking (LEC) via Synopsys Formality

set_svf mfma_core.svf

read_sverilog -libname WORK -work_library WORK ../rtl/fpga_mfma_accelerator.sv
set_top fpga_mfma_accelerator

read_verilog -container rev -libname WORK mfma_core_gated.v
set_top -container rev fpga_mfma_accelerator

match
verify

report_passing_points > reports/lec_passing.rpt
report_failing_points > reports/lec_failing.rpt
report_uncompared_points > reports/lec_uncompared.rpt

set unmatched [get_uncompared_points -count]
set failing [get_failing_points -count]
if {$failing > 0 || $unmatched > 0} {
    puts "ERROR: LEC Verification Failed! Failing: $failing, Unmatched: $unmatched"
    exit 1
} else {
    puts "SUCCESS: Post-route netlist is provably equivalent to golden HLS RTL."
}