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

always be practically feasible, and second, evaluating a nondeterministic automaton
requires keeping track of which transitions are to be combined with the same set of
local variable values.
Compile Time Performance
In general, the complexity of the automaton needed in implementations (1) and (2)
can grow exponentially with the size of the property as measured by the number
of operators and expressions in the property. However, implementation (3) based
on the interpretation of the syntactic structure remains linear in size. This implies
that form (1) for really complex properties involving nested property and sequence
operators may take prohibitive time to generate. The final representation may also
consume large amounts of memory, especially when large delay ranges are involved
or there is a large set of choices due to an or operation or large ranges. This is one
of the important efficiency considerations for formal verification to limit the size of
ranges of delays ( ## ) and repetitions of all kinds ( [ * [..] ) (see Sect. 21.4.1 ).
Run Time Performance
In general, evaluation based on automata, especially if the automata are deter-
minized, will yield higher performance, because there is minimum work involved
in evaluating an expression and then advancing to the next state. When failure is
detected, the simulator just reports the result and aborts further evaluation.
For the evaluation that keeps track of attempts, the simulator must maintain
information about attempt start times, the local variable values if any, as well as
information about multiple threads of evaluation within an attempt. This consumes
both time and memory.
In the following, we examine several typical cases that may have different run
time performance based on the algorithm scheme used for the implementation. In
the preceding chapters, we often raised performance issues as “efficiency tips”. We
thus revisit some of them and provide explanation why it is so based on the abstract
implementations.
￿ Fixed delay or repetition values ##N as well as [ * N] for some large N .
In an automaton-based implementation, large values used in these operators
that also include [->N] , [=N] create at least N states with transitions arranged
in a similar way as in counters. If used within other operators such as
intersect , within , and , or the memory requirements both at compilation
and at run time can rapidly grow.