synthesis tool will optimizes the design by removing redundancy, etc..
it can optimize nets. ex: DC will optimize the nets or logic. if it only optimizes nets, then no problem. conformal works on logical equivalence check. as the logic is remained in the netlist, conformal matches RTL & netlist even some nets are optimized away.there will be no unmathed points unless really a mismatch is there.
the synplifypro tool optimizes even the registers. & synplifypro generates some files for conformal tool. (those will be in encrypted format.) so conformal can work properly.
the new version of DC optimizes registers also. at that time, there is a mismatch in key points. i didn't work on newer version of DC. i too don't know how to do formal verification in this scenario.