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