Mechanics of Local Variables - SVA: The Power of Assertions in SystemVerilog - page 352

Chapter 16
Mechanics of Local Variables

I think I can safely say that nobody understands quantum
mechanics.

— Richard Feynman

The previous chapter introduced local variables by illustrating their use in intuitive
and realistic examples of increasing richness. This chapter covers the mechanics of
declaring, assigning, and referencing local variables in a more complete way. Input
and output with local variables, and behavior of local variables with LTL operators,
multiple clocks, and resets are discussed.
Local variables are divided into two kinds. A body local variable is one that
is declared in the body of a named sequence or property, whereas an argument
local variable is one that is declared as a formal argument of a named sequence or
property. The second kind is especially helpful for writing recursive properties (see
Chap. 17 ) in which local variable values need to be passed into recursive property
instances. In most respects, local variables of both kinds behave the same, and
the term local variable is used to refer to one of either kind. Another usability
feature enables initialization of a local variable to be specified in the local variable's
declaration.
Certain sequence and property operators (e.g., or , and , always ) cause the
evaluation of an assertion to fork into subevaluation threads. Depending on the
operator and its context, the forked subevaluation threads may or may not later
join. Local variables have been designed to work well in this multithreaded setting.
When evaluation forks, each of the subevaluation threads receives its own copy of
all the local variables together with all the values currently stored in them. As the
subevaluations continue, each thread independently manages its copies of the local
variables.
Forked subevaluation threads of property operators never join back, so the local
variables in the forked threads remain independent. For a sequence operator, the
nature of the operator ( or vs. and , e.g.) determines how the subevaluations join