Expression Sampling - SVA: The Power of Assertions in SystemVerilog - page 555

Appendix A
Expression Sampling

In concurrent assertions, in the scope of always_ff procedures in checkers and
in several other SVA constructs sampled values of expressions are used. In most
cases this sampling is done in the Preponed region, but there are exceptions for
different corner cases. In this appendix we provide an exhaustive formal definition
of sampling borrowed from the LRM with some modifications.

A.1 Default Sampled Value

As the first step we define the default sampled value —the sampled value that an
expression has at the beginning of simulation. In the examples below we will use
notation ǚ for the default sampled value; this notation, of course, is not a part of
SystemVerilog.
The default sampled value of an expression is defined as follows:

￿ The default sampled value of a static variable is the value assigned at its
declaration.

Example A.1. Given the declaration:

logic [7:0] a = 8'h15;
ǚ. a / D 8'h15 .

t

￿ If no value is assigned to the static variable at its declaration then the default
sampled value is the default value of the corresponding type.

Example A.2. Given the declaration:

logic [7:0] b;
ǚ. a / D 8'hxx , because the variables of type logic are initialized by default
with x . t