A forty-cycle counterexample with every input wiggling tells the designer nothing; a six-cycle replay with one relevant beat tells them exactly which word was lost. Minimisation turns the solver's witness into a human story, and replay turns it into a shared one: the same stimulus, run in simulation, shows the failure in the environment the team already trusts.
Job of this lesson: minimise a trace without losing the violation, and replay it as a stimulus table that a simulation actually ran.
Minimisation clears inputs cycle by cycle and keeps each clearing only if the violation survives; engine minimisation does this internally, manual clearing does it where the team can watch. Cycles that become idle are then dropped, except reset cycles, which are part of the story. Replay applies the counterexample inputs as deterministic stimulus on the same module, with no randomness and clock edges on exact multiples of the sampling slot, so every lane is a real simulation result. The course's own counterexample figures are produced exactly this way: replay, not drawing.
Step | What you do | Kept only if |
|---|---|---|
Clear irrelevant inputs | Set each input to its idle value in turn | The same violation still fires |
Drop idle cycles | Remove cycles that are now idle, never the reset cycle | The same violation still fires |
Replay | Drive the shortened trace in simulation on the good and the buggy design | The buggy design visibly violates the property and the good one does not |
The overflow bug in the 4-entry FIFO needs a full FIFO and one more push. The script models the FIFO's occupancy, so a push into a full FIFO is the violation, and starts from a noisy trace: a reset cycle, an idle cycle, a push and pop together, scattered pushes, and the fatal ones. The minimiser clears each push and pop in turn, keeping the clearing only while the overflow survives, then drops the idle cycles. Four tests can fail: the minimiser must shorten the trace and change it, five pushes and no pop must remain, no further push can be cleared, and an over-eager clearing of the fatal push must lose the violation:
DEPTH = 4
def overflows(trace):
n = 0
for c in trace:
if c["rst"]:
n = 0
continue
if c["push"] and n == DEPTH:
return True
n += (1 if c["push"] and n < DEPTH else 0) - (1 if c["pop"] and n > 0 else 0)
return False
def cycle(rst=0, push=0, pop=0):
return {"rst": rst, "push": push, "pop": pop}
noise = [cycle(rst=1), cycle(), cycle(push=1), cycle(push=1, pop=1), cycle(push=1), cycle(),
cycle(push=1), cycle(push=1), cycle(push=1), cycle(push=1)]
assert overflows(noise)
def minimise(trace, violates):
t = [dict(c) for c in trace]
for c in t:
for k in ("push", "pop"):
old = c[k]
c[k] = 0
if not violates(t):
c[k] = old
return [c for c in t if c["rst"] or c["push"] or c["pop"]]
short = minimise(noise, overflows)
assert overflows(short)
assert len(short) < len(noise) and short != noise # something was removed
assert sum(c["push"] for c in short) == DEPTH + 1 # four to fill, one fatal
assert sum(c["pop"] for c in short) == 0
assert short[0]["rst"] == 1 # the reset cycle stays
for i, c in enumerate(short): # 1-minimal: no push can go
if c["push"]:
fewer = [dict(x) for x in short]
fewer[i]["push"] = 0
assert not overflows(fewer)
print("PASS: noise of", len(noise), "cycles reduced to", len(short), "; the five fatal pushes remain")The replay is a runnable simulation block. It drives the minimised stimulus, a reset cycle and five pushes with illustrative data values A1 to A5, on the good FIFO and on the buggy one at the same time. It passes only if the buggy count reaches 5 while the good one stops at 4, and the rows it prints are the table below. The same stimulus is the regression after the fix: formal step number is cycle number minus one.
module sync_fifo #(parameter BUG = 0, parameter HELPER = 1) (
input wire clk,
input wire rst,
input wire push,
input wire [7:0] wdata,
input wire pop,
output wire [7:0] rdata,
output wire full,
output wire empty,
output reg [2:0] count
);
reg [7:0] mem [0:3];
reg [1:0] wptr, rptr;
assign full = (BUG == 3) ? (count >= 3'd3) : (count == 3'd4);
assign empty = (count == 3'd0);
assign rdata = mem[rptr];
wire do_push = push && (!full || BUG == 1);
wire do_pop = pop && (!empty || BUG == 2);
always @(posedge clk) begin
if (rst) begin
wptr <= 2'd0;
rptr <= 2'd0;
count <= 3'd0;
end else begin
if (do_push) begin
mem[wptr] <= (BUG == 5) ? {1'b0, wdata[6:0]} : wdata;
wptr <= wptr + 2'd1;
end
if (do_pop) rptr <= rptr + 2'd1;
if (BUG == 4 && do_push && do_pop) count <= count + 3'd1;
else count <= count + {2'b0, do_push} - {2'b0, do_pop};
end
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(*) if (!init) begin
a_range: assert (count <= 3'd4);
a_flags: assert (full == (count == 3'd4) && empty == (count == 3'd0));
a_not_both: assert (!(full && empty));
a_ptr: assert (count[1:0] == (wptr - rptr));
end
always @(posedge clk) if (!init && !$past(rst)) begin
a_push_inc: assert (!($past(push) && !$past(pop) && !$past(full)) || count == $past(count) + 3'd1);
a_pop_dec: assert (!($past(pop) && !$past(push) && !$past(empty)) || count == $past(count) - 3'd1);
a_ovf_ign: assert (!($past(push) && !$past(pop) && $past(count) == 3'd4) || count == $past(count));
a_both: assert (!($past(push) && $past(pop) && !$past(full) && !$past(empty)) || count == $past(count));
end
(* anyconst *) wire [1:0] tslot;
reg [1:0] tslot_q;
always @(posedge clk) tslot_q <= tslot;
always @(*) if (!init) assume (tslot == tslot_q);
reg tv;
reg [7:0] td;
always @(posedge clk) begin
if (rst) tv <= 1'b0;
else begin
if (do_push && wptr == tslot) begin tv <= 1'b1; td <= wdata; end
else if (do_pop && rptr == tslot) tv <= 1'b0;
end
end
always @(*) if (!init && tv && !empty && rptr == tslot) a_data: assert (rdata == td);
generate if (HELPER) begin : g_helper
always @(*) if (!init && tv) a_tracked: assert (mem[tslot] == td);
end endgenerate
always @(*) if (!init) begin
c_full: cover (count == 3'd4);
c_empty_after_use: cover (empty && tv == 1'b0 && wptr == 2'd2);
end
always @(posedge clk) if (!init) c_both: cover (push && pop && !full && !empty);
`endif
endmoduleCycle | push | wdata (illustrative) | count, buggy FIFO | count, good FIFO | Note |
|---|---|---|---|---|---|
1 | 0 | - | 0 | 0 | Reset cycle |
2 | 1 | A1 | 1 | 1 | Fill |
3 | 1 | A2 | 2 | 2 | Fill |
4 | 1 | A3 | 3 | 3 | Fill |
5 | 1 | A4 | 4 | 4 | Full |
6 | 1 | A5 | 5 | 4 | Buggy FIFO accepts the push into a full FIFO: count 5, the oldest word is lost. The good FIFO ignores it |
How to read it: each row is one cycle of deterministic stimulus, and the count columns are the registers after that cycle's edge, read from the simulation. The last row is the violation: the property limiting the count to 4 fails on the buggy FIFO only. Anyone rerunning the block sees the same numbers.
Every reported counterexample is minimised: idle cycles and irrelevant inputs are gone, the reset cycle is kept.
The replay is deterministic stimulus on the same module, run on the good and the buggy design, not a redrawn sketch.
The replayed simulation visibly violates exactly the property the text names.
After clearing, confirm the same property fails at the same condition, not merely that something fails: a minimiser that changes which property breaks has rewritten the story. Keep the original trace next to the short one until the fix is proven; if the fix clears the short trace but not the original, the clearing went too far.
No: it changed the story. Restore the input and clear only what keeps the same property failing at the same condition.
Determinism: the same table must show the same lanes on every run, or the replay proves nothing and cannot serve as a regression.