A source changes its data two cycles into a stall. The sink has already sampled the first word, and the second word overwrites it. The property passed, because it checked stability for one cycle after the first stalled cycle and the corruption landed in the second wait cycle. This lesson's one job is the full-duration rule: stable until the handshake completes, on both sides of the interface.
Stability is an interval obligation, not an edge obligation. While valid is high and the grant has not arrived, the payload must not change: every stalled cycle, not just the first. The edge-gated textbook form, $rose(req) |=> $stable(addr), checks one cycle and goes quiet, which is exactly the shape a late change slips through. The full form re-arms every cycle the stall persists: (req && !gnt) |=> $stable(addr).
// not-run: implication operators are not accepted by this front end
// weak (one cycle): $rose(req) |=> $stable(addr)
// checks addr only in the cycle after req rises; later wait cycles are never looked at
// full (the interval): (req && !gnt) |=> $stable(addr)
// an attempt in EVERY stalled cycle, so addr is held until gnt arrives
// valid must also survive the stall: (req && !gnt) |=> req
// Boolean form of the full rule (a history flop and a comparator):
// !($past(req) && !$past(gnt)) || addr == $past(addr)The two sides of the interface split the work. On the input side, stability is an assumption: the environment promises that a presented word is presented again, unchanged, until it is accepted, and the proof searches only traces that keep the promise. On the output side, stability is an assertion: the block promises the same to its downstream. The textbook input rule, and its Boolean form for the open flow, are:
// not-run: implication operators are not accepted by this front end
// input side (the environment owes this), assumed:
// assume property (in_valid && !in_ready |=> in_valid && $stable(in_data));
// Boolean form:
// !($past(in_valid) && !$past(in_ready)) || (in_valid && in_data == $past(in_data))
// A plain in_valid && !in_ready ... $stable(in_data) on the CURRENT cycle is wrong:
// it would forbid a fresh word presented for the first time while ready is low.A pass-through stage forwards its input to its output and lends its ready to the input. Its output hold rule is a legitimate guarantee only if the input holds a stalled word. With no input rule the solver changes the data in the middle of a stall and the output rule fails; the failure belongs to the environment, not the stage. With the input rule assumed, the same output rule passes:
// formal: bmc 8 expect fail slang top thru define ASM=0
`define FORMAL
// thru: a pass-through stage: out_valid and out_data follow the input and in_ready
// is out_ready. Its output hold rule can only be true if the input holds a stalled word.
// ASM=0: no input rule. ASM=1: the input rule is assumed (the environment owes it).
module thru #(parameter ASM = 1) (
input wire clk,
input wire rst,
input wire in_valid,
input wire [7:0] in_data,
output wire in_ready,
output wire out_valid,
output wire [7:0] out_data,
input wire out_ready
);
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
assign in_ready = out_ready;
assign out_valid = in_valid;
assign out_data = in_data;
// input side, assumed: a word presented and not accepted is presented again, unchanged
generate if (ASM == 1) begin : g_env
always @(posedge clk) if (!init && !$past(rst))
s_in_hold: assume (!($past(in_valid) && !$past(in_ready)) || (in_valid && in_data == $past(in_data)));
end endgenerate
// output side, asserted: the same rule on the block's own output
always @(posedge clk) if (!init && !$past(rst))
a_out_hold: assert (!($past(out_valid) && !$past(out_ready)) || (out_valid && out_data == $past(out_data)));
endmodule// formal: bmc 8 expect pass slang top thru define ASM=1
`define FORMAL
// thru: a pass-through stage: out_valid and out_data follow the input and in_ready
// is out_ready. Its output hold rule can only be true if the input holds a stalled word.
// ASM=0: no input rule. ASM=1: the input rule is assumed (the environment owes it).
module thru #(parameter ASM = 1) (
input wire clk,
input wire rst,
input wire in_valid,
input wire [7:0] in_data,
output wire in_ready,
output wire out_valid,
output wire [7:0] out_data,
input wire out_ready
);
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
assign in_ready = out_ready;
assign out_valid = in_valid;
assign out_data = in_data;
// input side, assumed: a word presented and not accepted is presented again, unchanged
generate if (ASM == 1) begin : g_env
always @(posedge clk) if (!init && !$past(rst))
s_in_hold: assume (!($past(in_valid) && !$past(in_ready)) || (in_valid && in_data == $past(in_data)));
end endgenerate
// output side, asserted: the same rule on the block's own output
always @(posedge clk) if (!init && !$past(rst))
a_out_hold: assert (!($past(out_valid) && !$past(out_ready)) || (out_valid && out_data == $past(out_data)));
endmoduleThe output register below must hold its word while stalled. Its mutant overwrites the held word in the second stalled cycle. The weak form checks only the cycle after the first stalled cycle, so the mutant passes it. The full form checks the cycle after every stalled cycle and fails:
// formal: bmc 8 expect pass slang top hold_out define BUG=1 define FULL=0
`define FORMAL
// hold_out: an output register that must keep its word while stalled (out_valid high,
// out_ready low). sc is high from the second stalled cycle on. BUG=1 overwrites the held
// word in the SECOND stalled cycle. FULL=0 checks only the cycle after the first stalled
// cycle (the weak one-cycle form); FULL=1 checks the cycle after every stalled cycle.
module hold_out #(parameter BUG = 0, parameter FULL = 1) (
input wire clk,
input wire rst,
input wire in_valid,
input wire [7:0] in_data,
input wire out_ready,
output wire out_valid,
output wire [7:0] out_data
);
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
reg ov, sc;
reg [7:0] od;
wire stall = ov && !out_ready;
assign out_valid = ov;
assign out_data = od;
always @(posedge clk) begin
if (rst) begin ov <= 1'b0; od <= 8'd0; sc <= 1'b0; end
else if (stall) begin
sc <= 1'b1;
if (BUG == 1 && sc) od <= in_data;
end else begin
sc <= 1'b0; ov <= in_valid; od <= in_data;
end
end
always @(posedge clk) if (!init && !$past(rst) && !$past(rst, 2)) begin
if (FULL == 0) a_hold_first: assert (!($past(out_valid) && !$past(out_ready) && !($past(out_valid, 2) && !$past(out_ready, 2))) || out_data == $past(out_data));
else a_hold_all: assert (!($past(out_valid) && !$past(out_ready)) || out_data == $past(out_data));
end
endmodule// formal: bmc 8 expect fail slang top hold_out define BUG=1 define FULL=1
`define FORMAL
// hold_out: an output register that must keep its word while stalled (out_valid high,
// out_ready low). sc is high from the second stalled cycle on. BUG=1 overwrites the held
// word in the SECOND stalled cycle. FULL=0 checks only the cycle after the first stalled
// cycle (the weak one-cycle form); FULL=1 checks the cycle after every stalled cycle.
module hold_out #(parameter BUG = 0, parameter FULL = 1) (
input wire clk,
input wire rst,
input wire in_valid,
input wire [7:0] in_data,
input wire out_ready,
output wire out_valid,
output wire [7:0] out_data
);
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
reg ov, sc;
reg [7:0] od;
wire stall = ov && !out_ready;
assign out_valid = ov;
assign out_data = od;
always @(posedge clk) begin
if (rst) begin ov <= 1'b0; od <= 8'd0; sc <= 1'b0; end
else if (stall) begin
sc <= 1'b1;
if (BUG == 1 && sc) od <= in_data;
end else begin
sc <= 1'b0; ov <= in_valid; od <= in_data;
end
end
always @(posedge clk) if (!init && !$past(rst) && !$past(rst, 2)) begin
if (FULL == 0) a_hold_first: assert (!($past(out_valid) && !$past(out_ready) && !($past(out_valid, 2) && !$past(out_ready, 2))) || out_data == $past(out_data));
else a_hold_all: assert (!($past(out_valid) && !$past(out_ready)) || out_data == $past(out_data));
end
endmoduleOn the unmutated register the full form passes, so the failure above is the mutant and not the property:
// formal: bmc 8 expect pass slang top hold_out define BUG=0 define FULL=1
`define FORMAL
// hold_out: an output register that must keep its word while stalled (out_valid high,
// out_ready low). sc is high from the second stalled cycle on. BUG=1 overwrites the held
// word in the SECOND stalled cycle. FULL=0 checks only the cycle after the first stalled
// cycle (the weak one-cycle form); FULL=1 checks the cycle after every stalled cycle.
module hold_out #(parameter BUG = 0, parameter FULL = 1) (
input wire clk,
input wire rst,
input wire in_valid,
input wire [7:0] in_data,
input wire out_ready,
output wire out_valid,
output wire [7:0] out_data
);
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
reg ov, sc;
reg [7:0] od;
wire stall = ov && !out_ready;
assign out_valid = ov;
assign out_data = od;
always @(posedge clk) begin
if (rst) begin ov <= 1'b0; od <= 8'd0; sc <= 1'b0; end
else if (stall) begin
sc <= 1'b1;
if (BUG == 1 && sc) od <= in_data;
end else begin
sc <= 1'b0; ov <= in_valid; od <= in_data;
end
end
always @(posedge clk) if (!init && !$past(rst) && !$past(rst, 2)) begin
if (FULL == 0) a_hold_first: assert (!($past(out_valid) && !$past(out_ready) && !($past(out_valid, 2) && !$past(out_ready, 2))) || out_data == $past(out_data));
else a_hold_all: assert (!($past(out_valid) && !$past(out_ready)) || out_data == $past(out_data));
end
endmoduleCycle | State | Weak form looks at | Full form looks at |
|---|---|---|---|
1 | Word D valid, ready low: first stalled cycle | Nothing yet | Nothing yet |
2 | Still stalled; the mutant loads input E at the edge | Cycle 2 against cycle 1 (D, D): holds | Cycle 2 against cycle 1: holds |
3 | Output now shows E | Not armed: cycle 2 was not the first stalled cycle | Cycle 3 against cycle 2: D then E, fails |
How to read it: one slot is one step, counted from the first step after reset, so slot 1 is step 1. in_valid is high in step 1 only and offers the word 0x00 on in_data. That word is the output in step 2: out_valid is high, and out_ready stays low from there, so step 2 is the first stalled cycle (cycle 1 of the table) and step 3 the second, where second_stalled_cycle goes high. The input carries 0x01 in steps 2 and 3, and the register loads it at the edge that ends step 3: out_data reads 0x00 in steps 2 and 3 and 0x01 in step 4 (cycle 3 of the table). weak_viol, the one-cycle form, is armed only in the step after the first stalled cycle, which is step 3, where the word is unchanged: it stays low in every slot. full_viol, the form armed after every stalled cycle, goes high in step 4, where the word differs from step 3, and is still high in step 5, where the output changes again, to 0x00, the value on the input in step 4.
The bridge carries the output half of the rule as its data-hold check, and the full property set is proved on the correct design:
// formal: prove 4 expect pass 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 sync_fifo.sv): 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
endmoduleThe bridge's own planted mutant overwrites the held word as soon as an input is accepted during a stall. That happens in the first stalled cycle, so a one-cycle check also sees it; the second-cycle mutant above is the case only the full form catches. Nothing is lost, only changed, so conservation passes and the data checks fire:
// formal: bmc 4 expect fail slang top hs_bridge define BUG=3
`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 sync_fifo.sv): 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
endmoduleStability re-arms every stalled cycle: the antecedent is the stall condition itself, never an edge that fires once.
The side is right: assumes constrain inputs the environment drives, asserts check outputs the block drives; a stability assert on an input is a review failure on its own.
Data and valid travel together: a hold check on valid without one on data lets corruption through, as the mutant shows.
Read a stability failure as an interval: which cycle did the payload change, and was the handshake still open? If the change lands after the grant, the rule is too long, not the design too short: the obligation ends at acceptance. If it lands while stalled, lengthen nothing and fix the source. Conservation counts pass on corruption, as the bridge mutant shows, so the hold check is not redundant.
The obligation lasts until the handshake completes, which may take many cycles. An edge fires once and goes quiet; any change after its single checked cycle is invisible. The stall condition itself is the antecedent, so the check lives as long as the stall does.