SystemVerilog Assertions (SVA) Interview

Immediate Assertion:

• Checked at the exact point of execution (procedural).
• Like an if statement with error reporting.
• No temporal (multi-cycle) checking.

// Immediate assertion
always @(posedge clk)
    assert (data != 0) else $error("Data is zero!");

Concurrent Assertion:

• Checked over multiple clock cycles (temporal).
• Uses sequences and properties.
• Evaluated in the Observed region.

// Concurrent assertion
assert property (@(posedge clk) req |-> ##[1:5] ack);

Breakdown:

• assert property: Declares a concurrent assertion.
• @(posedge clk): Clock event for evaluation.
• a |-> b: Implication operator.

|-> (Overlapped Implication):

• If the antecedent a is true, then the consequent b must be true in the SAME clock cycle.
• If a is false, the assertion passes vacuously (no check).

// If req is high, ack must also be high in the SAME cycle
assert property (@(posedge clk) req |-> ack);

disable iff: Disables the assertion when a specified condition is true. Commonly used to ignore assertions during reset.

assert property (
    @(posedge clk) 
    disable iff (rst || !enable)  // Disable during reset or when not enabled
    req |-> ##[1:5] ack
);

Behavior: When rst is high, the assertion is completely ignored—no pass, no fail, no vacuous pass.

// Overlapped: grant must be high when req is high
assert property (@(posedge clk) req |-> gnt);
// Non-overlapped: grant must be high ONE cycle after req
assert property (@(posedge clk) req |=> gnt);
// Equivalently:
assert property (@(posedge clk) req |-> ##1 gnt);

1. Consecutive Repetition [*n]: Signal must be true for n CONSECUTIVE cycles.

// data_valid high for 4 consecutive cycles
assert property (@(posedge clk) $rose(start) |=> data_valid[*4]);

2. Goto Repetition [->n]: Signal becomes true exactly n times, ending on the nth occurrence.

// Wait until ack has gone high 3 times (ends at 3rd ack)
assert property (@(posedge clk) req |-> ack[->3] ##1 done);

3. Non-Consecutive Repetition [=n]: Signal becomes true n times, but sequence may continue after nth occurrence.

// ack goes high 3 times, then eventually done (not necessarily immediately after 3rd ack)
assert property (@(posedge clk) req |-> ack[=3] ##1 done);

Sequence: Describes a pattern of events over time. Pure temporal pattern.

sequence req_ack_seq;
    req ##[1:5] ack;
endsequence

Property: Describes what SHOULD happen. Uses sequences with directions (implications, disable iff, etc.).

property req_followed_by_ack;
    @(posedge clk) disable iff (rst)
    req |-> req_ack_seq;
endproperty

Can you assert a sequence directly? Yes, technically:

assert property (@(posedge clk) req_ack_seq);
// But this means: "The sequence must start at EVERY clock edge."

Typically, sequences are wrapped in properties for meaningful conditional checking.

property handshake_protocol;
    @(posedge clk) disable iff (rst)
    $rose(valid) |-> 
        ($stable(data) throughout (##[0:4] ready)) ##0 (ready && valid);
endproperty
assert property (handshake_protocol) else $error("Handshake violation!");
// Alternative with explicit sequence:
sequence data_stable_until_ready;
    ##[0:4] (ready && valid);
endsequence
property handshake_v2;
    @(posedge clk) disable iff (rst)
    $rose(valid) |-> $stable(data) throughout data_stable_until_ready;
endproperty

Key Operators:

• $rose(): Detects rising edge.
• $stable(): Checks signal didn't change.
• throughout: Condition must hold during entire sequence.

$past(signal, n): Returns the value of signal from n clock cycles ago.

// When we see data_out, check it matches data_in from 2 cycles ago
assert property (
    @(posedge clk) disable iff (rst)
    $past(write_en, 2) |-> (data_out == $past(data_in, 2))
);
// Alternative perspective: at write time, predict future
assert property (
    @(posedge clk) disable iff (rst)
    write_en |-> ##2 (data_out == $past(data_in, 2))
);

Other Temporal Functions: $rose(), $fell(), $stable(), $changed().

Observed Region: Comes AFTER Active, Inactive, and NBA regions in the simulation time slot.

Why Assertions Here?

• All design logic (blocking/non-blocking) has completed.
• Signal values are stable and final for this time step.
• Assertions see the "settled" state of the design.

+-----------------------------+
|  Active (design logic)  |
├-----------------------------┤
|  Inactive (#0)          |
├-----------------------------┤
|  NBA (<=)               |
├-----------------------------┤
|  OBSERVED ← Assertions! |
├-----------------------------┤
|  Reactive (program)     |
+-----------------------------+

If assertions were in Active, they might see intermediate values mid-update.

Multi-Threaded Evaluation:

• Each time req is true, a new evaluation "thread" starts.
• Each thread independently tracks ##[1:5] ack.
• Multiple threads can be active simultaneously.

Failure Behavior:

• If ANY thread's antecedent matches (ack within 1-5 cycles) but consequent fails → ASSERTION FAILS.
• Other pending threads continue independently.

// Scenario: req at cycle 0
// Thread 1: checks for ack at cycle 1
// Thread 2: checks for ack at cycle 2
// ...
// Thread 5: checks for ack at cycle 5
// If ack comes at cycle 3, threads 1,2 die (no match), 
// thread 3 matches and checks 'done'.

Debugging Tip: Use $asserton/$assertoff and waveform viewers to trace threads.