Clock Resolution
Clock resolution is the process SystemVerilog uses to determine which clock samples a concurrent assertion. Once the clock is resolved, every cycle delay such as ##1 or ##3 is counted using edges of that clock.
The clock can be specified for properties in several ways.
Rules: The clock for an assertion is determined based on the priority mentioned below.
Priority 1: Use the explicitly mentioned clock for the assertion.
Priority 2: Infer clock from code context where it is used.
Priority 3: Use default specified clock.
Note: It is mandatory to mention the clock in case of concurrent assertion. If a clock is not used, statements are considered to be illegal.
Why Does a Concurrent Assertion Need a Clock?
A concurrent assertion checks behavior across sampled time. The clock tells the assertion exactly when signal values are observed and when the next sequence cycle begins.
For example, req1 ##3 req2 does not mean that req2 is checked three nanoseconds later. It means that req2 is checked three sampling edges after the edge on which req1 matched. Without a resolved clock, ##3 has no clear timing reference.
This requirement applies to concurrent assertions. An immediate assertion executes like a procedural statement and evaluates its expression when program execution reaches it, so it does not use the same clock-resolution rules.
How Clock Resolution Works
SystemVerilog looks for a clock in a priority order. The first valid clock it finds becomes the assertion’s sampling clock.
First, use an explicitly written clocking event, such as @(posedge clk), in the assertion, property, or sequence.
If no explicit clock is present, infer the clock from the context, such as an enclosing clocking block or an event-controlled procedural block.
If the context does not provide a clock, use the declared default clocking event when one is available.
If none of these sources provides a legal clock, the concurrent assertion is illegal and must be corrected.
Clock resolution selects one sampling event; it does not create a clock or change the design clock. It only determines when the assertion reads its signals.
Ways to specify the clock
Property has a clock defined
What this example explains: the sequence contains only the timing pattern, while the property supplies the positive-edge clock used to evaluate that pattern.
sequence seqA
req1 ##3 req2;
endsequence
property prop;
@(posedge clk) seqA;
endproperty
assert property (prop);seqA says that req1 must match first and req2 must match 3 sampled cycles later. Because the sequence has no clock of its own, it receives the clock from prop.
The event @(posedge clk) means that only positive edges of clk are sampling points. If req1 is true on one positive edge, the active sequence attempt checks req2 on the third following positive edge.
This style keeps the timing pattern reusable. Another property can use seqA with an appropriate clocking context without rewriting the sequence expression.
Sequence has a clock defined
The sampling event can be placed directly in the sequence, making the clock part of the reusable sequence definition.
sequence seqA
@(posedge clk) req1 ##3 req2;
endsequence
property prop;
seqA;
endproperty
assert property (prop);Here, seqA already declares @(posedge clk). The property does not need to repeat the event because the sequence brings its sampling clock into the property.
The timing meaning remains the same: match req1 on a positive edge, count three more positive edges, and then require req2. The difference is the location of the clock declaration, not the number of cycles counted.
Use this form when the sequence is intentionally tied to one clock. If the pattern should be reused in different clock domains, keeping the sequence unclocked and supplying the clock in each property is usually clearer.
Infer clock from clocking block
A property declared inside a clocking block can inherit that block’s clocking event.
clocking CB @(posedge clk);
property prop;
req1 ##3 req2;
endproperty
endclocking
assert property (CB.prop);The clocking block CB is associated with @(posedge clk). The property inside it does not write a separate clock, so the positive-edge event is inferred from the enclosing clocking block.
CB.prop uses scope resolution through the clocking-block name. When the assertion is evaluated, req1 and req2 are sampled according to the clocking block, and ##3 counts three CB sampling events.
This form is useful when many related properties share the same interface clock. It keeps the clock declaration in one place and reduces repeated event expressions.
Infer clock from procedural block
An assert property statement inside an event-controlled procedure can infer its clock from that procedure’s event control.
property prop;
req1 ##3 req2;
endproperty
always @(posedge clk) assert property (prop);The property does not contain a clock. However, the assertion is executed in an always block that wakes on posedge clk, so that event supplies the clocking context.
At each positive edge, the concurrent assertion evaluates prop using the inferred clock. A match of req1 starts an attempt, and req2 is required three positive edges later.
The inference depends on location. If assert property (prop) is moved outside this procedural context, the always event no longer supplies its clock, so another valid clock source is required.
Using a Default Clock
A default clocking declaration is helpful when many assertions in the same scope use one clock. Properties can omit repeated event expressions while still having a resolved sampling event.
default clocking cb @(posedge clk);
endclocking
property req_to_ack;
req ##1 ack;
endproperty
a_req_to_ack: assert property (req_to_ack);The default clock is considered only after SystemVerilog fails to find a higher-priority explicit or inferred clock. In this example, req_to_ack is sampled on posedge clk, and ack must be true on the next positive edge after req matches.
A default clock reduces repetition, but readers must still be able to find its declaration easily. Keep the declaration close to the assertions it controls and avoid hidden clock assumptions across large files.
Choosing Where to Declare the Clock
- Put the clock in the property when an unclocked sequence may be reused by several properties.
- Put the clock in the sequence when that sequence must always run on one specific sampling event.
- Use a clocking block when a group of interface-related properties shares the same clock and sampling rules.
- Use procedural inference only when the assertion naturally belongs to that event-controlled procedure and the inherited clock is obvious.
- Use default clocking for a scope containing many assertions on one dominant clock, while documenting the default close to those assertions.
Common Clock-Resolution Mistakes
- Writing a concurrent assertion without any explicit, inferred, or default clock.
- Reading ##3 as a simulation-time delay. It represents three edges of the resolved sampling clock.
- Moving an assertion out of a clocking block or procedural block and forgetting that it has lost its inferred clock.
- Assuming that the clock nearest in the source file is automatically selected. Only legal clocking contexts participate in resolution.
- Hiding a default clock far from the properties that depend on it, making the sampling event difficult to identify during review.
- Attaching a reusable sequence to a fixed clock when the same timing pattern must be checked in more than one clock domain.
SystemVerilog Assertions