Assertion Statements - SVA: The Power of Assertions in SystemVerilog - page 74

as posedge top.mod2_inst.clk . In this example, the module m_check sees a
different primary system clock depending on where the checker is instantiated in
the design.
Global clocking name is optional, and GCLK in Line 3 could be omitted as shown
in Line 17 .
A common purpose of declaring a global clock is to specify the primary clock for
formal verification. The ticks of the primary clock are at the finest granularity of time
in a formal model, and the global clock is assumed to tick forever. Global clocking in
formal verification is discussed in Chap. 21 . For consistency with simulation, it is
also recommended that in simulation all events be synchronized with the global
clock. Nevertheless, the simulator is not required to check this property of the global
clock.
The previous SystemVerilog Language Reference Manual (LRM) from 2009 [ 5 ]
allowed a single non-hierarchical specification of global clocking. This however
turned out to be insufficient in the context of System on Chip designs where different
subsystems—Intellectually Property blocks may come from different providers and
have their own global clocking declaration. The 2012 LRM [ 8 ] corrected this
weakness and provided a way to specify a hierarchical global clocking as illustrated
in Fig. 4.9 . Designs that used the 2009 interpretation of global clocking may have
to be slightly modified to conform to the new rules. In particular, global clocking
declared in an autonomous top-level module without any underlying hierarchy will
not be visible in any part of the design.
In the presence of global clocking, a number of sampled value functions may be
used that are synchronized to the global clock. These are discussed in Sect. 7.2.2 .
The global clocking declaration also defines a specific event to be referenced by
$global_clock and to govern the global clocking sampled value functions in
simulation. Global clock use cases are examined in subsequent chapters.

4.4.3 Sampled Values for Concurrent Assertion

In simulation, all values of variables appearing in a concurrent assertion used
sampled values of the variables. In most cases, such as static design variables, the
sampled value is the value of the variable in the Preponed region as explained
in Sect. 3.5 . It means that concurrent assertions use the values of signals at the
beginning of the simulation step in which the clocking event occurs. Assertion
value sampling makes concurrent assertions insensitive to simulation glitches. The
assertion body is evaluated using values collected in the Preponed region. The action
blocks are executed in the Reactive region.
One should be aware of this peculiarity of concurrent assertions to correctly
analyze their behavior in timing diagrams and simulation traces. Since the assertion
action blocks are executed in the Reactive region, the signal values used in the action
blocks may be inconsistent with the sampled values of the signals used in the
assertion. To remedy this, the sampled value of the variables should be used