Hardware Reference
In-Depth Information
module
simple_clock(
input logic
clk,a,b);
1
a1:
assert property
(
2
@(
posedge
clk)
3
a |=> b
4
);
5
endmodule
6
Fig. 12.1
Module with explicitly clocked concurrent assertion
10
20
30
40
50
60
70
80
90
100
clk
a
b
Fig. 12.2
Waveform for module
simple_clock
Figure
12.2
shows a possible waveform for the signals in this example. The
event
posedge
clk
occurs at times 20, 30, 50, 75, and 95. The intervals from
time 20 to 30, from time 30 to 50, etc. each constitute one cycle of discretized
time, although their lengths vary in units of simulation time. This illustrates the fact
that the clock ticks do not have to be regular as measured against simulation time.
From among these clock ticks, the sampled value of
a
is
1'b1
only at times 20
and 75. Therefore, the evaluation attempts of
a1
that begin at times 30, 50, and 95
succeed vacuously. The attempt that begins at time 20 checks the sampled value of
b
at time 30 and finds it to be
1'b1
, so this attempt succeeds. The attempt that begins
at time 75 checks the sampled value of
b
at time 95 and finds it to be
1'b0
,sothis
attempt fails. The fact that the sampled value of
b
is
1'b1
at the clock tick at time 50
is irrelevant for the evaluation of
a1
.
Clocking events form a rich subset of general SystemVerilog events and are
specified using a limited event control syntax:
clocking_event ::=
@
identifier
j
@(
event_expression
)
The event expression in the form
@(
event_expression
)
can be a familiar edge event,
such as
posedge
clk
, the name of a declared event, or a more general, and possibly
complex, event expression. The identifier in the form “
@
identifier” can be the name
of a declared event or the name of a clocking block, the latter specifying the clocking
event of the referenced clocking block.
Figure
12.3
illustrates some of the different forms of the clocking event control
syntax in a module with various explicit concurrent assertion clocking declarations.
Assertion
a2
is clocked by an explicit edge event expression and is similar to
a1
in the previous example. Assertion
a3
is clocked by named event
e
.The
always
Search WWH ::
Custom Search