Hardware Reference
In-Depth Information
module
multiply_clocked(
input logic
clk1, clk2, a, b, c);
1
a5:
assert property
(
2
@(
posedge
clk1) a |=> @(
posedge
clk2) b
3
);
4
endmodule
5
Fig. 12.8
Module with multiply clocked assertion
10
20
30
40
50
60
70
80
90
100
clk1
a
clk2
b
Fig. 12.9
Waveform for assertion
a5
in module
multiply_clocked
12.1.2
Multiple Clocks
All examples of concurrent assertions in the preceding section were singly clocked.
Figure
12.8
gives an example of a multiply clocked assertion. The leading clocking
event for
a5
is
posedge
clk1
, and the reference to
a
is within the scope of this
clock. The reference to
b
is within the scope of
posedge
clk2
.
The multiply clocked behavior of
a5
merits further explanation. Since the
leading clock is
posedge
clk1
and since
a5
is a static concurrent assertion, a new
evaluation attempt of
a5
begins at each tick of
posedge
clk1
.Lett
0
be such a time.
If the sampled value of
a
at t
0
is
1'b0
(or
1'bx
or
1'bz
), then the attempt succeeds
vacuously. Otherwise, the antecedent of
|=>
is matched at t
0
, and evaluation of the
consequent is obligated. Since the consequent is governed by a different clock,
|=>
does
not
specify advancement to the next tick of
posedge
clk1
after t
0
. Rather,
|=>
serves as a
synchronizer
between the two clocks. It specifies that evaluation of
the consequent begin at the nearest tick of
posedge
clk2
that is strictly after t
0
.In
that time step, the sampled value of
b
is checked, and if it is
1'b1
, then the overall
attempt succeeds. Otherwise, the overall attempt fails.
Figure
12.9
shows a possible waveform for
a5
. An attempt of
a5
begins at every
tick of
posedge
clk1
. The sampled value of
a
is
1'b1
at times 20, 40, 60, and 80,
so in each of these time steps the antecedent of
|=>
matches. The attempt beginning
at time 20 looks for the nearest tick of
posedge
clk2
that is strictly later than
time 20. This clock tick is at time 35, where the sampled value of
b
is found to
be
1'b0
, and so the attempt fails. Because the operator
|=>
has been used, it does
not matter that
posedge
clk2
occurs at time 20 since this occurrence is not strictly
later. The attempts beginning at times 40 and 60 both find the nearest strictly future
Search WWH ::
Custom Search