Clocks - SVA: The Power of Assertions in SystemVerilog - page 272

uses the current, Reactive region value. Since there was a tick of posedge clk in
the current time step, prior to the Observed region, the value of clk in the Reactive
region is 1'b1 . Therefore, there is a mismatch between the value in Line 3 that
causes the assertion failure and the value written by the display statement. Changing
the action block error call to

$error("FAIL: clk=%b", $sampled(clk));
fixes the mismatch. The assertion remains counterintuitive, though, because of the
relationship between Lines 2 and 3 . Care must always be taken when interpreting
assertions that reference the same variable in contexts where sampling is and is not
used.
There are the following kinds of references within concurrent assertions that use
current values as the sampled values:

￿ Local variables.
￿ const cast expressions or automatic variables in a concurrent assertion within
procedural code.
￿ Free checker variables.

References within a const cast expression or to an automatic variable in a
concurrent assertion within procedural code resolve to the values that existed when
the assertion was placed in the procedural assertion queue. See Sect. 14.2 for more
details. References to free checker variables use current values, which may reflect
the result of randomization in the current time step. See 23.1 for more details.
Preponed value sampling in a concurrent assertion is not allowed to conflict with
other sampling defined within a clocking block. In particular, if a clocking block
input variable is referenced in a concurrent assertion, then the variable must be
sampled with #1step 7 in the clocking block and the clock governing the reference
in the assertion (if there is one) must be the same as that of the clocking block.

12.2.2 Default Clocking

A clocking block may be declared as the default within a given module, interface,
program, or checker. There are two syntactic forms for specifying default clocking.
One prepends the keyword default to the clocking block declaration, as in the
following example:

default clocking PCLK @( posedge clk); endclocking
The other uses a separate top-level declaration to specify the default clocking, as in
the following example:
clocking PCLK @( posedge clk); endclocking
...
default clocking PCLK;