Support for JasperGold for Formal Property Verification about edalize HOT 2 OPEN

# clear previous settings
clear -all

# this one is debatable. we get several warnings in our flow due to the
# the coding style that we use if we do not disable these warnings. could be absorbed
# into a tool parameter in fusesoc that contains a list of waived messages.
# disables "parameter declared inside package XXX shall be treated as localparam".
set_message -disable VERI-2418

# only needed if coverage is measured, see below
check_cov -init -model {branch statement functional} \
-enable_prove_based_proof_core

#-------------------------------------------------------------------------
# read design sources
#-------------------------------------------------------------------------

# source file must also contain defines known to fusesoc
# in +define format, e.g. +define+FPV_ON
# sv09 could be absorbed into a tool parameter
analyze -sv09 -f sources.f

elaborate -top ${TOP_LEVEL_NAME}

#-------------------------------------------------------------------------
# specify clock(s) and reset(s) and additional constraints
#-------------------------------------------------------------------------

# source any additional TCL sources specified in fusesoc in the same way as 
# waiver or policy files are sourced in the ascentlint flow.
# these tcl files may include:
# nonstandard clock definitions
# additional constraints per block
# demotions (assertions -> assumptions)

# if no additional TCL source defined, use this default:
clock clk_i -both_edges
reset -expr {!rst_ni}

# these assumptions are always good to check as well,
# but we could absorb these in the user TCL files above for simplicity
check_assumptions -conflict
check_assumptions -live
check_assumptions -dead_end

#-------------------------------------------------------------------------
# configure proofgrid
#-------------------------------------------------------------------------

# could be made a tool parameter
# need to uncomment when using LSF:
# set_proofgrid_mode lsf

# this should be made a tool parameters in fusesoc, and just default 
# to some value that is reasonable machine/license wise (something in the range 1-4).
set_proofgrid_per_engine_max_local_jobs 16

#-------------------------------------------------------------------------
# prove all assertions and report
#-------------------------------------------------------------------------

# time limit could be made a tool parameter, and default to 60m or
# something like that
get_reset_info -x_value -with_reset_pin
prove -all -time_limit 120m
report -all     \
       -summary \
       -file fpv.rpt

#-------------------------------------------------------------------------
# check coverage and report
#-------------------------------------------------------------------------

# this needs to take place after proving the assertions
# since this can use a considerable amount of time, I would make this optional
# by adding another tool parameter which is called check_cov
check_cov -measure
check_cov -report -type all -no_return -report_file cover.html \
    -html -force -exclude { reset waived }

# only add this in batch mode
exit