hcu
Advanced Member level 4
Hello,
I am very new to formality and running a entire soc reference and its implementation for equivalence checking in formality tool.
i am getting this report
I can see 16k unmatched points in the report and only 20 failing points as shown above.
BTW iam using .svf file got from dc. here is the script below which iam using
my question is,
1. i want to know whether my script file is correct or not. any other commands or switches need to use. i.e any setup problem ?
2. why i am getting unmatched points even on the RTL that was from thirdparty IP like dw and em processor. if it was my custom RTL, then it is my responsibility to address that right ?
3. a clear briefing on DFF0x or DFF1x error type.?
i want to know/ask more on this if this post attains attention. thanks.
I am very new to formality and running a entire soc reference and its implementation for equivalence checking in formality tool.
i am getting this report
Code:
20 Failing compare points (20 matched, 0 unmatched)
0 Aborted compare points
88545 Unverified compare points
----------------------------------------------------------------------------------------
Matched Compare Points BBPin Loop BBNet Cut Port DFF LAT TOTAL
----------------------------------------------------------------------------------------
Passing (equivalent) 23787 0 0 0 1 2969 84 26841
Failing (not equivalent) 0 0 0 0 0 20 0 20
Unverified 3762 0 4 0 10 84629 140 88545
Not Compared
Constant reg 1945 0 1945
Unread 0 0 0 0 0 3389 0 3389
****************************************************************************************
BTW iam using .svf file got from dc. here is the script below which iam using
Code:
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
my question is,
1. i want to know whether my script file is correct or not. any other commands or switches need to use. i.e any setup problem ?
2. why i am getting unmatched points even on the RTL that was from thirdparty IP like dw and em processor. if it was my custom RTL, then it is my responsibility to address that right ?
3. a clear briefing on DFF0x or DFF1x error type.?
i want to know/ask more on this if this post attains attention. thanks.