SystemVerilog Language Overview - SVA: The Power of Assertions in SystemVerilog - page 35

Variables req and gnt are used as inputs in the clocking block and they get
sampled with the clocking event. The property p_req_granted is declared in
the clocking block. Because a clocking block creates a scope, the assertion a1
refers to property req_granted using its hierarchical name as cblk.req_granted .
The assertion a1 inherits its clock from the property cblk.req_granted (see
Sect. 12.2.6 ), and therefore no explicit clock specification in assertion a1 is needed.
The property req |=> !req is written directly in the body of assertion a2 , and
not declared in the clocking block. Therefore assertion a2 must specify its clocking
event explicitly.

t

2.3.2 Default Clocking

One clocking block may be specified as default for a given design element.
Specifying a default clocking allows to omit clock specification in concurrent
assertions belonging to the same design element (e.g., module, interface, etc.). In
this case the clocking event of the default clocking becomes an implicit clock of the
assertion. When the default clocking is used only for assertion purposes, its body is
usually left empty and no name is given to the default clocking block.

Example 2.8. The following code illustrates a typical usage of the default clocking
with assertions.

module m( input logic req, clk, output logic gnt);
default clocking @( posedge clk); endclocking
// Evaluation of gnt
...
property p_req_granted;
req |=> gnt;
endproperty
a1: assert property (p_req_granted)
else $error("Request not granted");
a2: assert property (req |=> !req)
else $error("Request asserted during two consecutive cycles");
endmodule :m
In this example the body of default clocking is empty and this block is left
anonymous. We could provide it a name:

default clocking dfltclk @( posedge clk); endclocking
but it serves, essentially, no purpose. The concurrent assertions a1 and a2 do
not have an explicit clock specified with them, and therefore a clocking event
@( posedge clk) from the default clocking block is inferred for them.