Detecting Spurious Events and Illegal State Transitions

1. Defining the "Bad Things": Spurious Events and Illegal Transitions

In any complex design, like the arbiters and read-return units you've worked on, there's an implicit set of rules governing behavior. A violation of these rules can lead to catastrophic failure. We can categorize these violations into two main types:

• Illegal State Transition: A finite state machine (FSM) or a protocol moves from a valid state to another state that is not a permitted successor. Think of a traffic light FSM transitioning directly from green to red, skipping yellow.
• Spurious Event: A signal exhibits unexpected behavior that violates protocol rules, even if it doesn't cause an immediate illegal FSM state change. This could be a control signal de-asserting prematurely, a data bus changing when it should be stable, or a signal briefly taking on an unknown ('X') value.

These are not theoretical problems. Formal verification is exceptionally good at finding these bugs, which often hide from simulation.

2. Asserting Against Illegal State Transitions

The most direct way to prevent illegal behavior is to formally codify the legal state transitions of your design's FSMs and forbid anything else.

Let's say an FSM has a state A and can legally transition to B or C. An illegal transition would be moving from A to D. While you could write a property asserting the positive case ((state == A) |-> (next_state == B || next_state == C)), it's often more direct and scalable to assert the negative case—that the illegal transition never happens.

The pattern is antecedent |-> !(illegal_consequence).

// Asserts that if the FSM is in state A, it NEVER transitions to state D on the next cycle.
a_no_A_to_D: assert property (@(posedge clk) (state == A) |-> !(next_state == D));

A common mistake is to misuse the not operator.

As the paper explains, not (a |-> b) is equivalent to a && !b, meaning a must be true every cycle and b must be false. The correct expression to forbid a sequence is a |-> !b.

Illegal transitions can also span multiple cycles.

The property shown is:
$rose(current_st == State2) |-> not((current_st == State4) ##1 (current_st == State6))

This assertion states: "At the cycle where the FSM enters State2, it is forbidden for the FSM to then be in State4 on some future cycle, and then State6 on the very next cycle." This prevents a specific illegal multi-step pathway.

3. Catching Protocol Violations and Spurious Signals

Beyond simple FSMs, most hardware communication is governed by protocols. A ready/valid handshake is one of the most fundamental. Violating its rules creates spurious events that can break the system.

Now that you're familiar with the protocol rules, let's write assertions to enforce them. We want to catch events like valid de-asserting too early or data changing when it should be held stable.

Let's dissect the key properties from the reading:

Checking for Unknowns ('X')

A signal taking on an 'X' value is a classic spurious event, often caused by uninitialized logic or bus contention. Using $isunknown is a simple but powerful safety net.

// From the article: Data should never be unknown when valid is high.
ASSERT(RV_Tx_NeverDataUnknown, read_valid |-> !$isunknown(read_data), clock, reset);

Interview Tip: A sharp follow-up question might be about the difference between == and === when checking for unknowns. Remember that (my_signal == 1'bx) will always evaluate to 1'bx (unknown), not true. To check if a signal is 'X', you must use the case equality operator: (my_signal === 1'bx). Asserting !$isunknown(my_signal) is the most robust approach.

Ensuring Signal Stability

The AMBA rule states: "Once VALID is asserted it must remain asserted until the handshake occurs." This is a stability requirement. The property RV_Tx_ValidDataStable captures this beautifully:

// If we are waiting for the receiver (`!read_ready && read_valid`)...
// ...then on the next cycle, `valid` must remain high and `data` must be stable.
ASSERT(RV_Tx_ValidDataStable, 
       (!read_ready && read_valid) |=> (read_valid && $stable(read_data)), 
       clock, reset);

The $stable() system task is your primary tool here. It returns true if the expression's value is the same in the current cycle as it was in the previous cycle. This elegantly checks that a signal isn't changing when it's supposed to be held constant—a direct check against a spurious event.

Conclusion

Today, we built a crucial part of our verification toolkit: writing safety properties to catch illegal and unexpected behavior. While liveness properties prove your design does something, these properties prove it doesn't do something wrong. A robust formal testbench needs both.

Key Takeaways:

• Illegal Transitions vs. Spurious Events: An illegal transition is a violation of a state machine's defined flow. A spurious event is a broader protocol violation, such as a signal changing value when it should be stable or becoming unknown.
• The Negative Check Pattern: Forbidding bad behavior with antecedent |-> !(illegal_consequence) is often more effective than listing all legal behaviors.
• Key System Tasks:
  • $stable(signal) is essential for checking that signals are not changing across cycles.
  • $isunknown(signal) is your first line of defense against uninitialized logic and 'X' propagation.
• Protocol is King: For any interface, understanding its protocol rules (like ready/valid) is the prerequisite for writing meaningful assertions to detect violations.

In our next lesson, we will tackle multi-clock domain assertions. Clock domain crossings (CDCs) are a notorious source of spurious events and metastability issues, and formal methods are an excellent way to verify them.

🧠 Interview & Practice Drill

Time to put these concepts into practice.

🎤 Interview Drill Section

1. Rapid Fire Theory:

   • You see assert property (@(posedge clk) (state == BUSY) |-> $stable(data_bus));. What kind of bug is this property designed to catch?
   • An FSM can go from IDLE to STATE_A. It should never go directly from IDLE to STATE_B. Which is a better property, and why?
     1. (state == IDLE) |-> (next_state == STATE_A)
     2. (state == IDLE) |-> !(next_state == STATE_B)
   • What is the semantic difference between $stable(sig) and sig == $past(sig)? (Hint: Think about the first cycle and how 'X' values are handled).
   • How do you write an assertion to check that a signal my_sig has not become 'X'?

2. Resume Deep Dive Question:

   • "Looking at your Multi-Client Arbiter project, let's assume it had a fixed-priority scheme. An illegal state would be granting to a lower-priority client while a higher-priority client is requesting. How would you write an SVA property to detect this specific illegal grant event? Describe the antecedent and the consequent."

3. Whiteboard Problem:

   • A simple FSM controls a memory read operation. Its states are IDLE, REQ, WAIT, DONE.
     • Legal transitions: IDLE -> REQ (when start is high).
     • REQ -> WAIT (unconditionally on the next cycle).
     • WAIT -> DONE (when mem_ready is high).
     • DONE -> IDLE (unconditionally on the next cycle).
   • Task: Write two SVA properties to check for illegal transitions:
     1. One that ensures the FSM never goes from IDLE to WAIT.
     2. One that ensures the FSM never leaves the WAIT state unless mem_ready is asserted.

🧩 Coding Exercises

Assume a default clock @(posedge clk).

1. Arbiter Spurious Grant: An arbiter has inputs req[3:0] and outputs gnt[3:0]. A grant gnt[i] should only ever be asserted if the corresponding request req[i] is asserted in the same cycle. Write a property a_no_spurious_grant that asserts that for any i from 0 to 3, if gnt[i] is high, then req[i] must also be high. (Hint: A for loop inside a generate block is a clean way to instantiate this four times).

2. Ready/Valid Protocol Violation: Based on the ready/valid protocol we studied, one optional rule is that once the receiver asserts ready (when valid is low), it must keep ready asserted until a transfer occurs (valid goes high). Write a property a_ready_is_stable that enforces this rule.

3. One-Hot FSM Check: A state machine uses a 4-bit one-hot encoding for its state register fsm_state[3:0]. An illegal state is any value that is not one-hot (e.g., 4'b0000, 4'b0011). Write a concurrent assertion a_state_is_onehot that continuously checks that fsm_state is always a one-hot value. Use the system function $onehot(fsm_state).