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

module various_clocks( input logic clk1, clk2, a, b, c);

1

event e;

2

always @( negedge clk1) ->e;

3

clocking PCLK2 @( posedge clk2); endclocking

4

a2: assert property (@( negedge clk1) a |=> b);

5

a3: assert property (@e a[ * 2] |=> c);

6

a4: assert property (@PCLK2 a |=> b);

7

endmodule

8

Fig. 12.3 Module with various explicit concurrent assertion clocking declarations

module various_clocks( input logic clk1, clk2, a, b, c);

1

default clocking NCLK1 @( negedge clk1); endclocking

2

clocking PCLK2 @( posedge clk2);

3

endclocking a2: assert property (a |=> b);

4

a3: assert property (a[ * 2] |=> c);

5

a4: assert property (@PCLK2 a |=> b);

6

endmodule

7

Fig. 12.4 Module with default clocking

procedure in Line 3 triggers e at every occurrence of negedge clk1 ,so a3 behaves
equivalently to the following variant:

a3_v2: assert property (@( negedge clk1) a[ * 2] |=> c);
The clocking event for a4 is PCLK2 , the name of the clocking block in Line 4 , and
so a4 is clocked by the event posedge clk2 of that clocking block. 3
Often, many assertions within a module, interface, program, or checker share the
same clock. In this situation, it is convenient to specify a default clocking block
(see also Sect. 2.3.2 ). The module various_clocks from Fig. 12.3 is recoded in an
equivalent way in Fig. 12.4 .Line 2 declares NCLK1 to be the default clocking for
the module, with event negedge clk1 . As a result, explicit clocking events can be
omitted on assertions a2 and a3 : the default is understood to apply to them. The
default can be overridden by an explicit clocking event, as in a4 .
Default clocking applies to concurrent assertions, not to sequence and property
declarations. This convention allows a sequence or property to be declared without
clocks and to inherit the clock from the context in which it is instantiated.
Figure 12.5 shows another equivalent encoding of module various_clocks illus-
trating this style. This encoding also dispenses with the declaration of clocking
block PCLK2 , putting the event expression posedge clk2 directly in a4 .
Clocks may also be declared within named sequence or property declarations.
A clock in the declaration of a named sequence or property declaration applies to all

3 According to the SystemVerilog LRM, Clause 14.13, the event associated with the clocking block
name, here PCLK2 , occurs in the Observed region, while posedge clk2 occurs in the Active
region. In singly clocked assertions that use sampled values from the Preponed region, there is no
observable difference in behavior between the two forms.