TOP 5 SVA QUESTION & ANSWER [3/1]

1. Request must be granted within 1-5 clock cycles ?

• This assertion checks a bounded latency guarantee between a request and grant signal. When a rising edge of req is detected, the design must assert grant within 1 to 5 clock cycles.
• Using $rose(req) is important because it prevents multiple parallel assertion threads when req stays high for multiple cycles, which is a common mistake.
• The ##[1:5] delay range models real arbitration or pipeline latency seen in:

—> Bus arbiters

—> NoC fabrics

—> Memory controllers

• disable iff (!rst_n) ensures the property is inactive during reset, avoiding false failures due to uninitialized logic.
• In verification , this type of property is used to catch:

1️⃣Deadlocks

2️⃣Starvation

3️⃣Latency violations in arbitration logic.

2. If valid=1 and ready=0, data must remain stable until transfer ?

• This assertion models a standard handshake protocol stability requirement (AXI, steaming interfaces, etc.).
• When valid is asserted but ready is de-asserted, the producer must hold the data stable until the transaction is accepted (valid && ready).
• $stable(data) ensures no glitches or data corruption during backpressure, which is critical in high-speed interfaces.
• The use of until_with (valid && ready) is :

—> It stops checking once the handshake completes.

In Real projects, this assertion is essential for verifying:

1️⃣AXI interfaces

2️⃣FIFO output data paths

3️⃣Streaming data paths

4️⃣CDC-safe handshake logic

3. Difference between | - > and | = > + ack must occur next cycle after req?

• This assertion enforces a one_cycle response protocol where ack must occur exactly in the cycle following the request.
• The key concept here is the use of non-overlapped implication | = >

| - > (overlapped) : RHS can start in the same cycle

| => (non-overlapped) : RHS starts in the next cycle

Since the question explicitly states “next cycle” | = > is the correct and cleaner choice compared to writing | - > ##1 ack.

Using $rose(req) avoids spawning multiple assertion threads when req is held high, which is a common practice.

This pattern is widely used in :

1️⃣Pipeline control logic

2️⃣FSM acknowledgments

3️⃣Interrupt response verification

4️⃣Command/response protocols

4. Ensure no X/Z on outputs after reset de-assertion ?

• This assertion ensures that output signal never enters an unknown (X) or high-impedance (Z) state during normal operation.
• X propagation is one of the most critical sources of hidden bugs, especially after reset release due to :

—> Uninitialized flops

—> Incomplete reset logic

—> Power domain issues

The $isunknown() system function is a sign-off quality check used in production regressions to guarantee signal integrity.

The disable iff (!rst_n) condition prevents false failures during reset when unknown values are expected.

In advanced advanced environments this type of assertion is mandatory of :

1️⃣Safety-critical IP

2️⃣Formal verification suites

3️⃣Sign off regression suites

4️⃣CDC and low power designs

Catching X/Z early prevents silicon escapes that are extremely costly post fabrication.

5. If start is asserted, it must remain high until done is asserted ?

This assertion verifies a transaction lifecycle constraint where the start signal must not de-assert before the operation completes ( done asserted).

The throughout (!done) construct ensures the start remains continuously high for the entire duration of the operation.

This is stronger and more robust formulation than simply checking start_until done, because it explicitly forbids any premature de-assertion during the active phase.

Such properties are critical for :

1️⃣DMA engines

2️⃣Accelerator control logic

3️⃣FSM based controllers

4️⃣Multi cycle operations

Without this check, the design could exhibit :

—> Partial transactions

—> State machine corruption

—> Data inconsistency