在做match和verify时，没有unmatch point，但是dff和bbpin 出现了unread points。不知道是否影响设计的正确性。 进到schematic里面看，一些rtl里面有赋值的信号变成了undriven而且导致unread。 如rtl中：assign sigma [18:0] = buf ? {19{1'b1}} : { {18{1'b0}},1'b1}; 进到schematic中，sigma[18:2]都变成undriven了，但rtl语句的功能由其他cell实现了。 请问这个问题怎样解决？不管行不行？ 谢谢

you can try "set verification_verify_unread_compare_points true" "

我也正想问这个问题！但是楼上的解决方法是否正确值得斟酌。 因为这并没有实质上解决楼主的问题。 到底unread points影不影响后续验证？

看来你们把formality都研究得很熟了哦~~~ 可以相互帮助吗 我的邮箱是xingyu.ping@163.com

楼主 你把你的buf设定 “1” 或者“0”； 再试一下！

An unread point is a point (mostly a register) that is not used by your code. You might for instance compute a sum and register it but in the next stage, you use only the most significant bits, so the least significant bits become unread. Unmatched means that Formality couldn't match it with a register in the implementation design. Typically, this is because your synthesis tool has removed the unread register (you can tell most tools to leave those registers, but normally you don't want this). So the real question is: did you expect the unread unmatched point(s) to be unread? If so, all is fine, if not, check your code. Having said this, the only place where this could matter is with some RAM BIST insertion flows where cores might be inserted but only be connected later in the flow.

引用:

原帖由 loisfun 于 2006-5-22 02:55 PM 发表
1 P  n6 O! J/ d7 ^7 ~4 w, cAn unread point is a point (mostly a register) that is not used by your code. You might for instance compute a sum and register it but in the next stage, you use only the most significant bits, so  ...

0 x4 n' r0 w! `* G2 G/ ]) a+ _
8 Y1 n5 w  R+ ]( }" g* r
Clear explainations. That means normally the code is not most optimized if there is "unread" points reported by FM ( except the BIST insertion as mentioned)

我也遇到过这样的问题，一直没有在意，今天看到才明白了。

又注意了一下,关于没有用到的部分,在综合或者LAYOUT的过程中会被优化掉.这个时候,如果用netlist和RTL做formality,我这里的显示,被有优化掉的register会成为Unmatch的point而不是unread.似乎和上面的不是很符合呢.
7 c8 u, p+ {  }3 w0 Q( Z8 |/ D1 n比如一份Matching Result如下:
5 ?: ?$ ?3 D1 w' h4 z! P& I) S# a8 Y% G4 y3 f/ z( m
22057 Compare points matched by name% e' l/ s) u' A2 ]0 w4 u2 O( F
4 Compare points matched by signature analysis
4 U4 `3 ]$ q3 Y0 Compare points matched by topology: E. Y: J2 u. c- ^# B0 }; ~
155 Matched primary inputs, black-box outputs* G4 H: J( F3 R# v; W1 s
0(839) Unmatched reference(implementation)  compare points& H* `+ L- [2 V
0(0) Unmatched reference(implementation) primary inputs, black-box outputs
2 Q4 v0 {$ b* V1 g) o5 V" G' u7 j7577(137) Unmatched reference(implementation) unread points1 Y- U; o/ Z4 F0 V: M$ t5 N" _
1 r2 W$ F0 I0 T- S
上面的Unmatched reference(implementation)  compare points 和Unmatched reference(implementation) unread points分别是什么呢?
0 B+ C, j- W# d2 C5 ?( }
) h  C8 E# y1 k9 D4 e5 N4 ^- w[ 本帖最后由 linda_0823 于 2008-6-24 04:38 PM 编辑 ]

Formality reports a register as an unread compare point if the register cannot affect the behavior of the design at its primary outputs (or black box inputs) because it has no functional path to a primary output (or black box input).) y/ q1 l9 h6 Z) s( j6 c: M" ]

) X$ @. }' c4 Xverify this kind of register when need9 l  B$ Q- Y. k; n# M! ?
" {9 s7 ~& B4 u- v; {5 ~  _
[ 本帖最后由 powerg3 于 2008-8-16 10:11 PM 编辑 ]