# Formal Verification Script for {{ DUT }}
# Auto-generated by UCAgent Template Engine

set SCRIPT_DIR [file dirname [info script]]

# RTL Files - glob both .v and .sv from the RTL directory
set RTL_DIR [file join $SCRIPT_DIR "../../{{ DUT }}"]
set RTL_FILES [glob -nocomplain [file join $RTL_DIR *.v] [file join $RTL_DIR *.sv]]

if {[llength $RTL_FILES] == 0} {
    error "ERROR: No RTL source files (*.v / *.sv) found in: $RTL_DIR"
}

# Verification Files (Checker + Wrapper)
lappend RTL_FILES [file join $SCRIPT_DIR {{ DUT }}_checker.sv]
lappend RTL_FILES [file join $SCRIPT_DIR {{ DUT }}_wrapper.sv]

# Read Design with Wrapper as Top
# Using -mfcu (Multi-File Compilation Unit) is recommended for SVA binding and parameter propagation
read_design -top {{ DUT }}_wrapper -sysv -mfcu $RTL_FILES

# Clock and Reset
{%- if extra_config and extra_config.tcl %}
{%- if extra_config.tcl.clock %}
def_clk {{ extra_config.tcl.clock.name | default('clk') }}
{%- else %}
def_clk clk
{%- endif %}
{%- if extra_config.tcl.reset %}
def_rst {{ extra_config.tcl.reset.name | default('rst_n') }} -value {{ extra_config.tcl.reset.value | default(0) }}
{%- else %}
def_rst rst_n -value 0
{%- endif %}
{%- else %}
def_clk clk
def_rst rst_n -value 0
{%- endif %}

# Set timeout (default 100000s)
set_opt -time 100000

# Start proof (default engine)
prove

# Report summary
show_prop -summary

# COI (Cone-of-Influence) coverage analysis
fanin -cover -list -dump

# ==============================================================================
# Pure Tcl VCD Patcher for 'surfer' compatibility
# ==============================================================================

proc find_files_recursively {basedir pattern} {
    set filelist {}
    set items [glob -nocomplain [file join $basedir *]]
    foreach item $items {
        if {[file isdirectory $item]} {
            set subfiles [find_files_recursively $item $pattern]
            foreach subfile $subfiles { lappend filelist $subfile }
        } elseif {[string match $pattern [file tail $item]]} {
            lappend filelist $item
        }
    }
    return $filelist
}

proc patch_vcd_timezero {} {
    set search_dir "."
    if {[catch {find_files_recursively $search_dir "*.vcd"} vcd_files]} { return }
    if {[llength $vcd_files] == 0} { return }

    foreach vcd_path $vcd_files {
        if {![file exists $vcd_path] || ![file isfile $vcd_path]} { continue }
        set fid_in [open $vcd_path r]
        set lines [split [read $fid_in] "\n"]
        close $fid_in

        set new_lines {}
        set in_timezero_block 0
        set patched 0

        foreach line $lines {
            set trimmed_line [string trim $line]
            if {[string match "\$timezero*" $trimmed_line]} {
                set in_timezero_block 1
                set patched 1
                continue
            }
            if {$in_timezero_block && [string match "\$end*" $trimmed_line]} {
                set in_timezero_block 0
                continue
            }
            if {!$in_timezero_block} { lappend new_lines $line }
        }

        if {$patched} {
            set fid_out [open $vcd_path w]
            puts $fid_out [join $new_lines "\n"]
            close $fid_out
        }
    }
}

patch_vcd_timezero
exit
