I have a golden RTL. I synthesize this RTL using Synplify and get a netlist, A. Using the VIF flow, I run LEC and find that netlist A and the RTL are equivalent.
I then synthesize the same golden RTL using different synthesis options and the same synthesizer and get a netlist, B. LEC shows that netlist B and the golden are not equivalent.
I then attempt to LEC netlist A and netlist B expecting mismatches, however LEC says they are equivalent! With respect to unmapped key points, I do have them, but in the golden RTL and both netlists, they are all unreachable. What can cause netlist A and B to be equivalent?