Hardware Reference
In-Depth Information
module
decl_in_clocking_block (
logic
a, b, c, clk);
clocking
PCLK; @(
posedge
clk);
property
p3; a |=> p4;
endproperty
endclocking
property
p4; b
until
c;
endproperty
a19:
assert property
(PCLK.p3);
endmodule
Since
p4
is declared without clocks, the instance of
p4
within the declaration of
p3
is legal. The clock of
p3
is
posedge
clk
, which flows into and clocks this instance
of
p4
.
Exercises
12.1.
Write an assertion to check that after an occurrence of event
ev_start
,
there is no occurrence of event
ev_wait
until strictly after an occurrence of event
ev_enable
(cf. Example
12.2
).
12.2.
Without
using
the
nexttime
operator,
rewrite
assertion
a14
from
Sect.
12.2.5.1
so that its behavior is identical to that of
a13
.
12.3.
Using the waveform in Fig.
12.12
, analyze the behavior of the following
assertion:
a1:
assert property
(
@(
posedge
clk1) a |=> @(
posedge
clk2)
nexttime
b
);
12.4.
Using the waveform in Fig.
12.12
, analyze the behavior of the assertions in
the following module for the evaluation attempts beginning at times 20 and 60:
module
m(
logic
a, b, clk1, clk2);
a1:
assert property
(
@(
posedge
clk1) a |->
(@(
posedge
clk2) a)
until
(@(
posedge
clk2) b)
);
a2:
assert property
(
@(
posedge
clk1) a |-> @(
posedge
clk2) a[
*
] ##1 b
);
endmodule
12.5.
Consider the assertion
a1:
assert property
(
@(
posedge
clk1) a |-> @(
posedge
clk2)
nexttime
b
);
Create waveforms in which
clk2
converges to
clk1
from the right to explain why
the synchronizing behavior of
nexttime
must both align and advance to the next
tick in order for the multiply clocked semantics to converge to the singly clocked
semantics. What happens if
clk2
converges to
clk1
from the left?
Search WWH ::
Custom Search