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.

Simulink Design Verifier Compatibility Check

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 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 the following unsupported software features or Simulink blocks in the model or model component that you want to analyze: Supported and Unsupported Simulink Blocks in Simulink Design Verifier Support Limitations for Model Blocks Support Limitations of Simulink Design Verifier for Simulink Software Features Support Limitations for Stateflow Software Features Support Limitations for MATLAB for Code Generation
Partially compatible	Use automatic stubbing to ignore the behavior of unsupported blocks during analysis. See Handle Incompatibilities with Automatic Stubbing Analyze components of your model separately. See Extract Subsystems for Analysis and Bottom-Up Approach to Model Analysis If you have a complex model with a large verification state space, see Sources of Model Complexity 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. By default, the input parameter Look under masks is set to all.

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

• Does not support exclusions.

See Also

• Run Model Advisor Checks and Review Results

• Handle Incompatibilities with Automatic Stubbing

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.

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

Result	Recommended Action
Failed, model incompatible	Resolve the model incompatibility. See: Supported and Unsupported Simulink Blocks in Simulink Design Verifier Support Limitations for Model Blocks Support Limitations of Simulink Design Verifier for Simulink Software Features Support Limitations for Stateflow Software Features Support Limitations for MATLAB for Code Generation Also see Handle Incompatibilities 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. From the Simulink Editor, select Apps > Design Verifier > Settings. In the Configuration Parameters window, from Design Verifier > Design Error Detection pane, select Dead logic (partial) or 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. From the Simulink Editor, select Apps > Design Verifier > Settings. In the Configuration Parameters window, from 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. By default, the input parameter Look under masks is set to all.

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

• Does not support exclusions.

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

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

Result	Recommended Action
Failed, model incompatible	Resolve the model incompatibility. See Supported and Unsupported Simulink Blocks in Simulink Design Verifier Support Limitations for Model Blocks Support Limitations of Simulink Design Verifier for Simulink Software Features Support Limitations for Stateflow Software Features Support Limitations for MATLAB for Code Generation 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.

Capabilities and Limitations

• Does not run on library models.

• Analyzes content in masked subsystems. By default, the input parameter Look under masks is set to all.

• Analyzes content of library-linked blocks. By default, the input parameter Follow links is 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

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

Result	Recommended Action
Failed, model incompatible	Resolve the model incompatibility. See Supported and Unsupported Simulink Blocks in Simulink Design Verifier Support Limitations for Model Blocks Support Limitations of Simulink Design Verifier for Simulink Software Features Support Limitations for Stateflow Software Features Support Limitations for MATLAB for Code Generation 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.

Capabilities and Limitations

• Does not run on library models.

• Analyzes content in masked subsystems. By default, the input parameter Look under masks is set to all.

• Analyzes content of library-linked blocks. By default, the input parameter Follow links is 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

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

Result	Recommended Action
Failed, model incompatible	Resolve the model incompatibility. See Supported and Unsupported Simulink Blocks in Simulink Design Verifier Support Limitations for Model Blocks Support Limitations of Simulink Design Verifier for Simulink Software Features Support Limitations for Stateflow Software Features Support Limitations for MATLAB for Code Generation 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.

Capabilities and Limitations

• Does not run on library models.

• Analyzes content in masked subsystems. By default, the input parameter Look under masks is set to all.

• Analyzes content of library-linked blocks. By default, the input parameter Follow links is 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

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

Result	Recommended Action
Failed, model incompatible	Resolve the model incompatibility. See Supported and Unsupported Simulink Blocks in Simulink Design Verifier Support Limitations for Model Blocks Support Limitations of Simulink Design Verifier for Simulink Software Features Support Limitations for Stateflow Software Features Support Limitations for MATLAB for Code Generation 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.

Capabilities and Limitations

• Does not run on library models.

• Analyzes content in masked subsystems. By default, the input parameter Look under masks is set to all.

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

• Does not support exclusions.

See Also

• Detect and Address Bugs

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

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

Result	Recommended Action
Failed, model incompatible	Resolve the model incompatibility. See Supported and Unsupported Simulink Blocks in Simulink Design Verifier Support Limitations for Model Blocks Support Limitations of Simulink Design Verifier for Simulink Software Features Support Limitations for Stateflow Software Features Support Limitations for MATLAB for Code Generation 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.

Capabilities and Limitations

• Does not run on library models.

• Analyzes content in masked subsystems. By default, the input parameter Look under masks is set to all.

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

• Does not support exclusions.

See Also

• Detect and Address Bugs

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

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

Result	Recommended Action
Failed, model incompatible	Resolve the model incompatibility. See Supported and Unsupported Simulink Blocks in Simulink Design Verifier Support Limitations for Model Blocks Support Limitations of Simulink Design Verifier for Simulink Software Features Support Limitations for Stateflow Software Features Support Limitations for MATLAB for Code Generation 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.

Capabilities and Limitations

• Does not run on library models.

• Analyzes content in masked subsystems. By default, the input parameter Look under masks is set to all.

• Analyzes content of library-linked blocks. By default, 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

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

Result	Recommended Action
Failed, model incompatible	Resolve the model incompatibility. See: Supported and Unsupported Simulink Blocks in Simulink Design Verifier Support Limitations for Model Blocks Support Limitations of Simulink Design Verifier for Simulink Software Features Support Limitations for Stateflow Software Features Support Limitations for MATLAB for Code Generation Handle Incompatibilities 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. By default, the input parameter Look under masks is set to all.

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

• Does not support exclusions.

See Also

• Detect and Address Bugs

• Detecting Access Order Errors

• Detect Data Store Access Violations

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:

• For these blocks, when the Diagnostic for out-of-range input parameter is set to Warning or Error:

  • n-D Lookup Table

  • Interpolation Using Prelookup

  • Prelookup

  • Direct Lookup Table (n-D)

• 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: Supported and Unsupported Simulink Blocks in Simulink Design Verifier Support Limitations for Model Blocks Support Limitations of Simulink Design Verifier for Simulink Software Features Support Limitations for Stateflow Software Features Support Limitations for MATLAB for Code Generation Handle Incompatibilities 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. By default, the input parameter Look under masks is set to all.

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

• Does not support exclusions.

See Also

• Detect and Address Bugs

Check usage of rem and reciprocal operations

Check ID: mathworks.sldv.hismviolationshisl_0002

Description

Identifies the usage of rem and reciprocal operations that cause non-finite results.

Results and Recommended Actions

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

Capabilities and Limitations

• Does not run on library models.

• Analyzes content in masked subsystems. By default, the input parameter Look under masks is set to all.

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

• Does not support exclusions.

See Also

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

Check usage of Sqrt operations

Check ID: mathworks.sldv.hismviolationshisl_0003

Description

Identify Sqrt operations with inputs that can be negative.

Results and Recommended Actions

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

Capabilities and Limitations

• Does not run on library models.

• Analyzes content in masked subsystems. By default, the input parameter Look under masks is set to all.

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

• Does not support exclusions.

See Also

• hisl_0003: Usage of square root operations

Check usage of log and log10 operations

Check ID: mathworks.sldv.hismviolationshisl_0004

Description

Identifies the log and log10 operations that cause non-finite results.

Results and Recommended Actions

Condition	Recommended Action
One or more log and log10 operations used in the model might require non-finite number support, which is not supported in real-time embedded systems.	Consider protecting the input of these operations such that it is not less than or equal to zero.

Capabilities and Limitations

• Does not run on library models.

• Analyzes content in masked subsystems. By default, the input parameter Look under masks is set to all.

• Analyzes content of library-linked blocks. By default, the input parameter Follow links is 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 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

Condition	Recommended 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.

Capabilities and Limitations

• Does not run on library models.

• Analyzes content in masked subsystems. By default, the input parameter Look under masks is set to all.

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

• Does not support exclusions.

See Also

• hisl_0028: Usage of Reciprocal Square Root blocks