Building Data-Integrity Checks

From timing rules to data rules

Most assertion tutorials stop at handshake timing — request gets a grant, valid waits for ready. The checks that actually catch corrupting bugs are data-integrity checks: the value that comes out equals the value that went in, suitably delayed, selected, or held. The sampled value functions are the raw material: $past supplies the historical reference value, $stable pins values that must not move, and the gating argument aligns histories to qualifying beats. This lesson assembles them into four checks you will write on real projects — and a preview of where they run out of steam and local variables take over.

DATA-INTEGRITY CHECK FAMILIES

  ┌─────────────────────┬──────────────────────────────────────────┐
  │ delayed-equality    │ out == $past(in, N [, qualifier])        │
  │                     │ FIFOs (in-order), fixed-latency pipes    │
  ├─────────────────────┼──────────────────────────────────────────┤
  │ hold / stability    │ qualifier |-> $stable(value)             │
  │                     │ config-while-busy, data-while-stalled    │
  ├─────────────────────┼──────────────────────────────────────────┤
  │ readback            │ read_resp |-> rdata == $past(wdata, ...) │
  │                     │ register files, write-then-read rules    │
  ├─────────────────────┼──────────────────────────────────────────┤
  │ phase matching      │ data-phase fields == $past(addr-phase)   │
  │                     │ split-transaction buses (AHB/AXI style)  │
  └─────────────────────┴──────────────────────────────────────────┘

FIFO: data out equals data in, delayed

For a FIFO in the simple regime — in-order, one element per push/pop — the element popped now is the element pushed OCCUPANCY pushes ago . With the gating argument, $past(wr_data, occupancy, push) reaches back exactly that many push beats. The catch: $past requires a constant depth argument on most tools, so the elegant dynamic form is illegal. The standard compromises: assert at a fixed occupancy (e.g. a flush-through test where occupancy is known), or generate one assertion per legal occupancy value.

// Legal pattern: one assertion per occupancy, generated
genvar k;
generate
  for (k = 1; k <= DEPTH; k++) begin : g_fifo_chk
    assert property (@(posedge clk) disable iff (!rst_n)
      (pop && occupancy == k) |->
        (rd_data == $past(wr_data, k, push)))
      else $error("FIFO integrity: occ=%0d", k);
  end
endgenerate

// ILLEGAL on most tools — $past depth must be elaboration-constant:
// rd_data == $past(wr_data, occupancy, push)   // do not write this

DEPTH-2 trace, occupancy shown after each tick's push/pop

  tick           :  1    2    3    4    5    6
  push           :  1    1    0    0    1    0
  wr_data        :  A    B    -    -    C    -
  pop            :  0    0    1    1    0    1
  rd_data        :  -    -    A    B    -    C
  occupancy@tick :  0    1    2    1    0    1   (sampled, pre-update)

  tick 3: pop with occupancy==2 → check rd_data == $past(wr_data,2,push)
          push history (newest→oldest): [B, A] → 2 back = A → A==A PASS
  tick 4: occupancy==1 → 1 push-beat back = B → B==B PASS
  tick 6: occupancy==1 → 1 back = C → C==C PASS

This generate-per-occupancy trick works but scales poorly and only covers in-order, no-simultaneous-push-pop regimes cleanly. The general solution — capture wr_data into a local variable at push time and compare at the matching pop — handles dynamic depth and out-of-order tags, and is the subject of the local-variables lesson. Knowing why $past alone cannot do it (non-constant depth) is itself a standard interview point.

Stable-while-busy and write-then-readback

// 1. Stability: configuration frozen for the whole operation.
//    Level antecedent is CORRECT here — the rule holds every cycle.
assert property (@(posedge clk) disable iff (!rst_n)
  busy |-> $stable({cfg_mode, cfg_len, cfg_base}));

// 2. Hold under stall: output data must not move while consumer stalls
assert property (@(posedge clk) disable iff (!rst_n)
  (out_valid && !out_ready) |-> ##1 ($stable(out_data) && out_valid));

// 3. Write-then-readback: a read that follows a write to the SAME
//    address with no intervening write returns the written data.
//    (Single outstanding write; reg-file with 1-cycle read.)
property p_readback;
  logic [7:0]  a;
  logic [31:0] d;
  @(posedge clk) disable iff (!rst_n)
    (wr_en, a = wr_addr, d = wr_data) ##1
    (!(wr_en && wr_addr == a)) [*0:$] ##0
    (rd_en && rd_addr == a)
    |-> ##1 (rd_data == d);
endproperty
assert property (p_readback);

Readback trace (1-cycle read latency)

  tick      :   1     2     3     4     5
  wr_en     :   1     0     0     1     0
  wr_addr   :  0x10   -     -    0x10   -
  wr_data   :  AAAA   -     -    BBBB   -
  rd_en     :   0     0     1     0     1
  rd_addr   :   -     -    0x10   -    0x10
  rd_data   :   -     -     -    AAAA  ...   ← tick-3 read returns at 4
                                       BBBB  ← tick-5 read returns at 6

  attempt from tick 1: a=0x10, d=AAAA; no intervening write at 2,3;
  read at tick 3 → consequent at tick 4: rd_data==AAAA  PASS.
  attempt from tick 4: d=BBBB; read at 5 → check at 6: BBBB  PASS.

Check 3 quietly introduced local variables (a, d captured at the write) because $past cannot express “the write that happened an unbounded number of cycles ago”. The boundary is worth internalizing: fixed, constant distance → $past; variable distance or per-transaction matching → local variables.

Address/data phase matching

Pipelined buses split a transfer into an address phase and a later data phase. A one-phase-deep pipeline (AHB-style, data phase immediately follows address phase) is the perfect $past use case: every data-phase attribute must equal the corresponding address-phase value from exactly one transfer beat ago — gated on transfer beats, since the bus can insert wait states between them.

// AHB-flavored: data phase attributes match prior address phase.
// trans_beat = address-phase handshake (htrans active && hready)
logic trans_beat;
assign trans_beat = (htrans inside {2'b10, 2'b11}) && hready;

// Write data presented in the data phase belongs to the write
// command issued in the previous transfer beat
assert property (@(posedge clk) disable iff (!rst_n)
  (data_phase_active && hready && $past(hwrite, 1, trans_beat)) |->
    !$isunknown(hwdata));

// Response checks aligned to the command one beat earlier
assert property (@(posedge clk) disable iff (!rst_n)
  (data_phase_active && hready) |->
    (cur_resp_addr == $past(haddr, 1, trans_beat)));

Address/data phase pipeline with one wait state

  tick        :    1       2       3       4
  haddr       :   A1      A2       -       -
  trans_beat  :    1       1       0       0
  hready      :    1       1       0       1
  data phase  :    -      D(A1)   D(A2)~  D(A2)   (~ = stretched)
  check at 2  : resp addr == $past(haddr,1,trans_beat) = A1  PASS
  check at 4  : gated history skipped the tick-3 wait state →
                still returns A2 (last trans beat)            PASS

  Ungated $past(haddr) at tick 4 would return tick-3's haddr ('-')
  → spurious FAIL. The gate IS the correctness here.

Interview angle

“Write an assertion that FIFO output equals input delayed” is a deliberately underspecified favorite. Strong answers interrogate the regime first: in-order? constant latency? Then: constant delay → $past(in, N); valid-qualified → add the gate; depth varies at runtime → $past cannot (non-constant argument), switch to local variables or per-occupancy generate. For stable-while-busy, expect the follow-up “edge or level antecedent?” — level, because the rule re-applies every cycle of the window. Being able to produce the wait-state phase-matching waveform above distinguishes candidates who have verified a real bus from those who have read about one.

Key takeaways

• Delayed-equality, stability, readback, and phase-matching cover most practical data checks.

• $past handles constant-distance lookback; gate it with the beat qualifier on elastic or wait-stated buses.

• $past's depth must be an elaboration-time constant — dynamic distance needs local variables.

• Stability rules want level antecedents: the obligation renews every cycle of the busy window.

• Concatenate related fields inside one $stable to check a whole config group atomically.

Common pitfalls

• Writing $past(wr_data, occupancy, push) with a run-time occupancy — illegal non-constant depth.

• Ungated $past across wait states — compares against an idle-cycle value and fails spuriously.

• Readback checks without the 'no intervening write' clause — a second write legally changes the data.

• Checking out_data stability under stall without re-asserting out_valid — data held but valid dropped.

• Reaching for local variables when the latency is constant — $past is simpler, cheaper, and clearer.