A response rule fails with a counterexample in which the environment simply never answers. The engineer has two wrong moves available: blame the design, or assume the answer onto the design's own output and watch everything pass. Both miss the one honest move. This lesson's one job is the fairness contract: what the environment owes, what the design owes, and how to tell them apart.
Liveness needs fairness, and fairness constrains environment choices only: the downstream answers within its documented bound, the requester holds its request until it is answered. The test for any assume is what it binds: it must constrain an input, and it may read internal state to say when. Constraining a design output instead prunes the design, not the environment, so the proof passes for a smaller machine than the one being built. The module below uses both: the two environment assumptions bind only req and rdy, and a third variant, labelled as the deliberate counter-example, assumes the output ack. The bounded form of fairness is a stall bound: at most one stalled cycle per wait. The responder in this lesson answers two cycles after the rising edge when the downstream is ready, so one allowed stall gives a three-cycle window: latency two plus stall bound one.
The requester side of the contract matters as much as the answer side: a request dropped before its answer releases the obligation, so the environment must hold the request until the handshake completes. Without that hold the obligation is ill-posed, because the requester can walk away.
Without any fairness the downstream may keep rdy low for ever, and the three-cycle window fails. The counterexample the solver returns is a finite prefix in which rdy stays low through the whole window; it stands for the infinite stall, which no bounded run can show directly. A trace of that shape, constructed by hand from the module (the solver's own values for the free inputs may differ):
Step | req | rdy | pend at the start of the step | ack | Reading |
|---|---|---|---|---|---|
0 | 0 | 0 | reset step | 0 | Not checked. |
1 | 1 | 0 | 0 | 0 | The request rises: the attempt starts. |
2 | 1 | 0 | 1 | 0 | Pending and stalled. |
3 | 1 | 0 | 1 | 0 | Stalled again. |
4 | 1 | 0 | 1 | 0 | The window of three cycles has closed with no answer. A clocked check reports it one step later. |
// formal: bmc 8 expect fail slang define ASSUME=0
`define FORMAL
// stall_bound: a responder behind a rising request edge. pend is set by the edge and cleared in
// the cycle the answer is issued; ack is registered, so with rdy high the answer appears two
// cycles after the rise, and every stalled cycle (pending, rdy low) adds one cycle.
// ASSUME=0 constrains nothing. ASSUME=1 adds the documented environment contract: a request is held
// until it is answered, and rdy is low for at most one cycle in a row. Both constraints bind inputs
// (req, rdy); they read the internal state only to say when. ASSUME=2 is the deliberate counter-example:
// it assumes the answer itself, a constraint on the design's own output, which the lesson forbids.
// p_bounded is rose |-> ##[1:3] ack in Boolean form, judged when the window closes.
module stall_bound #(parameter ASSUME = 0) (
input wire clk,
input wire rst,
input wire req,
input wire rdy,
output reg ack
);
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(*) if (rst) assume (!req);
reg req_q, rose_d1, rose_d2, rose_d3;
wire rose = req && !req_q;
reg pend;
reg [1:0] stall;
always @(posedge clk) begin
if (rst) begin
req_q <= 1'b0; rose_d1 <= 1'b0; rose_d2 <= 1'b0; rose_d3 <= 1'b0;
pend <= 1'b0; stall <= 2'd0; ack <= 1'b0;
end else begin
req_q <= req;
rose_d1 <= rose; rose_d2 <= rose_d1; rose_d3 <= rose_d2;
ack <= pend && rdy;
pend <= (rose || pend) && !(pend && rdy);
if (!rdy && pend) stall <= stall + 2'd1; else stall <= 2'd0;
end
end
generate if (ASSUME == 1) begin : g_env
always @(*) if (!init) begin
assume (!pend || req);
assume (!pend || stall <= 2'd1);
end
end endgenerate
generate if (ASSUME == 2) begin : g_bad
always @(*) if (!init) assume (ack);
end endgenerate
always @(posedge clk) if (!init && !$past(rst) && !$past(rst, 2) && !$past(rst, 3)) begin
p_bounded: assert (!rose_d3 || $past(ack, 2) || $past(ack) || ack);
end
always @(*) if (!init) c_stall: cover (pend && !rdy);
endmoduleWith the documented environment contract, held requests and at most one stalled cycle in a row, the same window passes on the same responder. The pass is bounded to depth 16, the deepest run made:
// formal: bmc 16 expect pass slang define ASSUME=1
`define FORMAL
// stall_bound: a responder behind a rising request edge. pend is set by the edge and cleared in
// the cycle the answer is issued; ack is registered, so with rdy high the answer appears two
// cycles after the rise, and every stalled cycle (pending, rdy low) adds one cycle.
// ASSUME=0 constrains nothing. ASSUME=1 adds the documented environment contract: a request is held
// until it is answered, and rdy is low for at most one cycle in a row. Both constraints bind inputs
// (req, rdy); they read the internal state only to say when. ASSUME=2 is the deliberate counter-example:
// it assumes the answer itself, a constraint on the design's own output, which the lesson forbids.
// p_bounded is rose |-> ##[1:3] ack in Boolean form, judged when the window closes.
module stall_bound #(parameter ASSUME = 0) (
input wire clk,
input wire rst,
input wire req,
input wire rdy,
output reg ack
);
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(*) if (rst) assume (!req);
reg req_q, rose_d1, rose_d2, rose_d3;
wire rose = req && !req_q;
reg pend;
reg [1:0] stall;
always @(posedge clk) begin
if (rst) begin
req_q <= 1'b0; rose_d1 <= 1'b0; rose_d2 <= 1'b0; rose_d3 <= 1'b0;
pend <= 1'b0; stall <= 2'd0; ack <= 1'b0;
end else begin
req_q <= req;
rose_d1 <= rose; rose_d2 <= rose_d1; rose_d3 <= rose_d2;
ack <= pend && rdy;
pend <= (rose || pend) && !(pend && rdy);
if (!rdy && pend) stall <= stall + 2'd1; else stall <= 2'd0;
end
end
generate if (ASSUME == 1) begin : g_env
always @(*) if (!init) begin
assume (!pend || req);
assume (!pend || stall <= 2'd1);
end
end endgenerate
generate if (ASSUME == 2) begin : g_bad
always @(*) if (!init) assume (ack);
end endgenerate
always @(posedge clk) if (!init && !$past(rst) && !$past(rst, 2) && !$past(rst, 3)) begin
p_bounded: assert (!rose_d3 || $past(ack, 2) || $past(ack) || ack);
end
always @(*) if (!init) c_stall: cover (pend && !rdy);
endmoduleThe next run is the deliberate counter-example, the very thing the rule above forbids: it assumes the design output ack itself. It also passes, for a machine with no behaviour left in it, and the pass is a false one. It is the same bounded depth as the honest run, which is why a pass alone cannot tell the two apart; the covers do:
// formal: bmc 16 expect pass slang define ASSUME=2
`define FORMAL
// stall_bound: a responder behind a rising request edge. pend is set by the edge and cleared in
// the cycle the answer is issued; ack is registered, so with rdy high the answer appears two
// cycles after the rise, and every stalled cycle (pending, rdy low) adds one cycle.
// ASSUME=0 constrains nothing. ASSUME=1 adds the documented environment contract: a request is held
// until it is answered, and rdy is low for at most one cycle in a row. Both constraints bind inputs
// (req, rdy); they read the internal state only to say when. ASSUME=2 is the deliberate counter-example:
// it assumes the answer itself, a constraint on the design's own output, which the lesson forbids.
// p_bounded is rose |-> ##[1:3] ack in Boolean form, judged when the window closes.
module stall_bound #(parameter ASSUME = 0) (
input wire clk,
input wire rst,
input wire req,
input wire rdy,
output reg ack
);
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(*) if (rst) assume (!req);
reg req_q, rose_d1, rose_d2, rose_d3;
wire rose = req && !req_q;
reg pend;
reg [1:0] stall;
always @(posedge clk) begin
if (rst) begin
req_q <= 1'b0; rose_d1 <= 1'b0; rose_d2 <= 1'b0; rose_d3 <= 1'b0;
pend <= 1'b0; stall <= 2'd0; ack <= 1'b0;
end else begin
req_q <= req;
rose_d1 <= rose; rose_d2 <= rose_d1; rose_d3 <= rose_d2;
ack <= pend && rdy;
pend <= (rose || pend) && !(pend && rdy);
if (!rdy && pend) stall <= stall + 2'd1; else stall <= 2'd0;
end
end
generate if (ASSUME == 1) begin : g_env
always @(*) if (!init) begin
assume (!pend || req);
assume (!pend || stall <= 2'd1);
end
end endgenerate
generate if (ASSUME == 2) begin : g_bad
always @(*) if (!init) assume (ack);
end endgenerate
always @(posedge clk) if (!init && !$past(rst) && !$past(rst, 2) && !$past(rst, 3)) begin
p_bounded: assert (!rose_d3 || $past(ack, 2) || $past(ack) || ack);
end
always @(*) if (!init) c_stall: cover (pend && !rdy);
endmoduleThe cover asks for a stalled cycle: a request pending while the downstream is not ready. With the honest contract the stall is reachable, so the fairness assumption left the bad environment behaviour in play and only bounded it:
// formal: cover 6 expect reached slang define ASSUME=1
`define FORMAL
// stall_bound: a responder behind a rising request edge. pend is set by the edge and cleared in
// the cycle the answer is issued; ack is registered, so with rdy high the answer appears two
// cycles after the rise, and every stalled cycle (pending, rdy low) adds one cycle.
// ASSUME=0 constrains nothing. ASSUME=1 adds the documented environment contract: a request is held
// until it is answered, and rdy is low for at most one cycle in a row. Both constraints bind inputs
// (req, rdy); they read the internal state only to say when. ASSUME=2 is the deliberate counter-example:
// it assumes the answer itself, a constraint on the design's own output, which the lesson forbids.
// p_bounded is rose |-> ##[1:3] ack in Boolean form, judged when the window closes.
module stall_bound #(parameter ASSUME = 0) (
input wire clk,
input wire rst,
input wire req,
input wire rdy,
output reg ack
);
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(*) if (rst) assume (!req);
reg req_q, rose_d1, rose_d2, rose_d3;
wire rose = req && !req_q;
reg pend;
reg [1:0] stall;
always @(posedge clk) begin
if (rst) begin
req_q <= 1'b0; rose_d1 <= 1'b0; rose_d2 <= 1'b0; rose_d3 <= 1'b0;
pend <= 1'b0; stall <= 2'd0; ack <= 1'b0;
end else begin
req_q <= req;
rose_d1 <= rose; rose_d2 <= rose_d1; rose_d3 <= rose_d2;
ack <= pend && rdy;
pend <= (rose || pend) && !(pend && rdy);
if (!rdy && pend) stall <= stall + 2'd1; else stall <= 2'd0;
end
end
generate if (ASSUME == 1) begin : g_env
always @(*) if (!init) begin
assume (!pend || req);
assume (!pend || stall <= 2'd1);
end
end endgenerate
generate if (ASSUME == 2) begin : g_bad
always @(*) if (!init) assume (ack);
end endgenerate
always @(posedge clk) if (!init && !$past(rst) && !$past(rst, 2) && !$past(rst, 3)) begin
p_bounded: assert (!rose_d3 || $past(ack, 2) || $past(ack) || ack);
end
always @(*) if (!init) c_stall: cover (pend && !rdy);
endmoduleWith the answer assumed the same cover is not reached within 6. Not reached within a depth is inconclusive on its own: a longer run or a deeper trace might reach it. Here the reason is visible in the assumption: it demands an answer in every cycle after the reset step, so a request that waits cannot exist. The cover did not prove that; it pointed at it, which is the use of a cover next to an assume:
// formal: cover 6 expect fail slang define ASSUME=2
`define FORMAL
// stall_bound: a responder behind a rising request edge. pend is set by the edge and cleared in
// the cycle the answer is issued; ack is registered, so with rdy high the answer appears two
// cycles after the rise, and every stalled cycle (pending, rdy low) adds one cycle.
// ASSUME=0 constrains nothing. ASSUME=1 adds the documented environment contract: a request is held
// until it is answered, and rdy is low for at most one cycle in a row. Both constraints bind inputs
// (req, rdy); they read the internal state only to say when. ASSUME=2 is the deliberate counter-example:
// it assumes the answer itself, a constraint on the design's own output, which the lesson forbids.
// p_bounded is rose |-> ##[1:3] ack in Boolean form, judged when the window closes.
module stall_bound #(parameter ASSUME = 0) (
input wire clk,
input wire rst,
input wire req,
input wire rdy,
output reg ack
);
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(*) if (rst) assume (!req);
reg req_q, rose_d1, rose_d2, rose_d3;
wire rose = req && !req_q;
reg pend;
reg [1:0] stall;
always @(posedge clk) begin
if (rst) begin
req_q <= 1'b0; rose_d1 <= 1'b0; rose_d2 <= 1'b0; rose_d3 <= 1'b0;
pend <= 1'b0; stall <= 2'd0; ack <= 1'b0;
end else begin
req_q <= req;
rose_d1 <= rose; rose_d2 <= rose_d1; rose_d3 <= rose_d2;
ack <= pend && rdy;
pend <= (rose || pend) && !(pend && rdy);
if (!rdy && pend) stall <= stall + 2'd1; else stall <= 2'd0;
end
end
generate if (ASSUME == 1) begin : g_env
always @(*) if (!init) begin
assume (!pend || req);
assume (!pend || stall <= 2'd1);
end
end endgenerate
generate if (ASSUME == 2) begin : g_bad
always @(*) if (!init) assume (ack);
end endgenerate
always @(posedge clk) if (!init && !$past(rst) && !$past(rst, 2) && !$past(rst, 3)) begin
p_bounded: assert (!rose_d3 || $past(ack, 2) || $past(ack) || ack);
end
always @(*) if (!init) c_stall: cover (pend && !rdy);
endmoduleEvery fairness assumption names an environment signal: ready, request hold, arbitration among requesters, never a design output.
The stall bound is documented with its source: the downstream specification's maximum backpressure, plus the simulation that shows it.
An assume on a design output is a review failure on its own: each assume is checked against the port list, and the question is what it binds. An output on the left of a constraint is rejected; an output read as a condition that restricts an input is fine.
A cover of the stalled situation is reached under the final assumption set; an unreached one is inconclusive and needs an explanation, not a deadline extension.
Read a liveness-shaped failure by asking who idles: if the loop that avoids the event drives only environment inputs, the design is owed fairness it was never given, and the fix is a documented assumption. If the loop needs no environment help, the design can starve on its own and the fix is in the arbitration. Then run the cover: a liveness proof whose environment never stalls in any witnessed trace assumed more than it documented.
Three cycles: the edge is cycle t, with the downstream ready the answer appears at t plus 2, and one allowed stall moves it to t plus 3. The window is latency plus stall bound, each stated, never a round number.