Pipeline & Datapath Assertions

The pipeline contract

A pipelined datapath makes four promises: results appear a fixed number of advancing cycles after their operands (latency); when the pipe stalls, every stage holds its contents (no data loss or duplication); results emerge in operand order (ordering); and any credit/occupancy accounting stays within bounds (flow control). Each promise maps to an assertion family you already have the pieces for — $past with a gate for latency, $stable for stalls, beat counters for ordering, and range checks for credits.

3-stage pipe with a stall: what "correct" looks like

  tick     :   1    2    3    4    5    6    7
  advance  :   1    1    1    0    0    1    1    (advance = !stall)
  in_vld   :   1    1    0    .    .    1    0
  in_data  :   A    B    -    .    .    C    -
  stage1   :   -    A    B    B    B    B*   C
  stage2   :   -    -    A    A    A    A    B
  out_vld  :   0    0    0    0    0    1    1
  out_data :   -    -    -    -    -    A    B
                              └────┘
                       stall: ALL stages hold (ticks 4,5)
  * stage1 takes C only on the advancing tick 6→7 boundary
  Latency rule: out equals in from 3 ADVANCING beats earlier —
  ticks 4,5 do not count. Gated $past handles exactly this.

The canonical ruleset

1. Latency: out_data == $past(in_data, LAT, advance) when out_vld — qualified by a valid pipe.

2. Valid pipe: out_vld is in_vld delayed by LAT advancing beats (valid travels with data).

3. Stall hold: on a stalled cycle, outputs (and valids) are unchanged on the next tick.

4. In-order completion: result sequence numbers increase by exactly one.

5. Credits: counter never negative, never above CAP, and matches issued-minus-completed.

Complete checker: pipelined multiplier

// DUT: 3-stage multiplier. stall freezes the whole pipe.
// in_vld/in_a/in_b at the input; out_vld/out_p at the output.
module mul3_checker #(
  parameter int LAT = 3,
  parameter int W   = 16
)(
  input logic           clk, rst_n, stall,
  input logic           in_vld,
  input logic [W-1:0]   in_a, in_b,
  input logic           out_vld,
  input logic [2*W-1:0] out_p
);
  logic adv;
  assign adv = !stall;

  // count advancing beats so early outputs are not checked
  // against unfilled $past history
  int unsigned adv_beats;
  always_ff @(posedge clk or negedge rst_n)
    if (!rst_n) adv_beats <= 0;
    else if (adv) adv_beats <= adv_beats + 1;

  // R1: result correctness at fixed advancing-beat latency
  a_latency: assert property (@(posedge clk) disable iff (!rst_n)
    (out_vld && adv && adv_beats >= LAT) |->
      (out_p == (2*W)'($past(in_a, LAT, adv) * $past(in_b, LAT, adv))))
    else $error("product wrong vs operands %0d beats back", LAT);

  // R2: valid travels with the data through the same pipe
  a_vld_pipe: assert property (@(posedge clk) disable iff (!rst_n)
    (adv && adv_beats >= LAT) |->
      (out_vld == $past(in_vld, LAT, adv)));

  // R3: stall holds everything — next sample unchanged
  a_stall_hold: assert property (@(posedge clk) disable iff (!rst_n)
    stall |-> ##1 ($stable(out_p) && $stable(out_vld)))
    else $error("output moved during stall");

  // X-safety on a consumed result
  a_no_x: assert property (@(posedge clk) disable iff (!rst_n)
    out_vld |-> !$isunknown(out_p));

  c_stall_mid: cover property (@(posedge clk)   // stall while full
    out_vld && stall ##1 stall ##1 !stall);
endmodule

R1 evaluation with the stall from the earlier waveform (LAT=3)

  tick               :  1   2   3   4   5   6   7
  adv                :  1   1   1   0   0   1   1
  in_a*in_b (vld)    :  A   B   -   .   .   C   -
  adv-beat history   : [A] [BA][.BA] —  — [C.BA]...
  out_vld && adv     :  0   0   0   0   0   1   1
  $past(in,3,adv) @6 :  reaches back 3 ADVANCING beats: ticks 3,2,1
                        → returns A → out_p must equal A's product PASS
  @7: 3 advancing beats back = tick 2 → B's product            PASS
  Ungated $past(in,3) @6 would return tick-3 operands ('-')
  → spurious FAIL. Stalled ticks must not consume history.

In-order completion and credit counters

// In-order completion via sequence numbers carried by the
// checker (auxiliary modeling code, as in the FIFO lesson)
int unsigned issue_sn, retire_sn;
logic [31:0] expected_sn_q[$];     // checker-side model queue

always_ff @(posedge clk or negedge rst_n)
  if (!rst_n) begin issue_sn <= 0; retire_sn <= 0; end
  else begin
    if (cmd_vld && cmd_rdy)   issue_sn  <= issue_sn + 1;
    if (rsp_vld && rsp_rdy)   retire_sn <= retire_sn + 1;
  end

// R4: responses retire in issue order — DUT-provided tag must
// equal the checker's running retire counter
a_in_order: assert property (@(posedge clk) disable iff (!rst_n)
  (rsp_vld && rsp_rdy) |-> (rsp_tag == retire_sn))
  else $error("out-of-order: tag %0d expected %0d", rsp_tag, retire_sn);

// R5: credit counter bounds and consistency
a_credit_floor: assert property (@(posedge clk) disable iff (!rst_n)
  credits <= CAP)                          // unsigned: no negatives,
  else $error("credit overflow");          // overflow shows as > CAP

a_credit_consist: assert property (@(posedge clk) disable iff (!rst_n)
  credits == CAP - (issue_sn - retire_sn))
  else $error("credits disagree with outstanding count");

// no issue without a credit
a_no_oversubscribe: assert property (@(posedge clk) disable iff (!rst_n)
  (cmd_vld && cmd_rdy) |-> (credits > 0));

Credit flow, CAP=2

  tick      :   1    2    3    4    5    6
  issue     :   1    1    0    1    0    0
  retire    :   0    0    1    0    1    1
  outstanding:  0    1    2    1    2    1   (sampled, pre-update)
  credits   :   2    1    0    1    0    1
  a_no_oversubscribe @4: issue with credits==1 (sampled) → PASS
  if issue also fired @3 (credits sampled 0) → FAIL: oversubscribed
  a_credit_consist holds every tick: credits + outstanding == CAP

  Unsigned trap: a 'credits-1' bug at credits==0 wraps to 2^N-1 —
  the <= CAP rule catches it the SAME cycle (huge value > CAP).

The unsigned-wrap point deserves emphasis: “credits never negative” cannot be asserted directly on an unsigned counter — negative values do not exist; they wrap to huge positives. The credits <= CAP bound plus the consistency equation catch the same bug deterministically, one cycle after the bad decrement.

Interview angle

Pipeline checking is where interviewers verify you can compose everything: expect “a 3-stage multiplier with a stall input — what do you assert?” Lead with the four promises (latency, stall hold, ordering, flow control), then write R1 with the gated $past and explain why stalled ticks must not consume history — that single sentence is the pass/fail line for the question. Standard follow-ups: “why check the valid pipe separately?” (data correct but valid misaligned duplicates or drops results — R1 alone, qualified by out_vld, never fires on a dropped result; R2 does); “how do you assert credits never go negative?” (you cannot on an unsigned counter — bound plus consistency equation); and “what if completion is out-of-order?” (tag-indexed scoreboard or per-tag local variables — wire-order sequence numbers stop working). Saying “auxiliary modeling code is normal in industrial checkers” marks you as someone who has shipped one.

Key takeaways

• Four pipeline promises: gated-$past latency, stall hold, in-order retirement, credit bounds.

• Qualify the latency check with a valid pipe AND an advancing-beat guard for start-up.

• Check the valid path separately from the data path — dropped results are invisible to data-only rules.

• Unsigned counters cannot go negative — assert the upper bound and the conservation equation instead.

• Auxiliary modeling code (beat counters, sequence numbers) is standard practice, not a workaround.

Common pitfalls

• Ungated $past(in, LAT) on a stallable pipe — the first stall misaligns every later comparison.

• Latency rule qualified only by out_vld — a result the DUT drops never triggers the check at all.

• Asserting credits >= 0 on an unsigned counter — vacuously true; wraps hide as huge positives.

• Checking out_data stability during stall but not out_vld — valid drops, consumer misses the result.

• Sequence-number ordering rules on an out-of-order pipe — you needed tag-indexed tracking instead.