The lab ends but the block does not: parameters change, twins multiply and new properties arrive with every change. These ten extensions rehearse that, one obligation each, with the expected outcome stated up front. File each as a ledger row before starting the next; the self-check cites the runs and refuses a silent pass.
Goal: ten new rows in your own ledger copy. Inputs: the six designs, the engine and the Solutions topic. Steps: attempt each exercise, run its proof, compare against the stated outcome category, file the row, run the self-check.
Every extension is one of three moves: a deeper fault that punishes a short bound, a mutant that gives a property a failure of its own, or a changed twin that replays an old argument in a new shape. The expected outcome names the category, proven, counterexample with its step, or inconclusive, never a verdict word alone.
# | Exercise | Expected outcome |
|---|---|---|
1 | FIFO: file the pair for the push-when-full variant, a pass at depth 6 and a kill at depth 7. | Counterexample at step 6 (depth 7); the pass at depth 6 is bounded and refused as evidence. |
2 | FIFO: run the three lesson-local mutants and report each killer and smallest depth. | Counterexamples at depths 2, 6 and 7, each by the named property. |
3 | Arbiter: replay the starvation variant with the helper assertions off, at depths 5 and 6. | Pass at depth 5, counterexample at depth 6 (step 5). |
4 | Bridge: replay the value-corrupting variant, once with the counting properties alone and once with the data properties. | Counting set: bounded pass to depth 14. Full set: counterexample at depth 4. |
5 | Counter: find the smallest window of the full set. | Window 1 inconclusive, window 2 proven. |
6 | Pipeline: build a second twin whose first stage adds its operands in the other order, and miter it, with and without the planted twin variant. | Proven at depth 5 (addition commutes); counterexample at depth 5 with the variant. |
7 | Registers: replay the mutant in which a clear beats a set, and read the failing property. | Counterexample at depth 4 by the hardware-set property. |
8 | Chain: swap the two valid sources and find the smallest failing depth. | Counterexample at depth 2 through the row for mode 1. |
9 | Counter: file the pair for the late-pulse variant, a pass at depth 10 and a kill at depth 11. | Counterexample at step 10 (depth 11); depth 10 is bounded and refused as evidence. |
10 | ECO: replay the partner that changed more than the reset, with the work properties dropped. | Counterexample at depth 3 by the scoped claim. |
Exercise 6 needs a listing. The block below is the miter of the stage with the twin's first stage reading b + a where the reference reads a + b. It is proved at depth 5; the same listing with the planted twin variant selected gives the counterexample, shown by the next block.
// formal: prove 5 expect pass slang top pipe3_eq
`define FORMAL
// pipe3: three-stage arithmetic pipeline, y = ((a + b)[3:0] * c[3:0]) + 1 (8 bits). Registers: stage 1
// {s = a + b, c1 = c[3:0]}, stage 2 {p = s[3:0] * c1}, stage 3 {y = p + 1}. Latency 3 cycles. Synchronous
// active-high reset clears every register. Only a[3:0], b[3:0], c[3:0] influence y.
// pipe3_retimed: the same function and latency with the registers moved across the multiplier: stage 2
// {s2 = s[3:0], c2 = c1}, stage 3 {y = s2 * c2 + 1}. BUG selects a variant of the twin.
// pipe3_eq: a miter of pipe3 against pipe3_retimed with common inputs and reset; BUG goes to the twin.
module pipe3 #(parameter CHECK = 1) (
input wire clk,
input wire rst,
input wire [7:0] a,
input wire [7:0] b,
input wire [7:0] c,
output reg [7:0] y,
output wire [7:0] dbg_p // stage-2 register, exposed for the miter's helper assertion
);
reg [7:0] s;
reg [3:0] c1;
reg [7:0] p;
assign dbg_p = p;
always @(posedge clk) begin
if (rst) begin s <= 8'd0; c1 <= 4'd0; p <= 8'd0; y <= 8'd0; end
else begin
s <= a + b;
c1 <= c[3:0];
p <= s[3:0] * c1;
y <= p + 8'd1;
end
end
`ifdef FORMAL
// CHECK=0 switches the properties off (used when pipe3 sits inside the miter)
generate if (CHECK) begin : g_chk
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// hist counts clean cycles since reset (saturates at 3): y is only specified after 3
reg [1:0] hist;
always @(posedge clk) begin
if (rst) hist <= 2'd0;
else if (hist != 2'd3) hist <= hist + 2'd1;
end
// input history as plain registers
reg [3:0] sa1, sb1, sc1, sa2, sb2, sc2, sa3, sb3, sc3;
always @(posedge clk) begin
sa1 <= a[3:0]; sb1 <= b[3:0]; sc1 <= c[3:0];
sa2 <= sa1; sb2 <= sb1; sc2 <= sc1;
sa3 <= sa2; sb3 <= sb2; sc3 <= sc2;
end
wire [3:0] sum3 = sa3 + sb3; // low 4 bits of a + b three cycles ago
// functional property with latency 3, checked only after 3 clean cycles
always @(*) if (!init && hist == 2'd3) a_latency3: assert (y == (sum3 * sc3) + 8'd1);
// the cycle after a reset the output register is 0
always @(posedge clk) if (!init && $past(rst)) a_reset_zero: assert (y == 8'd0);
always @(*) if (!init) c_y_nonzero: cover (hist == 2'd3 && y == 8'd7);
end endgenerate
`endif
endmodule
module pipe3_retimed #(parameter BUG = 0) (
input wire clk,
input wire rst,
input wire [7:0] a,
input wire [7:0] b,
input wire [7:0] c,
output reg [7:0] y,
output wire [3:0] dbg_s2, // stage-2 registers, exposed for the miter's helper assertion
output wire [3:0] dbg_c2
);
reg [7:0] s;
reg [3:0] c1;
reg [3:0] s2, c2;
assign dbg_s2 = s2;
assign dbg_c2 = c2;
always @(posedge clk) begin
if (rst) begin s <= 8'd0; c1 <= 4'd0; s2 <= 4'd0; c2 <= 4'd0; y <= 8'd0; end
else begin
s <= b + a;
c1 <= c[3:0];
s2 <= s[3:0];
c2 <= c1;
y <= s2 * ((BUG == 1) ? {1'b0, c2[2:0]} : c2) + 8'd1;
end
end
endmodule
module pipe3_eq #(parameter BUG = 0, parameter HELPER = 1) (
input wire clk,
input wire rst,
input wire [7:0] a,
input wire [7:0] b,
input wire [7:0] c,
output wire same
);
wire [7:0] y1, y2, p_ref;
wire [3:0] s2_ret, c2_ret;
pipe3 #(.CHECK(0)) u_ref (.clk(clk), .rst(rst), .a(a), .b(b), .c(c), .y(y1), .dbg_p(p_ref));
pipe3_retimed #(.BUG(BUG)) u_ret (.clk(clk), .rst(rst), .a(a), .b(b), .c(c), .y(y2), .dbg_s2(s2_ret), .dbg_c2(c2_ret));
assign same = (y1 == y2);
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(*) if (!init) a_equiv: assert (same);
// helper assertion across the moved register cut: the reference's stage-2 register equals the
// twin's stage-2 registers multiplied
generate if (HELPER) begin : g_helper
always @(*) if (!init) h_cut: assert (p_ref == s2_ret * c2_ret);
end endgenerate
always @(*) if (!init) c_nonzero: cover (y1 == 8'd7 && y2 == 8'd7);
`endif
endmodule// formal: bmc 5 expect fail slang top pipe3_eq define BUG=1
`define FORMAL
// pipe3: three-stage arithmetic pipeline, y = ((a + b)[3:0] * c[3:0]) + 1 (8 bits). Registers: stage 1
// {s = a + b, c1 = c[3:0]}, stage 2 {p = s[3:0] * c1}, stage 3 {y = p + 1}. Latency 3 cycles. Synchronous
// active-high reset clears every register. Only a[3:0], b[3:0], c[3:0] influence y.
// pipe3_retimed: the same function and latency with the registers moved across the multiplier: stage 2
// {s2 = s[3:0], c2 = c1}, stage 3 {y = s2 * c2 + 1}. BUG selects a variant of the twin.
// pipe3_eq: a miter of pipe3 against pipe3_retimed with common inputs and reset; BUG goes to the twin.
module pipe3 #(parameter CHECK = 1) (
input wire clk,
input wire rst,
input wire [7:0] a,
input wire [7:0] b,
input wire [7:0] c,
output reg [7:0] y,
output wire [7:0] dbg_p // stage-2 register, exposed for the miter's helper assertion
);
reg [7:0] s;
reg [3:0] c1;
reg [7:0] p;
assign dbg_p = p;
always @(posedge clk) begin
if (rst) begin s <= 8'd0; c1 <= 4'd0; p <= 8'd0; y <= 8'd0; end
else begin
s <= a + b;
c1 <= c[3:0];
p <= s[3:0] * c1;
y <= p + 8'd1;
end
end
`ifdef FORMAL
// CHECK=0 switches the properties off (used when pipe3 sits inside the miter)
generate if (CHECK) begin : g_chk
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// hist counts clean cycles since reset (saturates at 3): y is only specified after 3
reg [1:0] hist;
always @(posedge clk) begin
if (rst) hist <= 2'd0;
else if (hist != 2'd3) hist <= hist + 2'd1;
end
// input history as plain registers
reg [3:0] sa1, sb1, sc1, sa2, sb2, sc2, sa3, sb3, sc3;
always @(posedge clk) begin
sa1 <= a[3:0]; sb1 <= b[3:0]; sc1 <= c[3:0];
sa2 <= sa1; sb2 <= sb1; sc2 <= sc1;
sa3 <= sa2; sb3 <= sb2; sc3 <= sc2;
end
wire [3:0] sum3 = sa3 + sb3; // low 4 bits of a + b three cycles ago
// functional property with latency 3, checked only after 3 clean cycles
always @(*) if (!init && hist == 2'd3) a_latency3: assert (y == (sum3 * sc3) + 8'd1);
// the cycle after a reset the output register is 0
always @(posedge clk) if (!init && $past(rst)) a_reset_zero: assert (y == 8'd0);
always @(*) if (!init) c_y_nonzero: cover (hist == 2'd3 && y == 8'd7);
end endgenerate
`endif
endmodule
module pipe3_retimed #(parameter BUG = 0) (
input wire clk,
input wire rst,
input wire [7:0] a,
input wire [7:0] b,
input wire [7:0] c,
output reg [7:0] y,
output wire [3:0] dbg_s2, // stage-2 registers, exposed for the miter's helper assertion
output wire [3:0] dbg_c2
);
reg [7:0] s;
reg [3:0] c1;
reg [3:0] s2, c2;
assign dbg_s2 = s2;
assign dbg_c2 = c2;
always @(posedge clk) begin
if (rst) begin s <= 8'd0; c1 <= 4'd0; s2 <= 4'd0; c2 <= 4'd0; y <= 8'd0; end
else begin
s <= b + a;
c1 <= c[3:0];
s2 <= s[3:0];
c2 <= c1;
y <= s2 * ((BUG == 1) ? {1'b0, c2[2:0]} : c2) + 8'd1;
end
end
endmodule
module pipe3_eq #(parameter BUG = 0, parameter HELPER = 1) (
input wire clk,
input wire rst,
input wire [7:0] a,
input wire [7:0] b,
input wire [7:0] c,
output wire same
);
wire [7:0] y1, y2, p_ref;
wire [3:0] s2_ret, c2_ret;
pipe3 #(.CHECK(0)) u_ref (.clk(clk), .rst(rst), .a(a), .b(b), .c(c), .y(y1), .dbg_p(p_ref));
pipe3_retimed #(.BUG(BUG)) u_ret (.clk(clk), .rst(rst), .a(a), .b(b), .c(c), .y(y2), .dbg_s2(s2_ret), .dbg_c2(c2_ret));
assign same = (y1 == y2);
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(*) if (!init) a_equiv: assert (same);
// helper assertion across the moved register cut: the reference's stage-2 register equals the
// twin's stage-2 registers multiplied
generate if (HELPER) begin : g_helper
always @(*) if (!init) h_cut: assert (p_ref == s2_ret * c2_ret);
end endgenerate
always @(*) if (!init) c_nonzero: cover (y1 == 8'd7 && y2 == 8'd7);
`endif
endmoduleEach exercise becomes one row citing the run you made. The self-check files the ten rows against the run table and shows two shortcuts refused: a bounded pass offered as the evidence of a kill, and a bound that is not the depth of its run.
# ---- 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 = {
"fifo-w1": ("bmc", 7, "counterexample"),
"fifo-m-push-inc": ("bmc", 6, "counterexample"),
"arb-w1-nohelp": ("bmc", 6, "counterexample"),
"bridge-w3": ("bmc", 4, "counterexample"),
"ctr-k1": ("prove", 1, "unproven"),
"ctr-k2": ("prove", 2, "proved"),
"ex-twin-swap": ("prove", 5, "proved"),
"ex-twin-swap-bug": ("bmc", 5, "counterexample"),
"csr-m-race": ("bmc", 4, "counterexample"),
"chain-w2": ("bmc", 2, "counterexample"),
"ctr-w1": ("bmc", 11, "counterexample"),
"eco-leak": ("bmc", 3, "counterexample"),
"fifo-w1-short": ("bmc", 6, "bounded"),
}
A0 = ["reset-at-step-0"]
def R(property, design, status, bound, run, why="", cover="", kills=()):
return dict(property=property, design=design, status=status, bound=bound, run=run, why=why, cover=cover,
kills=list(kills), assumes=list(A0), rev=3)
ROWS = [
R("ex1-fifo-push-when-full", "sync_fifo", "cex", 7, "fifo-w1", kills=["fifo-W1"]),
R("ex2-fifo-push-inc-mutant", "sync_fifo", "cex", 6, "fifo-m-push-inc", kills=["fifo-m-push-inc"]),
R("ex3-arbiter-starvation-nohelper", "rr_arbiter", "cex", 6, "arb-w1-nohelp", kills=["arb-W1"]),
R("ex4-bridge-corruption", "hs_bridge", "cex", 4, "bridge-w3", kills=["bridge-W3"]),
R("ex5a-counter-window-1", "mod10_counter", "inconclusive", 1, "ctr-k1"),
R("ex5b-counter-window-2", "mod10_counter", "proven", 2, "ctr-k2", cover="c_wrap step 14", kills=["ctr-W1"]),
R("ex6a-second-twin", "pipe3_eq", "proven", 5, "ex-twin-swap", cover="c_nonzero step 4", kills=["ex-twin-swap-bug"]),
R("ex6b-second-twin-variant", "pipe3_eq", "cex", 5, "ex-twin-swap-bug", kills=["ex-twin-swap-bug"]),
R("ex7-csr-race-mutant", "csr_block", "cex", 4, "csr-m-race", kills=["csr-m-race"]),
R("ex8-chain-valid-swap", "sync_fifo", "cex", 2, "chain-w2", kills=["chain-swap-valid"]),
R("ex9-counter-late-pulse", "mod10_counter", "cex", 11, "ctr-w1", kills=["ctr-W1"]),
R("ex10-eco-partner", "rr_arbiter", "cex", 3, "eco-leak", kills=["eco-scope-leak"]),
]
MUTANTS = ["fifo-W1", "fifo-m-push-inc", "arb-W1", "bridge-W3", "ctr-W1", "ex-twin-swap-bug", "csr-m-race", "chain-swap-valid", "eco-scope-leak"]
REGISTER = {"reset-at-step-0": None}
def check(rows):
return ledger_ok(rows, RUNS, [r["property"] for r in ROWS], MUTANTS, REGISTER, set(), final=False)
assert check(ROWS) == [], check(ROWS)
shallow = [dict(r, run="fifo-w1-short", bound=6) if r["property"].startswith("ex1") else r for r in ROWS]
assert "status-not-from-run:ex1-fifo-push-when-full" in check(shallow), "a bounded pass is not the evidence of a kill"
assert "survivor:fifo-W1" in check(shallow)
off = [dict(r, bound=r["bound"] + 1) if r["property"].startswith("ex9") else r for r in ROWS]
assert "bound-not-run-depth:ex9-counter-late-pulse" in check(off)
print("PASS: ten extensions filed against their runs; a bounded pass and a wrong bound are refused")An exercise whose outcome differs from the table is a finding, not a grading error: rerun the proof, check the bound against the cover steps, and update the row, never the expectation, until you understand the gap. A self-check failure on the clean set means the engine or a row is malformed: fix that before attempting more exercises.
Do the ten in order: each reuses the habit of the one before, and the pair exercises 1 and 9 share one discipline: a pass one depth short of the fault is filed beside the counterexample, never alone. Keep the failing step beside every counterexample row; a kill that arrives later than the table says means the mutant or the set changed shape.
Because a counterexample is one of the three outcomes: a recorded and read counterexample with its step is evidence, and its row carries the depth that future proofs must exceed.
A bound that is not the depth of its run, or a kill claimed for a variant that no counterexample row shows. The engine refuses both.