Debugging Assertions and Efficiency Considerations - SVA: The Power of Assertions in SystemVerilog - page 427

be stated as hierarchical references to the signals in the original assertion. This
approach has the advantage that we do not modify the design in any way.
3. Alternately, we could make the new control module with ports that correspond to
the signals used in the assertion, and instrument the same assertion but referring
to these ports. We bind the new control module to the module instance that
contains the failing assertion. Care must be taken to control just the instrumented
assertion using the $asserton and $assertoff calls.

19.3 Efficiency Considerations

Depending on whether an implementation of assertions in simulation takes the
attempt-based view, different forms of assertions expressing the same requirements
may have different compile time and run time performance. Each simulator may
have different forms of implementation; nevertheless, there are some general situa-
tions that can be exposed. We base this exposition on three abstract implementations
of the assertions:

1. Assertion is an observer that issues only the fail result with no information about
attempt start time of failure. No failure in simulation means success.
2. Assertion issues only the fail result with information about the earliest or latest
attempt start time of the failure at a specific time (more than one attempt can
reach a failure at the same time by the same condition). No failure in simulation
means success.
3. Assertion is evaluated by maintaining information about all attempts, their start
times and fail/pass times.

An abstract implementation of the first kind may be achieved by compiling
the assertion into a single automaton of the negated property, as typically done
for formal tools (Sect. 21.4.1 ). When the automaton is evaluated it may only
provide information on the first failure detected and its failure time and perhaps
the earliest/latest start time as indicated by the 2nd bullet above. Only on Boolean
assertions of the form assert property (expr); both times would be exact.
For the third kind of implementation, it is possible to compile the assertion into
processes that interpret the syntactic form of the property. An evaluation attempt
would start at every tick of the leading clock, noting its time and then, when it
succeeds or fails, it would report the result and the start and fail times.
Naturally, these are descriptions of abstract implementations, and a particular
simulator may have a mixture of approaches. For example, there may be a different
algorithm to evaluate Boolean concurrent assertions than for evaluating complex or
recursive properties (Chaps. 10 and 17 ). Local variables may be another dimension
to the implementation spectrum (Chap. 15 ).
When local variables are involved, the purely automaton-based evaluation may
not be feasible for at least two reasons. First, determinizing the automaton may not