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

In a process-based implementation, compilation may not be costly, but if such
structures are part of an assertion that can create many overlapping attempts or
threads then the result can be a growing number of concurrent processes and/or
data structures that have to be allocated and evaluated at run time.
￿ Ranges ##[M:N] b as well as [ * M:N] ,forsomelarge N>M
The problem is similar to the preceding case, yet somewhat worse because of
the implied nondeterminism representing a disjunction of fixed delay or repetition
ranges. In this case, not only the value of N is of importance but also the
span N-M C 1 of the range itself. The consequences on compilation and run time
performance are significant.
￿ Unbounded delay at the beginning of an antecedent ##[ * ] s |-> p
The interpretation of this property reads as follows: Upon each occurrence of
sequence s , property p must hold. If this property is used in an assertion outside
an initial procedure, the assertion will evaluate the whole implication at every
clock tick.
In an implementation that does not keep track of attempts and reports failures
only, it may not cause problems since the multitude of evaluation threads that
have equivalent next states is collapsed into one evaluation. However, the assertion
evaluation may not complete in simulation if it does not fail in one of the evaluation
attempts of p . The presence of a local variable further complicates the task of
reducing the number evaluation threads, as the value of the local variable may not
be the same in all threads.
The situation is quite different in process-based evaluation that does keep track of
attempts. Here, if s and p are of temporal nature spanning several clock ticks, there
can be a rapid accumulation of processes, each doing essentially the same thing,
but needing to keep track of the attempt start times. Notice that unless p fails all
attempts will keep evaluating till the end of simulation.
Possible solutions are:
￿ Place the assertion into an initial procedure thus creating only one evaluation
attempt. Only the first failure will be reported.
￿ Remove ##[ * ] from the antecedent because it is redundant for assertions that
trigger at every clock tick.
Another problematic case is the occurrence of large delays in $past :
￿ Sampled value function $past(exp, N) ,forsomelarge N .
The sampled value function can be viewed as a shift register of length N .The
first stage is loaded by the sampled value of exp at every clock tick. The last stage
provides the value of the function $past . Therefore, the number of state bits is
equal to $bits(exp) * N . This may create a large state space for formal verification
(Chap. 21 ). For simulation, the issue is more related to the cost of updating the N
registers.
￿Using $rose(exp, $global_clock) or $rising_gclk(exp)