formality验证问题，求大神解疑！急急急！！！！！

1027199631

formality形式验证出现如下信息：

Net i:/WORK/halfband2_CSD_DW01_sub_142/DIFF[7] is undriven.

Info:  Net i:/WORK/halfband2_CSD_DW01_sub_142/DIFF[6] is undriven.

Info:  Net i:/WORK/halfband2_CSD_DW01_sub_142/DIFF[5] is undriven.

Info:  Net i:/WORK/halfband2_CSD_DW01_sub_142/DIFF[4] is undriven.

Info:  Net i:/WORK/halfband2_CSD_DW01_sub_142/DIFF[3] is undriven.

Info:  Net i:/WORK/halfband2_CSD_DW01_sub_142/DIFF[2] is undriven.

Info:  Net i:/WORK/halfband2_CSD_DW01_sub_142/DIFF[1] is undriven.

Info:  Net i:/WORK/halfband2_CSD_DW01_sub_142/DIFF[0] is undriven.

Info:  Net i:/WORK/halfband2_CSD_DW01_sub_142/CO is undriven.

Info:  Net i:/WORK/halfband2_CSD_DW01_add_488/SUM[1] is undriven.

Info:  Net i:/WORK/halfband2_CSD_DW01_add_488/SUM[0] is undriven.

Info:  Net i:/WORK/halfband2_CSD_DW01_add_488/CO is undriven.

Info:  Net i:/WORK/halfband2_CSD_DW01_add_491/CO is undriven.

Info:  Net i:/WORK/halfband2_CSD_DW01_sub_146/DIFF[9] is undriven.

Info:  Net i:/WORK/halfband2_CSD_DW01_sub_146/DIFF[8] is undriven.

Info:  Net i:/WORK/halfband2_CSD_DW01_sub_146/DIFF[7] is undriven.

Info:  Net i:/WORK/halfband2_CSD_DW01_sub_146/DIFF[6] is undriven.

Warning: 26 (4207) undriven nets found in reference (implementation) design; see formality.log for list (FM-399)

Warning: 75 (0) undriven pins found in reference (implementation) design; see formality.log for list (FM-399)

match时出现不匹配 问题：

*********************************** Matching Results ***********************************

11588 Compare points matched by name

0 Compare points matched by signature analysis

0 Compare points matched by topology

8 Matched primary inputs, black-box outputs

196(0) Unmatched reference(implementation) compare points

0(0) Unmatched reference(implementation) primary inputs, black-box outputs

42017(0) Unmatched reference(implementation) unread points

----------------------------------------------------------------------------------------

Unmatched Objects                                                        REF        IMPL

----------------------------------------------------------------------------------------

Cut-points (Cut)                                                         24           0

Registers                                                               172           0

   Constrained 0X                                                        172           0

****************************************************************************************

我man  FM-399结果如下：

messages                         N.  Messages                Command Reference

NAME

       FM-399  (warning)  %d  (%d) undriven %s found in reference (implementa-

       tion) design; see %s for list

DESCRIPTION

       Nets or pins with no driving logic  were  found  in  the  reference  or

       implementation  design.  These  nets/pins are assumed to have the value

       specified by the verification_set_undriven_signals TCL variable.

WHAT NEXT

       Verify the connections on the indicated nets and correct the design  if

       it is not what you intended. You can specify the value Formality should

       assume   for   undriven    signals    by    setting    the    verifica-

       tion_set_undriven_signals  variable  to X(default), Z, 0, 1, or PI(pri-

       mary input).

D-2010.03        Synopsys Inc. 1988-2010. All rights reserved.             n-1

不是很明白该如何做？不知道这是否为match、verify failed的原因？我该如何修正 ？跪求解决办法，多谢多谢

1027199631

回复 1# 1027199631

求大神解疑啊

iseepiglet

设计里存在没驱动的线，查rtl

杰克淡定

跟楼上想法一样，首先去检查RTL设计这里是不是无驱动。