Functional verification is done when we have our DUT RTL is ready and we here check for all the functionality of our design (for which it is designed). Basically we test functionality of design by some HVL language (like verilig, vhdl, specman, vera, system verilog and so on).
In Formal Verification we check intended design functionality has not been changed during any time in different stage of ASIC flow. As for example when we synthesize our RTL into netlist, we use formal verificatio to see if synthesis tool has not changed any functionlity (so we do formal verification between golden RTL and netlist) similarly we can perform formal verification on prelayout and post layout netlist to see nothing has been changed. For formal verification we generally use Cadence Conformal , Synopsis Formality.
Hope this helps.
Regards,
pintuinvlsi