Procedural Concurrent Assertions - SVA: The Power of Assertions in SystemVerilog - page 317

The number of evaluations of a22 is determined by the rate of occurrences of event
posedge e1 and of the assertion clock, posedge clk . There is one instance of a22
scheduled per occurrence of event posedge e1 , even if the assertion clock occurs
more frequently. This seems reasonable. The same rule applies if posedge e1
occurs much more frequently than the assertion clock. In that case, a22 is placed
into the matured assertion queue more than once, waiting for the next occurrence
of posedge clk , and all those instances get evaluated in parallel for the same
occurrences of the assertion clock. Indeed, the evaluation behavior of a22 is the
same as the following multiply clocked, non-procedural concurrent assertion:

a22_non_proc: assert property (
@( posedge e1) 1 |->
@( posedge clk) d1 |=> (i3 || i4)

t

);

When the leading clock of a procedural concurrent assertion is not inferred,
multiple redundant evaluation attempts may be possible.

We have seen how the procedural assertion evaluation framework can filter out
superfluous assertion evaluations due to the transient value changes in signals in the
Active region. This glitch protection can be lost if the signals change in the Reactive
region rather than the Active region. One such case is shown below.

Example 14.23. An assertion trigger due to a change in Reactive region:

program prg();

1

integer i;

2

initial

3

for (i=0; i<8 ; i++) begin

4

mod.v11= 1; #5;

5

mod.v11 = 0;

6

end

7

endprogram

8

9
10

module mod( input sig2,clk);

bit v11,r11,r12;

11

wire v12;

12

assign v12 = sig2;

13

always @( posedge v11 or posedge v12) begin :B1

14

r11 = v11 | v12;

15

a23: assert property (@( posedge clk) v11 |=> v12);

16

r12 = v11 & v12;

17

end

18

endmodule

19

When the event posedge v12 occurs due to the assign statement in Line 13 ,
block B1 is evaluated. As expected, an instance of assertion a23 is entered in the