VERIFICATION

The visualSTATE 7.1 release features a major update to the verification engine and especially the compositional mode. Below is a brief overview of the updates and changes:

• The Compositional mode of formal verification has been renamed to Full Compositional and extended to incorporate major new functionality. The Full Compositional mode is now similar to the traditional Full Forward mode of verification in terms of what it can verify. This means that all available design information, including guard and assignment expressions are now included in the verification .
• The compositional backwards verification works differently from the traditional full forward verification in that it checks one rule at a time, where a rule is a transition or a state configuration. By working backwards from a certain transition or state configuration and computing the reachability of the start configuration the compositional verification can exploit design locality in a way that the forward looking algorithm cannot, thus reducing verification complexity both in terms of time and space for models with favorable properties. See below for a discussion of different strategies for verification.
• The updated compositional mode now displays the rule that is currently being checked and gives the user the choice to interactively skip checking a specific rule if the checking takes too long. A universal timeout in seconds can also be specified. All skipped rules will be listed in the verification report. Note that skipping rules will never report any false positives or false negatives. If a rule is skipped it will just be excluded from checking and reported as skipped.
• The functionality to skip checks is also implemented in the default Full Forward mode. Here it means that the state space exploration will be interrupted and subsequent checks like reachability checks, dead-end checks etc will be performed on an incomplete representation of the state space. This means that design elements can be reported as not reachable etc even though they are reachable. The usability of skip for full forward mode is very dependent on the model.
• The set of verification options are simplified in the GUI. We have removed some of the seldom used verification options from the options dialogue. The options are still available for verification runs started from the command line.

VERIFICATION STRATEGIES

Different design models have different verification complexity and it is unfortunately very difficult to guess or estimate the complexity by just looking at a model. The visualSTATE user guide has a discussion of design patterns that can affect verification complexity, see Designing for verification in part 4 of the guide. In addition to the information in the guide, the following issues can also be worth considering:

• The guide recommends keeping down the usage of signals. This is in itself a sound advice as signals and especially the signal queue adds to the verification complexity. However, a moderate use of signals is generally not problematic. What heuristically can cause large complexity is use of transitions that trigger on a signal and then in turn emits one or more signals when triggered. Such cascading signals can in some circumstances increase the verification complexity dramatically.
• If possible avoid heavy interleaving, that is avoid assigning and reading the same variable in many different regions in the model. This way of designing is sometimes the only viable way to express something. However, the same effects on complexity can be caused by reusing a specific variable for different temporary computations at different places in the design.
• It can be beneficial to express certain boolean properties or properties with a small number of values as state machines, instead of using internal variables. Transitions can then use positive or negative state guards instead of a guard condition involving a variable. This can reduce verification complexity.
• A succesful verification run can very well take hours to run.

SUGGESTED WORKFLOW

Here is a suggested verification workflow.

1. Run verification frequently during design. For long runs it can be beneficial to set up a nightly verification job.
2. Use the default Full Forward verification mode.
3. If verification times or memory requirements increase dramatically switch to Full Compositional mode.
   • Use the feedback from the interaction window to pinpoint rules that seem complex to check
   • Use the skip functionality or specify an automatic timeout, to get a feeling for how many rules that are adding to verification complexity. Note that if reachability for a certain transition is difficult to compute, the real complexity might come from one or more transitions that must trigger before the checked transition can be reached. Such complexity can arise from complex signal patterns, or compund guard conditions where the guard condition is dependent on several variables for example.
   • Decide if it is acceptable to use a timeout to skip some rules from checking, or if a redesign should be attempted to bring down verification complexity.
4. Some models respond very favorable to a technique called variable reordering where the underlying data structures used to encode the design model are periodically reordered in a specific way. However, most models does not respond very well to this technique. To try it, do as follows:
   1. Turn on the option Use alternative verification heuristics.
   2. Try it in both Full Forward mode and Full Compositional Mode
5. For designs that continue to evolve, it can be a good idea to change the verification mode and options from time to time to see if an improvement in performance can be had.