A change note says the arbiter's pointer resets to a different value, so a different requester wins the first contention. The miter reports a mismatch on the first all-request cycle, and a careless reader files the change broken. It is not: the difference is intended, and the job is to show it where it is and prove agreement everywhere it should hold. Both revisions here are lesson-local copies of the arbiter, written for this lesson; the running arbiter ships with no such change.
The change note: the reset value of the pointer changes from 3 to 0. Nothing else changes.
The two revisions, before and after, as separate modules, each with its pointer exposed for the properties.
The model below, a pointer-level description of both revisions.
// formal: bmc 2 expect fail slang top arb_eco_miter
`define FORMAL
// lesson-local revision before the change: the pointer resets to 3, so requester 0 is served first
module rr_arbiter_gold (
input wire clk,
input wire rst,
input wire [3:0] req,
output wire [3:0] grant,
output wire [1:0] dbg_last
);
reg [1:0] last;
assign dbg_last = 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;
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(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) last <= gidx;
end
endmodule
// lesson-local revision after the change: the pointer resets to 0, so requester 1 is served first
module rr_arbiter_eco (
input wire clk,
input wire rst,
input wire [3:0] req,
output wire [3:0] grant,
output wire [1:0] dbg_last
);
reg [1:0] last;
assign dbg_last = 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;
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(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'd0;
else if (|grant) last <= gidx;
end
endmodule
module arb_eco_miter (
input wire clk,
input wire rst,
input wire [3:0] req,
output wire same
);
wire [3:0] g1, g2;
wire [1:0] l1, l2;
rr_arbiter_gold u1 (.clk(clk), .rst(rst), .req(req), .grant(g1), .dbg_last(l1));
rr_arbiter_eco u2 (.clk(clk), .rst(rst), .req(req), .grant(g2), .dbg_last(l2));
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);
`endif
endmoduleExpected outcome of the block: counterexample. The mismatch it finds is the change doing what the note says.
def run(reset, masks):
last, out = reset, []
for m in masks:
g = None
for off in range(1, 5):
i = (last + off) % 4
if m >> i & 1:
g = i
break
out.append((last, g))
if g is not None:
last = g
return out
BEFORE, AFTER = 3, 0
all_req = [15] * 6
gold, eco = run(BEFORE, all_req), run(AFTER, all_req)
assert gold[0] == (3, 0) and eco[0] == (0, 1), (gold[0], eco[0]) # the first grants differ: the intended difference
assert gold[0][1] != eco[0][1]
assert all(g[0] != e[0] for g, e in zip(gold, eco)), "the pointers differ in every cycle with all requests held"
print("PASS: the model reproduces the intended difference at the first cycle")The intended difference, exhibited by the block above and read against the change note.
A scoped claim, written by you and proved, that is not full equivalence: say under what condition the revisions must still agree, and prove it on both together.
Each revision still meets its own properties.
A failing partner for the scoped claim: a changed revision that touched more than the reset, which the claim must catch, with the failing step.
A cover that shows the claim's condition can hold while a request is present, and a statement, with your model's help, of the stimuli under which the revisions meet again and those under which they never do.
Rows: eco-intended-difference, eco-outside-the-change, the cover.
The miter fails at the first all-request cycle, matching the note.
Your scoped claim is proved at the window you report, and your partner makes it fail.
The rows pass the engine, with the counterexample row killing the change itself as a registered mutant.
# ---- formal lab results ledger, engine v2: every row cites a typed run (kind, depth, outcome[, design]) ----
STATUS = ("proven", "bounded", "cex", "cover-reached", "inconclusive")
FROM_RUN = {"proven": {("prove", "proved")},
"bounded": {("bmc", "bounded")},
"cex": {("bmc", "counterexample"), ("prove", "counterexample")},
"cover-reached": {("cover", "reached")},
"inconclusive": {("prove", "unproven"), ("cover", "not-reached")}}
NEED = {"sync_fifo": 9, "rr_arbiter": 5, "hs_bridge": 4, "csr_block": 3,
"pipe3": 5, "pipe3_eq": 5, "mod10_counter": 15, "toggle_demo": 4}
KEYS = ("property", "design", "status", "bound", "why", "run", "assumes", "cover", "kills", "rev")
REV = 3
ALWAYS = "reset-at-step-0"
TRACKED = "tracked-constant-stable"
def row_problems(e, runs, tracked):
n = e.get("property", "?")
miss = [k for k in KEYS if k not in e]
if miss:
return ["missing-field:%s:%s" % (n, ",".join(miss))]
if e["status"] not in STATUS:
return ["bad-status:" + n]
p = []
if e["rev"] != REV:
p.append("stale:" + n)
if e["run"] not in runs:
return p + ["no-such-run:" + n]
kind, depth, outcome = runs[e["run"]][:3]
if len(runs[e["run"]]) > 3 and runs[e["run"]][3] != e["design"]:
p.append("run-of-another-design:" + n) # a run typed with its design may be cited only by that design's rows
if (kind, outcome) not in FROM_RUN[e["status"]]:
p.append("status-not-from-run:" + n)
if e["bound"] != depth:
p.append("bound-not-run-depth:" + n)
has_cover = bool(str(e["cover"]).strip())
if e["status"] in ("proven", "bounded") and not (has_cover and e["kills"]):
p.append("no-evidence:" + n)
if e["status"] == "cover-reached" and not has_cover:
p.append("no-evidence:" + n)
if e["status"] == "cex" and not e["kills"]:
p.append("no-evidence:" + n)
if e["status"] == "bounded":
if e["design"] not in NEED:
p.append("unknown-design:" + n)
elif depth < NEED[e["design"]]:
p.append("short-bound:" + n)
if len(str(e["why"]).strip()) < 12:
p.append("unjustified:" + n)
if ALWAYS not in e["assumes"]:
p.append("hidden-assume:%s:%s" % (n, ALWAYS))
if n in tracked and TRACKED not in e["assumes"]:
p.append("hidden-assume:%s:%s" % (n, TRACKED))
return p
def ledger_ok(ledger, runs, required, mutants, register, tracked, final=True):
names = [e.get("property") for e in ledger]
bad = ["duplicate:" + n for n in sorted({n for n in names if names.count(n) > 1})]
bad += ["missing-row:" + r for r in sorted(set(required) - set(names))]
bad += [q for e in ledger for q in row_problems(e, runs, tracked)]
good = [e for e in ledger if not row_problems(e, runs, tracked)] # only a row without complaints counts as evidence
solid = {e["property"] for e in good if e["status"] in ("proven", "cover-reached")}
for a, rows in sorted(register.items()):
if rows is None:
if final:
bad.append("deferred-assume:" + a) # a stage may defer a discharge; a final package may not
elif not (rows and all(r in solid for r in rows)):
bad.append("open-assume:" + a)
bad += ["unregistered-assume:%s:%s" % (e.get("property"), a) for e in ledger
for a in e.get("assumes", []) if a not in register]
killed = {m for e in good if e["status"] == "cex" for m in e["kills"]}
bad += ["survivor:" + m for m in sorted(set(mutants) - killed)]
bad += ["unsupported-kill:%s:%s" % (e.get("property"), m) for e in ledger
if e.get("status") in ("proven", "bounded") for m in e.get("kills", []) if m not in killed]
return bad
def mutation_score(ledger, mutants):
assert mutants, "no mutants registered"
killed = {m for e in ledger if e.get("status") == "cex" for m in e.get("kills", [])}
return len(killed & set(mutants)) / len(mutants)
RUNS = {
"eco-miter": ("bmc", 2, "counterexample"),
}
REQUIRED = ["eco-intended-difference", "eco-outside-the-change", "eco-scope-cover"]
MUTANTS = ["eco-delta", "eco-scope-leak"]
REGISTER = {"reset-at-step-0": None} # discharged by the pair rows of stage 2
YOUR_ROWS = [] # fill from your own runs
bad = ledger_ok(YOUR_ROWS, RUNS, REQUIRED, MUTANTS, REGISTER, set(), final=False)
if YOUR_ROWS:
assert bad == [], bad
print("PASS: stage 3 change package consistent")
else:
expected = ["missing-row:" + r for r in REQUIRED] + ["survivor:" + m for m in MUTANTS]
assert sorted(bad) == sorted(expected), bad
print("PASS: the empty package is rejected with %d complaints" % len(bad))Hint 1: the only textual difference between the revisions is one line, so drive the case where that line still decides.
Hint 2: after the first grant, ask what the two pointers hold and whether they can ever hold the same value.
Hint 3: when the pointers are equal, the rest of the two revisions is identical text; the condition of your claim writes itself.
Hint 4: for the partner, change a second thing in the revised copy and check the claim notices it.
Compare the revisions textually before running anything: the miter should surprise you nowhere. Confirm that the exhibited mismatch matches the change note bit for bit; a mismatch anywhere else voids the scope. Rerun each revision's own properties after the change, not only the miter.
The revisions intentionally differ after reset, so full equivalence is false. The true claim is scoped to the condition you wrote; filing full equivalence would fail honestly.
That is exactly where the changed reset value still decides: the difference appears at the documented point and nowhere else is claimed.