SVA Repetition Operators for Complex Timing Patterns

1. The Building Blocks: Delay and Consecutive Repetition

You're already familiar with the fundamental delay operator, ##, from our last lesson. It specifies a fixed or ranged delay between events in terms of clock cycles.

• a ##1 b: b occurs one cycle after a.
• a ##[2:4] b: b occurs between 2 and 4 cycles (inclusive) after a.

While you can chain delays (a ##1 b ##1 b ##1 b), SVA provides a much cleaner syntax for patterns that repeat consecutively: the consecutive repetition operator [*].

• b[*3] is equivalent to b ##1 b ##1 b.
• b[*2:4] means b is true for 2, 3, or 4 consecutive cycles.

The following reading will walk you through these foundational operators.

A common use case is verifying handshake protocols where a signal must remain asserted for a specific duration. For instance, to check that after a req is seen, ack is asserted within 1 to 5 cycles and then stays high for exactly 4 cycles:

$rose(req) |=> ack[*4]; // This is too simple, ack must come 1-5 cycles later

A more accurate property would be:

$rose(req) |-> ##[1:5] ack[*4];

This sequence ##[1:5] ack[*4] means: wait 1 to 5 cycles, then find ack asserted, and then verify ack remains asserted for the next 3 cycles (totaling 4 consecutive cycles).

2. The Nuance of Grouping

A critical detail in SVA syntax is how operators apply to expressions. The repetition operator [*] binds to the immediate preceding expression. To repeat a multi-cycle sequence, you must group it with parentheses.

As you can see, valid ##2 ready[*3] is very different from valid (##2 ready)[*3]. This is a classic syntax trap and an easy source of bugs. Always be mindful of operator precedence.

3. Advanced Patterns: Non-Consecutive Repetition

Hardware protocols often involve events that must occur a certain number of times but not necessarily on back-to-back cycles. For this, SVA provides two powerful but often confused operators: non-consecutive [=] and goto [->].

• b[=N] (Non-consecutive repetition): This sequence matches if b has been true N times. The matches for b can be separated by any number of cycles. The sequence can continue its match check for a subsequent event anytime after the N-th occurrence of b.
• b[->N] (Goto repetition): This sequence also matches after b has been true N times non-consecutively. The crucial difference is that the next part of the sequence must begin on the clock tick immediately following the N-th occurrence of b.

Let's visualize this.

As the image shows, [->] is stricter. It forces the sequence to "go to" the next part immediately. [=] is more relaxed about when the next part begins.

Let's ground this with a concrete example and formal definitions.

The reset checker example brilliantly highlights the difference. The sequence with reset[=3] passes as long as reset_done eventually happens after the third reset. The sequence with reset[->3] ##2 reset_done requires reset_done to happen exactly two cycles after the third reset.

For a deeper, more formal understanding, which is valuable for complex debug scenarios, it helps to know how these operators can be expressed in terms of simpler constructs. The SVA expert Ben Cohen provides these equivalences:

• b[->m] is equivalent to (!b[*0:$] ##1 b)[*m]
  • This means "wait for b to be true, and do this m times." The sequence advances from the m-th occurrence.
• b[=m] is equivalent to (b[->m] ##1 !b[*0:$])
  • This means "find b m times, and then there can be any number of cycles where b is false before the sequence continues."

This level of detail is what separates a good engineer from a great one, especially when debugging a failing property where the timing is subtle.

4. Choosing the Right Operator

Your choice of repetition operator must precisely match the specification.

• Use [*] for events that must be contiguous (e.g., a signal held stable).
• Use [->] when a specific count of non-contiguous events triggers an immediate next step in a protocol. This is common in state machines where exiting a state depends on seeing a trigger N times.
• Use [=] when you need to check that an event has occurred N times within a window, but the next step is not tightly coupled to the N-th occurrence. For example, "within a transaction frame, there must be exactly 4 data beats."

Conclusion

In this lesson, we've built a powerful vocabulary for describing complex temporal behavior in SVA. You can now express not just simple delays, but also consecutive and non-consecutive repetitions of events, which are essential for verifying realistic hardware protocols.

Key Takeaways:

• ## is the fundamental delay operator for fixed or ranged cycle delays.
• b[*N] verifies that b is true for N consecutive cycles.
• b[=N] verifies that b has been true N times non-consecutively, and allows the rest of the sequence to match at any point after the N-th occurrence.
• b[->N] (goto) verifies b has been true N times non-consecutively, and requires the rest of the sequence to begin immediately after the N-th occurrence.
• Use parentheses () to group sequences when applying repetition operators to avoid common syntax errors.

In our next lesson, we will shift focus from sequence construction to the assertion statement itself, discussing the strategic choice between concurrent and immediate assertions.

🧠 Interview & Practice Drill

Time to solidify your understanding under pressure.

🎤 Interview Drill Section

1. Rapid Fire Theory:

   • What is the difference between ack[*4] and ack[=4]?
   • An engineer wants to check that after a start_burst signal, a data_valid signal asserts exactly 8 times before an end_burst signal is seen. The data_valid cycles are not necessarily consecutive. Which operator, [=8] or [->8], is more appropriate for data_valid, and why?
   • Explain what the sequence (a ##1 b)[*3] checks for. How is it different from a ##1 b[*3]?
   • "I wrote req |=> busy[->5] ##1 done. The intent is that after req, busy happens 5 times, and then done happens one cycle later. Is this correct? What could go wrong?"

2. Whiteboard Coding Problem:

   • A DMA controller signals the start of a burst with dma_start. It then performs a burst of exactly 4 data transfers, indicated by dma_valid being high. These transfers can be stalled by the bus, so they are not guaranteed to be on consecutive cycles. One cycle after the 4th and final dma_valid pulse, the controller must assert dma_done. Write a single SVA property to verify this entire behavior.

🧩 Coding Exercises

Write the SVA properties for the following scenarios. Assume a default clocking block @(posedge clk).

1. Burst Write: After a write command (wr_cmd) is asserted, a data valid signal (wr_dv) must be asserted for exactly 8 consecutive clock cycles.
2. Retry Mechanism: When a transaction fails (txn_fail), the master must re-attempt the transaction by asserting txn_req exactly 3 times. The retries do not need to be on consecutive cycles. After the 3rd retry attempt, the master must wait at least 10 cycles before asserting txn_req again. Write a property that checks for the 3 non-consecutive retries. (Hint: Focus on the retry part first).
3. Credit Counter: A module starts with 4 credits. Each time it sends a request (send_req), it uses one credit. It must not send a request if it has no credits. A get_credit signal can arrive at any time, incrementing its credit count. For simplicity, let's check a slice of this behavior: After a reset, the module can send at most 4 requests (send_req) before it receives a get_credit signal. Write a property that checks that between reset and the first get_credit, send_req does not occur more than 4 times. (Hint: Use (send_req[=N]) throughout (!get_credit) logic).