A bounded-wait check on the arbiter passes in seconds. The celebration is premature: if no requester ever waits, the check fired zero times and proved nothing about waiting. Every implication-style property in this course therefore ships with a cover of its trigger. This lesson shows both halves: reached covers with witnesses read cycle by cycle, on the arbiter and on the skid-buffer bridge, and a dead trigger whose property passes while its cover stays silent.
A cover asks the tool to find one trace where a condition holds. Reached means the scenario is possible and the witness is the evidence; not reached within the bound is inconclusive, never a proof of absence. A required cover that is not reached is a sign-off failure with an owner, not a side note. Vacuity, in the precise sense, means the trigger is never true. A weak sequence that simply never completes is a different case, and the two must not share a name.
The arbiter carries a cover for each grant and one for full contention with requester 3 at its wait limit; the bounded-wait checks fire only if that scenario exists. The run reaches every cover within depth 6, and the slowest, requester 3 waiting three cycles under full contention, first occurs at step 4. A cover run passes only when every cover in the module is reached.
// formal: cover 6 expect reached slang top rr_arbiter
`define FORMAL
// rr_arbiter: 4-requester round-robin arbiter. Grant is combinational from req and
// the 2-bit pointer `last` (index granted most recently). Search order starts at
// last+1 and wraps. A grant is given in the same cycle a request is seen, and a
// grant lasts one cycle only (no lock). Synchronous active-high reset: last = 3, so
// requester 0 has priority first.
// BUG: 0 none, 1 starvation (pointer not advanced when requester 0 wins),
// 2 double grant (low-priority path ORed in even when a higher-priority request exists),
// 3 grant without request (the last holder is ORed into the low-priority search).
module rr_arbiter #(parameter BUG = 0, parameter HELPER = 1) (
input wire clk,
input wire rst,
input wire [3:0] req,
output wire [3:0] grant
);
reg [1:0] last;
// requests strictly after `last` in rotation order (higher priority part)
wire [3:0] hi_mask = (last == 2'd0) ? 4'b1110 :
(last == 2'd1) ? 4'b1100 :
(last == 2'd2) ? 4'b1000 : 4'b0000;
wire [3:0] hi_req = req & hi_mask;
wire [3:0] lo_req = (BUG == 3) ? (req | (4'b0001 << last)) : req;
function [3:0] lowest; // lowest set bit, one-hot (0 if none)
input [3:0] v;
lowest = v & (~v + 4'd1);
endfunction
wire [3:0] g_hi = lowest(hi_req);
wire [3:0] g_lo = lowest(lo_req) & {4{(hi_req == 4'b0) || (BUG == 2)}};
assign grant = g_hi | g_lo;
wire [1:0] gidx = grant[0] ? 2'd0 : grant[1] ? 2'd1 : grant[2] ? 2'd2 : 2'd3;
always @(posedge clk) begin
if (rst) last <= 2'd3;
else if (|grant && !(BUG == 1 && grant[0])) last <= gidx;
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// wt[i]: consecutive cycles requester i has requested without being granted
reg [2:0] wt0, wt1, wt2, wt3;
always @(posedge clk) begin
if (rst) begin wt0 <= 3'd0; wt1 <= 3'd0; wt2 <= 3'd0; wt3 <= 3'd0; end
else begin
wt0 <= (req[0] && !grant[0]) ? wt0 + 3'd1 : 3'd0;
wt1 <= (req[1] && !grant[1]) ? wt1 + 3'd1 : 3'd0;
wt2 <= (req[2] && !grant[2]) ? wt2 + 3'd1 : 3'd0;
wt3 <= (req[3] && !grant[3]) ? wt3 + 3'd1 : 3'd0;
end
end
always @(*) if (!init) begin
a_onehot0: assert ((grant & (grant - 4'd1)) == 4'd0); // at most one grant
a_no_phantom: assert ((grant & ~req) == 4'd0); // grant implies request
a_work_cons: assert (!(|req) || (|grant)); // some request -> some grant
// bounded response (a starvation-freedom proxy): nobody waits more than 3 cycles
a_wt0: assert (wt0 <= 3'd3);
a_wt1: assert (wt1 <= 3'd3);
a_wt2: assert (wt2 <= 3'd3);
a_wt3: assert (wt3 <= 3'd3);
end
// helper invariants for the induction step of the wait bounds: waited cycles plus the
// requesters still ahead in rotation order never exceed 3
function [1:0] ahead; // how many grants can still precede requester i
input [1:0] i;
ahead = i - last - 2'd1; // 0..3 (mod 4)
endfunction
generate if (HELPER) begin : g_helper
always @(*) if (!init) begin
h_wt0: assert (wt0 + {1'b0, ahead(2'd0)} <= 3'd3);
h_wt1: assert (wt1 + {1'b0, ahead(2'd1)} <= 3'd3);
h_wt2: assert (wt2 + {1'b0, ahead(2'd2)} <= 3'd3);
h_wt3: assert (wt3 + {1'b0, ahead(2'd3)} <= 3'd3);
end
end endgenerate
// covers
always @(*) if (!init) begin
c_g0: cover (grant[0]);
c_g1: cover (grant[1]);
c_g2: cover (grant[2]);
c_g3: cover (grant[3]);
c_contend: cover (req == 4'b1111 && wt3 == 3'd3);
c_idle: cover (req == 4'b0000 && grant == 4'b0000);
end
`endif
endmoduleThe contention witness, with all four requesters holding their requests from step 1:
Step | req | last (before edge) | grant | What the row shows |
|---|---|---|---|---|
1 | 1111 | 3 | 0001 | After reset requester 0 has priority; requester 3 starts waiting. |
2 | 1111 | 0 | 0010 | Pointer advanced past 0; requester 3 has waited one cycle. |
3 | 1111 | 1 | 0100 | Rotation continues; requester 3 has waited two cycles. |
4 | 1111 | 2 | 1000 | Requester 3 is granted with its wait counter at 3: the cover fires here. |
Each row checks three things: the inputs are legal, the state follows from the previous row, and the covered condition is the conjunction the cover names, not one signal. A witness that needs illegal inputs is a harness bug, not evidence.
The bridge's hold checks, one for valid and one for data, are implications: if the output was stalled (valid high, ready low) in the previous cycle, then valid and data are unchanged. Their antecedent is the stall, so the stall cover is the antecedent cover; the property reads the condition one cycle after the cover names it. The same run also reaches the skid use and the back-pressure covers.
// formal: cover 4 expect reached slang top hs_bridge
`define FORMAL
// hs_bridge: valid/ready register stage with a skid buffer (2-entry elastic stage).
// Output stage `ovld/odat` plus skid `svld/sdat`. in_ready = !svld, so it depends on a
// register only (no combinational path from out_ready to in_ready). Synchronous
// active-high reset empties both stages. A transfer happens on a cycle where valid
// and ready are both 1.
// BUG: 0 none, 1 data dropped on stall (skid never captures), 2 valid dropped
// (stalled output loses valid when the input idles), 3 data changes under backpressure
// (stalled output overwritten by new input).
module hs_bridge #(parameter BUG = 0, parameter HELPER = 1) (
input wire clk,
input wire rst,
input wire in_valid,
output wire in_ready,
input wire [7:0] in_data,
output wire out_valid,
input wire out_ready,
output wire [7:0] out_data
);
reg ovld, svld;
reg [7:0] odat, sdat;
assign in_ready = !svld;
assign out_valid = ovld;
assign out_data = odat;
wire in_xfer = in_valid && in_ready;
wire out_xfer = ovld && out_ready;
wire stalled = ovld && !out_ready;
always @(posedge clk) begin
if (rst) begin
ovld <= 1'b0;
svld <= 1'b0;
end else if (stalled) begin
// output holds; a new input is parked in the skid register
if (in_xfer && BUG != 1) begin svld <= 1'b1; sdat <= in_data; end
if (BUG == 2 && !in_valid) ovld <= 1'b0;
if (BUG == 3 && in_xfer) odat <= in_data;
end else begin
// output empty or consumed this cycle
if (svld) begin
odat <= sdat; ovld <= 1'b1; svld <= 1'b0;
end else begin
odat <= in_data; ovld <= in_valid;
end
end
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// ---- conservation: accepted - delivered = items held (counters wrap at 16) ----
reg [3:0] acc, dlv;
always @(posedge clk) begin
if (rst) begin acc <= 4'd0; dlv <= 4'd0; end
else begin
if (in_xfer) acc <= acc + 4'd1;
if (out_xfer) dlv <= dlv + 4'd1;
end
end
always @(*) if (!init) begin
a_skid_needs_out: assert (!svld || ovld); // skid only used behind a full output
a_conserve: assert (acc - dlv == {3'b0, ovld} + {3'b0, svld});
end
// ---- protocol: a stalled output must hold valid and data ----
always @(posedge clk) if (!init && !$past(rst)) begin
a_valid_hold: assert (!($past(out_valid) && !$past(out_ready)) || out_valid);
a_data_hold: assert (!($past(out_valid) && !$past(out_ready)) || out_data == $past(out_data));
// ready is a registered function: it cannot depend on out_ready in the same cycle
a_no_ready_comb: assert (in_ready == !svld);
end
// ---- data integrity by tracked-item abstraction: follow the n-th accepted word ----
// free constant (see the FIFO module): anyconst wire plus an equal-to-its-old-copy assumption
(* anyconst *) wire [3:0] tn;
reg [3:0] tn_q;
always @(posedge clk) tn_q <= tn;
always @(*) if (!init) assume (tn == tn_q);
reg tv; // the tracked word has been accepted and not yet delivered
reg [7:0] td;
always @(posedge clk) begin
if (rst) tv <= 1'b0;
else begin
if (in_xfer && acc == tn) begin tv <= 1'b1; td <= in_data; end
else if (out_xfer && dlv == tn) tv <= 1'b0;
end
end
always @(*) if (!init && out_xfer && tv && dlv == tn) a_data: assert (out_data == td);
generate if (HELPER) begin : g_helper
always @(*) if (!init) begin
// where the tracked word lives: output stage if it is next to leave, else skid
h_in_out: assert (!(tv && dlv == tn) || (ovld && odat == td));
h_in_skid: assert (!(tv && dlv + 4'd1 == tn) || (svld && sdat == td));
h_pos: assert (!tv || (dlv == tn) || (dlv + 4'd1 == tn));
end
end endgenerate
// ---- covers ----
always @(*) if (!init) begin
c_stall: cover (stalled);
c_skid_used: cover (svld);
c_backpress_full: cover (!in_ready);
c_flow: cover (in_xfer && out_xfer);
end
`endif
endmoduleStep | in_valid | in_data | out_ready | out_valid | svld | What the row shows |
|---|---|---|---|---|---|---|
1 | 1 | 11 | 1 | 0 | 0 | First word accepted; the output register is still empty. |
2 | 1 | 22 | 0 | 1 | 0 | Output holds word 11 and ready is low: the stall cover fires. Word 22 goes to the skid register. |
3 | 1 | 33 | 0 | 1 | 1 | Skid occupied, so in_ready is low: the skid-use and back-pressure covers fire. Word 33 is not accepted. |
The data values are the ones of a typical stall trace; the tool may pick other values for the same shape. What the reviewer reads is the shape: a stall exists, so the hold checks have something to hold.
Now the contrast: a two-bit counter with a check whose trigger can never occur. The property passes at every bound, and the cover of the same trigger is not reached at any bound.
// formal: bmc 6 expect pass top dead_en
module dead_en (input wire clk, input wire rst);
reg [1:0] cnt;
always @(posedge clk) begin
if (rst) cnt <= 2'd0;
else cnt <= cnt + 2'd1;
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// the trigger needs cnt == 1 one cycle after cnt == 3, but the counter wraps 3 -> 0,
// so this antecedent is dead and the implication passes without ever firing
always @(posedge clk) if (!init && !$past(rst)) begin
a_dead: assert (!(cnt == 2'd1 && $past(cnt) == 2'd3) || cnt == $past(cnt) + 2'd1);
// the proof that the trigger is unreachable: the excluded pair never occurs
a_never: assert (!(cnt == 2'd1 && $past(cnt) == 2'd3));
end
always @(posedge clk) if (!init) begin
c_dead: cover (cnt == 2'd1 && $past(cnt) == 2'd3);
end
`endif
endmodule// formal: cover 6 expect fail top dead_en
module dead_en (input wire clk, input wire rst);
reg [1:0] cnt;
always @(posedge clk) begin
if (rst) cnt <= 2'd0;
else cnt <= cnt + 2'd1;
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// the trigger needs cnt == 1 one cycle after cnt == 3, but the counter wraps 3 -> 0,
// so this antecedent is dead and the implication passes without ever firing
always @(posedge clk) if (!init && !$past(rst)) begin
a_dead: assert (!(cnt == 2'd1 && $past(cnt) == 2'd3) || cnt == $past(cnt) + 2'd1);
// the proof that the trigger is unreachable: the excluded pair never occurs
a_never: assert (!(cnt == 2'd1 && $past(cnt) == 2'd3));
end
always @(posedge clk) if (!init) begin
c_dead: cover (cnt == 2'd1 && $past(cnt) == 2'd3);
end
`endif
endmoduleThe first block is the trap: bounded to 6, the assertion passes, and a reader who stops there files it as proven behaviour. The second block shows the trigger is not reached within 6, which on its own is only inconclusive. This counter is small enough to settle it: the third block proves that the excluded pair never occurs, so the pass is vacuous and the pair must be fixed or removed, never reported as evidence.
// formal: prove 4 expect pass top dead_en
module dead_en (input wire clk, input wire rst);
reg [1:0] cnt;
always @(posedge clk) begin
if (rst) cnt <= 2'd0;
else cnt <= cnt + 2'd1;
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// the trigger needs cnt == 1 one cycle after cnt == 3, but the counter wraps 3 -> 0,
// so this antecedent is dead and the implication passes without ever firing
always @(posedge clk) if (!init && !$past(rst)) begin
a_dead: assert (!(cnt == 2'd1 && $past(cnt) == 2'd3) || cnt == $past(cnt) + 2'd1);
// the proof that the trigger is unreachable: the excluded pair never occurs
a_never: assert (!(cnt == 2'd1 && $past(cnt) == 2'd3));
end
always @(posedge clk) if (!init) begin
c_dead: cover (cnt == 2'd1 && $past(cnt) == 2'd3);
end
`endif
endmoduleEvery implication-style property names its trigger cover, and the cover is reached at a stated depth.
Each reached cover has a witness the author has read: inputs legal, state reachable, condition exact.
No report lists a property as proven while its trigger cover is silent; silence is a failure with an owner.
When an expected cover is unreached, check in order: the trigger against the real encoding (wrong reset polarity and dead enables live here), the assumptions that might prune the scenario, and the bound (next lessons). Flip the trigger into an assertion temporarily: if it fails exactly where the witness should be, the scenario is reachable and the cover was miswritten.
Unknown. The environment may be so constrained that nothing interesting happens. Treat the silent cover as the primary finding and audit the assumptions before believing any pass.