Advanced Properties - SVA: The Power of Assertions in SystemVerilog - page 229

Or, since req is a Boolean expression (or a signal), the assertion can be written
more simply as

a3: assert property (req |=> !req);
or as

a4: assert property ( not strong (req[ * 2]);

t

Example 10.15. If there is no acknowledgment ack after req , then in two clock
ticks rtry should be asserted.
Solution: This can be reformulated as “if there is a request then either at the next
tick there should be an acknowledgment, or in two cycles rtry should be asserted”:
a1: assert property (
req implies ( nexttime ack) or nexttime [2] rtry);
The same assertion may be rewritten as:

a2: assert property (
req implies ( nexttime (ack or nexttime rtry));
If req , ack , and rtry are Boolean expressions then the assertion can be
simplified as follows:

t

a: assert property (req |=> (ack or ##1 rtry));

Bounded Eventually and Always Operators

￿ eventually [m:n] p
￿ s_eventually [m:n] p
￿ s_eventually [m:$] p
￿ always [m:n] p
￿ s_always [m:n] p
￿ always [m:$] p

The bounded forms of the operators eventually and always , both weak and
strong, are derived operators that are defined using weak and strong forms of
nexttime , respectively.
1. Let m 0. eventually [m:m] p is the same as nexttime [m] p .Thisisa
simple equivalence between weak forms. Similarly, ( s_eventually [m:m] p)
is equivalent to s_nexttime [m] p .
2. Let m 0, n > m . eventually [m:n] p is

defined recursively as

eventually [m:n-1] p or nexttime [n] p .
This recursive definition can be expanded into a disjunction of n-m+1 nexttime
properties. For example, eventually [2:4] p is equivalent to
nexttime [2] p or nexttime [3] p or nexttime [4] p .