formality verification

[scholin]

hi guys:
i perform the verification for rtl vs. netlist.
i encounter a problem in the match stage of formality.
there are some of unmatched points in the reference object, but these unmatched points do not appear in the implementation object.
the type of unmatched points is DFF.
pls tell me what is this problem and how to fix it?

thanks!!

 

[sree205]

this is what i infer from ur question, the DFFs in the RTL(reference object) are not present in the netlist(implementation object). Is this what you mean? Its possible that the DFFs in the RTL can be optimized by the synthesis tool. I'm not a synthesis guy. But what i can suggest is, to get around it, in ur synthesis script, use set_dont_touch or such similar command to ensure the DFFs don't get removed during optimization

 

[scholin]

this is what i infer from ur question, the DFFs in the RTL(reference object) are not present in the netlist(implementation object). Is this what you mean? Its possible that the DFFs in the RTL can be optimized by the synthesis tool. I'm not a synthesis guy. But what i can suggest is, to get around it, in ur synthesis script, use set_dont_touch or such similar command to ensure the DFFs don't get removed during optimization

Thank you for ur suggestion.
there is one thing make me confuse. that is first time i verify the rtl vs netlist. the netlist is produced by compile option in synthesis tool, the formal is ok. But when i take the netlist file that is produced by compile_ultra option in sythesis to do formality again, it is not ok. it will happen that situation. is it caused by compile_ultra option????.

Thanks a lot!!

 

[sree205]

i think compile_ultra is an option which uses a different algorithm than compile, i've heard that its a better one and does better optimization than the earlier compile option.

Yes, its possible that with compile ultra, ur RTL might be optimized a lot more and hence causes the problem. As a measure of comparison, look at the timing/area reports generated by doing these two and it'll be easier to see the difference.

But, even with compile_ultra, its possible to use "set_dont_touch" and still get the formality to pass.