Exceptions (set_multicycle_path and set_false_path) are added by the designer to their timing environment to relax timing where needed to meet the timing specification of the circuit.

These exceptions are added for a number of different reasons :
Because the circuit can be allowed to take multiple clock cycles to complete due to logical relationships between controlling signals, or
Due to protocol knowledge of the designer, who "knows" that certain transfers can take multiple cycles even if it's not formally true of the circuit behavior, or
It's a dont-care condition that the designer is aware of.
Formal verification can be used to check exceptions of the first type - where the logical timing relationships between signals can be proven by formally checking a property of the circuit.

Timevision Exception Verification reads RTL or gate descriptions of the design, and clock and timing exception information from SDC or TCL files, and proves or disproves timing exceptions using a state-of-the-art formal verification engine. Timevision’s underlying formal engine can reach bounded (Correct) or unbounded (Fixed-Point) proofs of properties, giving extra confidence to exceptions proven with an unbounded model.
Value Proposition
Incorrect timing exceptions can result in silicon that does not work at-speed, or worse, has a hold-time issue, causing a silicon fail. These issues are painful to find in silicon or at gate-level timing simulation time, since at this point timing is already closed and the design is ready to tapeout. Timevision-ExceptionVerifier allows exceptions to be proven at RTL or gatelevel, bringing forward this verification activity to the front-end of the flow & without manual reviews and “eyeballing” of exception files.