Clocks - SVA: The Power of Assertions in SystemVerilog - page 262

governed by a single clocking event. Other concurrent assertions have portions
that fall under the scopes of two or more clocking events and are called multiply
clocked . 1

12.1 Overview of Clocks

This section gives an intuitive overview of clocks based on examples.
Clocks , or, more precisely, clocking events , define the discretization of time
within concurrent assertions. They are declarations with scopes, not operators.
A clocking event for a concurrent assertion must not occur more than once per time
step. If a clocking event occurs more than once in a time step, then the LRM defines
no behavior for the assertion and a tool may issue an error. It is the assertion writer's
responsibility to ensure that the clocks for assertions are “glitch-free” in this sense.
Within the scope of a clocking event, one unit, or cycle , of discrete time is measured
from one occurrence of the clocking event (i.e., clock tick) to the next. Since the
clocking event must be glitch-free, one unit of discrete time is at least one time
step. Clocks also influence the sampling of values within a concurrent assertion. In
most cases the sampled value of a variable or net is the value from the Preponed
region of a time step (see Sect. 4.4.3 and Appendix A ). If a reference to a variable
or net appears within the scope of a clocking event, then the time steps relevant for
sampling are those in which the clocking event occurs.

12.1.1 Specifying Clocks

This section describes various ways to specify clocks for concurrent assertions,
illustrated by singly clocked examples.
The concurrent assertion in Fig. 12.1 specifies an explicit clocking event control, 2
@( posedge clk) ,inLine 3 . The scope of the clocking event is the entire property
expression a |=> b ,so a1 is an example of a singly clocked assertion. This implies
that the references to a and b in Line 4 are evaluated using sampled values in time
steps in which posedge clk occurs. The one cycle delay specified by |=> from its
antecedent to its consequent is from one occurrence of posedge clk to the next.
Finally, the leading clocking event of a1 is also posedge clk . Since a1 is a static
concurrent assertion (i.e., one that is not in a procedural context), a new evaluation
attempt of a1 begins at each occurrence of posedge clk .

1 The SystemVerilog LRM avoids the phrase “multiply clocked”, using instead the grammatically
suspicious adjectives “multiclock” and “multiclocked”.
2 We use the phrase “clocking event control” to emphasize the inclusion of the @ symbol in the
syntax.