Hardware Reference
In-Depth Information
Negation
The property
not
p
is true iff the property
p
is false.
Example 10.2.
What is
not
e
where
e
is a Boolean expression? According to the
definition,
not
e
is true iff
e
is false as a property. If the clock ticks, then
e
is false
as a property iff
!e
is true as a Boolean expression at the first clock tick. If the clock
does not tick, then
e
is false as a property iff it is a strong sequential property at
the first position of the trace. If the property clock is the global clock, then
not
e
is
equivalent to
!e
(see Chap.
22
, Example
21.29
).
t
Disjunction
Property
p
or
q
is true iff either property
p
or property
q
is true (Sect.
5.5
).
The syntax is the same as for sequence disjunction discussed in Sect.
6.6
. When
the sequence disjunction is used as a property it can be replaced by property
disjunction with the same constraint on the strength of the sequence disjunction
as on both
p
and
q
.
Conjunction
Property
p
and
q
is true iff both properties
p
and
q
are true (Sect.
5.5
).
Note that the syntax of property
and
is similar to that of the sequence
and
operator described as
s1
and
s2
in Sect.
11.1.5
. However, they have similar
meaning only when the sequence
and
is used as a property, and the strength of
both
p
and
q
is the same as the strength of the sequence
s1
and
s2
.
For further discussion, refer to Sects.
11.1.5
and
5.5
.
Implication
The property
p
implies
q
is true iff either property
p
is false or
q
is true (see
Chap.
22
).
When
p
and
q
are Boolean expressions
e1
and
e2
, respectively, then
e1
implies
e2
is equivalent to
e1 -> e2
provided the clock ticks. This
equivalence holds, e.g., if the sampling clock is the global clock, which is guaranteed
not to stop. For further discussion on the semantics of
implies
, see Chap.
22
.
Previously (Sect.
6.4
) we discussed suffix implication
|->
, which also involves
a property, but only in the consequent. This has to be contrasted with property
implication
implies
:
Search WWH ::
Custom Search