The revised arbiter matches the golden on every grant pattern across every bound the team runs. The ECO is signed off. A month later the system hangs: with no requesters active, the arbiter asserts a grant to nobody, and the downstream logic waits forever on a handshake that means nothing. Both implementations shared the phantom-grant bug, so agreement proved nothing about correctness. This lesson states the limit and the repair.
This lesson has one job: show that agreement without a property proof is not evidence, and write the signoff statement that is.
Equivalence is a relative statement: these two agree. Correctness is an absolute statement: this one obeys its specification. Two implementations can share a bug and agree perfectly, and the miter will pass with a straight face. The evidence that closes the gap is a property proof on the reference: no grant without a request, one-hot grants, bounded wait, each proved against the design, each paired with a cover that shows the property can fire.
The signoff statement for any equivalence therefore has three rows: what was compared and under which assumptions, what differs by intent, and which property proofs on the reference say the shared behaviour is right. Two rows without the third is an unfinished signoff.
The two implementations are the token ring and the rotating mask of the previous lesson, now written with the same defect: with no request at all, each grants the requester that has priority. They are different implementations (one-hot token against binary pointer) that share one bug. The first block proves them equivalent, state correspondence included. The second asserts the specification, no grant without a request, on both: it fails at depth 2, the first idle cycle after reset. The third shows the specification proven on both once the defect is removed. The fourth is the failing partner of the first: change the defect in one twin only and the equivalence check fails at once, so the pass of the first block is a real comparison and not a tautology:
// formal: prove 4 expect pass slang top twins define PHA=1 define PHB=1 define MODE=0
`define FORMAL
module tok_ring #(parameter PH = 0) (
input wire clk, rst,
input wire [1:0] req,
output wire [1:0] grant
);
reg [1:0] tok;
always @(posedge clk)
if (rst) tok <= 2'b10;
else if (|(req & tok)) tok <= {tok[0], tok[1]};
// PH = 1: with no request at all, the priority holder is granted anyway
assign grant = |(req & tok) ? tok :
|req ? req :
(PH == 1) ? tok : 2'b00;
endmodule
module rot_mask #(parameter PH = 0) (
input wire clk, rst,
input wire [1:0] req,
output wire [1:0] grant
);
reg pos;
wire [1:0] pri = pos ? 2'b01 : 2'b10;
wire adv = |(req & pri);
assign grant = adv ? (req & pri) :
|req ? req :
(PH == 1) ? pri : 2'b00;
always @(posedge clk)
if (rst) pos <= 1'b0;
else if (adv) pos <= ~pos;
endmodule
module twins #(parameter PHA = 1, parameter PHB = 1, parameter MODE = 0) (
input wire clk, rst,
input wire [1:0] req,
output wire same
);
wire [1:0] g1, g2;
tok_ring #(.PH(PHA)) u_t (.clk(clk), .rst(rst), .req(req), .grant(g1));
rot_mask #(.PH(PHB)) u_m (.clk(clk), .rst(rst), .req(req), .grant(g2));
assign same = (g1 == g2);
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(*) if (!init) h_pos: assert (u_t.tok == (u_m.pos ? 2'b01 : 2'b10));
// MODE 0: the two implementations agree. MODE 1: the reference property holds on both.
always @(*) if (!init && MODE == 0) a_equiv: assert (same);
always @(*) if (!init && MODE == 1) begin
a_no_phantom_t: assert ((g1 & ~req) == 2'b00);
a_no_phantom_m: assert ((g2 & ~req) == 2'b00);
end
`endif
endmodule// formal: bmc 2 expect fail slang top twins define PHA=1 define PHB=1 define MODE=1
`define FORMAL
module tok_ring #(parameter PH = 0) (
input wire clk, rst,
input wire [1:0] req,
output wire [1:0] grant
);
reg [1:0] tok;
always @(posedge clk)
if (rst) tok <= 2'b10;
else if (|(req & tok)) tok <= {tok[0], tok[1]};
// PH = 1: with no request at all, the priority holder is granted anyway
assign grant = |(req & tok) ? tok :
|req ? req :
(PH == 1) ? tok : 2'b00;
endmodule
module rot_mask #(parameter PH = 0) (
input wire clk, rst,
input wire [1:0] req,
output wire [1:0] grant
);
reg pos;
wire [1:0] pri = pos ? 2'b01 : 2'b10;
wire adv = |(req & pri);
assign grant = adv ? (req & pri) :
|req ? req :
(PH == 1) ? pri : 2'b00;
always @(posedge clk)
if (rst) pos <= 1'b0;
else if (adv) pos <= ~pos;
endmodule
module twins #(parameter PHA = 1, parameter PHB = 1, parameter MODE = 0) (
input wire clk, rst,
input wire [1:0] req,
output wire same
);
wire [1:0] g1, g2;
tok_ring #(.PH(PHA)) u_t (.clk(clk), .rst(rst), .req(req), .grant(g1));
rot_mask #(.PH(PHB)) u_m (.clk(clk), .rst(rst), .req(req), .grant(g2));
assign same = (g1 == g2);
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(*) if (!init) h_pos: assert (u_t.tok == (u_m.pos ? 2'b01 : 2'b10));
// MODE 0: the two implementations agree. MODE 1: the reference property holds on both.
always @(*) if (!init && MODE == 0) a_equiv: assert (same);
always @(*) if (!init && MODE == 1) begin
a_no_phantom_t: assert ((g1 & ~req) == 2'b00);
a_no_phantom_m: assert ((g2 & ~req) == 2'b00);
end
`endif
endmodule// formal: prove 4 expect pass slang top twins define PHA=0 define PHB=0 define MODE=1
`define FORMAL
module tok_ring #(parameter PH = 0) (
input wire clk, rst,
input wire [1:0] req,
output wire [1:0] grant
);
reg [1:0] tok;
always @(posedge clk)
if (rst) tok <= 2'b10;
else if (|(req & tok)) tok <= {tok[0], tok[1]};
// PH = 1: with no request at all, the priority holder is granted anyway
assign grant = |(req & tok) ? tok :
|req ? req :
(PH == 1) ? tok : 2'b00;
endmodule
module rot_mask #(parameter PH = 0) (
input wire clk, rst,
input wire [1:0] req,
output wire [1:0] grant
);
reg pos;
wire [1:0] pri = pos ? 2'b01 : 2'b10;
wire adv = |(req & pri);
assign grant = adv ? (req & pri) :
|req ? req :
(PH == 1) ? pri : 2'b00;
always @(posedge clk)
if (rst) pos <= 1'b0;
else if (adv) pos <= ~pos;
endmodule
module twins #(parameter PHA = 1, parameter PHB = 1, parameter MODE = 0) (
input wire clk, rst,
input wire [1:0] req,
output wire same
);
wire [1:0] g1, g2;
tok_ring #(.PH(PHA)) u_t (.clk(clk), .rst(rst), .req(req), .grant(g1));
rot_mask #(.PH(PHB)) u_m (.clk(clk), .rst(rst), .req(req), .grant(g2));
assign same = (g1 == g2);
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(*) if (!init) h_pos: assert (u_t.tok == (u_m.pos ? 2'b01 : 2'b10));
// MODE 0: the two implementations agree. MODE 1: the reference property holds on both.
always @(*) if (!init && MODE == 0) a_equiv: assert (same);
always @(*) if (!init && MODE == 1) begin
a_no_phantom_t: assert ((g1 & ~req) == 2'b00);
a_no_phantom_m: assert ((g2 & ~req) == 2'b00);
end
`endif
endmodule// formal: prove 4 expect fail slang top twins define PHA=1 define PHB=0 define MODE=0
`define FORMAL
module tok_ring #(parameter PH = 0) (
input wire clk, rst,
input wire [1:0] req,
output wire [1:0] grant
);
reg [1:0] tok;
always @(posedge clk)
if (rst) tok <= 2'b10;
else if (|(req & tok)) tok <= {tok[0], tok[1]};
// PH = 1: with no request at all, the priority holder is granted anyway
assign grant = |(req & tok) ? tok :
|req ? req :
(PH == 1) ? tok : 2'b00;
endmodule
module rot_mask #(parameter PH = 0) (
input wire clk, rst,
input wire [1:0] req,
output wire [1:0] grant
);
reg pos;
wire [1:0] pri = pos ? 2'b01 : 2'b10;
wire adv = |(req & pri);
assign grant = adv ? (req & pri) :
|req ? req :
(PH == 1) ? pri : 2'b00;
always @(posedge clk)
if (rst) pos <= 1'b0;
else if (adv) pos <= ~pos;
endmodule
module twins #(parameter PHA = 1, parameter PHB = 1, parameter MODE = 0) (
input wire clk, rst,
input wire [1:0] req,
output wire same
);
wire [1:0] g1, g2;
tok_ring #(.PH(PHA)) u_t (.clk(clk), .rst(rst), .req(req), .grant(g1));
rot_mask #(.PH(PHB)) u_m (.clk(clk), .rst(rst), .req(req), .grant(g2));
assign same = (g1 == g2);
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(*) if (!init) h_pos: assert (u_t.tok == (u_m.pos ? 2'b01 : 2'b10));
// MODE 0: the two implementations agree. MODE 1: the reference property holds on both.
always @(*) if (!init && MODE == 0) a_equiv: assert (same);
always @(*) if (!init && MODE == 1) begin
a_no_phantom_t: assert ((g1 & ~req) == 2'b00);
a_no_phantom_m: assert ((g2 & ~req) == 2'b00);
end
`endif
endmoduleSignoff for the arbiter ECO of the previous lessons, filled in. The first row cites the miter proof of the ECO lesson, the third the arbiter proof of the same lesson. Every result is bounded or proven as stated there; nothing below is wider than what those blocks ran:
Signoff row | Question answered | Statement for the arbiter ECO |
|---|---|---|
Equivalence outside the change | Did anything else move? | Golden (pointer held when requester 0 wins) against revised (pointer updated on every grant): grants agree on every input until the golden first grants requester 0, proved at depth 5 with the pointer correspondence proved; no constraint on the inputs; same reset. |
Intended difference | Did the fix act? | The difference is witnessed: the cover is reached at depth 3, requester 0 served twice by the golden and not by the revised. On the specification, the golden fails the bounded-wait property at depth 6 and the revised passes. |
Reference correctness | Is the shared behaviour right? | On the revised arbiter, proved at depth 4: at most one grant, no grant without a request, a grant whenever there is a request, and a wait of at most 3 cycles for every requester, with the covers for each requester reached. |
Not proved | What is left? | Behaviour after the first grant of requester 0 is not compared (the designs differ there by intent); results hold for the unconstrained inputs of the arbiter model only; no claim about the surrounding system. |
Every equivalence verdict is accompanied by the reference property list: no-grant-without-request, one-hot, bounded wait.
Each property has a firing cover: an untriggered correctness property is as suspicious as an uncompared mode.
The signoff names what was not proved: uncovered modes, bounded-only results with their justification, waived points with reasons.
Mutate the reference alone and confirm the property proof fails while the equivalence still passes: that split is the whole point of the lesson, demonstrated rather than asserted. Then mutate both twins identically and confirm the equivalence still passes: the pair is blind to shared bugs by construction, so the property list is the only eye on them. Mutate one twin and confirm the equivalence fails, as the fourth block does.
The assumptions behind both: input rules, reset behaviour, constraints and excluded modes. A proof is relative to its assumptions, so the signoff lists them and each assumption names where it is discharged.