Hardware Reference
In-Depth Information
a |=>
case
(l_v[0])
1'b1:
s_eventually
(b == l_v);
1'b0: c != l_v;
endcase
;
endproperty
5.
sequence
s5;
byte
l_v;
(
( (a[->1], l_v = e)
and
b[->1] )
or
(c, l_v = f)[
*
1:2] ##1 !c
)
##1 (d == l_v);
endproperty
16.5.
The nonoverlapped followed-by operator
#=#
is defined such that for a
sequence
R
and a property
P
, the passing or failing of the following two properties
is equivalent:
1.
R #=# P
.
2.
not
(R |=>
not
P)
.
Use flow rules to show that local variable flows through these two properties is also
equivalent.
16.6.
Use rules of local variable flow to show that
v
flows out of
R[
*
0:1]
iff both
of the following two conditions are satisfied:
1.
v
flows into
R[
*
0:1]
.
2. If
v
flows into
R
, then
v
flows out of
R
.
What can you say about the conditions for
v
to flow out of
R[
*
0:n]
, where
n
is
positive? What about
R[
*
]
?
16.7.
Consider the following variant of
p_ttype_check
:
property
p_ttype_check;
1
transType l_ttype;
2
(start && (ttype == INV || ttype == PRG), l_ttype = ttype)
3
|=>
4
(
5
(1'b1, l_ttype = ttype)
6
#-#
7
p_no_repeat_ttype(
8
.varying_ttype(ttype), .captured_ttype(l_ttype)
9
)
10
);
11
endproperty
12
Explain the local variable flow. Does the assignment in Line
6
affect the instance of
p_no_repeat_ttype
? Compare or contrast the behavior of this property with the
encoding that results by replacing
#-#
with
and
.
Search WWH ::
Custom Search