Formal Verification of the fitted netlist

[Altera_Forum]

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.