Hardware Reference
In-Depth Information
Solution:
a1:
assert property
(@(
posedge
clk) ##2 a);
Discussion:
The same intent may be expressed using property operator
nexttime
:
a2:
assert property
(@(
posedge
clk)
nexttime
[2] a);
t
6.4
Suffix Implication
In Sect.
6.2
, it was shown how properties may be built from sequences by promoting
sequences to sequential properties. There are additional ways to build properties
from sequences, the most important one being the
suffix implication
.Asuffix
implication is built from a sequence (
s
) and a property (
p
).
s
is called the
antecedent
,
and
p
is called the
consequent
. A suffix implication is true when its consequent
is true upon completion of its antecedent. Below we provide a more accurate
definition.
There are two versions of suffix implication:
overlapping
, denoted as
s |-> p
,
and
nonoverlapping
, denoted as
s |=> p
. In the overlapping implication the
consequent is checked starting from the moment of
every
nonempty match of the
antecedent. In the nonoverlapping implication the consequent is checked starting
from the next clock tick after each match of the antecedent.
Nonoverlapping implication
s |-> p
is
true in clock tick
i iff for
every
tight
satisfaction point j
i of
s
with initial point i , property p is true in clock tick j .
For each match of the antecedent, the consequent is separately evaluated. According
to the property truth definition from Sect.
5.1
, property
s |-> p
is true iff it is true
in clock tick 0.
Nonoverlapping implication
s |=> p
is defined as
(s ##1 @$global_clock 1)|-> p
. The meaning of this definition is explained in
Chap.
12
. For singly clocked assertions, this definition may be simplified:
s ##1 1 |-> p
.
We want to stress that both overlapping
s |-> p
and nonoverlapping
s |=> p
implications and their consequent
p
are
properties
, whereas their antecedent is a
sequence
, and it is
not
promoted to a sequential property.
Except for Boolean assertions, suffix implication is the most common way
of building assertions. Antecedent
s
represents a
triggering condition
: when this
condition holds, consequent
p
is checked. The suffix implication is very often used
with stand-alone assertions (having an implicit outermost
always
operator)—the
antecedent defines “interesting” attempts where we want to check the consequent.
Example 6.17.
When
rdy
is asserted
rst
must be low.
Solution:
We can use the overlapping implication. When
rdy
is true, Boolean
sequence
rdy
has a match. At this point we need to check a Boolean property stating
that
rst
is false:
Search WWH ::
Custom Search