Some characteristics of Simulink® models can cause problems during a Simulink Design Verifier™ analysis in the following ways:
Complexity of model inputs due to:
Large number of inputs (The number of inputs can vary, depending on the individual model.)
Types of inputs (floating-point values, for example)
The way the inputs affect the model state and the objectives of the analysis
Number of possible simulation paths through a model
Portions of the model that cannot be reached
Large counters in the model
The topics in Complexity Reduction describe techniques designed to reduce the impact of this complexity and achieve the best performance from Simulink Design Verifier.
Most of these techniques focus on test generation for large models. However, you can use many of them to detect design errors or prove the properties of a large model and generate counterexamples when a property is disproved. In addition, Prove Properties in Large Models describes specific techniques for proving properties in a large model.