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

one operand clocked by ev1 and one clocked by ev2 . The antecedent of |=> matches
if the sampled value of a is 1'b1 at two successive ticks of ev1 . Suppose that such a
match ends at t 0 .Line 4 of the consequent says that at the nearest tick of ev1 strictly
after t 0 , the sampled value of a must be 1'b0 .Line 6 of the consequent says that at
the nearest tick of ev2 strictly after t 0 , the sampled value of b must be 1'b1 .
A multiply clocked concurrent assertion is required to have a unique leading
clock. If the concurrent assertion is static (i.e., not within a procedural context),
then it has implicit “always” semantics and the leading clock determines when new
evaluation attempts of the assertion begin. If the concurrent assertion is procedural,
then the leading clock determines when evaluation begins of an attempt that
has matured from the procedural assertion queue (see Sect. 14.5 ). The following
example is illegal:

a8_illegal: assert property (
@(ev1) a or @(ev2) b

);
The assertion is illegal because it has two leading clocks, ev1 and ev2 . There is a
simple way to get around this restriction as shown in the modified example:

a8_illegal: assert property (
@(ev1 or ev2) 1'b1 |-> @(ev1) a or @(ev2) b

);
The restriction and the workaround forces the author of the assertion to be aware
of the events that trigger the evaluation attempts. Note that the detection of
simultaneous clocking events is guaranteed in simulators even if the events occur
in different scheduling regions.
The remainder of this section discusses a few abstract, but practically motivated,
examples of multiply clocked properties.

Example 12.1. Write an assertion to check that the time from any occurrence of EV1
to the nearest strictly subsequent occurrence of EV2 is at least MINTIME simulation
time steps.

Solution: This encoding uses local variables (see Chap. 15 ) to capture timestamps
for comparisons. Because of the use of timestamps, it is not so well suited for formal
verification.

property p_mintime( event ev1, ev2, time mintime);

1

time basetime;

2

@(ev1) (1'b1, basetime = $time)

3

|=> @(ev2) $time >= basetime + mintime;

4

endproperty

5

a_EV1_EV2_MINTIME: assert property (

6

p_mintime(.ev1(EV1), .ev2(EV2), .mintime(MINTIME))

7

);

8

The expectation is that MINTIME is a constant, perhaps a parameter, that has
been coordinated with the simulation timescale. Line 2 declares the local variable