Sources of Model Complexity

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 Reduce Model Complexity 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.