Hi.
Formal verification can be viewed from two points of view: one is model checking and the other is equivalence checking. Model checking is to check the equivalence between the specification and the design. Equivalence checking is to check the original design and the transformed design. Here, the examples of the transformed design are synthesized design, back-annotated design, etc., that is obtained from the original design, say, VHDL or Verilog HDL design.
By the way, the objective of the functional simulation is checking the logic of the design from the functionality point of view. The functional simulation is very important in the design flow in case of some debugging required.