Hardware Reference
In-Depth Information
12.6.
Analyze the clock flow in each of the following expressions.
1.
@(ev1) a |=> @(ev2) b
until
c
.
2.
@(ev1) a |=> (@(ev2) b)
until
c
.
3.
not
(@(ev1) a) #-# (@(ev2) b)
implies
(@(ev3) c)
.
4.
@(ev1) (a ##1 @(ev2) b) |=>
if
(c) @(ev3) d
else
e
.
5.
@(ev1)
sync_accept_on
(a) b
until
@(ev2) c
and nexttime
@(ev3)
d
.
12.7.
Compute the set of semantic leading clocks for each of the following
properties.
1.
(@(ev1) a ##1 b[
*
]) |=> c
.
2.
if
(a) @(ev1) p
else
q
.
3.
@(ev1)
if
(a) p
else
q
.
4.
@(ev1) a
implies
(@(ev2) b)
or
c
.
5.
(@(ev1) a)
implies
(@(ev2) b)
or
c
.
6.
accept_on
(a) (@(ev1) b)
and strong
(c
throughout
@(ev2) d)
.
12.8.
Using rules of clocking, determine for each of the following whether it is
legal, illegal, or its legality depends on the existence or nature of an incoming clock.
For those in the last category, identify the conditions on an incoming clock to make
the expression legal. Assume that
a
,
b
,
c
, etc. are Boolean expressions with no
embedded clocking event controls.
1.
@(ev1) a ##1 b[
*
] |=> c
.
2.
(@(ev1) a ##1 b[
*
]) |=> c
.
3.
@(ev1) a
within
@(ev2) b[->1]
.
4.
(@(ev1) a)
within
b[->1]
.
5.
assert property
(
if
(a) @(ev1) b
else
c);
.
6.
assert property
(@(ev1)
if
(a) b
else
c);
.
7.
assert property
(@(ev1) a
implies
(@(ev2) b)
or
c);
.
12.9.
Suppose that Fig.
12.14
is modified as follows:
sequence
s_req_ack;
req ##1 ack;
endsequence
a_triggered:
assert property
(
@(
posedge
dclk)
dvalid |->
s_req_ack.triggered
);
Is the assertion legal? If no, why? If yes, interpret the behavior of the assertion on
the waveforms in Fig.
12.15
.
Search WWH ::
Custom Search