Supported and Unsupported Simulink Blocks in Simulink Design Verifier

Simulink^® Design Verifier™ provides various levels of support for the Simulink blocks:

• Supported

• Not supported

In order to improve the scalability of the analysis, automatic stubbing conservatively abstracts the block behavior. As a result, the analysis may not successfully analyze all the objectives. For more details about automatic stubbing, see Handle Incompatibilities with Automatic Stubbing.

The following tables summarize Simulink Design Verifier analysis support for Simulink blocks. Each table lists the blocks in a Simulink library and also describes support information for that particular block.

 Additional Math and Discrete Library

The software supports all blocks in the Additional Math and Discrete library.

 Commonly Used Blocks Library

The Commonly Used Blocks library includes blocks from other libraries. Those blocks are listed under their respective libraries.

 Continuous Library

Block	Support Notes
Derivative	Not supported
Integrator	Not supported
Integrator Limited	Not supported
PID Controller	Not supported
PID Controller (2DOF)	Not supported
Second-Order Integrator	Not supported
Second-Order Integrator Limited	Not supported
State-Space	Not supported
Transfer Fcn	Not supported
Transport Delay	Not supported
Variable Time Delay	Not supported
Variable Transport Delay	Not supported
Zero-Pole	Not supported

 Discontinuities Library

The software supports all blocks in the Discontinuities library.

 Discrete Library

Block	Support Notes
Delay	Supported
Difference	Supported
Discrete Derivative	Supported
Discrete Filter	Supported
Discrete FIR Filter	Supported
Discrete PID Controller	Supported
Discrete PID Controller (2DOF)	Supported
Discrete State-Space	Not supported
Discrete Transfer Fcn	Supported
Discrete Zero-Pole	Not supported
Discrete-Time Integrator	Supported
Memory	Supported
Tapped Delay	Supported
Transfer Fcn First Order	Supported
Transfer Fcn Lead or Lag	Supported
Transfer Fcn Real Zero	Supported
Unit Delay	Supported
Zero-Order Hold	Supported

 Logic and Bit Operations Library

The software supports all blocks in the Logic and Bit Operations library.

 Lookup Tables Library

Block	Support Notes
Cosine	Supported
Direct Lookup Table (n-D)	Supported
Interpolation Using Prelookup	Not supported when: The Interpolation method parameter is Linear and the Number of table dimensions parameter is greater than 4. or The Interpolation method parameter is Linear and the Number of sub-table selection dimensions parameter is not 0.
1-D Lookup Table	Not supported when the Interpolation method or the Extrapolation method parameter is Cubic Spline.
2-D Lookup Table	Not supported when the Interpolation method or the Extrapolation method parameter is Akima Spline.
n-D Lookup Table	Not supported when: The Interpolation method or the Extrapolation method parameter is Cubic Spline. or The Interpolation method parameter is Linear and the Number of table dimensions parameter is greater than 5. Not supported when the Interpolation method or the Extrapolation method parameter is Akima Spline.
Lookup Table Dynamic	Supported
Prelookup	Supported
Sine	Supported

 Math Operations Library

Block	Support Notes
Abs	Supported
Add	Supported
Algebraic Constraint	Supported
Assignment	Supported
Bias	Supported
Complex to Magnitude-Angle	Supported
Complex to Real-Imag	Supported
Divide	Supported
Dot Product	Supported
Find Nonzero Elements	Not supported
Gain	Supported
Magnitude-Angle to Complex	Supported
Math Function	Supported. Support for pow function is limited to integer exponents only.
Matrix Concatenate	Supported
MinMax	Supported
MinMax Running Resettable	Supported
Permute Dimensions	Supported
Polynomial	Supported
Product	Supported
Product of Elements	Supported
Real-Imag to Complex	Supported
Reciprocal Sqrt	Not supported
Reshape	Supported
Rounding Function	Supported
Sign	Supported
Signed Sqrt	Not supported
Sine Wave Function	Not supported
Slider Gain	Supported
Sqrt	Supported
Squeeze	Supported
Subtract	Supported
Sum	Supported
Sum of Elements	Supported
Trigonometric Function	Supported if Function is sin, cos, or sincos, and Approximation method is CORDIC. Partially supported otherwise.
Unary Minus	Supported
Vector Concatenate	Supported
Weighted Sample Time Math	Supported

 Model Verification Library

The software supports all blocks in the Model Verification library.

 Model-Wide Utilities Library

Block	Support Notes
Block Support Table	Supported
DocBlock	Supported
Model Info	Supported
Timed-Based Linearization	Not supported
Trigger-Based Linearization	Not supported

 Ports & Subsystems Library

Block	Support Notes
Atomic Subsystem	Supported
Code Reuse Subsystem	Supported
Enable	Supported
Enabled Subsystem	Design range checks do not consider specified minimum and maximum values for blocks connected to the output port of the subsystem. For more information on design range checks, see Check for Specified Minimum and Maximum Value Violations. Simulink Design Verifier treats Enabled Subsystems as short-circuited during test generation.
Enabled and Triggered Subsystem	Not supported when the trigger control signal specifies a fixed-point data type. Design range checks do not consider specified minimum and maximum values for blocks connected to the output port of the subsystem. For more information on design range checks, see Check for Specified Minimum and Maximum Value Violations. Simulink Design Verifier treats Enabled and Triggered Subsystems as short-circuited during test generation.
For Each	Supported with the following limitations: When For Each Subsystem contains one or more Simulink Design Verifier Test Condition, Test Objective, Proof Assumption, or Proof Objective blocks, not supported. When the mask parameters of the For Each Subsystem are partitioned, not supported.
For Each Subsystem	Supported with the following limitations: When For Each Subsystem contains one or more Simulink Design Verifier Test Condition, Test Objective, Proof Assumption, or Proof Objective blocks, not supported. When the mask parameters of the For Each Subsystem are partitioned, not supported.
For Iterator Subsystem	Supported
Function-Call Feedback Latch	Supported
Function-Call Generator	Supported
Function-Call Split	Supported
Function-Call Subsystem	Design range checks do not consider specified minimum and maximum values for blocks connected to the output port of the subsystem. For more information on design range checks, see Check for Specified Minimum and Maximum Value Violations.
Function Element	Not supported
Function Element Call	Not supported
If	Parameter configurations are not supported. The analysis ignores parameter configurations that you specify for an If block.
If Action Subsystem	Supported
In Bus Element	Supported
Inport	Supported
Model	Supported except for the limitations described in Support Limitations for Model Blocks.
Message Polling Subsystem	Not supported
Message Triggered Subsystem	Not supported
Out Bus Element	Supported
Outport	Supported
Resettable Subsystem	Supported
Subsystem	Supported
Variant Transitions in Stateflow (Stateflow)	Supported Only the active variant is analyzed.
Switch Case	Supported
Switch Case Action Subsystem	Supported
Trigger	Supported
Triggered Subsystem	Not supported when the trigger control signal specifies a fixed-point data type. Design range checks do not consider specified minimum and maximum values for blocks connected to the output port of the subsystem. For more information on design range checks, see Check for Specified Minimum and Maximum Value Violations. Simulink Design Verifier treats Enabled Subsystems as short-circuited during test generation.
Variant Subsystem	Simulink Design Verifier analyzes all variant choices when Variant activation time is set to startup. For remaining types of Variant activation time, Simulink Design Verifier analyzes only the active variant choice.
While Iterator Subsystem	Supported

 Signal Attributes Library

The software supports all blocks in the Signal Attributes library.

 Signal Routing Library

Block	Support Notes
Bus Assignment	Supported
Bus Creator	Supported
Bus Selector	Supported
Data Store Memory	Not supported when Data Store Memory block is used to define a reference to a Data Store Memory block in a higher level in the model hierarchy
Data Store Read	Supported
Data Store Write	Supported
Demux	Supported
Environment Controller	Supported
From	Supported
Goto	Supported
Goto Tag Visibility	Supported
Index Vector	Supported
Manual Switch	The Manual Switch block is compatible with the software, but the analysis ignores this block in a model. The analysis does not flag the coverage objectives for this block as satisfiable or unsatisfiable. Model coverage data is collected for the Manual Switch block.
Merge	Supported
Multiport Switch	Supported
Mux	Supported
Selector	Supported
Switch	Supported
Vector Concatenate	Supported

 Sinks Library

Block	Support Notes
Display	Supported
Floating Scope	Supported
Outport (Out1)	Supported
Out Bus Element	Supported
Scope	Supported
Stop Simulation	Not supported
Terminator	Supported
To File	Supported
To Workspace	Supported

 Sources Library

Block	Support Notes
Band-Limited White Noise	Not supported
Chirp Signal	Not supported
Clock	Supported
Constant	Supported unless Constant value is inf or nan (in which case, it is not supported).
Counter Free-Running	Supported
Counter Limited	Supported
Digital Clock	Supported
Enumerated Constant	Supported
From File	Not supported. When MAT-file data is stored in MATLAB® timeseries format, not supported.
From Workspace	Not supported
Ground	Supported
Inport (In1)	Supported
In Bus Element	Supported if Simulink.Bus type is defined for the In Bus Element.
Pulse Generator	Supported
Ramp	Supported
Random Number	Not supported
Repeating Sequence	Not supported
Repeating Sequence Interpolated	Not supported
Repeating Sequence Stair	Supported
Signal Editor	Not supported
Signal Generator	Not supported if wave form is sine. Supported if wave form is square. Not supported if wave form is random.
Sine Wave	Not supported
Step	Supported
Uniform Random Number	Not supported

 Toolbox Libraries

Toolbox Library	Support Notes
Simscape™	Not supported
Vehicle Network Toolbox™	Not supported

 User-Defined Functions Library

Block	Support Notes
C Function	Not supported. The C Function block is stubbed out during the Simulink Design Verifier analysis.
C Caller	Supported.
Initialize Function	Not Supported for Initialize function containing Parameter Writer blocks. Not supported as a target for subsystem analysis.
Interpreted MATLAB Function	Not supported
Level-2 MATLAB S-Function	Not supported.
MATLAB Function	For limitations, see Support Limitations for MATLAB for Code Generation.
MATLAB System	Decision, Condition and MCDC Coverage objectives are supported in Test Generation. Enhanced MCDC, Relational Boundary and Custom Test objectives are not supported. Custom Proof objectives are not supported in Property Proving. For further limitations, see Support Limitations for MATLAB for Code Generation. Logical expressions within assignment statements are not analyzed for coverage objectives.
Reset Function	Supported when harness is provided.
Reinitialize Function	Supported when harness is provided.
S-Function Builder	For limitations, see Support Limitations and Considerations for S-Functions and C/C++ Code.
Simulink Function	For export-function models, see Analyze Export-Function Models. Global Simulink functions within a non export-function model reference are not supported.
Terminate Function	Not supported. The behavior of Terminate function is ignored and is replaced by an empty function during the analysis. Not supported as a target for subsystem analysis.
Observer Reference (Simulink Test)	Supported with limitations. See Isolate Verification Logic with Observers.