Formal Verification fails while checking the post-PAR design.
This problem can occur when the "-dp" option has been used in MAP. This option causes a pattern of "LUT driving a flip-flop" to get mapped into unused block RAMs. Since the formal verification tools cannot map the logic inside the block RAM to the RTL netlist, errors will be reported.
To work around this problem, do not use the "-dp" option in MAP.