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