set REPORTS_DIR "REPORTS_DIR"
set FMRM_UNMATCHED_POINTS_REPORT "FMRM_UNMATCHED_POINTS_REPORT"
set FMRM_FAILING_SESSION_NAME "FMRM_FAILING_SESSION_NAME"
set FMRM_FAILING_POINTS_REPORT "FMRM_FAILING_POINTS_REPORT"
set FMRM_ABORTED_POINTS_REPORT "FMRM_ABORTED_POINTS_REPORT"
set FMRM_ANALYZE_POINTS_REPORT "FMRM_ANALYZE_POINTS_REPORT"
file mkdir ${REPORTS_DIR}/${FMRM_UNMATCHED_POINTS_REPORT}
file mkdir ${REPORTS_DIR}/${FMRM_FAILING_SESSION_NAME}
file mkdir ${REPORTS_DIR}/${FMRM_FAILING_POINTS_REPORT}
file mkdir ${REPORTS_DIR}/${FMRM_ABORTED_POINTS_REPORT}
file mkdir ${REPORTS_DIR}/${FMRM_ANALYZE_POINTS_REPORT}
set_app_var synopsys_auto_setup true
#set_app_var suppress_errors {FMR_VLOG-928 FMR_ELAB-147 FMR_VLOG-079 FMR_ELAB-117}
# Read in the SVF file(s)
set_svf default.svf
//here somelines reading all std libraries,sram libraries, pll and IO pad libraries are given //// i am not showing those lines in this post.
source formality_flist.tcl
set_top r:/WORK/xyz
read_verilog -i { SoC_SVT_35P_RUN3_800MHz_250PS_02April20_gates_1.25nsns.v }
set_top i:/WORK/xyz
#################################################################################
# Match compare points and report unmatched points
#################################################################################
match
report_unmatched_points > ${REPORTS_DIR}/${FMRM_UNMATCHED_POINTS_REPORT}/unmatched_points.rpt
#################################################################################
# Verify and Report
#
# If the verification is not successful, the session will be saved and reports
# will be generated to help debug the failed or inconclusive verification.
#################################################################################
if { ![verify] } {
save_session -replace ${REPORTS_DIR}/${FMRM_FAILING_SESSION_NAME}/failing_session_name.rpt
report_failing_points > ${REPORTS_DIR}/${FMRM_FAILING_POINTS_REPORT}/failing_points.rpt
report_aborted > ${REPORTS_DIR}/${FMRM_ABORTED_POINTS_REPORT}/aborted_points.rpt
# Use analyze_points to help determine the next step in resolving verification
# issues. It runs heuristic analysis to determine if there are potential causes
# other than logical differences for failing or hard verification points.
analyze_points -all > ${REPORTS_DIR}/${FMRM_ANALYZE_POINTS_REPORT}/analyze_points.rpt
# Output this message to be used as a Lynx metric indicating verification failed
#sproc_msg -info "METRIC | BOOLEAN VERIFY.PASS_FORMAL | 0"
} else {
# Output this message to be used as a Lynx metric indicating verification passed
save_session -replace ${REPORTS_DIR}/${FMRM_FAILING_SESSION_NAME}/failing_session_name.rpt
report_failing_points > ${REPORTS_DIR}/${FMRM_FAILING_POINTS_REPORT}/failing_points.rpt
report_aborted > ${REPORTS_DIR}/${FMRM_ABORTED_POINTS_REPORT}/aborted_points.rpt
# Use analyze_points to help determine the next step in resolving verification
# issues. It runs heuristic analysis to determine if there are potential causes
# other than logical differences for failing or hard verification points.
analyze_points -all > ${REPORTS_DIR}/${FMRM_ANALYZE_POINTS_REPORT}/analyze_points.rpt
#sproc_msg -info "METRIC | BOOLEAN VERIFY.PASS_FORMAL | 1"
}
# Lynx Compatible procedure which performs final metric processing and exits
#sproc_script_stop
#exit