Main Content

Simulink Design Verifier Checks

Simulink Design Verifier Checks Overview

These checks help you prepare your model for Simulink® Design Verifier™ analysis. When you run a Simulink Design Verifier check, the Model Advisor checks out the Simulink Design Verifier license.

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

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

ConditionRecommended Action
Incompatible

Avoid using the following unsupported software features or Simulink blocks in the model or model component that you want to analyze:

Partially compatible
CompatibleSimulink Design Verifier can analyze your model.

See Also

Detect 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

ResultRecommended Action
Failed, model incompatible

Resolve the model incompatibility. See:

Also see Handle Incompatibilities with Automatic Stubbing.

Dead logic found in modelSimulink 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. From the Simulink Editor, select Apps > Design Verifier > Settings. In the Configuration Parameters window, from Design Verifier > Design Error Detection pane, select both Dead logic and Identify active logic.
Dead logic not found in modelSimulink 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. From the Simulink Editor, select Apps > Design Verifier > Settings. In the Configuration Parameters window, from Design Verifier > Design Error Detection pane, select both Dead logic and Identify active logic.

See Also

Detect Out Of Bound Array Access

Check ID: mathworks.sldv.arraybounds

Detects operations that access outside the bounds of an array index

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, ISO/IEC TS 17961 standards.

Results and Recommended Actions

ResultRecommended Action
Failed, model incompatible

Resolve the model incompatibility. See

Also see Handle Incompatibilities 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, the inputs replicate the error. Click View test case in the Model Advisor report.

See Also

Detect 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, ISO/IEC TS 17961 standards.

Results and Recommended Actions

ResultRecommended Action
Failed, model incompatible

Resolve the model incompatibility. See

Also see Handle Incompatibilities 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, the inputs replicate the error. Click View test case in the Model Advisor report.

See Also

Detect 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, ISO/IEC TS 17961 standards.

Results and Recommended Actions

ResultRecommended Action
Failed, model incompatible

Resolve the model incompatibility. See

Also see Handle Incompatibilities 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, the inputs replicate the error. Click View test case in the Model Advisor report.

See Also

Detect 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

ResultRecommended Action
Failed, model incompatible

Resolve the model incompatibility. See

Also see Handle Incompatibilities 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, the inputs replicate the error. Click View test case in the Model Advisor report.

See Also

Detect 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

ResultRecommended Action
Failed, model incompatible

Resolve the model incompatibility. See

Also see Handle Incompatibilities 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, the inputs replicate the error. Click View test case in the Model Advisor report.

See Also

Detect Specified Minimum and Maximum Value Violations

Check ID: mathworks.sldv.minmax

Detect signals which 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

ResultRecommended Action
Failed, model incompatible

Resolve the model incompatibility. See

Also see Handle Incompatibilities 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, the inputs replicate the error. Click View test case in the Model Advisor report.

See Also

Detect 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

ResultRecommended Action
Failed, model incompatible

Resolve the model incompatibility. See:

Data store access violations found

In the Model Advisor report, click View test case. The software creates a harness model and the Signal Builder block displays the test case that replicates the error.

See Also

Detect Block Input Range Violations

Check ID: mathworks.sldv.blockinputrangeviolations

Detect block input range violations in your model.

Description

This check detects input range violations for blocks with these settings:

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

ResultRecommended Action
Failed, model incompatible

Resolve the model incompatibility. See:

Block input range violations found

In the Model Advisor report, click View test case. The software creates a harness model and the Signal Builder block displays the test case that replicates the error.

See Also

Check usage of Math Function blocks (rem and reciprocal functions)

Check ID: mathworks.sldv.hismviolationshisl_0002

Description

Identifies the usage of Math Function blocks using rem and reciprocal functions that cause non-finite results.

Results and Recommended Actions

ConditionRecommended Action
The model or subsystem contains Math Function - reciprocal (reciprocal) or remainder (rem) blocks that might result in non-finite output signals. Non-finite signals are not supported in real-time embedded systems.When using the Math Function block with a rem or reciprocalfunction blocks, protect the input to the block from being less than or equal to zero.

See Also

Check usage of Sqrt blocks

Check ID: mathworks.sldv.hismviolationshisl_0003

Description

Identify Sqrt blocks with inputs that can be negative.

Results and Recommended Actions

ConditionRecommended Action
One or more Sqrt blocks in the model have inputs that can go negative during simulation.Remodel to protect the input of the Sqrt blocks from going negative.

See Also

Check usage of Math Function blocks (log and log10 functions)

Check ID: mathworks.sldv.hismviolationshisl_0004

Description

Identifies the Math Function blocks using log and log10 functions that cause non-finite results.

Results and Recommended Actions

ConditionRecommended Action
One or more Math blocks in the model use the natural/base 10 logarithm (Log and Log10) blocks and might require non-finite number support, which is not supported in real-time embedded systems.Consider protecting the input of the blocks such that it is not less than or equal to zero.

See Also

Check usage of Reciprocal Sqrt blocks

Check ID: mathworks.sldv.hismviolationshisl_0028

Description

Identifies Reciprocal Sqrt blocks with inputs that can go zero or negative.

Results and Recommended Actions

ConditionRecommended Action
One or more Reciprocal Sqrt blocks in the model have inputs that can go to zero or negative during simulation.Remodel to protect the input of the Reciprocal Sqrt blocks from going negative.

See Also