Run Simulink Design Verifier Checks Using Model Advisor

R2026b

Run Simulink^® Design Verifier™ checks using Model Advisor to assess whether your model is ready for analysis. Running these checks identifies modeling issues, guideline violations, and patterns that can affect Simulink Design Verifier analysis results.

To open Model Advisor, on the Modeling tab in Simulink Toolstrip, click Model Advisor. For more information, see Model Advisor Overview.

Simulink Design Verifier Checks Overview

To select Simulink Design Verifier checks in Model Advisor, select Simulink Design Verifier filters in the Check Selector panel. Under By Product, select:

• Simulink Design Verifier

Under By Task, select:

Simulink Design Verifier Compatibility Check

Simulink Design Verifier Defect Checker

Simulink Design Verifier Design Error Checks

When you run a Simulink Design Verifier check, the Model Advisor checks out the Simulink Design Verifier license.

By using the Model Advisor, you can save check results in HTML files. See Save and View Model Advisor Check Reports.

For more information on using the Model Advisor, see Run Model Advisor Checks. For more information on customizing the Model Advisor, see Automate Model Advisor Check Execution.

Note

When you run Simulink Design Verifier checks through Model Advisor, the Look inside masks parameter is automatically set to all, and the Follow links parameter is automatically set to on, regardless of the Model Advisor configuration. Use a filter to exclude specific subsystems. For more information, see Filter Objectives by Using Simulink Design Verifier Filter Explorer.

Simulink Design Verifier Compatibility Check

Simulink Design Verifier compatibility check helps you prepare your model for Simulink Design Verifier analysis by identifying elements of your model that might require special attention.

Check compatibility with Simulink Design Verifier

Check ID: mathworks.sldv.compatibility

Identify elements that Simulink Design Verifier analysis does not support.

Description.  This check assesses your model for compatibility with Simulink Design Verifier.

Results and Recommended Actions

Condition	Recommended Action
Incompatible	Avoid using unsupported software features or Simulink blocks in the model or model component that you want to analyze. See: Unsupported Simulink Blocks in Analysis Analysis Limitations and Considerations for Model Blocks Limitations of Simulink Design Verifier for Simulink Software Features Limitations of Simulink Design Verifier with Stateflow Features Simulink Design Verifier Limitations for MATLAB for Code Generation For models with unsupported blocks, use automatic stubbing to ignore the behavior of unsupported blocks during analysis. See Handle Model Complexities with Automatic Stubbing If you have a complex model with a large verification state space, see Perform Analysis on Large and Complex Models for tips on performing Simulink Design Verifier analysis.
Compatible	Simulink Design Verifier can analyze your model.

Capabilities and Limitations

• Does not run on library models.

• Analyzes content in masked subsystems. The input parameter Look inside masks is always set to all. You can use a filter to exclude specific subsystems. For more information, see Filter Objectives by Using Simulink Design Verifier Filter Explorer.

• Analyzes content of library-linked blocks. The input parameter Follow links is always set to on.

• Does not support exclusions.

See Also

• Run Model Advisor Checks and Review Results

• Check Model Compatibility for Analysis

• Handle Model Complexities with Automatic Stubbing

Simulink Design Verifier Defect Checker

Since R2025a

Defect Checker analyzes a model to identify design defects and unintended behaviors. It uses formal methods to determine whether defects such as dead logic, integer overflows, division by zero, and other run-time errors can occur for any combination of inputs and model states. It explores all possible execution paths within the specified bounds, enabling early detection of issues that might not be revealed by test cases. Defect Checker provides a predefined set of common checks and is not exhaustive. To perform an exhaustive analysis, use the individual design error detection checks.

Check for common defects using Simulink Design Verifier Defect Checker

Check ID: mathworks.sldv.defectchecker

Defect Checker is an optimized, preconfigured check that detects defects in a system, but does not confirm their absence.

Description.  Check for common defects in your model, such as dead logic, array out of bounds, integer overflow, division by zero, and design range violations. Run this check frequently. Running the check is quick and can detect defects early in the development process. For more information, see Detect Defects Using Optimized Checks.

Results and Recommended Actions

Result	Recommended Action
Failed, model incompatible with Simulink Design Verifier analysis	Resolve the model incompatibility. To identify unsupported blocks of model features, see: Unsupported Simulink Blocks in Analysis Analysis Limitations and Considerations for Model Blocks Limitations of Simulink Design Verifier for Simulink Software Features Limitations of Simulink Design Verifier with Stateflow Features Simulink Design Verifier Limitations for MATLAB for Code Generation Also see Detect Defects Using Optimized Checks.
Array out of bounds, integer overflow, division by zero, or design range violations found in model	To view the conditions that cause the defects, create a harness model. When you simulate the harness, the inputs replicate the error. Click View test case in the Model Advisor report.
Dead logic found in model	Simulink Design Verifier proved that these decision and condition outcomes cannot occur and are dead logic in the model. Dead logic can also be a side effect of specified constraints on parameters or specified minimum and maximum constraints on input ports.

Capabilities and Limitations

• The check is not exhaustive. To prove the absence of violations, run checks for dead logic, array out of bounds, integer overflow, division by zero, and design range violations separately.

• The check runs simplified checking of common defects and can be quicker than the exhaustive checks.

• The check cannot be run together with other design error checks.

• Because the check focuses on defects in the system, it does not report valid objectives. As a result, reports can be more readable.

• Analyzes content in masked subsystems. The input parameter Look inside masks is always set to all. You can use a filter to exclude specific subsystems. For more information, see Filter Objectives by Using Simulink Design Verifier Filter Explorer.

• Analyzes content of library-linked blocks. The input parameter Follow links is always set to on.

Simulink Design Verifier Design Error Checks

Simulink Design Verifier checks help you prepare your model for Simulink Design Verifier analysis by identifying elements of your model that might require special attention.

When you run a Simulink Design Verifier check, the Model Advisor performs a checkout of the Simulink Design Verifier license.

Using the Model Advisor, you can save check results in HTML files. See Save and View Model Advisor Check Reports. For more information on using the Model Advisor, see Run Model Advisor Checks. For more information on customizing the Model Advisor, see Automate Model Advisor Check Execution.

Check for dead logic

Check ID: mathworks.sldv.deadlogic

Identify logic that stays inactive during simulation.

Description.  This check identifies portions of your model that stay inactive during simulation.

You can run a more detailed analysis that identifies both dead logic and active logic using Simulink Design Verifier design error detection. For more information, see Detect Dead Logic Caused by an Incorrect Value.

Following the recommendations of this check increases the likelihood of generating MISRA™ C:2012 compliant code for embedded applications, as well as code that complies with the CERT^® C and CWE™ standards.

Results and Recommended Actions

Result	Recommended Action
Failed, model incompatible	Resolve the model incompatibility. See: Unsupported Simulink Blocks in Analysis Analysis Limitations and Considerations for Model Blocks Limitations of Simulink Design Verifier for Simulink Software Features Limitations of Simulink Design Verifier with Stateflow Features Simulink Design Verifier Limitations for MATLAB for Code Generation Also see Handle Model Complexities with Automatic Stubbing.
Dead logic found in model	Simulink Design Verifier proved that these decision and condition outcomes cannot occur and are dead logic in the model. Dead logic can also be a side effect of specified constraints on parameters or specified minimum and maximum constraints on input ports. In rare cases, dead logic can result from approximations performed by Simulink Design Verifier. It is possible that there are objectives that this analysis did not decide. To extend the results of this analysis, use Simulink Design Verifier design error detection to also identify active logic. In the Configuration Parameters dialog box, on the Design Verifier > Design Error Detection pane, select Dead logic (partial). Alternatively, set DVDetectDeadLogic and DVDetectActiveLogic to "on".
Dead logic not found in model	Simulink Design Verifier did not find dead logic in the model. It is possible that there are objectives that this analysis did not decide. To extend the results of this analysis, use Simulink Design Verifier design error detection to also identify active logic. In the Configuration Parameters dialog box, on the Design Verifier > Design Error Detection pane, select Dead logic (partial) or set DVDetectDeadLogic and DVDetectActiveLogic to "on".

Capabilities and Limitations

• Does not run on library models.

• Analyzes content in masked subsystems. The input parameter Look inside masks is always set to all. You can use a filter to exclude specific subsystems. For more information, see Filter Objectives by Using Simulink Design Verifier Filter Explorer.

• Analyzes content of library-linked blocks. The input parameter Follow links is always set to on.

• Does not support exclusions.

Tips.  If a dead logic warning results from a parameter that is intended to be tunable (for example, a parameter with an enumerated data type), configure that parameter for tuning in Simulink Design Verifier. When the parameter is tunable, the dead logic check considers alternative parameter values and can determine whether a previously dead branch is reachable. To configure parameters, use the Automatically infer parameter specification setting or the Parameter table in the Configuration Parameters dialog box to specify possible enumerated values. Then, run the Check for dead logic analysis on the model. For more information, see Create Parameter Configuration for Simulink Design Verifier Analysis.

See Also

• MISRA C:2012: Rule 2.1

• CERT C, MSC07-C

• CWE, CWE-561

• Run Model Advisor Checks

• Secure Coding (Embedded Coder)

• Detect Dead Logic Caused by an Incorrect Value

• Design Verifier Pane: Design Error Detection

• hisl_0101: Prevent operations that result in dead logic to improve code compliance

Check for out of bound array access

Check ID: mathworks.sldv.arraybounds

Detects operations that access memory outside the bounds of an array.

Description.  This check detects instances of out of bound array access in Simulink Design Verifier.

Following the recommendations of this check increases the likelihood of generating MISRA C:2012 compliant code for embedded applications, as well as code that complies with the CERT C, CWE, and ISO/IEC TS 17961 standards.

Results and Recommended Actions

Result	Recommended Action
Failed, model incompatible	Resolve the model incompatibility. See Unsupported Simulink Blocks in Analysis Analysis Limitations and Considerations for Model Blocks Limitations of Simulink Design Verifier for Simulink Software Features Limitations of Simulink Design Verifier with Stateflow Features Simulink Design Verifier Limitations for MATLAB for Code Generation Also see Handle Model Complexities with Automatic Stubbing.
Out of bound array access found in model	To view the conditions that cause the out of bound array access, create a harness model. When you simulate the harness with the given inputs, it replicates the error. Click View test case in the Model Advisor report.

Capabilities and Limitations

• Does not run on library models.

• Analyzes content in masked subsystems. The input parameter Look inside masks is always set to all. You can use a filter to exclude specific subsystems. For more information, see Filter Objectives by Using Simulink Design Verifier Filter Explorer.

• Analyzes content of library-linked blocks. The input parameter Follow links is always set to on.

• Does not support exclusions.

See Also

• MISRA C:2012: Rule 18.1

• ISO/IEC TS 17961: 2013, invptr

• CERT C, ARR30-C

• CWE, CWE-118

• Secure Coding (Embedded Coder)

• Detect and Address Bugs

• Detect Out of Bound Array Access Errors

Check for division by zero

Check ID: mathworks.sldv.divbyzero

Detects division-by-zero errors in your model.

Description.  This check identifies operations in your model that cause division-by-zero errors.

Following the recommendations of this check increases the likelihood of generating MISRA C:2012 compliant code for embedded applications, as well as code that complies with the CERT C, CWE, and ISO/IEC TS 17961 standards.

Results and Recommended Actions

Result	Recommended Action
Failed, model incompatible	Resolve the model incompatibility. See Unsupported Simulink Blocks in Analysis Analysis Limitations and Considerations for Model Blocks Limitations of Simulink Design Verifier for Simulink Software Features Limitations of Simulink Design Verifier with Stateflow Features Simulink Design Verifier Limitations for MATLAB for Code Generation Also see Handle Model Complexities with Automatic Stubbing.
Division by zero found in model	To view the conditions that cause the division by zero, create a harness model. When you simulate the harness with the given inputs, it replicates the error. Click View test case in the Model Advisor report.

Capabilities and Limitations

• Does not run on library models.

• Analyzes content in masked subsystems. The input parameter Look inside masks is always set to all. You can use a filter to exclude specific subsystems. For more information, see Filter Objectives by Using Simulink Design Verifier Filter Explorer.

• Analyzes content of library-linked blocks. The input parameter Follow links is always set to on.

• Does not support exclusions.

See Also

• MISRA C:2012: Directive 4.1

• ISO/IEC TS 17961: 2013, diverr

• CERT C, INT33-C and FLP03-C

• CWE, CWE-369

• Secure Coding (Embedded Coder)

• Detect and Address Bugs

• Detect Integer Overflow and Division-by-Zero Errors

• hisl_0067: Protect against divide-by-zero calculations

Check for integer overflow

Check ID: mathworks.sldv.integeroverflow

Detects integer or fixed-point data overflow errors in your model.

Description.  This check identifies operations that exceed the data type range for integer or fixed-point operations.

Following the recommendations of this check increases the likelihood of generating MISRA C:2012 compliant code for embedded applications, as well as code that complies with the CERT C, CWE, and ISO/IEC TS 17961 standards.

Results and Recommended Actions

Result	Recommended Action
Failed, model incompatible	Resolve the model incompatibility. See Unsupported Simulink Blocks in Analysis Analysis Limitations and Considerations for Model Blocks Limitations of Simulink Design Verifier for Simulink Software Features Limitations of Simulink Design Verifier with Stateflow Features Simulink Design Verifier Limitations for MATLAB for Code Generation Also see Handle Model Complexities with Automatic Stubbing.
Integer overflow found in model	To view the conditions that cause the integer overflow, create a harness model. When you simulate the harness with the given inputs, it replicates the error. Click View test case in the Model Advisor report.

Capabilities and Limitations

• Does not run on library models.

• Analyzes content in masked subsystems. The input parameter Look inside masks is always set to all. You can use a filter to exclude specific subsystems. For more information, see Filter Objectives by Using Simulink Design Verifier Filter Explorer.

• Analyzes content of library-linked blocks. The input parameter Follow links is always set to on.

• Does not support exclusions.

See Also

• MISRA C:2012: Directive 4.1

• ISO/IEC TS 17961: 2013, intoflow

• CERT C, INT30-C and INT32-C

• CWE, CWE-190

• Secure Coding (Embedded Coder)

• Detect and Address Bugs

• Detect Integer Overflow and Division-by-Zero Errors

Check for non-finite and NaN floating-point values

Check ID: mathworks.sldv.infnan

Detects nonfinite and NaN floating-point values in your model.

Description.  This check detects the occurrences of nonfinite and NaN floating-point values in your model.

Results and Recommended Actions

Result	Recommended Action
Failed, model incompatible	Resolve the model incompatibility. See Unsupported Simulink Blocks in Analysis Analysis Limitations and Considerations for Model Blocks Limitations of Simulink Design Verifier for Simulink Software Features Limitations of Simulink Design Verifier with Stateflow Features Simulink Design Verifier Limitations for MATLAB for Code Generation Also see Handle Model Complexities with Automatic Stubbing.
Nonfinite and NaN floating-point values found in model	To view the conditions that cause the occurrence of nonfinite and NaN floating-point values, create a harness model. When you simulate the harness with the given inputs, it replicates the error. Click View test case in the Model Advisor report.

Capabilities and Limitations

• Does not run on library models.

• Analyzes content in masked subsystems. The input parameter Look inside masks is always set to all. You can use a filter to exclude specific subsystems. For more information, see Filter Objectives by Using Simulink Design Verifier Filter Explorer.

• Analyzes content of library-linked blocks. The input parameter Follow links is always set to on.

• Does not support exclusions.

See Also

• Detect and Address Bugs

• Detect Non-Finite, NaN, and Subnormal Floating-Point Values

Check for subnormal floating-point values

Check ID: mathworks.sldv.subnormal

Detects subnormal floating-point values in your model.

Description.  This check detects the occurrences of subnormal floating-point values in your model.

Results and Recommended Actions

Result	Recommended Action
Failed, model incompatible	Resolve the model incompatibility. See Unsupported Simulink Blocks in Analysis Analysis Limitations and Considerations for Model Blocks Limitations of Simulink Design Verifier for Simulink Software Features Limitations of Simulink Design Verifier with Stateflow Features Simulink Design Verifier Limitations for MATLAB for Code Generation Also see Handle Model Complexities with Automatic Stubbing.
Subnormal floating-point values found in model	To view the conditions that cause the occurrence of subnormal floating-point values, create a harness model. When you simulate the harness with the given inputs, it replicates the error. Click View test case in the Model Advisor report.

Capabilities and Limitations

• Does not run on library models.

• Analyzes content in masked subsystems. The input parameter Look inside masks is always set to all. You can use a filter to exclude specific subsystems. For more information, see Filter Objectives by Using Simulink Design Verifier Filter Explorer.

• Analyzes content of library-linked blocks. The input parameter Follow links is always set to on.

• Does not support exclusions.

See Also

• Detect and Address Bugs

• Detect Non-Finite, NaN, and Subnormal Floating-Point Values

Check for specified minimum and maximum value violations

Check ID: mathworks.sldv.minmax

Detect signals that exceed specified minimum and maximum values.

Description.  This analysis checks the specified minimum and maximum values (the design ranges) on intermediate signals throughout the model and on the output ports. If the analysis detects that a signal exceeds the design range, the results identify where in the model the errors occurred.

Following the recommendations of this check increases the likelihood of generating MISRA C:2012 compliant code for embedded applications, as well as code that complies with the CERT C and CWE standards.

Results and Recommended Actions

Result	Recommended Action
Failed, model incompatible	Resolve the model incompatibility. See Unsupported Simulink Blocks in Analysis Analysis Limitations and Considerations for Model Blocks Limitations of Simulink Design Verifier for Simulink Software Features Limitations of Simulink Design Verifier with Stateflow Features Simulink Design Verifier Limitations for MATLAB for Code Generation Also see Handle Model Complexities with Automatic Stubbing.
Violation of minimum and/or maximum found in model	To view the conditions that cause the violation, create a harness model. When you simulate the harness with the given inputs, it replicates the error. Click View test case in the Model Advisor report.

Capabilities and Limitations

• Does not run on library models.

• Analyzes content in masked subsystems. The input parameter Look inside masks is set to all. You can use a filter to exclude specific subsystems. For more information, see Filter Objectives by Using Simulink Design Verifier Filter Explorer.

• Analyzes content of library-linked blocks. The input parameter Follow links is set to on.

• Does not support exclusions.

See Also

• MISRA C:2012: Directive 4.1

• CERT C, API00-C

• CWE, CWE-628

• Secure Coding (Embedded Coder)

• Detect and Address Run-Time Errors

• Check for Specified Minimum and Maximum Value Violations

Check for data store access violations

Check ID: mathworks.sldv.dsmaccessviolations

Detect data store access violations in your model.

Description.  This check detects these data store access violations:

• Read-before-write

• Write-after-read

• Write-after-write

Results and Recommended Actions

Result	Recommended Action
Failed, model incompatible	Resolve the model incompatibility. See: Unsupported Simulink Blocks in Analysis Analysis Limitations and Considerations for Model Blocks Limitations of Simulink Design Verifier for Simulink Software Features Limitations of Simulink Design Verifier with Stateflow Features Simulink Design Verifier Limitations for MATLAB for Code Generation Handle Model Complexities with Automatic Stubbing.
Data store access violations found	In the Model Advisor report, click View test case. The software creates a harness model and the Signal Editor block displays the test case that replicates the error.

Capabilities and Limitations

• Does not run on library models.

• Analyzes content in masked subsystems. The input parameter Look inside masks is always set to all. You can use a filter to exclude specific subsystems. For more information, see Filter Objectives by Using Simulink Design Verifier Filter Explorer.

• Analyzes content of library-linked blocks. By default, the input parameter Follow links is always set to on.

• Does not support exclusions.

See Also

• Detect and Address Bugs

• Detecting Access Order Errors

• Detect Data Store Access Violations

Check for block input range violations

Check ID: mathworks.sldv.blockinputrangeviolations

Detect block input range violations in your model.

Description.  This check detects input range violations when these blocks have the Diagnostic for out-of-range input input parameter set to Warning or Error:

• n-D Lookup Table

• Interpolation Using Prelookup

• Prelookup

• Direct Lookup Table (n-D)

The check also detects input range violations for:

• Multiport Switch blocks, when the Diagnostic for default case parameter is set to Warning or Error

• Trigonometric Function blocks, when the Approximation method parameter is set to CORDIC

Note

The check does not flag block input range violations for n-D Lookup Table blocks when the Interpolation method is set to Akima spline or Cubic spline.

Results and Recommended Actions

Result	Recommended Action
Failed, model incompatible	Resolve the model incompatibility. See: Unsupported Simulink Blocks in Analysis Analysis Limitations and Considerations for Model Blocks Limitations of Simulink Design Verifier for Simulink Software Features Limitations of Simulink Design Verifier with Stateflow Features Simulink Design Verifier Limitations for MATLAB for Code Generation Handle Model Complexities with Automatic Stubbing
Block input range violations found	In the Model Advisor report, click View test case. The software creates a harness model and the Signal Editor block displays the test case that replicates the error.

Capabilities and Limitations

• Does not run on library models.

• Analyzes content in masked subsystems. The input parameter Look inside masks is always set to all. You can use a filter to exclude specific subsystems. For more information, see Filter Objectives by Using Simulink Design Verifier Filter Explorer.

• Analyzes content of library-linked blocks. The input parameter Follow links is always set to on.

• Does not support exclusions.

See Also

• Detect and Address Bugs

Check usage of remainder and reciprocal operations - hisl_0002

Check ID: mathworks.sldv.hismviolationshisl_0002

Description.  This check identifies the usage of remand reciprocal operations that cause nonfinite results.

Results and Recommended Actions

Condition	Recommended Action
The model or subsystem contains rem or reciprocal operations that might result in nonfinite output signals. Nonfinite signals are not supported in real-time embedded systems.	When using the rem or reciprocal operation, prevent the corresponding input from being equal to zero.

Capabilities and Limitations

• Does not run on library models.

• Analyzes content in masked subsystems. The input parameter Look inside masks is always set to all. You can use a filter to exclude specific subsystems. For more information, see Filter Objectives by Using Simulink Design Verifier Filter Explorer.

• Analyzes content of library-linked blocks. The input parameter Follow links is always set to on.

• Does not support exclusions.

See Also

• hisl_0002: Usage of Math Function blocks (rem and reciprocal)

Check usage of square root operations - hisl_0003

Check ID: mathworks.sldv.hismviolationshisl_0003

Description.  This check Identifies square root operations with inputs that can be negative.

Results and Recommended Actions

Condition	Recommended Action
One or more square root operations in the model have inputs that can become negative during simulation.	Remodel to prevent the input of the square root operations from becoming negative.

Capabilities and Limitations

• Does not run on library models.

• Analyzes content in masked subsystems. The input parameter Look inside masks is always set to all. You can use a filter to exclude specific subsystems. For more information, see Filter Objectives by Using Simulink Design Verifier Filter Explorer.

• Analyzes content of library-linked blocks. The input parameter Follow links is always set to on.

• Does not support exclusions.

See Also

• hisl_0003: Usage of square root operations

Check usage of log and log10 operations - hisl_0004

Check ID: mathworks.sldv.hismviolationshisl_0004

Description.  Identifies the log and log10 operations that cause nonfinite results.

Results and Recommended Actions

Condition	Recommended Action
One or more log and log10 operations used in the model might require nonfinite number support, which is not supported in real-time embedded systems.	Prevent the input of log and log10 operations from being less than or equal to zero.

Capabilities and Limitations

• Does not run on library models.

• Analyzes content in masked subsystems. The input parameter Look inside masks is always set to all. You can use a filter to exclude specific subsystems. For more information, see Filter Objectives by Using Simulink Design Verifier Filter Explorer.

• Analyzes content of library-linked blocks. The input parameter Follow links is always set to on.

• Does not support exclusions.

See Also

• hisl_0004: Usage of Math Function blocks (natural logarithm and base 10 logarithm)

Check usage of Reciprocal Square Root blocks - hisl_0028

Check ID: mathworks.sldv.hismviolationshisl_0028

Description.  This check identifies Reciprocal Sqrt blocks with inputs that can be zero or negative.

Results and Recommended Actions

Condition	Recommended Action
One or more Reciprocal Sqrt blocks in the model have inputs that can become to zero or negative during simulation.	Remodel to prevent the input of the Reciprocal Sqrt blocks from becoming zero or negative.

Capabilities and Limitations

• Does not run on library models.

• Analyzes content in masked subsystems. The input parameter Look inside masks is always set to all. You can use a filter to exclude specific subsystems. For more information, see Filter Objectives by Using Simulink Design Verifier Filter Explorer.

• Analyzes content of library-linked blocks. The input parameter Follow links is always set to on.

• Does not support exclusions.

See Also

• hisl_0028: Usage of Reciprocal Square Root blocks