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