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 ID:
mathworks.sldv.compatibility
Identify elements that Simulink Design Verifier analysis does not support.
This check assesses your model for compatibility with Simulink Design Verifier.
| 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. |
Check ID:
mathworks.sldv.deadlogic
Identify logic that stays inactive during simulation.
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
| Result | Recommended Action |
|---|---|
| Failed, model incompatible | Resolve the model incompatibility. See:
|
| 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 both Dead logic and Identify active logic. |
| 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 both Dead logic and Identify active logic. |
MISRA C:2012: Rule 2.1
CERT C, MSC07-C
CWE, CWE-561
Secure Coding Standards (Embedded Coder)
Check ID:
mathworks.sldv.arraybounds
Detects operations that access outside the bounds of an array index
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.
| Result | Recommended Action |
|---|---|
| Failed, model incompatible | Resolve the model incompatibility. See
|
| 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. |
MISRA C:2012: Rule 18.1
ISO/IEC TS 17961: 2013, invptr
CERT C, ARR30-C
CWE, CWE-118
Secure Coding Standards (Embedded Coder)
Check ID:
mathworks.sldv.divbyzero
Detects division-by-zero errors in your model
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.
| Result | Recommended Action |
|---|---|
| Failed, model incompatible | Resolve the model incompatibility. See
|
| 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. |
MISRA C:2012: Directive 4.1
ISO/IEC TS 17961: 2013, diverr
CERT C, INT33-C and FLP03-C
CWE, CWE-369
Secure Coding Standards (Embedded Coder)
Check ID:
mathworks.sldv.integeroverflow
Detects integer or fixed-point data overflow errors in your model
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.
| Result | Recommended Action |
|---|---|
| Failed, model incompatible | Resolve the model incompatibility. See
|
| 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. |
MISRA C:2012: Directive 4.1
ISO/IEC TS 17961: 2013, intoflow
CERT C, INT30-C and INT32-C
CWE, CWE-190
Secure Coding Standards (Embedded Coder)
Check ID: mathworks.sldv.infnan
Detects Nonfinite and NaN floating-point values in your model
This check detects the occurrences of nonfinite and NaN floating-point values in your model.
| Result | Recommended Action |
|---|---|
| Failed, model incompatible | Resolve the model incompatibility. See
|
| 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. |
Check ID:
mathworks.sldv.subnormal
Detects subnormal floating-point values in your model
This check detects the occurrences of subnormal floating-point values in your model.
| Result | Recommended Action |
|---|---|
| Failed, model incompatible | Resolve the model incompatibility. See
|
| 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. |
Check ID: mathworks.sldv.minmax
Detect signals which exceed specified minimum and maximum values
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.
| Result | Recommended Action |
|---|---|
| Failed, model incompatible | Resolve the model incompatibility. See
|
| 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. |
MISRA C:2012: Directive 4.1
CERT C, API00-C
CWE, CWE-628
Secure Coding Standards (Embedded Coder)
Check ID:
mathworks.sldv.dsmaccessviolations
Detect data store access violations in your model.
This check detects these data store access violations:
Read-before-write
Write-after-read
Write-after-write
| 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 Builder block displays the test case that replicates the error. |
Check ID:
mathworks.sldv.blockinputrangeviolations
Detect block input range violations in your model.
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:
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.
| 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 Builder block displays the test case that replicates the error. |
Check ID:
mathworks.sldv.hismviolationshisl_0002
Identifies the usage of Math Function blocks using rem and reciprocal functions that cause non-finite results.
| Condition | Recommended 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. |
Check ID:
mathworks.sldv.hismviolationshisl_0003
Identify Sqrt blocks with inputs that can be negative.
| Condition | Recommended 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. |
Check ID:
mathworks.sldv.hismviolationshisl_0004
Identifies the Math Function blocks using log and log10 functions that cause non-finite results.
| Condition | Recommended 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. |
Check ID:
mathworks.sldv.hismviolationshisl_0028
Identifies Reciprocal Sqrt blocks with inputs that can go zero or negative.
| 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. |