Two teams implement the same round-robin arbiter two ways: a token ring that passes a one-hot token, and a rotating mask that keeps a binary pointer and recomputes priority each cycle. Gate-level structure shares nothing, so simulation is the only comparison until this lesson. The proof below runs both from the same reset on the same requests and asserts the same grant, with the invariant that the token and the pointer always encode the same priority.
This lesson has one job: prove two structurally different arbiters sequentially equivalent, and show the invariant doing the work. The arbiters here serve two requesters, a lesson-local reduction of the four-requester running design that keeps the proof small.
The product machine resets both arbiters together, drives identical request vectors, and asserts identical grants every cycle. The induction step needs the correspondence between the two state encodings: the one-hot token equals the mask that the binary pointer selects, proved as a helper. From an arbitrary pair the token and the pointer can disagree even when both designs are correct, so without the invariant the step fails from an unreachable pair, exactly as the product-machine lesson teaches.
Both arbiters serve two requesters round-robin. The token ring stores a one-hot token that marks the requester with priority and passes it on after the priority holder is served. The rotating mask stores one pointer bit and derives the priority mask from it every cycle. The invariant asserts that the token equals that mask. The first block proves the pair. The second removes the invariant: the bounded check passes and the induction step fails from a token and pointer that disagree, a pair no reset can produce. The third injects a bug in the mask arbiter: it advances its pointer on any request, including a request served out of turn, while the token ring passes its token only when the priority holder is served:
// formal: prove 4 expect pass slang top arb_twins
`define FORMAL
module tok_ring (
input wire clk, rst,
input wire [1:0] req,
output wire [1:0] grant
);
// one-hot token: the set bit marks the requester with priority
reg [1:0] tok;
always @(posedge clk)
if (rst) tok <= 2'b10;
else if (|(req & tok)) tok <= {tok[0], tok[1]};
assign grant = |(req & tok) ? tok : req;
endmodule
module rot_mask #(parameter BUG = 0) (
input wire clk, rst,
input wire [1:0] req,
output wire [1:0] grant
);
// binary pointer: priority mask derived from the pointer each cycle
reg pos;
wire [1:0] pri = pos ? 2'b01 : 2'b10;
wire adv = |(req & pri);
assign grant = adv ? (req & pri) : req;
always @(posedge clk)
if (rst) pos <= 1'b0;
else if ((BUG == 1) ? |req : adv) pos <= ~pos;
endmodule
module arb_twins #(parameter BUG = 0, parameter HELPER = 1) (
input wire clk, rst,
input wire [1:0] req,
output wire same
);
wire [1:0] g1, g2;
tok_ring u_t (.clk(clk), .rst(rst), .req(req), .grant(g1));
rot_mask #(.BUG(BUG)) 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) a_equiv: assert (same);
// state correspondence, written with hierarchical references (accepted by this front end only)
generate if (HELPER) begin : g_map
always @(*) if (!init) h_pos: assert (u_t.tok == (u_m.pos ? 2'b01 : 2'b10));
end endgenerate
`endif
endmodule// formal: prove 4 expect unproven slang top arb_twins define HELPER=0
`define FORMAL
module tok_ring (
input wire clk, rst,
input wire [1:0] req,
output wire [1:0] grant
);
// one-hot token: the set bit marks the requester with priority
reg [1:0] tok;
always @(posedge clk)
if (rst) tok <= 2'b10;
else if (|(req & tok)) tok <= {tok[0], tok[1]};
assign grant = |(req & tok) ? tok : req;
endmodule
module rot_mask #(parameter BUG = 0) (
input wire clk, rst,
input wire [1:0] req,
output wire [1:0] grant
);
// binary pointer: priority mask derived from the pointer each cycle
reg pos;
wire [1:0] pri = pos ? 2'b01 : 2'b10;
wire adv = |(req & pri);
assign grant = adv ? (req & pri) : req;
always @(posedge clk)
if (rst) pos <= 1'b0;
else if ((BUG == 1) ? |req : adv) pos <= ~pos;
endmodule
module arb_twins #(parameter BUG = 0, parameter HELPER = 1) (
input wire clk, rst,
input wire [1:0] req,
output wire same
);
wire [1:0] g1, g2;
tok_ring u_t (.clk(clk), .rst(rst), .req(req), .grant(g1));
rot_mask #(.BUG(BUG)) 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) a_equiv: assert (same);
// state correspondence, written with hierarchical references (accepted by this front end only)
generate if (HELPER) begin : g_map
always @(*) if (!init) h_pos: assert (u_t.tok == (u_m.pos ? 2'b01 : 2'b10));
end endgenerate
`endif
endmodule// formal: prove 4 expect fail slang top arb_twins define BUG=1
`define FORMAL
module tok_ring (
input wire clk, rst,
input wire [1:0] req,
output wire [1:0] grant
);
// one-hot token: the set bit marks the requester with priority
reg [1:0] tok;
always @(posedge clk)
if (rst) tok <= 2'b10;
else if (|(req & tok)) tok <= {tok[0], tok[1]};
assign grant = |(req & tok) ? tok : req;
endmodule
module rot_mask #(parameter BUG = 0) (
input wire clk, rst,
input wire [1:0] req,
output wire [1:0] grant
);
// binary pointer: priority mask derived from the pointer each cycle
reg pos;
wire [1:0] pri = pos ? 2'b01 : 2'b10;
wire adv = |(req & pri);
assign grant = adv ? (req & pri) : req;
always @(posedge clk)
if (rst) pos <= 1'b0;
else if ((BUG == 1) ? |req : adv) pos <= ~pos;
endmodule
module arb_twins #(parameter BUG = 0, parameter HELPER = 1) (
input wire clk, rst,
input wire [1:0] req,
output wire same
);
wire [1:0] g1, g2;
tok_ring u_t (.clk(clk), .rst(rst), .req(req), .grant(g1));
rot_mask #(.BUG(BUG)) 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) a_equiv: assert (same);
// state correspondence, written with hierarchical references (accepted by this front end only)
generate if (HELPER) begin : g_map
always @(*) if (!init) h_pos: assert (u_t.tok == (u_m.pos ? 2'b01 : 2'b10));
end endgenerate
`endif
endmoduleStep | req | Token ring (token) | Mask, buggy (pointer mask) | Grants | Broken condition |
|---|---|---|---|---|---|
1 | 01 | 10 (requester 1 has priority) | 10 | 01 and 01: requester 0 served out of turn | none yet |
2 | 11 | token stayed at 10 | pointer advanced on the request: mask 01 | 10 against 01 | map fails (10 against 01), grants differ |
The shortest counterexample is at step 2, depth 3 (measured: depth 2 passes). The root cause is a pointer-advance condition that is wider than the token-pass condition, so the two state encodings stop describing the same priority. The fix is to advance the pointer only when the priority holder is served, which is the condition the token ring already uses.
Hierarchical references. The invariant reads the registers of the two instances by hierarchical name. This front end accepts that, and not every flow does; a portable harness exposes the state of each instance as an output port, as the pipeline lesson does with its debug ports, and states the invariant on the ports.
The invariant relates the two state styles by meaning, not by name: the token and the pointer encode the same priority, not the registers match.
Both arbiters see identical requests from the same reset; no side has private stimulus.
The rotation bug is read as a pointer story first: where the encodings part, then what the grants do.
Replay the failing request sequence in simulation on both arbiters and confirm the grants part exactly one step after the encodings part. The invariant block with the invariant removed is the second proof above: the step fails from an unreachable pair, which shows the invariant carries the proof rather than decorating it. A twin proof that passes without any invariant on stateful designs deserves suspicion, not celebration.
The bounded agreement is encouraging but proves nothing unbounded, and the step failure names the missing invariant: find the unreachable starting pair in the CTI and assert the relation that excludes it.