How to judge a complete verification

[Andy]

hi,
I do not quite understand the way Formality judge a successful
verification. According to Formality user's guide, we are able to get a
complete verification even if there are extra registers in reference or
implementation design. I guess that means even if there are unmatched
points between 2 designs, I can still come to the conclusion that these
2 hold design consistency as long as no failure occurs in verify phase
(I am not sure if I have the correct understanding of that statement).
And this will lead to a hypothesis that when synthesis tools make some
kind of optimization to eliminate those unmatched points from the
implementation design, the action is justified as long as all of the
remaining verifiable compare points maintains consistency. I am quite
puzzled and could anyone kindly give some explanation?

 

Your understanding is correct. Synthesis tools can remove redundant
logic without affecting functionality. And these logic will appear as
unmatched points in Formality.

Nandy
www.nandigits.com
Netlist Debug/ECO in GUI mode.

 

[Andy]

Thanks a lot! But Is there any possiblity to come into a success in
Formality while actually misinterpreting exists in synthesis tools like
DC?

 

[Andy]

Actually when I want to go through a rtl2gate verification, I use the
command write_hierarchical_verification_script to automatically
generate script for each module respectively. In the auto generated
script, there are several lines indicating outputs which are not read
by the higher level and therefore marked as "set_dont_verify_point".
And some of them, as I remember, will fail the verification phase if I
do not set them as "dont_verify". I do not know what's up.

 

Formality tool and synthesis tool use different approaches to interpret
gates. So they can't make same error.
I don't understand why outputs port are not read by the higher level.
Another thing, why don't you use top down verification? Synthesize all
RTL to get one hierarchical netlist, compare the netlist with RTL.

Nandy
www.nandigits.com
Netlist Debug/ECO in GUI mode.