A pipe promises four things. Results match operands from a fixed number of advancing beats back; stalls freeze every stage; results retire in order; credits stay within bounds.
Stalled slots do not advance data; each word reaches the output on its third advancing edge, counting the edge that issued it.
Slot 0: word A issued; first advancing edge.
Slot 1: word B issued; A moves to stage 2.
Slot 2: stall begins; every stage holds, nothing is issued.
Slot 3: stall continues; every stage still holds.
Slot 4: advance resumes; A emerges on its third advancing edge, two wall cycles late.
Slot 5: B emerges on its third advancing edge.
Slot 6: a bubble reaches the output, so out_vld drops.
Promise | Assertion shape |
|---|---|
Latency |
|
Valid pipe |
|
Stall hold |
|
Ordering and credits | Tags retire in order; |
The textbook latency rule is out_p == $past(in_a, LAT, adv) * $past(in_b, LAT, adv). Verilator 5.048 rejects the gated $past, so this checker keeps a short history that advances only on adv, which is what the gate means.
The listing is one file you can paste into the Code Lab: the checker first, then a small design and a bench that runs legal traffic before planting one bug at a time. Every rule reports through fail(), which counts and prints the report and lets the run go on; Verilator 5.048 stops at the first $error, and production checkers often count the same way. It holds both checkers on this page: mul3_checker and the credit_checker described below.
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
);
int n_fail = 0, n_stall_mid = 0;
function automatic void fail(string msg);
n_fail++;
$display("[%0t] mul3_checker: %s", $time, msg);
endfunction
logic adv;
assign adv = !stall;
// History that advances only on adv: the job of $past(x, LAT, adv), which the
// open simulator rejects. h_a[k] holds in_a from k+1 advancing beats back.
logic [W-1:0] h_a [LAT], h_b [LAT];
logic h_v [LAT];
int unsigned adv_beats;
always_ff @(posedge clk or negedge rst_n)
if (!rst_n) begin
adv_beats <= 0;
for (int k = 0; k < LAT; k++) begin h_a[k] <= 0; h_b[k] <= 0; h_v[k] <= 0; end
end else if (adv) begin
adv_beats <= adv_beats + 1;
h_a[0] <= in_a; h_b[0] <= in_b; h_v[0] <= in_vld;
for (int k = 1; k < LAT; k++) begin h_a[k] <= h_a[k-1]; h_b[k] <= h_b[k-1]; h_v[k] <= h_v[k-1]; end
end
// Each operand is cast wide before the multiply.
a_latency: assert property (@(posedge clk) disable iff (!rst_n)
(out_vld && adv && adv_beats >= LAT) |->
(out_p == (2*W)'(h_a[LAT-1]) * (2*W)'(h_b[LAT-1])))
else fail("product wrong vs operands LAT beats back");
// 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 == h_v[LAT-1]))
else fail("valid lost or invented in the pipe");
// 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 fail("output moved during stall");
c_stall_mid: cover property (@(posedge clk)
out_vld && stall ##1 stall ##1 ~stall) n_stall_mid++;
endmodule
module credit_checker #(
parameter int CAP = 4,
parameter int TAGW = 4,
parameter int CW = 3
)(
input logic clk, rst_n,
input logic cmd_vld, cmd_rdy, rsp_vld, rsp_rdy,
input logic [TAGW-1:0] rsp_tag,
input logic [CW-1:0] credits
);
int n_fail = 0;
function automatic void fail(string msg);
n_fail++;
$display("[%0t] credit_checker: %s", $time, msg);
endfunction
int unsigned issue_sn, retire_sn;
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
a_in_order: assert property (@(posedge clk) disable iff (!rst_n)
(rsp_vld && rsp_rdy) |-> (rsp_tag == retire_sn[TAGW-1:0]))
else fail("out-of-order tag");
a_credit_ceiling: assert property (@(posedge clk) disable iff (!rst_n)
credits <= CAP)
else fail("credit overflow");
a_credit_consist: assert property (@(posedge clk) disable iff (!rst_n)
credits == CAP - (issue_sn - retire_sn))
else fail("credits disagree with outstanding count");
a_no_oversubscribe: assert property (@(posedge clk) disable iff (!rst_n)
(cmd_vld && cmd_rdy) |-> (credits > 0))
else fail("issued with no credit");
endmodule
// The stallable multiplier, with a plantable bug: the last stage moves during a stall.
module mpipe #(parameter int LAT = 3, parameter int W = 8) (
input logic clk, rst_n, stall, in_vld, bug,
input logic [W-1:0] in_a, in_b,
output logic out_vld,
output logic [2*W-1:0] out_p
);
logic [W-1:0] a_p [LAT], b_p [LAT];
logic v_p [LAT];
assign out_p = (2*W)'(a_p[LAT-1]) * (2*W)'(b_p[LAT-1]);
assign out_vld = v_p[LAT-1];
always_ff @(posedge clk or negedge rst_n)
if (!rst_n) for (int k = 0; k < LAT; k++) begin a_p[k] <= 0; b_p[k] <= 0; v_p[k] <= 0; end
else if (!stall) begin
a_p[0] <= in_a; b_p[0] <= in_b; v_p[0] <= in_vld;
for (int k = 1; k < LAT; k++) begin a_p[k] <= a_p[k-1]; b_p[k] <= b_p[k-1]; v_p[k] <= v_p[k-1]; end
end else if (bug) begin
a_p[LAT-1] <= a_p[LAT-2]; b_p[LAT-1] <= b_p[LAT-2]; v_p[LAT-1] <= v_p[LAT-2];
end
endmodule
legal: 3 products across a 2-cycle stall, 3 commands and 3 in-order responses: 0 new report(s)
cover, a result held through a stall: 1
[245] mul3_checker: output moved during stall
[255] mul3_checker: product wrong vs operands LAT beats back
planted: the last stage moves during a stall: 2 new report(s)
[315] credit_checker: out-of-order tag
[325] credit_checker: out-of-order tag
responses retired 4 before 3: 2 new report(s)
[395] credit_checker: issued with no credit
[405] credit_checker: credit overflow
[405] credit_checker: credits disagree with outstanding count
[415] credit_checker: credit overflow
[415] credit_checker: credits disagree with outstanding count
a fifth command against a cap of 4: 5 new report(s)
PASS: legal traffic was clean, and the stall, ordering and credit bugs were each reportedThe valid pipe is checked apart from the data. A dropped result never triggers a data-only rule, since that rule is qualified by out_vld; the valid rule sees the gap.
Flow control is a conservation law. Outstanding requests plus credits equal the cap, every cycle.
credit_checker is the second module in the listing above. It counts issues and retirements in modeling code, then checks order, the ceiling, conservation and oversubscription.
Config stability has two forms. Both fail at the cycle where cfg changes. The window form is delimited by the start and done events; the cycle-local form needs a busy level that covers the window.
// snippet
// Window form, delimited by start/done events. It begins at the $rose(start)
// cycle, where $stable(cfg) compares against the pre-start value:
// $rose(start) |-> $stable(cfg) throughout (##1 (!done)[*0:MAX] ##1 done);
// If cfg may be written in the same cycle as start, open the window a cycle later.
// Cycle-local form, needs a busy level:
// busy |-> $stable(cfg);The valid-pipe rule. Data-only rules are qualified by out_vld, so a missing result never triggers them.
credits is decremented at zero. What does the ceiling rule see?A huge wrapped value above CAP. The rule fires the same cycle; a credits >= 0 rule would stay true forever.
Three products across a two-cycle stall, three commands and three in-order responses give no reports, and the stall cover hits. A last stage that moves during a stall is reported twice: the hold rule sees the move, and the latency rule sees the wrong product on the next advancing beat. Two responses retired out of order give one report each. A fifth command against a cap of 4 gives five: no credit at issue, then the wrapped counter breaks the ceiling and conservation for two cycles.
Run with Verilator 5.048 (--binary --timing --assert, plus --coverage when a listing has a cover property) on 2026-10-18; every bench printed the PASS line shown. Verilator stops at the first $error or failing assertion without an action block, so the benches count failures in the action block. Icarus 13 has no concurrent assertions.
Gated $past was replaced by a history that advances on adv; the stall cover hit once the stall happened with a result at the output.