Assertion System Functions and Tasks - SVA: The Power of Assertions in SystemVerilog - page 138

Values Before Initial Clock Tick. The definition of $past given above is incom-
plete: what happens if for a given time step there are not enough previous clock
ticks? In this case, $past(e) returns the initial value of e . The initial value of a
static variable is that as computed using the initial values stated in the declaration
of the variables involved in e . If a static variable has no explicit initialization, the
default value of the corresponding type is used, even if the variable is assigned a
value in an initial procedure.

FV tools may ignore variable initialization everywhere, except in checker
constructs. 2 Also, many FV tools consider all variables to be of two-state
value type, and therefore they assume that $past(e) is 0 at clock tick 0 for
any e.

Example 7.11. For the following declaration:

logic a=1'b1,b=1'b0;
logic c;
bit d;
wire w=a;
initial c = 1'b1;
the initial value of

￿ a is 1'b1 .
￿ b is 1'b0 .
￿ a|b is 1'b1 .
￿ c is 1'bx , even though c is assigned a value in the initial procedure.
￿ d is 1'b0 .
￿ w is 1'bz . w is a net, and wire w=a; is an implicit continuous assignments, and
not initialization.

Beyond clock tick 0 the past values of these signals are their initial values. Note that
we number clock ticks starting from 0. For example,

$past(a,,,@( posedge clk)) = 1'b1
and

$past(c,,,@( posedge clk)) = 1'bx
Beyond clock tick 1 (including)

$past(a, 2,,@( posedge clk)) = 1'b1

2 FV tools usually work with the synthesis model of DUT, and variable initialization is non-
synthesizable. However, FV algorithms can deal with initial states and the tools can infer initial
states by analyzing the variable initializations.