formality求助
时间：10-02
整理：3721RD
点击：
求助formality高手。我现在做了一个RTL和netlist（没加JTAG和DFT）的formal，最后报48个fail point，其中16个是是PWR之类管脚，我觉得可以忽略。还有32个是一个data bus 的registers，死活过不了。我把一些log和其中一个point的fail patten发上来了。请大家帮忙看看是什么原因。谢谢了！
***************************** Guidance Summary *****************************
Status
Command Accepted Rejected Unsupported Unprocessed Total
----------------------------------------------------------------------------
architecture_netlist: 7 0 0 0 7
boundary : 68 0 0 0 68
boundary_netlist : 6 0 0 0 6
change_names : 1255 124 0 0 1379
constraints : 12 0 0 0 12
datapath : 67 1 0 0 68
environment : 6 0 0 0 6
instance_map : 212 0 0 0 212
inv_push : 73 0 0 0 73
merge : 59 0 0 0 59
multiplier : 95 0 0 0 95
reg_constant : 4908 320 0 0 5228
reg_merging : 182 0 0 0 182
replace : 612 0 0 0 612
ungroup : 649 0 0 0 649
uniquify : 839 97 0 0 936
ununiquify : 2 0 0 0 2
Note: If verification succeeds you can safely ignore unaccepted guidance commands.
SVF files read:
/home/xxxx/work/chin5/run/SYN/ddr/mcm.svf
SVF files produced:
formality_svf/
svf.txt
****************************************************************************
Status: Matching...
*********************************** Matching Results ***********************************
29567 Compare points matched by name
1 Compare points matched by signature analysis
0 Compare points matched by topology
287 Matched primary inputs, black-box outputs
4183(310131) Unmatched reference(implementation) compare points
0(0) Unmatched reference(implementation) primary inputs, black-box outputs
41462(2) Unmatched reference(implementation) unread points
----------------------------------------------------------------------------------------
Unmatched Objects REF IMPL
----------------------------------------------------------------------------------------
Black-boxes (BBox) 0 309856
Black-box input pins (BBPin) 0 309856
Cut-points (Cut) 18 0
Registers 4165 275
DFF 228 0
Clock-gate LAT 0 267
Constant 0 0 8
Constrained 0X 3889 0
Constrained 1X 48 0
****************************************************************************************
Reference design is 'r:/WORK/mcm'
Implementation design is 'i:/WORK/mcm'
*********************************** Matching Results ***********************************
29567 Compare points matched by name
1 Compare points matched by signature analysis
0 Compare points matched by topology
287 Matched primary inputs, black-box outputs
4183(310131) Unmatched reference(implementation) compare points
0(0) Unmatched reference(implementation) primary inputs, black-box outputs
41462(2) Unmatched reference(implementation) unread points
----------------------------------------------------------------------------------------
Unmatched Objects REF IMPL
----------------------------------------------------------------------------------------
Black-boxes (BBox) 0 309856
Black-box input pins (BBPin) 0 309856
Cut-points (Cut) 18 0
Registers 4165 275
DFF 228 0
Clock-gate LAT 0 267
Constant 0 0 8
Constrained 0X 3889 0
Constrained 1X 48 0
****************************************************************************************
Status: Verifying...
Compare point mc_mc_mc_U_pbiu_p_rdata_reg_29_ failed (is not equivalent)
Compare point mc_mc_mc_U_pbiu_p_rdata_reg_27_ failed (is not equivalent)
Compare point mc_mc_mc_U_pbiu_p_rdata_reg_28_ failed (is not equivalent)
Compare point mc_mc_mc_U_pbiu_p_rdata_reg_30_ failed (is not equivalent)
Compare point mc_mc_mc_U_pbiu_p_rdata_reg_25_ failed (is not equivalent)
Compare point mc_mc_mc_U_pbiu_p_rdata_reg_26_ failed (is not equivalent)
Compare point mc_mc_mc_U_pbiu_p_rdata_reg_21_ failed (is not equivalent)
Compare point mc_mc_mc_U_pbiu_p_rdata_reg_22_ failed (is not equivalent)
Compare point mc_mc_mc_U_pbiu_p_rdata_reg_23_ failed (is not equivalent)
Compare point mc_mc_mc_U_pbiu_p_rdata_reg_24_ failed (is not equivalent)
Compare point mc_mc_mc_U_pbiu_p_rdata_reg_15_ failed (is not equivalent)
Compare point mc_mc_mc_U_pbiu_p_rdata_reg_31_ failed (is not equivalent)
Compare point mc_mc_mc_U_pbiu_p_rdata_reg_14_ failed (is not equivalent)
Compare point mc_mc_mc_U_pbiu_p_rdata_reg_19_ failed (is not equivalent)
Compare point mc_mc_mc_U_pbiu_p_rdata_reg_20_ failed (is not equivalent)
Compare point mc_mc_mc_U_pbiu_p_rdata_reg_13_ failed (is not equivalent)
Compare point mc_mc_mc_U_pbiu_p_rdata_reg_18_ failed (is not equivalent)
Compare point mc_mc_mc_U_pbiu_p_rdata_reg_11_ failed (is not equivalent)
Compare point mc_mc_mc_U_pbiu_p_rdata_reg_16_ failed (is not equivalent)
Compare point mc_mc_mc_U_pbiu_p_rdata_reg_12_ failed (is not equivalent)
Compare point mc_mc_mc_U_pbiu_p_rdata_reg_17_ failed (is not equivalent)
Compare point mc_mc_mc_U_pbiu_p_rdata_reg_10_ failed (is not equivalent)
Compare point mc_mc_mc_U_pbiu_p_rdata_reg_9_ failed (is not equivalent)
Compare point mc_mc_mc_U_pbiu_p_rdata_reg_7_ failed (is not equivalent)
Compare point mc_mc_mc_U_pbiu_p_rdata_reg_8_ failed (is not equivalent)
Compare point mc_mc_mc_U_pbiu_p_rdata_reg_6_ failed (is not equivalent)
Compare point mc_mc_mc_U_pbiu_p_rdata_reg_5_ failed (is not equivalent)
Compare point mc_mc_mc_U_pbiu_p_rdata_reg_4_ failed (is not equivalent)
Compare point mc_mc_mc_U_pbiu_p_rdata_reg_3_ failed (is not equivalent)
Compare point mc_mc_mc_U_pbiu_p_rdata_reg_2_ failed (is not equivalent)
Compare point mc_mc_mc_U_pbiu_p_rdata_reg_1_ failed (is not equivalent)
Compare point mc_mc_mc_U_pbiu_p_rdata_reg_0_ failed (is not equivalent)
Compare point mc_mc_axi2nif_cgSrc_cg_cg failed (is not equivalent)
Compare point mc_dCLKSampler_cg_cg_cg failed (is not equivalent)
Compare point mc_dphy_cb_cb_cb failed (is not equivalent)
Compare point mc_dCLKSampler_cb_cb_cb failed (is not equivalent)
Compare point mc_mc_axi2nif_cgSrc_cg_cg failed (is not equivalent)
Compare point mc_dCLKSampler_cg_cg_cg failed (is not equivalent)
Compare point mc_dphy_cb_cb_cb failed (is not equivalent)
Compare point mc_dCLKSampler_cb_cb_cb failed (is not equivalent)
Compare point mc_mc_axi2nif_cgSrc_cg_cg failed (is not equivalent)
Compare point mc_dCLKSampler_cg_cg_cg failed (is not equivalent)
Compare point mc_dphy_cb_cb_cb failed (is not equivalent)
Compare point mc_dCLKSampler_cb_cb_cb failed (is not equivalent)
Compare point mc_mc_axi2nif_cgSrc_cg_cg failed (is not equivalent)
Compare point mc_dCLKSampler_cg_cg_cg failed (is not equivalent)
Compare point mc_dphy_cb_cb_cb failed (is not equivalent)
Compare point mc_dCLKSampler_cb_cb_cb failed (is not equivalent)
************ RTL Interpretation Summary ************
************ Design: r:/WORK/mcm
2 FMR_ELAB-147 messages produced
Please refer to the Formality log file for more details,
or execute report_hdlin_mismatches.
****************************************************
***************************** Synopsys Auto Setup Summary ******************************
！ Synopsys Auto Setup Mode was enabled. ！
！ Verification results are valid assuming the following setup constraints: ！
### RTL Interpretation Setup
set hdlin_ignore_parallel_case false
set hdlin_ignore_full_case false
set hdlin_error_on_mismatch_message false
set hdlin_ignore_embedded_configuration true
### FSM information
set svf_ignore_unqualified_fsm_information false
### Test Logic Setup
set verification_verify_directly_undriven_output false
For details see report_dont_verify_points and report_constants
For further details on Synopsys Auto Setup Mode: Type man synopsys_auto_setup
****************************************************************************************
********************************* Verification Results *********************************
Verification FAILED
ATTENTION: synopsys_auto_setup mode was enabled.
See Synopsys Auto Setup Summary for details.
ATTENTION: RTL interpretation messages were produced during link
of reference design.
Verification results may disagree with a logic simulator.
ATTENTION: 16 failing compare points have unmatched undriven signals in their
reference fan-in. To report such failing points, use
"report_failing_points -inputs unmatched -inputs undriven".
To read about undriven signal handling, use
"man verification_set_undriven_signals".
----------------------------------------------------------------------------------------
Reference design: r:/WORK/mcm
Implementation design: i:/WORK/mcm
29520 Passing compare points
48 Failing compare points
0 Aborted compare points
0 Unverified compare points
----------------------------------------------------------------------------------------
Matched Compare Points BBPin Loop BBNet Cut Port DFF LAT TOTAL
----------------------------------------------------------------------------------------
Passing (equivalent) 8710 0 26 0 157 20521 106 29520
Failing (not equivalent) 16 0 0 0 0 32 0 48
Not Compared
Constant reg 146 0 146
Unread 368 0 0 0 0 399 0 767
****************************************************************************************
Status: Diagnosing i:/WORK/mcm vs r:/WORK/mcm...
Status: Diagnosis initializing...
Status: Analyzing patterns...
Warning: Failing patterns do not have sufficient coverage for distinct errors. No error candidates identified. Please diagnose a smaller group of points. (FM-420)
Analysis completed
Status: Finding matching regions in reference design...
No matching regions detected in reference design
Info: Session being saved in minimal format.
Info: Session containers saved as read-only.
***************************** Guidance Summary *****************************
Status
Command Accepted Rejected Unsupported Unprocessed Total
----------------------------------------------------------------------------
architecture_netlist: 7 0 0 0 7
boundary : 68 0 0 0 68
boundary_netlist : 6 0 0 0 6
change_names : 1255 124 0 0 1379
constraints : 12 0 0 0 12
datapath : 67 1 0 0 68
environment : 6 0 0 0 6
instance_map : 212 0 0 0 212
inv_push : 73 0 0 0 73
merge : 59 0 0 0 59
multiplier : 95 0 0 0 95
reg_constant : 4908 320 0 0 5228
reg_merging : 182 0 0 0 182
replace : 612 0 0 0 612
ungroup : 649 0 0 0 649
uniquify : 839 97 0 0 936
ununiquify : 2 0 0 0 2
Note: If verification succeeds you can safely ignore unaccepted guidance commands.
SVF files read:
/home/xxxx/work/chin5/run/SYN/ddr/mcm.svf
SVF files produced:
formality_svf/
svf.txt
****************************************************************************
Status: Matching...
*********************************** Matching Results ***********************************
29567 Compare points matched by name
1 Compare points matched by signature analysis
0 Compare points matched by topology
287 Matched primary inputs, black-box outputs
4183(310131) Unmatched reference(implementation) compare points
0(0) Unmatched reference(implementation) primary inputs, black-box outputs
41462(2) Unmatched reference(implementation) unread points
----------------------------------------------------------------------------------------
Unmatched Objects REF IMPL
----------------------------------------------------------------------------------------
Black-boxes (BBox) 0 309856
Black-box input pins (BBPin) 0 309856
Cut-points (Cut) 18 0
Registers 4165 275
DFF 228 0
Clock-gate LAT 0 267
Constant 0 0 8
Constrained 0X 3889 0
Constrained 1X 48 0
****************************************************************************************
Reference design is 'r:/WORK/mcm'
Implementation design is 'i:/WORK/mcm'
*********************************** Matching Results ***********************************
29567 Compare points matched by name
1 Compare points matched by signature analysis
0 Compare points matched by topology
287 Matched primary inputs, black-box outputs
4183(310131) Unmatched reference(implementation) compare points
0(0) Unmatched reference(implementation) primary inputs, black-box outputs
41462(2) Unmatched reference(implementation) unread points
----------------------------------------------------------------------------------------
Unmatched Objects REF IMPL
----------------------------------------------------------------------------------------
Black-boxes (BBox) 0 309856
Black-box input pins (BBPin) 0 309856
Cut-points (Cut) 18 0
Registers 4165 275
DFF 228 0
Clock-gate LAT 0 267
Constant 0 0 8
Constrained 0X 3889 0
Constrained 1X 48 0
****************************************************************************************
Status: Verifying...
Compare point mc_mc_mc_U_pbiu_p_rdata_reg_29_ failed (is not equivalent)
Compare point mc_mc_mc_U_pbiu_p_rdata_reg_27_ failed (is not equivalent)
Compare point mc_mc_mc_U_pbiu_p_rdata_reg_28_ failed (is not equivalent)
Compare point mc_mc_mc_U_pbiu_p_rdata_reg_30_ failed (is not equivalent)
Compare point mc_mc_mc_U_pbiu_p_rdata_reg_25_ failed (is not equivalent)
Compare point mc_mc_mc_U_pbiu_p_rdata_reg_26_ failed (is not equivalent)
Compare point mc_mc_mc_U_pbiu_p_rdata_reg_21_ failed (is not equivalent)
Compare point mc_mc_mc_U_pbiu_p_rdata_reg_22_ failed (is not equivalent)
Compare point mc_mc_mc_U_pbiu_p_rdata_reg_23_ failed (is not equivalent)
Compare point mc_mc_mc_U_pbiu_p_rdata_reg_24_ failed (is not equivalent)
Compare point mc_mc_mc_U_pbiu_p_rdata_reg_15_ failed (is not equivalent)
Compare point mc_mc_mc_U_pbiu_p_rdata_reg_31_ failed (is not equivalent)
Compare point mc_mc_mc_U_pbiu_p_rdata_reg_14_ failed (is not equivalent)
Compare point mc_mc_mc_U_pbiu_p_rdata_reg_19_ failed (is not equivalent)
Compare point mc_mc_mc_U_pbiu_p_rdata_reg_20_ failed (is not equivalent)
Compare point mc_mc_mc_U_pbiu_p_rdata_reg_13_ failed (is not equivalent)
Compare point mc_mc_mc_U_pbiu_p_rdata_reg_18_ failed (is not equivalent)
Compare point mc_mc_mc_U_pbiu_p_rdata_reg_11_ failed (is not equivalent)
Compare point mc_mc_mc_U_pbiu_p_rdata_reg_16_ failed (is not equivalent)
Compare point mc_mc_mc_U_pbiu_p_rdata_reg_12_ failed (is not equivalent)
Compare point mc_mc_mc_U_pbiu_p_rdata_reg_17_ failed (is not equivalent)
Compare point mc_mc_mc_U_pbiu_p_rdata_reg_10_ failed (is not equivalent)
Compare point mc_mc_mc_U_pbiu_p_rdata_reg_9_ failed (is not equivalent)
Compare point mc_mc_mc_U_pbiu_p_rdata_reg_7_ failed (is not equivalent)
Compare point mc_mc_mc_U_pbiu_p_rdata_reg_8_ failed (is not equivalent)
Compare point mc_mc_mc_U_pbiu_p_rdata_reg_6_ failed (is not equivalent)
Compare point mc_mc_mc_U_pbiu_p_rdata_reg_5_ failed (is not equivalent)
Compare point mc_mc_mc_U_pbiu_p_rdata_reg_4_ failed (is not equivalent)
Compare point mc_mc_mc_U_pbiu_p_rdata_reg_3_ failed (is not equivalent)
Compare point mc_mc_mc_U_pbiu_p_rdata_reg_2_ failed (is not equivalent)
Compare point mc_mc_mc_U_pbiu_p_rdata_reg_1_ failed (is not equivalent)
Compare point mc_mc_mc_U_pbiu_p_rdata_reg_0_ failed (is not equivalent)
Compare point mc_mc_axi2nif_cgSrc_cg_cg failed (is not equivalent)
Compare point mc_dCLKSampler_cg_cg_cg failed (is not equivalent)
Compare point mc_dphy_cb_cb_cb failed (is not equivalent)
Compare point mc_dCLKSampler_cb_cb_cb failed (is not equivalent)
Compare point mc_mc_axi2nif_cgSrc_cg_cg failed (is not equivalent)
Compare point mc_dCLKSampler_cg_cg_cg failed (is not equivalent)
Compare point mc_dphy_cb_cb_cb failed (is not equivalent)
Compare point mc_dCLKSampler_cb_cb_cb failed (is not equivalent)
Compare point mc_mc_axi2nif_cgSrc_cg_cg failed (is not equivalent)
Compare point mc_dCLKSampler_cg_cg_cg failed (is not equivalent)
Compare point mc_dphy_cb_cb_cb failed (is not equivalent)
Compare point mc_dCLKSampler_cb_cb_cb failed (is not equivalent)
Compare point mc_mc_axi2nif_cgSrc_cg_cg failed (is not equivalent)
Compare point mc_dCLKSampler_cg_cg_cg failed (is not equivalent)
Compare point mc_dphy_cb_cb_cb failed (is not equivalent)
Compare point mc_dCLKSampler_cb_cb_cb failed (is not equivalent)
************ RTL Interpretation Summary ************
************ Design: r:/WORK/mcm
2 FMR_ELAB-147 messages produced
Please refer to the Formality log file for more details,
or execute report_hdlin_mismatches.
****************************************************
***************************** Synopsys Auto Setup Summary ******************************
！ Synopsys Auto Setup Mode was enabled. ！
！ Verification results are valid assuming the following setup constraints: ！
### RTL Interpretation Setup
set hdlin_ignore_parallel_case false
set hdlin_ignore_full_case false
set hdlin_error_on_mismatch_message false
set hdlin_ignore_embedded_configuration true
### FSM information
set svf_ignore_unqualified_fsm_information false
### Test Logic Setup
set verification_verify_directly_undriven_output false
For details see report_dont_verify_points and report_constants
For further details on Synopsys Auto Setup Mode: Type man synopsys_auto_setup
****************************************************************************************
********************************* Verification Results *********************************
Verification FAILED
ATTENTION: synopsys_auto_setup mode was enabled.
See Synopsys Auto Setup Summary for details.
ATTENTION: RTL interpretation messages were produced during link
of reference design.
Verification results may disagree with a logic simulator.
ATTENTION: 16 failing compare points have unmatched undriven signals in their
reference fan-in. To report such failing points, use
"report_failing_points -inputs unmatched -inputs undriven".
To read about undriven signal handling, use
"man verification_set_undriven_signals".
----------------------------------------------------------------------------------------
Reference design: r:/WORK/mcm
Implementation design: i:/WORK/mcm
29520 Passing compare points
48 Failing compare points
0 Aborted compare points
0 Unverified compare points
----------------------------------------------------------------------------------------
Matched Compare Points BBPin Loop BBNet Cut Port DFF LAT TOTAL
----------------------------------------------------------------------------------------
Passing (equivalent) 8710 0 26 0 157 20521 106 29520
Failing (not equivalent) 16 0 0 0 0 32 0 48
Not Compared
Constant reg 146 0 146
Unread 368 0 0 0 0 399 0 767
****************************************************************************************
Status: Diagnosing i:/WORK/mcm vs r:/WORK/mcm...
Status: Diagnosis initializing...
Status: Analyzing patterns...
Warning: Failing patterns do not have sufficient coverage for distinct errors. No error candidates identified. Please diagnose a smaller group of points. (FM-420)
Analysis completed
Status: Finding matching regions in reference design...
No matching regions detected in reference design
Info: Session being saved in minimal format.
Info: Session containers saved as read-only.
re。没人帮助吗?
你增加这个命令试试，应该会好些：
set verification_set_undriven_signal 0:X
还有set hdlin_error_on_mismatch_message false应该定义为true吧；
auto setup 应该可以解决很多问题吧?
感觉不对！不能解决问题
Thank you very much. Oh.