Proving a Bug Fix Changed Only the Bug

Check a late fix as "equal to the old design outside the bug, correct inside it", and see why the condition comes from the bug report.

Lesson: F6.4
Time: 20 min
Runs on: SymbiYosys
Check: 5 questions

A memory controller addressed WRAP bursts like INCR, and the fix passed every test, including new WRAP tests. Weeks later an unaligned INCR burst read the wrong word. The fix had applied the wrap window to INCR too. "Did the fix change anything except WRAP?" has a formal answer that needs no test.

start	len	size	burst	n	addr_old	addr_new
0x66FFFC39	1	0	INCR	1	0x66FFFC3A	0x66FFFC38

The bad fix's counterexample. Beat 1 of this INCR burst should be 0x66FFFC3A; the bad fix sends it back to 0x66FFFC38.

Equal Outside the Condition, Correct Inside It

The Miter with a Condition on the CompareOld design (with the bug) and new design (with the fix) on shared burst inputs. Outside the bug's condition they must agree; inside it, the new one must meet the spec.

Read the diagram as text

Shared inputs: start, len, size, burst, n
axi_addr, FIX 0: WRAP addressed like INCR
axi_addr, the fix: WRAP returns to its window
burst != WRAP: addr_new == addr_old: the fix changed nothing else
burst == WRAP: inside the window: the fix does what the spec says

Shared inputs → axi_addr, FIX 0
Shared inputs → axi_addr, the fix
axi_addr, FIX 0 → burst != WRAP: addr_new == addr_old
axi_addr, the fix → burst != WRAP: addr_new == addr_old
axi_addr, the fix → burst == WRAP: inside the window

Both are assertions on one bench. A fix that passes both changed exactly the behaviour it meant to.

Conditional equivalence compares two designs only where they are meant to agree. Where the bug lives, the new design is checked against the specification instead.

The address function is the one behind P2.6: transfer n of a burst, given its start, length, size and type. Here it is a module with a switch for each version.

Every Point at Once

The Input Space, Split by the Bug ReportEvery combination of start, len, size, burst and n is a point. Tests are a few points; the conditional miter covers every point.

Read the diagram as text

burst == WRAP: allowed to differ; must stay in the window
FIXED and INCR: must agree with the old design
The bad fix's point: INCR at 0x66FFFC39, beat 1
A test suite: a handful of chosen points

The bad fix's point → FIXED and INCR: lies in

The bad fix moved a point in the "must agree" region. No WRAP test can find it.

The two rules in concurrent SVA.

assert property (@(posedge clk) burst != WRAP |-> new_.addr == old_.addr);
assert property (@(posedge clk) burst == WRAP && n > 0 |->
  new_.addr >= boundary && new_.addr < boundary + window);

What the engine runs. The window and its start are modelling code (F3.6) written from the AXI spec, in 33 bits.

  // modelling code: the WRAP window as the spec defines it, in 33 bits so the top of memory cannot overflow
  wire [32:0] f_window = ({29'd0, len} + 33'd1) << size;
  wire [32:0] f_boundary = ({1'b0, start} / f_window) * f_window;
  always @(posedge clk) begin
    assume(size <= 3'd2);                 // a 32-bit bus
    assume(burst != 2'd3);                // reserved encoding
    assume(n <= len);                     // a beat of this burst
    if (burst == WRAP) assume(len == 4'd1 || len == 4'd3 || len == 4'd7 || len == 4'd15);
    if (burst == WRAP) assume((start & ((32'd1 << size) - 32'd1)) == 32'd0);
    if (burst != WRAP) assert(addr_new == addr_old);
    if (burst == WRAP && n != 4'd0) assert({1'b0, addr_new} >= f_boundary && {1'b0, addr_new} < f_boundary + f_window);
  end

Write the condition from the bug report: "WRAP bursts are addressed like INCR". A condition read off the diff describes what was changed, and what was changed is exactly what is under test.

Three Fixes, Three Verdicts

Fix under test	prove, k = 2	Which assertion
The fix, comparison `a - boundary >= window`	Prove PASS (k = 2)	both hold
Bad fix: the window applied to every burst but FIXED	FAIL at reported step 1	the equality
The fix as the P2 function writes it: `a >= boundary + window`	FAIL at reported step 1	the WRAP rule
The same, equality only	Prove PASS (k = 2)	the equality holds

Measured with the site's runner, smtbmc yices. The design has no flops, so every check is a single step.

The bad fix fails the equality on an INCR burst, the point in the hook. The fix as the P2 function writes it passes the equality and fails the WRAP rule:

start	len	size	burst	n	addr_old	addr_new
0xFFFFFFF4	15	2	WRAP	2	0xFFFFFFFC	0xFFFFFFBC

A WRAP burst in the last 64 bytes of the 32-bit space. The window's end is 2^32, which a 32-bit sum writes as 0.

The comparison a >= boundary + window overflows there, so the burst leaves its window. The P2 memory previously had the same corner; it now uses the offset comparison below, with a regression at the top of the address space. Comparing a - boundary with the window cannot overflow, and that version proves.

The Assumptions It Needs

start	len	size	burst	n	addr_old	addr_new
0x001FFF9C	14	2	WRAP	6	0x001FFFB4	0x001FFFB4

Without the WRAP-length assumption: FAIL at reported step 1 on the WRAP rule. A 15-beat WRAP is illegal, and its window is no power of two.

AXI allows WRAP lengths of 2, 4, 8 and 16 transfers only (IHI 0022L A3.1.2). Drop that assumption and the solver finds an illegal burst at once: a missing assumption, read as in F3.3. The alignment assumption turns out unnecessary here: Prove PASS (k = 2) without it, because every beat after the first is aligned by construction.

Asked in Interviews

Question	Answer
How do you prove a bug fix changed only what you meant?	A miter of old and new: the equality asserted wherever the bug's condition is false, the spec asserted where it is true, both proven.
Where does the condition come from?	The bug report. A condition taken from the diff only restates the change.
What else is this used for?	Any ECO on a frozen design, and RTL-to-RTL equivalence in general.

Try It

The address function with its four versions. FIX 0 is the old design.

module axi_addr #(parameter FIX = 3)(input [31:0] start, input [3:0] len,
  input [2:0] size, input [1:0] burst, input [3:0] n, output [31:0] addr);
  localparam FIXED = 2'd0, INCR = 2'd1, WRAP = 2'd2;
  wire [31:0] nb = 32'd1 << size;                  // bytes per transfer
  wire [31:0] aligned = start & ~(nb - 32'd1);      // start aligned down to the transfer size
  wire [31:0] window = ({28'd0, len} + 32'd1) << size;   // bytes in the whole burst
  wire [31:0] boundary = start & ~(window - 32'd1); // the wrap boundary (window is a power of two for WRAP)
  wire [31:0] a = aligned + ({28'd0, n} << size);
  wire wraps = FIX == 0 ? 1'b0 : FIX == 2 ? burst != FIXED : burst == WRAP;
  wire past_end = FIX == 1 ? a >= boundary + window : a - boundary >= window;
  assign addr = (burst == FIXED || n == 4'd0) ? start : (wraps && past_end) ? a - window : a;
endmodule

The task.

[options]
mode prove
depth 2
[engines]
smtbmc yices
[script]
read_verilog -formal -sv design.sv
prep -top eco_top
[files]
design.sv

Run the bad fix
As loaded (FIX(2)): FAIL at reported step 1. Which burst type and which beat?
Apply the fix
Set the new instance to FIX(3): Prove PASS (k = 2).
Try the P2 comparison
Set it to FIX(1): FAIL at reported step 1. Find the start address in the trace.
Write a condition
A new bug report: "a FIXED burst repeats the aligned address instead of the start". Write the condition for the equality, and say which region of the plane it leaves free.

Top moduleModeDepthEngine

design.sv

props.sv

Use assert property (@(posedge clk) ...);. Leave blank for immediate assertions in the design.

Inputs are free unless constrained. Run to find a counterexample or check a proof.

Model: one positive-edge clock, binary data. Sampled history requires declaration-initialized variables; primary-input history is unsupported.

SBY summary and log

Enable JavaScript to edit and run. The original design and properties follow.

module axi_addr #(parameter FIX = 3)(input [31:0] start, input [3:0] len,
  input [2:0] size, input [1:0] burst, input [3:0] n, output [31:0] addr);
  localparam FIXED = 2'd0, INCR = 2'd1, WRAP = 2'd2;
  wire [31:0] nb = 32'd1 << size;                  // bytes per transfer
  wire [31:0] aligned = start & ~(nb - 32'd1);      // start aligned down to the transfer size
  wire [31:0] window = ({28'd0, len} + 32'd1) << size;   // bytes in the whole burst
  wire [31:0] boundary = start & ~(window - 32'd1); // the wrap boundary (window is a power of two for WRAP)
  wire [31:0] a = aligned + ({28'd0, n} << size);
  wire wraps = FIX == 0 ? 1'b0 : FIX == 2 ? burst != FIXED : burst == WRAP;
  wire past_end = FIX == 1 ? a >= boundary + window : a - boundary >= window;
  assign addr = (burst == FIXED || n == 4'd0) ? start : (wraps && past_end) ? a - window : a;
endmodule

module eco_top(input clk, input [31:0] start, input [3:0] len, input [2:0] size, input [1:0] burst, input [3:0] n);
  localparam FIXED = 2'd0, INCR = 2'd1, WRAP = 2'd2;
  wire [31:0] addr_old, addr_new;
  axi_addr #(.FIX(0))   old_(.start(start), .len(len), .size(size), .burst(burst), .n(n), .addr(addr_old));
  axi_addr #(.FIX(2)) new_(.start(start), .len(len), .size(size), .burst(burst), .n(n), .addr(addr_new));
`ifdef FORMAL
  // modelling code: the WRAP window as the spec defines it, in 33 bits so the top of memory cannot overflow
  wire [32:0] f_window = ({29'd0, len} + 33'd1) << size;
  wire [32:0] f_boundary = ({1'b0, start} / f_window) * f_window;
  always @(posedge clk) begin
    assume(size <= 3'd2);                 // a 32-bit bus
    assume(burst != 2'd3);                // reserved encoding
    assume(n <= len);                     // a beat of this burst
    if (burst == WRAP) assume(len == 4'd1 || len == 4'd3 || len == 4'd7 || len == 4'd15);
    if (burst == WRAP) assume((start & ((32'd1 << size) - 32'd1)) == 32'd0);
    if (burst != WRAP) assert(addr_new == addr_old);
    if (burst == WRAP && n != 4'd0) assert({1'b0, addr_new} >= f_boundary && {1'b0, addr_new} < f_boundary + f_window);
  end
`endif
endmodule

Check Yourself

Predict the outputeco_top with the overflow-safe fix (FIX(3)), mode prove, depth 2, smtbmc yices, the WRAP-length and alignment assumptions in place. The verdict is:

module axi_addr #(parameter FIX = 3)(input [31:0] start, input [3:0] len,
  input [2:0] size, input [1:0] burst, input [3:0] n, output [31:0] addr);
  localparam FIXED = 2'd0, INCR = 2'd1, WRAP = 2'd2;
  wire [31:0] nb = 32'd1 << size;                  // bytes per transfer
  wire [31:0] aligned = start & ~(nb - 32'd1);      // start aligned down to the transfer size
  wire [31:0] window = ({28'd0, len} + 32'd1) << size;   // bytes in the whole burst
  wire [31:0] boundary = start & ~(window - 32'd1); // the wrap boundary (window is a power of two for WRAP)
  wire [31:0] a = aligned + ({28'd0, n} << size);
  wire wraps = FIX == 0 ? 1'b0 : FIX == 2 ? burst != FIXED : burst == WRAP;
  wire past_end = FIX == 1 ? a >= boundary + window : a - boundary >= window;
  assign addr = (burst == FIXED || n == 4'd0) ? start : (wraps && past_end) ? a - window : a;
endmodule

module eco_top(input clk, input [31:0] start, input [3:0] len, input [2:0] size, input [1:0] burst, input [3:0] n);
  localparam FIXED = 2'd0, INCR = 2'd1, WRAP = 2'd2;
  wire [31:0] addr_old, addr_new;
  axi_addr #(.FIX(0))   old_(.start(start), .len(len), .size(size), .burst(burst), .n(n), .addr(addr_old));
  axi_addr #(.FIX(3)) new_(.start(start), .len(len), .size(size), .burst(burst), .n(n), .addr(addr_new));
`ifdef FORMAL
  // modelling code: the WRAP window as the spec defines it, in 33 bits so the top of memory cannot overflow
  wire [32:0] f_window = ({29'd0, len} + 33'd1) << size;
  wire [32:0] f_boundary = ({1'b0, start} / f_window) * f_window;
  always @(posedge clk) begin
    assume(size <= 3'd2);                 // a 32-bit bus
    assume(burst != 2'd3);                // reserved encoding
    assume(n <= len);                     // a beat of this burst
    if (burst == WRAP) assume(len == 4'd1 || len == 4'd3 || len == 4'd7 || len == 4'd15);
    if (burst == WRAP) assume((start & ((32'd1 << size) - 32'd1)) == 32'd0);
    if (burst != WRAP) assert(addr_new == addr_old);
    if (burst == WRAP && n != 4'd0) assert({1'b0, addr_new} >= f_boundary && {1'b0, addr_new} < f_boundary + f_window);
  end
`endif
endmodule

ConceptWhat does conditional equivalence prove that a regression cannot?

That the two designs have the same flopsThat the fix is correct for every WRAP burstThat the fix is small and touches one moduleThat old and new agree outside the condition

ConceptAn engineer writes the equality's condition as burst == FIXED because "the fix only touched INCR and WRAP code". The bad fix is applied. What does the equality report?

PASS: INCR is outside the conditionUNKNOWN at k = 2, base case onlyFAIL on a FIXED burst at beat 0FAIL on an INCR burst at beat 1

ConceptWithout the WRAP-length assumption the fix fails on a 15-beat WRAP burst. What is the right response?

Change the fix so that any length wraps correctly.Restore it: AXI allows WRAP lengths of 2, 4, 8 or 16.Lower the depth until the failure disappears.Delete the WRAP rule, since the equality is enough.

ConceptThe fix as the P2 function writes it fails the WRAP rule at start 0xFFFFFFF4. Why does no simulation of the P2 memory see it?

The WRAP rule itself is wrong at the top of memory.The simulator computes the address in 64 bits.No test issues a burst in the last 64 bytes.AXI forbids WRAP bursts in that region of memory.

Remember

Conditional equivalence: equal to the old design outside the bug's condition, correct against the spec inside it.
Write the condition from the bug report, never from the diff.
The miter covers every input in the "must agree" region; tests cover a few points.
Counterexamples on illegal inputs mean a missing assumption, written from the spec.

Find Your Next Track

Put Your Skills to Work

Prepare to Explain Your Thinking

An Idea to Try? Pick a Tool.