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
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:
|
Partially compatible |
|
Compatible | Simulink Design Verifier can analyze your model. |
See Also
Run Model Advisor Checks and Review Results
Check Model Compatibility
Handle Incompatibilities with Automatic Stubbing
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:
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 . |
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: Avoid 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
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
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
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
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
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
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
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 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
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 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
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
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:
|
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. |
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
orError
: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
orError
.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:
|
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. |
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. |
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. |
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. |
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. |
See Also
hisl_0028: Usage of Reciprocal Square Root blocks