the definition of unreachable and not-mapped in LEC?

[bradyue]

I have read the LEC document, but still I am so confused about the definition of unreachable and not-mapped key points. Who can do me a favor to explain it in detail? Thanks in advance...

 

[iwpia50s]

Unreachable state points are state points where it is not possible for LEC to condition your logic to get to a flop or latch.

Not-mapped is where there are state points in one implementation which are not in the other, thus it does not map to anything so it cannot mismatch.

 

[bradyue]

would you please give some examples for that? cause I am still a little bit not understood...thanks

 

[sree205]

not mapped in the sense, whats present in either RTL or netlist is not present in the other or its not been mapped.

unreachable - iwpia50s's definition is good enough