Formality Template

set_host_options -max_cores 8

set_app_var hdlin_interface_only ""
set_app_var verification_failing_point_limit 3000
set_app_var sh_continue_on_error true
set_app_var sh_new_variable_message false
set_app_var synopsys_auto_setup true
set_app_var hdlin_library_auto_correct true
set_app_var verification_set_undriven_signals BINARY:X
set_app_var verification_force_upf_supplies_on false
set_app_var upf_ground_logic_value 0
set_app_var signature_analysis_match_compare_points false

set hdlin_error_on_mismatch_message false

set signature_analysis_allow_subset_match false
set svf_ignore_unqualified_fsm_information true ; # false
set verification_clock_gate_hold_mode any
set hdlin_dyn_array_bnd_check Both
set hdlin_unresolved_modules "black_box"
set verification_ignore_unmatched_implementation_blackbox_input true

set verification_constant_prop_mode top
set verification_set_undriven_signals "0";# usually 0, synthesis, BINARY is more strict

set hdlin_ignore_parallel_case false
set hdlin_ignore_full_case false
set verification_verify_directly_undriven_output false
set verification_netlist_verify_mode on
#analyze_points -all ; # -failing -aborted -unverified -effort low, high

 read_db -technology_lib { \

*/*/*.db}

set top "top_name"

set_svf  -ordered */*/.svf

set RTL_SOURCE_FILES {}

foreach file [glob -nocomplain */*.v */*.sv] {
 lappend RTL_SOURCE_FILES [file normalize $file]
}

read_sverilog -r $RTL_SOURCE_FILES
set_top r:/WORK/$top
current_design $top

# imp as:
set NETLIST_LIST "*/lvro_wrapper_slice.v"

read_verilog -i $NETLIST_LIST
set_top i:/WORK/$top
current_design $top

report_libraries -defects all

#load_upf -i outputs/export/$DESIGN_NAME.upf

report_setup_status

match
verify

report_unmatched_points > unmatch.rpt
report_failing_points > fail.rpt
report_unverified_points > unveri.rpt
report_aborted_points > abort.rpt
report_undriven_nets > undriven.rpt
report_unread_endpoints -all > unread.rpt

report_status > status.rpt
if {[sh grep "Verification FAILED" status.rpt | wc -l] > 0} \
{ save_session -replace ./fm_session }

exit