形式验证formality中match阶段unread point问题

1252005989

我在用formality时，在match阶段会报出117（0）unmatched reference （implementation） unread points，但是verification显示的是succeeded，请问这种情况需要处理这种unread points么
谢谢大家，还请不吝赐教

lilin_ll

如果verification最后是succeeded，那就没有关系。

ZHZIC

你是哪两个做的对比？是RTL和综合后的还是综合后的和PR后的

1252005989

ZHZIC 发表于 2020-8-9 18:24
你是哪两个做的对比？是RTL和综合后的还是综合后的和PR后的

rtl代码与综合后的网表文件

dooyii

Unread compare points are matched points that don't drive anything, thus
they do not affect downstream compare points. By default these are not
verified; however, from the U-2003.06 release there is a new variable
verification_verify_unread_compare_point which will allow Formality to
verify all these points.

Just set the following variable before issuing the verify command:

set verification_verify_unread_compare_points true

shawnmicheals

应该需要手动检查这些compare point是否会影响你的设计吧，如果确实可以优化，且verify succeed应该就没问题

fanyf

set verification_verify_unread_compare_points true
这句加了之后formality就报错了

satans

fanyf 发表于 2023-6-16 10:17
set verification_verify_unread_compare_points true
这句加了之后formality就报错了

Try  set_app_var verification_verify_unread_compare_points true