a |-> bOverlapped. b starts at the antecedent endpoint.
Part 2 · Timing and operators
SystemVerilog AssertionsImplication, endpoints, and repetition
Place obligations on exact sampled edges, inspect pass and failure waveforms, and distinguish the sequence operators that control occurrence and match endpoints.
Question directory
Questions for Timing + operators
Open a question at its supporting explanation. The complete property reference stays directly above each answer set.
Implication and timingWhat is the difference between |-> and |=>?→Implication and timingDoes |=> prevent overlapping property attempts?→Implication and timingWhat is vacuous success, and how do you expose it?→Sequence operatorsHow do [*], [=], and [->] repetition differ?→Sequence operatorsHow do you check that a pulse is at least two sampled clocks wide?→Sequence operatorsHow do you require alert after err is high for two consecutive cycles?→Sequence operatorsWhat does throughout guarantee?→Sequence operatorsWhat do first_match and a sequence's ended method control?→
03 · Implication and timingPlace the consequent on the intended edge.
Draw the trace first, mark the antecedent endpoint, and only then choose overlapped or nonoverlapped implication and any explicit delay.
Concept modelMove one operator and the obligation moves one clock
a |=> bNonoverlapped. b starts one sample later.
The operator changes one attempt's timing. It does not block a new antecedent from starting another attempt.
Always-visible reference
Learn the mechanism before testing the interview answer.
These notes, tables, examples, and design limits contain the working knowledge for this chapter. The interview questions below are a checkpoint, not the primary explanation.
Conditional property
Implication creates an obligation only after an antecedent match.
For every legal antecedent match, the consequent must succeed. If the antecedent has no match from a sampled start point, no consequent obligation is created and the implication succeeds vacuously.
| Antecedent | Consequent | Property result | Interpretation |
|---|---|---|---|
No match | Not evaluated | Vacuous success | No obligation was created |
Match | Success | Success | The obligation was met |
Match | Failure | Failure | The obligation was violated |
Match | Pending | Pending or end-of-run dependent | A future endpoint is still required |
Edge arithmetic
Start counting from the selected antecedent endpoint.
Overlapped implication starts the consequent on the antecedent endpoint. Nonoverlapped implication starts it one sampling event later. An explicit delay then advances from that start.
| Property | For a one-cycle a at sample t | b is checked |
|---|---|---|
a |-> b | Consequent starts at t | At t |
a |=> b | Consequent starts at t+1 | At t+1 |
a |-> ##1 b | Overlapped start plus one delay | At t+1 |
a |=> ##1 b | Nonoverlapped start plus one delay | At t+2 |
a |-> ##[1:3] b | Three legal endpoints | At t+1, t+2, or t+3 |
Same-cycle and next-cycle responseSystemVerilog
a_same_cycle: assert property (
@(posedge clk) req |-> ack
);
a_next_cycle: assert property (
@(posedge clk) req |=> ack
);
Candidate matches
Ranges create candidate endpoints, not a single scheduled check.
A ranged sequence can match at more than one endpoint. Each legal antecedent match can create a consequent obligation, and a new trigger can start a separate property attempt before an earlier one finishes.
Bounded candidates
The first matching endpoint can satisfy a simple response property, but composition may preserve multiple candidate matches.
Earliest endpoint
Keep the earliest complete sequence match within one attempt. It does not reserve the response event globally.
Required completion
Make an eventual sequence fail if it cannot complete by the relevant end condition. Prefer a finite deadline when the architecture has one.
Independent attempts
A second trigger starts a second attempt unless a separate admission rule or outstanding-state model forbids it.
Worked trace
Convert the waveform into endpoints before writing code.
For a request at sample 5 with an exact two-cycle contract, acknowledgement must rise at sample 7. A response at sample 6 is early, at sample 8 is late, and no response leaves a bounded property failed.
| Trigger | Contract | Observed response | Verdict |
|---|---|---|---|
req rises at 5 | exactly +2 | ack rises at 7 | Pass |
req rises at 5 | exactly +2 | ack rises at 6 | Fail: early response |
req rises at 5 | within 1..3 | ack rises at 8 | Pass at latest boundary |
req rises at 5 | within 1..3 | ack rises at 9 | Fail: late response |
req never rises | within 1..3 | ack never rises | Vacuous success; trigger cover is empty |
Interactive timing lab
Move the obligation across the trace.
Select a scenario. The sampled waveform, property, outcome, and explanation update together.
Pass
Overlapped implication checks the antecedent endpoint.
req and ack are both sampled high at clock 2. The consequent of req |-> ack begins on that same sampled edge, so this attempt passes.
Same cycle propertySystemVerilog
a_same_cycle: assert property (
@(posedge clk) disable iff (!rst_n)
req |-> ack
);
Pass. req and ack are both sampled high at clock 2. The consequent of req |-> ack begins on that same sampled edge, so this attempt passes.
Waveform casebook
See the operator before memorizing its syntax.
Each column is a sampled positive clock edge. Read left to right: trigger, legal endpoint, then verdict.
Implication
A request receives its response on the next sampled edge.
$rose(req) |=> ackThe request edge at t2 creates an obligation at t3. ack is high there, so the attempt passes.
Pulse width
A pulse that drops on the next sample is too short.
$rose(pulse) |=> pulsepulse rises at t2 but is low at t3. Nonoverlapped implication checks the next sample and exposes the one-cycle-short pulse.
Backpressure
Valid and payload remain stable until ready accepts them.
valid && !ready |=> valid && $stable(data)The transfer stalls at t1 and t2. valid stays asserted and the Boolean predicate data == A stays true until ready rises at t3.
Consecutive repetition
The error condition holds on two adjacent samples.
$rose(err) |-> err[*2]The antecedent starts at t2. Because |-> overlaps, err[*2] consumes t2 and t3 and completes the required consecutive run.
Interview checkpoint
Explain the rule, then defend its edge cases.
Open a prompt after studying the reference above. A strong answer should name the sampled edge, match endpoint, failure mode, and proof evidence.
Strong answer
Overlapped implication, |->, starts the consequent at the antecedent endpoint. Nonoverlapped implication, |=>, starts the consequent on the sampling event after the antecedent ends.
Why it works
- For a one-cycle antecedent, a |=> b aligns with a |-> ##1 b when both use the same property clock.
- For a multi-cycle antecedent, count from the selected antecedent match endpoint, not from its first cycle.
- An explicit ## delay belongs to the consequent sequence and shifts the actual Boolean test from that starting point.
What the interviewer is testing
Whether you can place the consequent exactly on a trace and state the limited case in which two formulations are equivalent.
Common trap
Do not memorize |-> as current cycle and |=> as next cycle without considering a multi-cycle antecedent endpoint.
| Property | First b sample for one-cycle a | Meaning |
|---|---|---|
a |-> b | Same sampled edge | Overlapped |
a |=> b | One sampled edge later | Nonoverlapped |
a |-> ##1 b | One sampled edge later | Explicit delayed consequent |
Strong answer
No. Nonoverlapped describes where one attempt's consequent starts. Every matching antecedent can still launch another independent attempt on a later clock, even while an earlier attempt is pending.
Why it works
- Use $rose(start) when one attempt should begin per transaction edge instead of once per high cycle.
- To forbid a second request before completion, assert that serialization rule separately or model an outstanding bit or credit count.
- Pipelined protocols should usually allow overlapping attempts and correlate them with IDs, sequence numbers, or explicit state.
What the interviewer is testing
Whether you separate temporal alignment inside one attempt from admission control across several attempts.
Common trap
Replacing |-> with |=> is not a no-overlap solution.
Separate response timing from serializationSystemVerilog
a_done_in_four: assert property (
@(posedge clk) disable iff (!rst_n)
$rose(start) |-> ##[1:4] done
);
a_no_second_start: assert property (
@(posedge clk) disable iff (!rst_n)
$rose(start) |=>
!$rose(start) until_with done
);
Strong answer
An implication succeeds vacuously when its antecedent does not match, because no consequent obligation was created. Add cover properties for the trigger and representative end-to-end matches so a green assertion is not mistaken for exercised behavior.
Why it works
- Vacuity is useful conditional logic, not automatically a bug.
- Cover the antecedent to prove that the requirement was activated in a simulation or is reachable in formal analysis.
- Cover useful boundary responses separately, such as the earliest and latest legal acknowledgement.
What the interviewer is testing
Whether you distinguish absence of a failure from evidence that the intended scenario occurred.
Common trap
A passing request-to-acknowledge assertion proves nothing about response logic if request never rose.
Pair the check with reachability evidenceSystemVerilog
a_req_ack: assert property (
@(posedge clk) disable iff (!rst_n)
$rose(req) |-> ##[1:3] ack
);
c_request: cover property (
@(posedge clk) disable iff (!rst_n)
$rose(req)
);
c_latest_ack: cover property (
@(posedge clk) disable iff (!rst_n)
$rose(req) ##3 ack
);
04 · Sequence operatorsKnow what repeats, and where the match ends.
Distinguish consecutive, nonconsecutive, and goto repetition, then combine sequences only when their start and endpoint contracts are clear.
Concept modelThe occurrence count is not the whole contract
b[*3]Consecutiveb[=3]Gaps and trailing slackb[->3]Ends on final bAlways-visible reference
Learn the mechanism before testing the interview answer.
These notes, tables, examples, and design limits contain the working knowledge for this chapter. The interview questions below are a checkpoint, not the primary explanation.
Repetition handbook
The operator defines both the hit pattern and the match endpoint.
Consecutive repetition can repeat a Boolean expression or a sequence. Nonconsecutive and goto repetition apply to Boolean expressions and allow gaps, but they differ after the final hit.
| Form | Operand | Gaps | Where the match ends |
|---|---|---|---|
b[*3] | Boolean or sequence | No | On the third consecutive repetition |
b[*2:4] | Boolean or sequence | No | On a legal second, third, or fourth repetition |
b[=3] | Boolean expression | Yes | At or after the third hit; trailing non-b slack is allowed |
b[=3:5] | Boolean expression | Yes | After a legal third through fifth hit, with possible trailing slack |
b[->3] | Boolean expression | Yes | Exactly on the third hit |
b[->3:5] | Boolean expression | Yes | On a legal third through fifth hit |
Algebra
Expand repetition when the endpoint is not obvious.
Writing the long form is an excellent interview technique. It exposes the implicit one-sample concatenation between consecutive repetitions.
Equivalent consecutive formsSystemVerilog
a[*3]
// equivalent to
a ##1 a ##1 a
a ##1 b[*3] ##1 c
// equivalent to
a ##1 b ##1 b ##1 b ##1 c
(a ##2 b)[*3]
// equivalent to
(a ##2 b) ##1 (a ##2 b) ##1 (a ##2 b)
Endpoint contrast
Nonconsecutive repetition can wait after the last hit; goto cannot.
Both forms permit gaps between occurrences. The decisive difference appears when another sequence element follows the repetition.
| Sequence | Legal sampled trace after a | Reason |
|---|---|---|
a ##1 b[=3] ##1 c | b · b · b · · c | Three b hits, then trailing non-b slack before c |
a ##1 b[=3] ##1 c | b · b · b b c | Illegal: an extra b occurs in the trailing region |
a ##1 b[->3] ##1 c | b · b · b c | Third b is the repetition endpoint; c is next sample |
a ##1 b[->3] ##1 c | b · b · b · c | Illegal: c is not immediately after the goto endpoint |
Sequence composition
Track start points, spans, and endpoints separately.
Sequence composition is temporal. It is not interchangeable with Boolean logic or property-level and/or.
| Construct | Start relationship | Endpoint rule | Use |
|---|---|---|---|
s1 or s2 | One compound start | Either legal endpoint | Alternative temporal pattern |
s1 and s2 | Same compound start | Later successful endpoint | Both patterns, different lengths allowed |
s1 intersect s2 | Same compound start | Common endpoint required | Two views of one bounded interval |
expr throughout seq | expr begins with selected seq match | Includes every sample through seq endpoint | Hold condition over a known span |
inner within outer | inner may begin inside outer | Inner must complete before outer ends | Temporal containment |
first_match(seq) | Same as seq | Earliest complete match only | Deterministic endpoint selection |
named_seq.ended | Named sequence's own start | True on its match endpoint | Align another sequence to completion |
Inclusive throughout endpointSystemVerilog
a_req_held_to_grant: assert property (
@(posedge clk) disable iff (!rst_n)
$rose(req) |->
req throughout (gnt[->1])
);
Waveform drills
Minimum width and consecutive-run properties need an event trigger.
Triggering on a level starts an attempt on every high sample. Trigger on the edge when the requirement applies once per pulse or once per run.
| Requirement | Preferred property | Trace | Verdict |
|---|---|---|---|
At least 2 sampled clocks high | $rose(p) |=> p | p: 0 1 0 | Fail: low on the next sample |
At least 2 sampled clocks high | $rose(p) |=> p | p: 0 1 1 0 | Pass |
Exactly 2 sampled clocks high | $rose(p) |-> p[*2] ##1 !p | p: 0 1 1 1 0 | Fail: pulse is too long |
Alert after two err samples | ($rose(err) ##1 err) |=> alert | err: 0 1 1; alert next | One obligation per err run |
Alert for every adjacent pair | err[*2] |=> alert | err: 1 1 1 | Two overlapping pair obligations |
Interview checkpoint
Explain the rule, then defend its edge cases.
Open a prompt after studying the reference above. A strong answer should name the sampled edge, match endpoint, failure mode, and proof evidence.
Strong answer
Consecutive repetition [*] requires adjacent sampled matches. Nonconsecutive repetition [=] counts possibly gapped occurrences and permits trailing nonmatch cycles in the sequence match. Goto repetition [->] also permits gaps, but the final occurrence ends the match.
Why it works
- b[*3] means b is true on three consecutive sampled clocks.
- b[=3] can include false samples between occurrences and after the third occurrence before a following concatenation aligns.
- b[->3] can include false samples between occurrences, but its match endpoint is the third true sample.
What the interviewer is testing
Whether you can predict the endpoint that a later ## delay or intersect operator will use.
Common trap
Calling [=3] and [->3] equivalent loses the trailing-slack distinction.
| Operator | Gaps allowed | Match endpoint |
|---|---|---|
b[*3] | No | Third consecutive b |
b[=3] | Yes | May extend after third b |
b[->3] | Yes | Exactly on third b |
Strong answer
Trigger once on the rising edge and require the signal to remain high on the next sampled clock. Because the signal is already high on the trigger sample, $rose(p) |=> p establishes a minimum width of two sampled clocks.
Why it works
- This property allows the pulse to remain high longer because it does not require a falling edge after the second sample.
- For exactly two sampled clocks, add an explicit low check on the third sample.
- Define width in sampled clocks, not analog time, unless the specification requires a separate real-time checker.
What the interviewer is testing
Whether you count the trigger sample and distinguish minimum width from exact width.
Common trap
An unbounded repetition such as p[*2:$] adds unnecessary match ambiguity when one next-cycle check states the minimum-width rule directly.
Minimum and exact pulse widthSystemVerilog
a_min_two: assert property (
@(posedge clk) disable iff (!rst_n)
$rose(p) |=> p
);
a_exact_two: assert property (
@(posedge clk) disable iff (!rst_n)
$rose(p) |-> p[*2] ##1 !p
);
Strong answer
Put the two-cycle err sequence in the antecedent, then imply alert on the following cycle. If the rule should fire once per contiguous err run, begin the antecedent with $rose(err).
Why it works
- ($rose(err) ##1 err) |=> alert checks alert one sampled clock after the second err sample.
- err[*2] |=> alert starts a new antecedent match for every adjacent pair in a long high run, which may be the intended stronger rule.
- A bare err[*2] ##1 alert sequence used as a property also fails on every unrelated start cycle, so it is not the conditional rule described.
What the interviewer is testing
Whether you can control attempt count and explain how a long run changes the number of obligations.
Common trap
Do not omit implication when the English requirement begins with whenever or if.
Fire once per err runSystemVerilog
a_alert_once_per_run: assert property (
@(posedge clk) disable iff (!rst_n)
($rose(err) ##1 err) |=> alert
);
Strong answer
expr throughout seq requires expr to remain true on every sampled tick occupied by the selected match of seq. It constrains the complete sequence span, including its endpoint.
Why it works
- The language defines the idea through unbounded consecutive repetition intersected with the sequence match.
- Use throughout when the requirement genuinely spans a known sequence. For ready-valid stability, small next-cycle invariants are often clearer and easier to debug.
- Be explicit about whether the endpoint is included when translating an until-style English requirement.
What the interviewer is testing
Whether you can identify the exact span that throughout covers and avoid hiding a simple invariant inside an unbounded sequence.
Common trap
Do not read throughout as an implication trigger. It constrains a sequence match that must already be part of a property.
Strong answer
first_match(seq) keeps only the earliest complete match when a sequence has several legal endpoints. seq.ended is true on the sampled clock where that named sequence reaches a match endpoint, which lets another sequence align to completion rather than to the start.
Why it works
- A ranged delay such as ##[1:5] can create several candidate endpoints; first_match deliberately selects the earliest one.
- Use .ended when the contract is expressed relative to a named sequence's completion and the start time is not the relevant alignment point.
- Neither construct consumes a transaction event. Two overlapping property attempts can still use the same response unless separate accounting prevents it.
What the interviewer is testing
Whether you can distinguish endpoint selection inside one property attempt from ordering and one-to-one matching across attempts.
Common trap
first_match does not prove FIFO order, reserve the earliest grant for the oldest request, or replace a scoreboard.
| Construct | What it selects | What it does not prove |
|---|---|---|
first_match(seq) | Earliest complete match | Transaction ownership |
seq.ended | The match endpoint cycle | Which attempt owns an event |
intersect | A common endpoint | FIFO ordering |