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.
Slots 0 and 1 issue words A and B. The stall in slots 2 and 3 freezes every stage and issues nothing. A emerges in slot 4 and B in slot 5, each on its third advancing edge, and the bubble in slot 6 drops out_vld.
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 pasteable file with both checkers on this page, mul3_checker and the credit_checker described below, a small design and a bench that plants one bug at a time. Every rule reports through fail(), which counts and lets the run go on, because Verilator 5.048 stops at the first $error.
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 data-only rule is qualified by out_vld, so only the valid rule sees a dropped result.
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 a window form, delimited by the start and done events, and a cycle-local form that needs a busy level. Both fail at the cycle where cfg changes.
// 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.