SVA Implication Operators: Timing and Trade-offs

1. The Need for Implication: Why Not Just Sequences?

As you know, concurrent assertions are tied to a clock and are evaluated at every active clock edge. A naive approach might be to simply write a sequence and assert it directly. However, this leads to a significant problem.

Let's consider a simple property: "If req is asserted, then ack must be asserted two cycles later." One might try to write this as:

// Incorrect attempt
assert property (@(posedge clk) req ##2 ack);

This property will check for req at every positive clock edge. On cycles where req is not asserted, the assertion will fail immediately. This is not our intent. We only care about the behavior if and when req occurs.

To see a clear illustration of this issue, please review the following material.

This problem is precisely what implication operators are designed to solve. They provide a conditional structure: if a trigger condition occurs, then check the corresponding behavior.

2. The Language of Implication: Antecedent, Consequent, and Vacuity

An SVA property with implication is structured as:

antecedent operator consequent

To discuss these constructs professionally, it's vital to use the correct terminology.

As the reading highlights, here are the key takeaways:

• Antecedent (the "if" part): This is the trigger or a pre-condition. It can be a simple boolean expression or a complex sequence.
• Consequent (the "then" part): This is the expected behavior or sequence of events that must follow if the antecedent is true.
• Vacuous Success (or Vacuous Pass): If the antecedent is false at a given clock edge, the property is considered trivially true. The check is not relevant, so the property passes vacuously without evaluating the consequent. This is a crucial concept for both simulation efficiency and formal analysis. In an interview, using the term "vacuous" correctly demonstrates a deeper understanding.

3. Overlapped (|->) vs. Non-overlapped (|=>) Implication

The choice between |-> and |=> determines the precise starting time of the consequent's evaluation relative to the completion of the antecedent. This is a frequent source of off-by-one errors and a classic interview topic.

Overlapped Implication: |->

• Timing: The consequent starts evaluation on the same clock edge that the antecedent completes.
• Analogy: Think of it as a combinational or immediate consequence.
• Example: req |-> gnt
  • At a posedge clk, if req is true, the property requires gnt to also be true in that same cycle.

Non-overlapped Implication: |=>

• Timing: The consequent starts evaluation on the next clock edge after the antecedent completes.
• Analogy: Think of it as a registered or next-cycle consequence.
• Example: req |=> gnt
  • At a posedge clk, if req is true, the property requires gnt to be true on the following posedge clk.
• Key Identity: A non-overlapped implication a |=> b is semantically identical to a |-> ##1 b. Remembering this can simplify complex properties.

The following resource provides excellent diagrams to visualize this difference.

To further solidify this, analyze the waveform below.

4. Strategic Selection and Trade-offs

Choosing the correct implication operator is not just about syntax; it's about correctly modeling the design's micro-architectural intent.

• Use |-> (Overlapped) for properties describing behavior within the same clock cycle. This is common for:

  • Combinational logic relationships: sel |-> (out == a)
  • Conditions on data buses when a valid signal is high: vld |-> $stable(data)
  • Checking properties where the antecedent and consequent are causally linked in the same cycle.

• Use |=> (Non-overlapped) for properties describing behavior across consecutive clock cycles. This is far more common for verifying control logic and pipelines:

  • Standard request/grant protocols: req |=> gnt (If you request this cycle, you are granted next cycle).
  • Pipeline behavior: stage1_vld |=> stage2_vld
  • Checking the output of a register: (d_in == 5) |=> (q_out == 5)

An Important Performance Trade-off

What happens if your antecedent is true for multiple consecutive cycles? For example, req is held high for 4 cycles. A property like req |=> gnt will start four separate evaluation threads, one on each cycle req is high. This can be inefficient in simulation.

A more precise and efficient way to write this is to trigger the assertion only on the start of the event.

The key takeaway is that using edge-detection functions like $rose() or $fell() in the antecedent makes your property's intent clearer and reduces simulation overhead by preventing redundant threads.

Conclusion

In this lesson, we established the foundational role of SVA implication. You can now precisely explain the timing semantics of both |-> and |=>, articulate the key terminology (antecedent, consequent, vacuity), and make strategic choices based on design intent and performance considerations.

Key Takeaways:

• Implication (antecedent |-> consequent) is used to conditionally check a property.
• |-> (Overlapped): Consequent starts in the same cycle the antecedent ends. Best for same-cycle and combinational checks.
• |=> (Non-overlapped): Consequent starts in the next cycle after the antecedent ends. Best for registered and pipelined logic. It is equivalent to |-> ##1.
• A property passes vacuously if its antecedent is false.
• For efficiency, use specific trigger conditions like $rose() in the antecedent to avoid redundant evaluation threads.

In the next lesson, we will build upon this foundation to explore repetition operators (##, [*], [->], [=]), allowing you to write powerful sequences for complex multi-cycle timing patterns.

🧠 Interview & Practice Drill

Time to put this theory into practice. Answer these questions as you would in a high-pressure interview.

🎤 Interview Drill Section

1. Rapid Fire Theory:

   • What is the fundamental difference between |-> and |=>?
   • What does it mean for a property to pass vacuously? Why is this concept important in formal verification?
   • I have a property a |=> b. Can I rewrite this using |->? If so, how?
   • An engineer on my team wrote assert property (@(posedge clk) req ##1 gnt);. What's wrong with this, and how would you fix it?

2. Scenario-based Question:

   • "I have a 3-stage pipeline. A valid transaction enters stage0 indicated by s0_vld. It is expected to appear in stage1 (indicated by s1_vld) one cycle later, and in stage2 (indicated by s2_vld) two cycles after that. However, the pipeline can be stalled at any stage. A stall is indicated by s1_stall or s2_stall. If s1_stall is high, the data in stage0 does not move to stage1.
   • Forget the stall condition for a moment. Whiteboard the SVA property to check that if a transaction is valid in stage0, it becomes valid in stage1 on the next cycle. Which implication operator will you use and why?"

🧩 Coding Exercises

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

1. Combinational Mux Check: A 2-to-1 multiplexer has inputs a, b, a selector sel, and output y. Write a property that asserts: whenever sel is high, the output y must be equal to input b in the same cycle.
2. Registered Assignment: A register q is loaded with the value of d when load_en is high. Write a property to verify that if load_en is high on a given cycle, the value of q in the next cycle will be equal to the value that d had.
3. Modified Handshake: A req signal is sent to a module. The module is expected to respond with ack exactly 3 clock cycles later. Write a property that verifies this relationship only for the first cycle that req goes high (i.e., on its rising edge).