Continue to Site

Welcome to EDAboard.com

Welcome to our site! EDAboard.com is an international Electronics Discussion Forum focused on EDA software, circuits, schematics, books, theory, papers, asic, pld, 8051, DSP, Network, RF, Analog Design, PCB, Service Manuals... and a whole lot more! To participate you need to register. Registration is free. Click here to register now.

Formality script (RTL vs netlist)

Status
Not open for further replies.

hcu

Advanced Member level 4
Joined
Feb 28, 2017
Messages
101
Helped
0
Reputation
0
Reaction score
0
Trophy points
16
Activity points
874
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

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
****************************************************************************************
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
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.
 

DFF0X/DFF1X are constrained registers which can take only 0X/1X values.
 

Status
Not open for further replies.

Part and Inventory Search

Welcome to EDABoard.com

Sponsor

Back
Top