Hardware Reference
In-Depth Information
property
p2(
event
ev1, ev2,
bit
a, b);
1
@(ev1) a[
*
2] |=>
2
(
3
!a
4
and
5
@(ev2) b
6
);
7
endproperty
8
Fig. 12.10
Logical operator joining differently clocked properties
In addition to
|=>
and
|->
, the property operators
#=#
and
#-#
can be used
as synchronizers between different clocks. The timing of
#=#
(resp.,
#-#
)asa
synchronizer is the same as that of
|=>
(resp.,
|->
).
if
-
else
and
case
can also
serve as synchronizers, with timing the same as that of
|->
. Here is an example:
a7:
assert property
(
@(ev1)
if
(a)
@(ev2) b[
*
2]
else
@(ev3) c
);
In
a7
, the scope of
ev1
is the condition
a
of the
if
-
else
. Assuming that
a
is of type
bit
, the following variant behaves equivalently to
a7
and explains how the timing
of
if
-
else
as a synchronizer is the same as that of
|->
:
a7_v2:
assert property
(
1
@(ev1)
2
( a |-> @(ev2) b[
*
2])
3
and
4
(!a |-> @(ev3) c)
5
);
6
This encoding also illustrates some of the
clock flow
rules of clock scoping. The
scope of
ev1
distributes to the two operands of
and
and flows into the parenthesized
subproperties in Lines
3
and
5
. As a result,
a
in Line
3
and
!a
in Line
5
are both
under the scope of
ev1
.
4
The LTL operators
nexttime
,
always
,
s_eventually
,
until
, and their variants
can also be used as synchronizers. When this is done, the time advance specified by
the LTL operator is determined by the
incoming
clock, not by the leading clock or
clocks of the operands. See Sect.
12.2.5.1
for more details.
The logical property operators
and
,
or
,
iff
, and
implies
can be used to join
differently clocked properties. Figure
12.10
gives an example. The scope of
ev1
includes the antecedent
a[
*
2]
of
|=>
and the operand
!a
of
and
in Line
4
and
joins
4
If
a
were of type
logic
, to preserve the semantics of
if
-
else
in the presence of X/Z values
the negation of
a
in
a7_v2
wouldhavetobewrittenas
(!
bit
'(a)|-> @(ev3)c)
.
Search WWH ::
Custom Search