Data Integrity Drills

Drill 1 — output equals input delayed N cycles

Problem

Interviewer: 'A 3-stage pipeline: dout must equal din from 3 cycles earlier. First write the free-running version, then the version where data only moves when valid is high.'

Think it through

• Free-running: a plain invariant with $past(din, 3). Choose WHERE to stand: stand at the output and look back. Standing at the input (din |-> ##3 ...) needs a local variable to carry the value forward — more machinery for the same check.

• $past(din, 3) is unknown/garbage for the first 3 cycles after reset — gate the check so early attempts don't fire (here: a cycle counter or simply riding on disable iff if reset is long enough; the explicit gate is the defensible answer).

• Valid-qualified: $past takes a GATING expression as its 4th argument — $past(din, 3, , valid) means 'din three VALID-cycles ago'. This is the senior answer; juniors try to hand-build shift registers.

// Free-running pipeline, with startup gate
logic [1:0] warm;
always_ff @(posedge clk or negedge rst_n)
  if (!rst_n) warm <= '0;
  else if (warm != 3) warm <= warm + 1;

a_pipe3: assert property (
  @(posedge clk) disable iff (!rst_n)
  (warm == 3) |-> (dout == $past(din, 3)));

// Valid-gated pipeline: compare against the 3rd-last VALID din,
// and only when the output side presents a valid beat
a_pipe3_valid: assert property (
  @(posedge clk) disable iff (!rst_n)
  vld_out |-> (dout == $past(din, 3, , vld_in)));

PASS trace (free-running, N=3)      FAIL trace
cycle :  0   1   2   3   4   5      cycle :  0   1   2   3   4   5
din   :  A   B   C   D   E   F      din   :  A   B   C   D   E   F
dout  :  -   -   -   A   B   C      dout  :  -   -   -   A   X7  C

At 3: dout==A==din@0 → PASS         At 4: dout==X7, $past(din,3)
At 4: dout==B==din@1 → PASS         is din@1==B → FAIL at cycle 4.
(warm gate suppresses cycles 0-2)   Corruption localized to the beat.

Common wrong answers

• din_changed |-> ##3 (dout == din) — by the time the consequent samples, din holds the CURRENT value, not the value from 3 cycles ago. You must either look back with $past or capture forward with a local variable.

• No startup gate — first cycles compare against X/stale history; on 4-state simulation, X == X comparisons can even pass silently and hide the gap.

• Hand-rolling a shift register for the valid-gated case without knowing $past's gating argument — works, but signals unfamiliarity with the tool.

Drill 2 — FIFO in/out data matching with local variables

Problem

Interviewer: 'Data written into a FIFO must come out unchanged and in order. Show me the local-variable assertion for the simple case, and tell me exactly where it stops working.'

Think it through

• Local variable captures wr_data at the write; the consequent waits for the matching read and compares. The capture syntax (expr, lv = sig) attaches the assignment to a sequence point.

• Which read matches? For in-order single-entry traffic, 'the first read after my write' — rd_en[->1].

• The limit: with multiple writes in flight, EACH write's attempt waits for the FIRST subsequent read — two writes can both compare against the same read. Local variables don't queue. State this limit unprompted; it is the real test.

// Valid while at most ONE entry is in flight
property p_fifo_d1;
  logic [7:0] d;
  @(posedge clk) disable iff (!rst_n)
  (wr_en, d = wr_data) |=> rd_en[->1] ##0 (rd_data == d);
endproperty
a_fifo_d1: assert property (p_fifo_d1);

PASS trace                          WHERE IT BREAKS (2 in flight)
cycle  :  0  1  2  3  4             cycle  :  0  1  2  3  4
wr_en  :  0  1  0  0  0             wr_en  :  0  1  1  0  0
wr_data:  -  A  -  -  -             wr_data:  -  A  B  -  -
rd_en  :  0  0  0  1  0             rd_en  :  0  0  0  1  1
rd_data:  -  -  -  A  -             rd_data:  -  -  -  A  B

write A @1, read A @3 → PASS        Attempt(A): first read @3 → A ✓
                                    Attempt(B): first read @3 too!
                                    compares B vs A → FALSE FAIL.
                                    Local vars don't queue.

Variation — the scalable fix: auxiliary model

// Reference queue beside the assertions — handles any depth
logic [7:0] model_q [$];
always_ff @(posedge clk or negedge rst_n) begin
  if (!rst_n) model_q.delete();
  else begin
    if (wr_en) model_q.push_back(wr_data);
    if (rd_en) begin
      a_order: assert (model_q.size() > 0 && rd_data == model_q[0])
        else $error("FIFO data/order mismatch");
      void'(model_q.pop_front());
    end
  end
end

Common wrong answers

• Claiming the local-variable property handles a deep FIFO — the multi-attempt aliasing above is the classic trap; the interviewer is waiting for you to find it.

• rd_en ##0 rd_data == d without [->1] — only checks a read in the very next cycle; gaps fail.

• Comparing with |=> rd_data == d (no read qualifier) — compares against bus garbage on non-read cycles.

Drill 3 — tagged request/response matching

Problem

Interviewer: 'Requests carry a 4-bit tag; responses return the tag. Every request must get a response with ITS tag within 20 cycles. Out-of-order responses are allowed. Why do local variables work here when they failed for the FIFO?'

Think it through

• Each $rose-of-request attempt captures ITS OWN tag into a private local variable — per-attempt privacy, which broke the FIFO drill, is exactly what makes tag matching work.

• The consequent waits for a response carrying THAT tag: (rsp_vld && rsp_tag == t)[->1], bounded to 20 cycles with intersect or a ranged delay.

• Out-of-order is free: each attempt only watches for its own tag and ignores others.

property p_tag_match;
  logic [3:0] t;
  @(posedge clk) disable iff (!rst_n)
  (req_vld, t = req_tag) |->
    ##[1:20] (rsp_vld && (rsp_tag == t));
endproperty
a_tag_match: assert property (p_tag_match);

// companion: no response with a tag nobody requested needs
// an aux scoreboard of live tags (bit [15:0] live; set on req,
// clear on rsp) — pure SVA cannot express 'no unmatched rsp'.

PASS trace (out-of-order)
cycle   :  0  1  2  3  4  5
req_vld :  0  1  1  0  0  0
req_tag :  -  5  9  -  -  -
rsp_vld :  0  0  0  1  1  0
rsp_tag :  -  -  -  9  5  -

Attempt(tag5)@1: sees rsp tag 9 @3 (ignored), tag 5 @4 → PASS
Attempt(tag9)@2: sees rsp tag 9 @3 → PASS. Order irrelevant.

FAIL trace: rsp_tag @4 is 7 instead of 5; attempt(tag5)
scans cycles 2..21, never sees tag 5 → FAIL at cycle 21.

Common wrong answers

• Comparing rsp_tag == req_tag directly in the consequent — req_tag has long since changed; the whole point of the local variable is freezing the value at request time.

• ##[1:20] rsp_vld ##0 (rsp_tag == t) — binds the tag check to the FIRST response in the window, whatever its tag; out-of-order traffic falsely fails. Keep tag and valid in ONE boolean.

• Asserting tag uniqueness implicitly — if two live requests share a tag, both attempts match the same response; note the protocol must forbid tag reuse, or add an aux check.

Drill 4 — write-readback consistency

Problem

Interviewer: 'A register file: after a write to address A, the next read of A must return the written data — unless another write to A happened in between. Write the property; the in-between clause is the hard part.'

Think it through

• Capture BOTH address and data in local variables at the write.

• The 'unless overwritten' clause lives in the antecedent path: between the write and the read there must be NO other write to the same address — a throughout-style constraint on the waiting period.

• Structure: write, then (no-write-to-A)* gap, then read-of-A — all as the antecedent sequence — and the consequent is just the data compare. Putting the gap in the antecedent means overwritten cases simply never trigger (vacuous), which matches the spec's 'unless'.

property p_wr_rd_consistency;
  logic [4: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)) )
  |-> (rd_data == d);
endproperty
a_wr_rd: assert property (p_wr_rd_consistency);
// (assumes same-cycle read data; for registered read data,
//  consequent becomes |=> (rd_data == d) — say which spec you assumed)

PASS trace
cycle  :  0    1     2     3     4
wr_en  :  0    1     0     1     0
wr_addr:  -    A5    -     B0    -
wr_data:  -    11    -     22    -
rd_en  :  0    0     0     0     1
rd_addr:  -    -     -     -     A5
rd_data:  -    -     -     -     11
write A5=11 @1; intervening write @3 is to B0 (different addr,
gap term still true); read A5 @4 returns 11 → PASS

FAIL trace: same, but rd_data@4 = 33 → compare 33 vs 11 → FAIL.
OVERWRITE trace: write A5=22 @3 → gap term false at 3, the @1
attempt dies WITHOUT obligation (vacuous) — exactly the 'unless'.

Common wrong answers

• wr_en |-> ##[1:$] (rd_en && rd_addr == a && rd_data == d) — no overwrite clause: stale-data failures after a legal overwrite; also bakes the data compare into the search, so a WRONG readback is silently skipped while the property keeps hunting for a matching one. Compare in the consequent, search in the antecedent.

• Putting the no-overwrite condition in the consequent — turns legal overwrites into failures instead of vacuous passes.

• Forgetting [*0:$] allows a zero-length gap — back-to-back write-then-read next cycle must still be checked.

Key takeaways

• Stand at the output and look back with $past, or stand at the input and carry values forward with local variables — pick one and gate startup.

• Local variables are per-attempt: perfect for tag matching, structurally wrong for shared counts or queued FIFO data.

• Encode 'unless X happened in between' as a gap term in the ANTECEDENT, so the exception becomes vacuous rather than failing.

Common pitfalls

• Comparing live signals in delayed consequents — the value moved on; freeze it in a local or use $past.

• $past in the first cycles after reset — gate it; X-vs-X equality can silently pass.

• Data compare inside the antecedent search — mismatches get skipped, not reported.

• Assuming one local-variable property scales to N in-flight items — aliasing across attempts; switch to an aux queue model.