Simulink® Design Verifier™ analysis searches through sequences of states to find input values that drive the analysis to reach a state that satisfies an objective. Each counter value or timer step corresponds to a different state, so the presence of long timers or counters can dramatically increase the size of the state representation. Since analysis complexity depends on the size of the state representation, you must give special consideration to counters and timers in your model to avoid over complicating Simulink Design Verifier analysis.
For the purposes of Simulink Design Verifier analysis, the term configuration refers to a set of values for all the persistent information in your model.
The search process investigates all configurations that can be reached in a single timer step before considering any of the configurations that can be reached in two timer steps. Likewise, the search investigates all configurations that can be reached in two timer steps before it considers any configuration that requires three or more timer steps, and so on. The number of timer steps required to exhaust the counter directly affects the number of states that the analysis needs to search. Models that contain time delays, such as countdown timers, complicate the analysis by forcing the search to span a large number of states.
You may see similar effects when systems use extensive averaging and filtering to delay the response to a change in inputs. Any aspect of the design that delays the response causes the test sequences to contain more timer steps, resulting in longer test cases that are more difficult to identify.
Some basic techniques you can use to improve analysis performance in models with counters or timers include the following:
Choose very small values for time delays. A system with a logical error when a time delay is set to 2000 steps usually demonstrates that error if the time delay is changed to 2 steps. If your system has several delays, choose small but unique values for each of them so that your delays are progressively satisfied.
Make the initial values of counters and timers parameter values that Simulink Design Verifier can modify. The software finds initial values that allow shorter test cases to exceed thresholds. For more information, see Parameter Constraint Values.
Choose higher frequency cutoffs for filters and fewer samples to average to minimize filtering delays.
Some more advanced techniques you can use to improve analysis performance in models with counters or timers include the following:
sldvtimer to identify timer
patterns that can be optimized for Simulink
Design Verifier test generation.
Use an existing test case or set of test cases that exhausts the counter or timer, and extend those test cases to create a full test suite. For more information, see Defining and Extending Existing Tests Cases.