Asserting Liveness with Strong and Weak Operators

1. From Safety to Liveness: Why We Need Both

Imagine a request-grant protocol. Our data integrity properties from the last lesson can ensure that if a grant occurs, it carries the correct data. But what if the grant never comes? The system is effectively frozen. This isn't a data corruption bug; it's a forward progress bug.

This distinction between "not doing something wrong" (safety) and "eventually doing something right" (liveness) is a core concept in verification.

As the video explains, a system that guarantees safety but not liveness is incomplete. A processor that never fetches the next instruction or an arbiter that never grants a request may not be violating any data integrity rules, but they are clearly broken. In hardware verification, we categorize these liveness failures into a few common types.

2. The Vocabulary of Liveness Failures: Deadlock, Livelock, Starvation

When an interviewer asks about "forward progress," they are typically referring to preventing three types of hangs. Understanding the difference is key to a precise answer.

Let's summarize those key definitions:

• Deadlock: A system component gets stuck in a single state and can never leave. (e.g., an FSM state with no exit transitions).
• Livelock: A system component cycles through a set of states but never makes meaningful progress to its goal state. (e.g., an FSM oscillating between two states, never returning to IDLE).
• Starvation: A lower-priority request is perpetually blocked by higher-priority ones and is never serviced.

Our goal is to write SVA properties that formally prove these conditions can never occur.

3. The Crux of Liveness in SVA: weak vs. strong

Let's try to write a property for a simple liveness requirement: "When req happens, gnt must eventually happen." A first attempt might look like this:

a_req_gnt: assert property (req |-> ##[1:$] gnt);

This property reads correctly, but for formal verification, it is functionally useless. This is because, by default, SVA properties are weak.

The formal tool reasons about the weak property req |-> ##[1:$] gnt as follows: "Can I find a finite trace where req is high, and gnt is never asserted afterwards?" The answer is no, because for any finite trace where gnt hasn't happened, it might happen on the next cycle. The tool can't find a finite counterexample, so the property passes vacuously, even if the design has a deadlock where gnt can never occur.

The Solution: strong

To fix this, we must explicitly tell the formal tool to search for infinite counterexamples. We do this with the strong operator.

a_req_gnt_strong: assert property (req |-> strong(##[1:$] gnt));

The strong keyword transforms the property. It now means: "For every req, there must be a corresponding gnt in the future, and there must not exist any infinite path where gnt never arrives." This forces the formal tool to search for deadlock, livelock, or starvation scenarios, which are precisely the bugs we want to find.

You can also use the s_eventually operator, which is equivalent to strong(##[1:$]).

a_req_gnt_seventually: assert property (req |-> s_eventually gnt);

As a rule of thumb for formal verification: any unbounded forward-progress property must use strong or s_eventually to be meaningful.

4. Practical Patterns for Liveness Assertions

Armed with the strong operator, we can now write effective liveness properties. Let's look at some common patterns you'll need in interviews.

Let's analyze two of the most common patterns from the reading.

1. Arbiter No-Starvation

This is a classic interview question. To prove an arbiter is fair, you must prove that every request is eventually granted.

// For a specific client 'N'
property p_no_starvation (request, grant);
  @(posedge clk)
  request |-> strong(##[0:$] grant);
endproperty

// Instantiate for client 0
a_no_starvation_client0: assert property(p_no_starvation(req[0], gnt[0]));

Note: This simple property assumes no other conditions can legitimately block the grant. In a real design, you might need a more complex antecedent, like req[0] && arbiter_enabled.

2. FSM/Counter Returns to Initial State

To prevent deadlock or livelock, we must prove that a sequential machine can always return to a known-good state (e.g., IDLE).

parameter IDLE = 2'b00;

property p_fsm_returns_to_idle (state);
  @(posedge clk)
  // Antecedent: The FSM is NOT in the idle state
  (state != IDLE) |-> strong(##[1:$] state == IDLE);
endproperty

a_fsm_progress: assert property(p_fsm_returns_to_idle(current_state));

This property ensures that from any non-idle state, there is always a path back to idle, formally proving the absence of deadlock and livelock bugs related to progress.

Conclusion

Today we took a deep dive into liveness, the counterpart to safety. We established a clear theoretical and practical understanding of what liveness is and how to verify it. Getting this right is a hallmark of an experienced FV engineer.

Key Takeaways:

• Safety vs. Liveness: Safety properties ("bad thing never happens") are checked on finite traces. Liveness properties ("good thing eventually happens") must be checked on infinite traces.
• Forward Progress Failures: Liveness properties are used to prevent deadlock, livelock, and starvation. Be ready to define these terms.
• weak is for Simulation, strong is for Formal: A weak property like A |-> ##[1:$] B will pass vacuously in formal if B can be postponed forever.
• strong(##[1:$] B) or s_eventually B are mandatory for proving forward progress in formal verification, as they force the tool to look for infinite counterexamples.
• Key Patterns: Memorize the liveness patterns for arbiters (no starvation) and FSMs (return to idle).

In our next lesson, we will focus on another critical class of properties: spurious event detection and illegal state transitions. We'll learn how to write assertions that prove certain events never happen or that a state machine never makes an illegal jump.

🧠 Interview & Practice Drill

Let's reinforce these concepts under pressure.

🎤 Interview Drill Section

1. Rapid Fire Theory:

   • What is the fundamental difference in how a formal tool evaluates a safety property versus a liveness property?
   • An engineer on your team writes req |-> ##[0:$] gnt;. Why would you flag this during a code review for a formal testbench? What is the one-word change you would suggest?
   • Explain the difference between deadlock and livelock as if you were talking to a design engineer.
   • Does a strong property have any different behavior in simulation compared to a weak one? (Hint: Consider end-of-simulation reporting).

2. Resume Deep Dive Question:

   • "On your Multi-Client Arbiter FPV project, you mentioned verifying forward progress. Let's say your arbiter used a round-robin scheme. A junior engineer could be starved if a higher-priority client had a continuous stream of requests. How would you prove this starvation is impossible? Walk me through the exact SVA property you would write. What would the antecedent and consequent be?"

3. Whiteboard Problem:

   • Consider a simple 2-to-1 fixed-priority arbiter. req[1] has higher priority than req[0]. The interface is clk, rst_n, req[1:0], gnt[1:0]. A grant is held for one cycle.
   • Task 1: Write the liveness property to prove that the high-priority client req[1] is never starved.
   • Task 2 (Harder): Write the liveness property to prove the low-priority client req[0] is never starved. What additional condition must you add to the antecedent to make this property valid and non-vacuous? (Hint: What if req[1] is asserted forever?).

🧩 Coding Exercises

Assume a default clock @(posedge clk).

1. FSM Progress: An FSM has a 3-bit state register current_state. The reset state is 3'b000 (IDLE). Write a single SVA property named a_always_returns_to_idle that proves the FSM can never get permanently stuck in a non-idle state.

2. Handshake Completion: A simple valid/ready handshake is used to transfer data. A transaction begins when valid is asserted. It completes when valid && ready is seen. Write a property a_transaction_completes that asserts: if valid is asserted, then valid && ready must eventually occur. Assume the ready signal is not guaranteed to be asserted.

3. Interrupt Serviced: When a hardware interrupt irq is raised, it must eventually be cleared by the processor writing to a clear register, indicated by a single-cycle pulse irq_clear. Write a property a_irq_is_serviced that proves every irq is eventually cleared.