MATLAB: Difference between Simulink diagnostics and Simulink Design Verifier error checking

Question

Simulink Design Verifier can perform error checking to determine whether a model contains dead logic, division by zero, overflows, and other checks. However, Simulink diagnostics already performs these checks at simulation-time (see https://www.mathworks.com/help/simulink/gui/diagnostics-pane-data-validity.html). For example, the simple model below shows that during simulation there is a divide by zero error. What is the advantage of using the SDV toolbox instead of relying on the Simulink diagnostics?

Answer 1

Simulink Design Verifier can detect these errors before simulation by using formal methods to analyze the model for errors such as integer overflow, division by zero, array out of bounds, subnormal values, and floating-point errors as well as data validity errors. A single simulation run may not encounter any error based on the value of the signals during the simulation. Design Verifier analyzes the model to find these errors without exhaustive simulation. Simulink Design Verifier generates a counter example for each error to reproduce it. Simulink Design Verifier can also detect dead logic which would not be executed by simulation.