true non equivalence during rtl2gate LEC check ?

[alokem]

Is it possible that there are non equivalent points during RTL2Gate LEC check assuming
all key points are properly mapped , constraints like disabaling scan_enable etc and modeling
options are perfect ? If yes , can you please provide some examples ?

 

[rca]

Yes it could.
For example, some flip unlocked, which will be removed by synthesis.

 

[jbeniston]

Wrong logic synthesized. The tools aren't perfect.

 

[englishdogg]

The reasons could be many- though you mention that the pin constraints and modelling options i.e commands you used are correct.
To add a few more - incorrect modelling of clock gating, transparent latches, incorrect cut point mapping, unbalanced bbox, incorrect optimization of logic by synthesis tools, incorrect parsing of RTL by LEC.. etc

 

[alokem]

Thanks all for your inputs !

Hi ed,

Can you please elaborate more on the following reasons mentioned by you ?

"unbalanced bbox, incorrect optimization of logic by synthesis tools"

 

[mail4idle2]

LEC tool also optimizes the RTL before it compares with the netlist you have given. if the synthesis tool used to generate netlist has done incorrect optimization then there can be non equivalent points.
Blackbox instances for golden and revised not being equal.

 

[englishdogg]

The purpose of LEC is to ensure that functionally the design as coded in the RTL is synthesized accordingly to give desired outputs. Now at times i have seen that synthesis optimize some of the logic which should not for example optimizing some logic which was not redundant incorrect constant propagation or incorrect merging of sequential elements. This needs to be verified and these would comprise as incorrect optimization of logic.

Now LEC can also sometimes lead to false non-eqs in which case if the setup is not proper for example BBOX's needs to be balanced on both sides. ensure that your pads are added to the add notranslate section etc and so on.

I hope this clarifies.