Points Reachable/Unreachable in Conformal LEC

[psachinscanon]

lec unreachable


Here is the Scenario of the Problem I am facing.
1.Read a Golden Design and a Revised Design

Map the Points and Compare

2.Read the Same Golden Design and The Different Revised Design.

This time the Revised Design has been created by changing some Constarints in DC


The Problem I am facing is
Some Points in the Golden Design are not reachable for the First Run , But they are NOT_MAPPED for the Second Run

How this can be? because Conformal Says NOT_MAPPED unmapped points are reachable but do not have correspoding point in the Logic Fanin Cone of the Corresponding Design.

So How the same Point in Golden which is reachable becomes unreachable when the revised is changed....


Thank You,
Sachin Shahsikantrao Pampattiwar

 

[shnain]

conformal unreachable points

Hi,

Normally the main check with LEC is to find non-equivalent points.

Why are you interested in not-mapped points ?

Yours,
Said.

 

[psachinscanon]

sachin shashikantrao pampattiwar

Thank You For the Reply,

I am debugging Un-Mapped Points because,


Whenever I debug the Not Equivalent Point, I come across the Non-Mapped Point as a Non Corresponding Support.

So I am assuming that this is the cause of the failure.


Thank You,
Sachin Shashikantrao Pampattiwar

 

[shnain]

unreachable point + lec

what kind of EqCheck are you doing : g2g or r2g ?

 

[psachinscanon]

conformal unreach

RTL to Netlist,

Thank You,
Sachin Shashikantrao Pampattiwar

Added after 3 minutes:

what kind of EqCheck are you doing : g2g or r2g ?

by the way ...

for your information...

In the same Setup where I am getting the point Not Mapped...

I have done few exercise..I have set the root module for which I was getting the Point as NOTMapped...

Starngely now that point is unreachable again...

How a Point which is unreachable for a Module can become reachable if that Module is instantiated in Some Other Module?

Thank You,
Sachin Shashikantrao Pampattiwar

 

[joe2moon]

unreachable in lec

Is the corresponding "unreachable" point in the RTL design able to find in the gate-level netlist ?

 

[psachinscanon]

lec+mapping one point to two points

No,

That has been removed while synthesis...

Thank You,
Sachin Shashikantrao Pampattiwar

 

[joe2moon]

conformal lec handling unreach

So in the case of "not mapped", the key point has NOT been optimized away by synthesis tool ?

 

[psachinscanon]

lec equivalent check unreachable

Hi,

Thank You,

I will confirm on this...
But the Point is the RTL means Golden is not changed then how the Point is Becoming Not Mapped?
For Not-Mapped Unmapped Points it has to be reachbale ....right?


Wheather that point is in Reference Design or not should not decide the point in Golden is reachable or Not?

Thank You,
Sachin Shashikantrao Pampattiwar

Added after 38 minutes:

I have Confirmed that,


In case of Not Mapped also it has been removed away...


Thank You,
Sachin Shashikantrao Pampattiwar

 

[joe2moon]

conformal not mapped

It seems that the Modeling of the RTL code(the golden design) is dependent on the revised design.

I have seen this kind of behavior before.
(But I'm not sure if this is a bug or feature...)

 

[psachinscanon]

conformal lec

Thank You for the Help,

Let us Confirm,

I will surely update you if I find something.

Thank You,
Sachin Shashikantrao Pampattiwar

 

[rajesh9999]

lec unreachable gate

If you look at the definition of ' Unreachable' points - they are those points which will not reach any of the compare points/outputs. Obviusly then they do not influence any of the functionality. Therefore it is possible that synthesis (during optimization) has removed this point. Now it is unmapped as there is no corrosponding equivalent point in the revised design. Looks Logical.

By the way, check the log file. If it says "DESIGNS EQUAL" then you are fine.

 

[psachinscanon]

debug unreachable points in lec tool

Hello,

The points whcih are unreachable are shown Unreachable and Not -NOT mapped.

Not Mapped points defination says , the point is reachable but do not have cooresponding point in the other design.

I have Already explained the scenario.


Thank You,
Sachin Shashikantrao Pampattiwar

 

[kulkarn7]

Hello Sachin,

1. Due to DC constraint your revised changed during synthesis (say during synthesis mapping the naming convention of the registers Also depends on the optimization during synthesis ). It will cause you to get the not-mapped point in your second scenario. which are unreachable in first case.
--- Have you check the naming convention. Have applied any renaming rule for the same.
--- See it could be okay when your LEC is log is having the unreachable points but it is issue when your logs shows not-mapped point.
--- first you have to map those points.
--- also try with compare effort high option.

I hope you will get some clue from this

 

[narureddyk]

Some times the not-mapped points are due to the sequential merging of the logic during the synthesis
Look in to your synthesis log file if there are any sequentially merged statements present .
If present then add the instance equivalences constraints in the do script and run the lec and this may solve the issue.

 

[amitk3553]

Hello,
How will I know about sequential merging of the logic in synthesis log file?
Means tell me the procedure to find this in log file.Thanks

Regards
Amit

 

[englishdogg]

Wow.. multiple views on multiple points
here are my few paise...
# During compare not-mapped points are a problem they ahve to ve be debugged and esnured that they are mapped and compared - this could be due to many reasons - incorrect mapping, incorrect modelling, incoreect pin constraints etc
# Unreachables could beclock gating latches etc which are not present in the revised or points that do not reach a compare point; but these has to be reviewed as well since this your sign-off

If your performing RTL2Gate that means your using hierarchical compare (if not pl stry this) now check the not-mapped point if in golden then see in the synthesis logfile if it was optimized away say as a constant or a seq merge - in which case ensure that your LEC dofile has the necessary "set flatten model" options to address that modelling. If it does and still does not add it as a part of your hier dofile

I hope this helps..

- - - Updated - - -

@Amit

Depends on the synthesis tool your using.. try and search the log by the FF name itself you should be able to get it
But in any tool the messaging may be different but the keyword "merge" or "merging" will be there

 

[amitk3553]

hello,
There is One FF on the Golden side and nothing is there in revised side.Means corresponding FF which we want to create is present in RTL but not created in Synthesised design.And this flip-flop is shown as UNREACHABLE in golden side.I tried to find in synthesis log file but unable to find about this unreachable FF.I am using DC Shell for synthesis and CADENCE'conformal for LEC.Please help me to sort out this problem.

Regards
Amit

 

[englishdogg]

@Amit

I am a bit confused - what is the problem sequential merging or unreachables
I think what ureachables are are clearly mentioned in the documentation and in this discussion as well.

If it is in the RTL then it has to be in the revised netlist - if it is not there has to be an information in the synthesis logfile as to what happened to this logic; was it constant, redundant logic, merged etc

 

[amitk3553]

@Amit

I am a bit confused - what is the problem sequential merging or unreachables
I think what ureachables are are clearly mentioned in the documentation and in this discussion as well.

If it is in the RTL then it has to be in the revised netlist - if it is not there has to be an information in the synthesis logfile as to what happened to this logic; was it constant, redundant logic, merged etc

Problem solved.The FF (shown as unreachable) which i had used is not affecting fuctionality.Thanks for your replies