Terminology related to the formal tool

SystemVerilog
1

While the formal tool I am getting the follwing doubt. Can somebody please tell me the following concept:

  1. In formal tool what does the depth signifies? Is it some kind of clock cycle?

  2. Which is the graph for the CEX? Is it the witness waveform or the failure waveform?

  3. Why do we use the witness waveform when we have the failure waveform already to debug?

  4. what is the driver and load in the formal tool?

    I tried to read the document of the formal questa onespin tool but did not understand the concept. It would be helpful if somebody explain it in simple terms with examples.

Thanks