Requester 0 hogs the arbiter: the pointer does not advance when requester 0 wins, so requesters 1 to 3 starve while 0 is served forever. The fix is one line: update the pointer on every grant. The functional test of the fixed scenario passes. The question nobody asks is whether the one-line change altered any grant pattern it should not have touched. This lesson proves both halves on the four-requester arbiter.
This lesson has one job: show the ECO pattern of agree-outside plus differ-exactly-inside as a real golden-against-revised proof, with a counterexample for an unintended side effect.
The roles are fixed before any proof. The golden is the design before the change: the arbiter whose pointer is held when requester 0 wins. The revised is the design after the change. An ECO proof compares them on shared inputs and shared reset. Outside the condition the fix acts on, the outputs must agree: this is the regression half, and a counterexample here is an unintended side effect. Inside the condition they must differ as intended: this is the repair half, shown by a witness that the difference exists and by the specification, where the golden fails a property the revised one proves.
In this ECO the condition the fix acts on is the first grant of requester 0 in the golden. Until that happens the two designs hold the same state, so every grant must agree; the miter keeps a flag touched that is set when the golden has granted requester 0. The proof needs one more fact, the correspondence the lesson on product machines teaches: while the flag is clear, the two pointers are equal. Without that helper the induction step starts from pairs with different pointers and fails.
The first block proves agree-outside for the real fix, together with the pointer correspondence. The second removes the pointer helper: the bounded check passes and the induction step fails, so the helper carries the proof. The third gives the revised design an unintended extra change, a grant to a requester that is not requesting when the bus is idle: the agree-outside check fails. Reading the counterexample: at step 0 the arbiter is in reset; at step 1 no requester asks, the golden grants nothing, and the revised design grants requester 3. The flag is still clear, so the two must agree, and they do not (depth 2, the first depth that shows it).
// formal: prove 5 expect pass slang top eco_miter
`define FORMAL
module rr_core #(parameter BUG = 0) (
input wire clk,
input wire rst,
input wire [3:0] req,
output wire [3:0] grant,
output reg [1:0] last
);
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;
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)}};
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
endmodule
module eco_miter #(parameter REV = 0, parameter CONSTRAIN = 0, parameter HELPER = 1) (
input wire clk,
input wire rst,
input wire [3:0] req,
output wire same
);
wire [3:0] g_old, g_new;
wire [1:0] l_old, l_new;
// golden: the arbiter before the fix (pointer held when requester 0 wins)
rr_core #(.BUG(1)) u_old (.clk(clk), .rst(rst), .req(req), .grant(g_old), .last(l_old));
// revised: the fix (REV = 0), or the fix plus an unintended extra change (REV = 3)
rr_core #(.BUG(REV)) u_new (.clk(clk), .rst(rst), .req(req), .grant(g_new), .last(l_new));
assign same = (g_old == g_new);
// touched: the golden has granted requester 0 at least once, the condition the fix acts on
reg touched;
always @(posedge clk) if (rst) touched <= 1'b0; else if (g_old[0]) touched <= 1'b1;
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(*) if (CONSTRAIN == 1) assume (req != 4'b0000);
always @(*) if (!init) a_agree_outside: assert (touched || same);
generate if (HELPER) begin : g_helper
always @(*) if (!init) h_same_ptr: assert (touched || (l_old == l_new));
end endgenerate
always @(*) if (!init) c_intended: cover (touched && !same);
`endif
endmodule// formal: prove 5 expect unproven slang top eco_miter define HELPER=0
`define FORMAL
module rr_core #(parameter BUG = 0) (
input wire clk,
input wire rst,
input wire [3:0] req,
output wire [3:0] grant,
output reg [1:0] last
);
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;
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)}};
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
endmodule
module eco_miter #(parameter REV = 0, parameter CONSTRAIN = 0, parameter HELPER = 1) (
input wire clk,
input wire rst,
input wire [3:0] req,
output wire same
);
wire [3:0] g_old, g_new;
wire [1:0] l_old, l_new;
// golden: the arbiter before the fix (pointer held when requester 0 wins)
rr_core #(.BUG(1)) u_old (.clk(clk), .rst(rst), .req(req), .grant(g_old), .last(l_old));
// revised: the fix (REV = 0), or the fix plus an unintended extra change (REV = 3)
rr_core #(.BUG(REV)) u_new (.clk(clk), .rst(rst), .req(req), .grant(g_new), .last(l_new));
assign same = (g_old == g_new);
// touched: the golden has granted requester 0 at least once, the condition the fix acts on
reg touched;
always @(posedge clk) if (rst) touched <= 1'b0; else if (g_old[0]) touched <= 1'b1;
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(*) if (CONSTRAIN == 1) assume (req != 4'b0000);
always @(*) if (!init) a_agree_outside: assert (touched || same);
generate if (HELPER) begin : g_helper
always @(*) if (!init) h_same_ptr: assert (touched || (l_old == l_new));
end endgenerate
always @(*) if (!init) c_intended: cover (touched && !same);
`endif
endmodule// formal: prove 5 expect fail slang top eco_miter define REV=3
`define FORMAL
module rr_core #(parameter BUG = 0) (
input wire clk,
input wire rst,
input wire [3:0] req,
output wire [3:0] grant,
output reg [1:0] last
);
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;
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)}};
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
endmodule
module eco_miter #(parameter REV = 0, parameter CONSTRAIN = 0, parameter HELPER = 1) (
input wire clk,
input wire rst,
input wire [3:0] req,
output wire same
);
wire [3:0] g_old, g_new;
wire [1:0] l_old, l_new;
// golden: the arbiter before the fix (pointer held when requester 0 wins)
rr_core #(.BUG(1)) u_old (.clk(clk), .rst(rst), .req(req), .grant(g_old), .last(l_old));
// revised: the fix (REV = 0), or the fix plus an unintended extra change (REV = 3)
rr_core #(.BUG(REV)) u_new (.clk(clk), .rst(rst), .req(req), .grant(g_new), .last(l_new));
assign same = (g_old == g_new);
// touched: the golden has granted requester 0 at least once, the condition the fix acts on
reg touched;
always @(posedge clk) if (rst) touched <= 1'b0; else if (g_old[0]) touched <= 1'b1;
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(*) if (CONSTRAIN == 1) assume (req != 4'b0000);
always @(*) if (!init) a_agree_outside: assert (touched || same);
generate if (HELPER) begin : g_helper
always @(*) if (!init) h_same_ptr: assert (touched || (l_old == l_new));
end endgenerate
always @(*) if (!init) c_intended: cover (touched && !same);
`endif
endmoduleStep | req | Golden grant | Revised grant | touched | Agree-outside |
|---|---|---|---|---|---|
0 | reset | - | - | 0 | not checked (reset step) |
1 | 0000 | 0000 | 1000 (requester 3, not requesting) | 0 | fails: grants differ while the flag is clear |
The repair half is a witness that the difference exists: the same miter with the cover reached. The golden grants requester 0 at step 1 and holds its pointer, the revised updates its pointer, and at step 2 the golden serves requester 0 again while the revised serves requester 1. Reaching it needs depth 3. A cover that is not reached within its depth is inconclusive, not proof of absence; here it is reached:
// formal: cover 3 expect reached slang top eco_miter
`define FORMAL
module rr_core #(parameter BUG = 0) (
input wire clk,
input wire rst,
input wire [3:0] req,
output wire [3:0] grant,
output reg [1:0] last
);
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;
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)}};
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
endmodule
module eco_miter #(parameter REV = 0, parameter CONSTRAIN = 0, parameter HELPER = 1) (
input wire clk,
input wire rst,
input wire [3:0] req,
output wire same
);
wire [3:0] g_old, g_new;
wire [1:0] l_old, l_new;
// golden: the arbiter before the fix (pointer held when requester 0 wins)
rr_core #(.BUG(1)) u_old (.clk(clk), .rst(rst), .req(req), .grant(g_old), .last(l_old));
// revised: the fix (REV = 0), or the fix plus an unintended extra change (REV = 3)
rr_core #(.BUG(REV)) u_new (.clk(clk), .rst(rst), .req(req), .grant(g_new), .last(l_new));
assign same = (g_old == g_new);
// touched: the golden has granted requester 0 at least once, the condition the fix acts on
reg touched;
always @(posedge clk) if (rst) touched <= 1'b0; else if (g_old[0]) touched <= 1'b1;
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(*) if (CONSTRAIN == 1) assume (req != 4'b0000);
always @(*) if (!init) a_agree_outside: assert (touched || same);
generate if (HELPER) begin : g_helper
always @(*) if (!init) h_same_ptr: assert (touched || (l_old == l_new));
end endgenerate
always @(*) if (!init) c_intended: cover (touched && !same);
`endif
endmoduleThe specification side of the repair half uses the arbiter file of the running design, with its wait counters: the golden fails the bounded-wait property, the revised design proves every property. The numbers are tool-measured: with the helper invariants off, the golden passes to depth 5 and fails at depth 6, because requester 1 must wait four cycles before the bound of 3 is exceeded. Any comparison bound shorter than that cannot show why the ECO was needed. The three runs:
// formal: prove 4 expect pass slang top rr_arbiter
`define FORMAL
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;
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;
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);
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);
a_no_phantom: assert ((grant & ~req) == 4'd0);
a_work_cons: assert (!(|req) || (|grant));
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
function [1:0] ahead;
input [1:0] i;
ahead = i - last - 2'd1;
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
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
endmodule// formal: bmc 6 expect fail slang top rr_arbiter define BUG=1 define HELPER=0
`define FORMAL
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;
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;
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);
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);
a_no_phantom: assert ((grant & ~req) == 4'd0);
a_work_cons: assert (!(|req) || (|grant));
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
function [1:0] ahead;
input [1:0] i;
ahead = i - last - 2'd1;
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
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
endmodule// formal: bmc 5 expect pass slang top rr_arbiter define BUG=1 define HELPER=0
`define FORMAL
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;
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;
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);
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);
a_no_phantom: assert ((grant & ~req) == 4'd0);
a_work_cons: assert (!(|req) || (|grant));
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
function [1:0] ahead;
input [1:0] i;
ahead = i - last - 2'd1;
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
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
endmodule# not-run: illustrative trace, not executable here
golden (pointer held), all four request from step 1:
step 1: grant 0001, pointer stays 3 | step 2: grant 0001 again ... requester 1 waits
by step 5 requester 1 has waited 4 cycles > bound 3 (depth 6 fails, depth 5 passes)
revised (pointer updated on every grant): grants rotate 0001, 0010, 0100, 1000
constraint caveat: assume req != 0 in the miter -> the idle-grant side effect cannot occurThe constraint caveat is the last piece. Add the assumption that the arbiter is never idle (req never 0000) to the side-effect miter and the same run is proven: the unintended grant only exists when nobody requests, and the constraint removed exactly that case. The result is true under the constraint and is not a signoff of the ECO. It is the pair of statements, with the constraint written next to the verdict, that is honest:
// formal: prove 5 expect pass slang top eco_miter define REV=3 define CONSTRAIN=1
`define FORMAL
module rr_core #(parameter BUG = 0) (
input wire clk,
input wire rst,
input wire [3:0] req,
output wire [3:0] grant,
output reg [1:0] last
);
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;
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)}};
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
endmodule
module eco_miter #(parameter REV = 0, parameter CONSTRAIN = 0, parameter HELPER = 1) (
input wire clk,
input wire rst,
input wire [3:0] req,
output wire same
);
wire [3:0] g_old, g_new;
wire [1:0] l_old, l_new;
// golden: the arbiter before the fix (pointer held when requester 0 wins)
rr_core #(.BUG(1)) u_old (.clk(clk), .rst(rst), .req(req), .grant(g_old), .last(l_old));
// revised: the fix (REV = 0), or the fix plus an unintended extra change (REV = 3)
rr_core #(.BUG(REV)) u_new (.clk(clk), .rst(rst), .req(req), .grant(g_new), .last(l_new));
assign same = (g_old == g_new);
// touched: the golden has granted requester 0 at least once, the condition the fix acts on
reg touched;
always @(posedge clk) if (rst) touched <= 1'b0; else if (g_old[0]) touched <= 1'b1;
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(*) if (CONSTRAIN == 1) assume (req != 4'b0000);
always @(*) if (!init) a_agree_outside: assert (touched || same);
generate if (HELPER) begin : g_helper
always @(*) if (!init) h_same_ptr: assert (touched || (l_old == l_new));
end endgenerate
always @(*) if (!init) c_intended: cover (touched && !same);
`endif
endmoduleThe ECO names golden and revised, the condition the fix acts on, and the agree-outside proof and the differ-inside evidence as separate rows.
The comparison bound exceeds the worst latency the change can affect: here deeper than 5 on the specification side, because the starvation needs four waiting cycles.
Any constraint on the comparison is listed with the verdict, per the constrained-equivalence lesson, and the excluded case has its own proof or owner.
Read the counterexample as a grant sequence, not a waveform: who was served, who waited, for how long. Confirm the intended difference appears where the fix acts and nowhere else. Then mutate an unrelated grant path deliberately, as the second revised variant does, and confirm the agree-outside proof catches it: a regression half that cannot fail is not checking the design.
The setup, not the fix: shared reset, shared input rules, and identical constants on both sides. Reproduce the mismatch with the fix reverted; if it persists, the harness differs between the two sides.