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

As the names of these functions imply, they differ by the clock tick at which they
indicate that the least significant bit of exp changed to 1'b1 . $rose evaluates to true
at the clock tick when the least significant bit of exp has risen, while the future value
function $rising_gclk evaluates to true at the tick that precedes the tick when the
signal rises, i.e., when the least significant bit of exp is to rise.
Future value functions are more efficient in FV because in the automata
representation of the overall property, the next-state is already encoded in the
automaton. If past-value functions, e.g., $rose are used, then the implied past-value
register is created independently of the property automaton and thus adds one state
bit to the overall state space. If many such functions are used, it may impact the
performance of FV. For future-value functions, no such extra registers are needed.
Furthermore, the future value functions often simplify the formulation of stability
properties, make them more easily understandable, e.g., Example 7.31 .
In simulation however, the effect on performance can be quite different. Simu-
lation cannot know the value a signal will have at the next clock tick, it can only
evaluate the present and store the past values. Therefore, if a future value function
is used in a property, the compiler must shift the entire property evaluation by
one global clock tick into the past. Furthermore, the reported failure times must
be adjusted to values as if the evaluations were actually based on the future value
functions, i.e., shifted by one clock period of the global clock. However, in general
that global clock period is not known and must be computed by the simulator. This
processing adds overhead in simulation.
￿ Ranges in always [M:N] p as well as eventually [M:N] p ,forsomelarge
N>M (see Sect. 10.5 ).
As before, large upper bounds N and large span N-M+1 increase the state space,
and, in an attempt-based evaluation, if the assertion retriggers while previous
evaluations are still in progress, the run time performance can be significantly
affected.
￿ Trigger by level req |-> p or by value change $rose(req)|-> p
In many situations, $rose(req) is a more efficient form as it only triggers
evaluation on a change.
As mentioned earlier, the use of sampled value functions implies additional
registers. However, to avoid false firing at time 0, it may be necessary to shift the
antecedent as ##1 $rose(req) (see Sect. 7.2.1 ).
￿ Property and versus sequence and in seq_1 and seq_2 (see Sect. 10.2 )
In an automata-based implementation, sequence and requires performing
intersection of the argument sequences. Depending on the complexity of these
sequences, the resulting automaton may be quite large, thus requiring more memory
to represent, as well as slowing down the compilation. Therefore, if and is the
top-level operator in the consequent property then it is more efficient in both
simulation and formal verification to replace the sequence and with a property and .
It is also likely that the verification tool, formal or simulator, does the replacement
automatically.