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

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

1

default clocking NCLK1 @( negedge clk1); endclocking

2

property p1; a |=> b; endproperty

3

a2: assert property (p1);

4

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

5

a4: assert property (@( posedge clk2) p1);

6

endmodule

7

Fig. 12.5 Module with default clocking and unclocked property declaration

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

1

default clocking NCLK1 @( negedge clk1); endclocking

2

property p1; @( posedge clk2) a |=> b; endproperty

3

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

4

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

5

a4: assert property (p1);

6

endmodule

7

Fig. 12.6 Module with default clocking and clocked property declaration

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

1

default clocking NCLK1 @( negedge clk1); endclocking

2

property p1( event ev = $inferred_clock);

3

@ev a |=> b;

4

endproperty

5

a2: assert property (p1);

6

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

7

a4: assert property (p1(.ev( posedge clk2)));

8

endmodule

9

Fig. 12.7 Module with default clocking and clocked property declaration with event argument

instances of the named sequence or property, overriding any clock from the context
in which it is instantiated. Figure 12.6 illustrates this style with another equivalent
encoding of module various_clocks . The named property p1 can no longer be
instantiated in a2 because the clocking event posedge clk2 in the declaration of
p1 would override the default clocking in the instance.
Another approach for specifying clocks in declarations of named sequences
and properties is to pass the clocking events as arguments. This can be done
with untyped arguments or with arguments of type event . The system function
$inferred_clock can be used as a default actual argument. If no actual argument
is passed to the formal in an instance, then $inferred_clock as default actual
specifies that the clock from the instantiation context applies. Figure 12.7 illustrates
this usage with a final equivalent coding of module various_clocks . a2 instanti-
ates p1 without an actual, so $inferred_clock specifies that the default clocking
applies. a4 instantiates p1 and passes the event expression posedge clk2 to the
event argument ev .