Formal Verification of the fitted netlist

I have mapped and synthesised a design and also have generated verilog netlist and am trying to do Formal verification using Conformal using the .ctc script. Running into the following issues:

1. when i select the 'Speed' option during synthesis to meet timing, i get about 13K key points that are not getting mapped. I have tried using syn_noprune option on the hierarchies so as to avoid registers from getting pruned out, but still get such big no. of 'Not-mapped' points.

2. when i select the 'Balanced' option during synthesis, my timing is bad. but get only about 400 key-points that are not mapped. But still end up getting about 30K non-equivalent points.

3. During synthesis i get lot of these warnings:

Warning: Combinational loop detected. Provide cut point information to the formal verification tool. Insert cut buffer "rtl~9"

Warning: Combinational loop detected. Provide cut point information to the formal verification tool. Insert cut buffer "rtl~10"

I am guessing this is part of my problem with FV for which i need to add cut-point to the .ctc script in Conformal. do anyone know of an automatic way generating these cut points. I am having hard time locating these nets/instances in either the synthesized netlist as well as the corresponding nets that need to be broken in the RTL to avoid these combinational loops.

I would very much appreciate any suggestions on resolving the above issues. Also wanted to get an idea if it is even a common practise to try to do Formal verification of the fitted netlist in the FPGA world.