Formal Verification and Models - SVA: The Power of Assertions in SystemVerilog - page 470

Example 21.28. Property not (a until b) is strong. It checks that the clock
ticks enough times to witness that a until b does not hold. Property not
(a s_until b) is weak. If the clock stops ticking early, property a s_until b
will fail, and its negation will pass.

t

Since property implication p implies q is equivalent to ( not p) or q ,the
strength of the antecedent is reversed and the strength of the consequent is preserved.
Therefore, for the implication to be weak, property p should be strong and property
q should be weak.
Example 21.29.

Consider the following assertions:

a1: assert property (@clk !a);
a2: assert property (@clk not a);
initial a3: assert property (@clk !a);
initial a4: assert property (@clk not a);
Assertions a1 and a2 are equivalent. Property @clk not a is equivalent to property
@clk strong (!a) (Example 21.27 ). In the context of assertion a2 , properties
@clk strong (!a) and @clk weak (!a) are equivalent as we check them only at
all the ticks of clk due to the implicit top-level always .
Assertions a3 and a4 are not equivalent: a3 is satisfied if clk never ticks, whereas
assertion a4 fails in this case. t

The implicit always in continuously monitored assertions causes the clock to
be treated weakly at the top-level.

Operator Composition

We know that strong operators require their clock to tick enough times, while there
is no such restriction in weak operators. To interpret the semantics of a property
containing both weak and strong operators, one should refer to the formal semantics
of these operators and to their clock rewriting rules.

Example 21.30. Which requirements are imposed on the clock in property @clk
always s_eventually p ? Property @clk always s_eventually p holds if in
each tick of clk property @clk s_eventually p holds. This means that if there is
an i th tick of clk , then there must exist a j th tick of clk , j i , at which property
p holds. To summarize, property @clk always s_eventually p is satisfied if one
of the following conditions holds:

￿ Clock clk does not tick at all.

￿ Clock clk ticks finitely many times and p holds when the clock ticks for the last

time.