Hardware Reference
In-Depth Information
Note: Recall that
b[
*
]
is a shortcut for
b[
*
0:$]
and
##[+]
is a shortcut for
##[1:$]
. The sequence in assertion
a1
is weak because it is used as the property
of an assert statement, and there the default is weak. Therefore, when an attempt
is triggered by
a
true and
b
does not become true, that evaluation attempt of
the assertion succeeds. In this situation, however,
a2
fails because the sequential
property is explicitly qualified as strong.
Assertions
a3
and
a4
are a little more complex. Each contains two sequences:
!a ##1 a
and
b[
*
] ##1 c
. The former sequence is used as the antecedent
(or precondition) of the suffix implication
|->
. If a thread of evaluation of that
sequence does not complete due to lack of clock ticks or because
!a
is false or
is not followed by
a
in the next clock tick, that thread fails, and in the context of the
antecedent it contributes no match. In those cases the assertion attempt has a vacuous
success (Sect.
10.6
). The consequent sequence
b[
*
] ##1 c
is a weak property in
a3
and a strong property in
a4
. The interpretation is similar to that of
a1
and
a2
. That
is, in the absence of a sufficient number of clock ticks or if
b
remains true forever
while
c
is never true, the consequent of
a3
succeeds, while that of
a4
fails.
In the case of covers
c1
and
c2
, the default strength of a sequence used as the
coverage property is strong. This is done so that a coverage hit is not registered
when the sequence does not complete evaluation, e.g., due to lack of clock ticks. To
override the default behavior, the qualifier
weak
should be used, as in
c2
.
1
t
Let us now examine the various property operators from Table
10.1
.
10.2
Boolean Property Operators
The following property operators express Boolean connectives between properties:
not
p
—negation
p
or
q
—disjunction
p
and
q
—conjunction
p
implies
q
—implication
p
iff
q
—equivalence
if
(b)p
else
q
—if conditional
case
(b)...
—case conditional
Here is their informal description; their formal semantics can be found in
Chap.
22
.
1
Though cover
c2
is rather meaningless.
Search WWH ::
Custom Search