Design errors detection include dead logic, integer overflow, division by zero, and violations of design properties and assertions. Simulink^® Design Verifier™ uses formal methods to identify hard-to-find design errors in models without requiring extensive tests or simulation runs. You use Simulink Design Verifier to highlight blocks in a model containing design errors and blocks proven to be without them. For each block with an error, you calculate signal-range boundaries and generate a test vector that reproduces the error in simulation.