How to split an AXI burst at a 4 KB boundary (and prove you did it right)

The problem

You can write a burst splitter in an afternoon. The version you write will pass every simulation, then quietly run at one-sixteenth of its designed throughput in silicon - and never raise an error. This post shows why that happens, how to catch it, and how to prove it cannot, with a corruption bug along the way that no simulation will ever find.

AXI has a rule that is easy to state and easy to violate: a burst must never cross a 4 KB boundary. Cross one and you have addressed two different pages, possibly two different slaves, in a single transaction. Real slaves respond with SLVERR, or worse, accept it and corrupt memory.

So somewhere between a DMA engine that wants to move 64 KB and the interconnect that will not accept it, something has to chop each oversized burst into legal pieces: sub-bursts that respect the 4 KB boundary and a downstream length limit, that together cover the original byte range exactly, and that can be stitched back into one response for the master. That something is a burst splitter, and it is the kind of block you write in an afternoon and debug for a week, because its failures hide from the one tool you trust most: simulation.

This post builds one, breaks it, explains the break, fixes it, and proves the fix. By the end you should be able to write the splitter and the properties that guarantee it.

The naive splitter, and the bug you will not see in simulation

For an INCR burst, the number of beats you can emit before the next boundary is “bytes left in this page, divided by the bytes per beat.” A first cut:

localparam int REM_W = 9;                       // enough for 256 beats (0..256)

logic [REM_W-1:0] bdry_beats, sub_beats;
always_comb begin
  bdry_beats = REM_W'((BOUNDARY - (cur_addr & (BOUNDARY-1))) >> req_size); // beats to boundary
  if (bdry_beats == 0) bdry_beats = 1;          // never emit a zero-beat sub-burst
  sub_beats  = min3(bdry_beats, MAX_LEN, remaining);
end

Now simulate it. Point it at a 4 KB-aligned address, hand it a long INCR burst, watch the sub-bursts come out legal and boundary-respecting. Green. Ship it.

In silicon, your 256-beat bursts leave as 256 single-beat sub-bursts instead of 16 bursts of 16. The data is correct. No boundary is crossed. Throughput is down 16x and nothing, anywhere, reports an error.

Why it fails

Look at where the narrowing happens. With BOUNDARY = 4096, DATA_WIDTH = 64 (so 8 bytes/beat, req_size = 3), and a page-aligned address:

quantity	value	bits needed	stored in REM_W = 9 bits
BOUNDARY - offset	4096	13	-
>> req_size (beats to boundary)	512	10	0 (512 mod 512)
after the == 0 -> 1 guard	-	-	1
min(1, MAX_LEN=16, remaining=256)	-	-	1

512 needs ten bits. The REM_W'(...) cast keeps nine. 512 is 10'b10_0000_0000; drop the top bit and you get 0. The guard, written to stop a legitimate zero (you are already on the boundary), now papers over a truncation, and quietly forces single-beat sub-bursts.

The lesson is the shape of the bug, not the off-by-one: you narrowed before you reduced. The intermediate bdry_beats can be far larger than any value you will actually emit, because the real output is the minimum of three numbers. Truncate the wide intermediate first and you corrupt the comparison that was about to throw most of its bits away anyway.

Key Lesson: Reduce first, narrow last. A cast that runs before the min can throw away the one bit that mattered, and a guard meant for a legitimate edge case will hide the wreckage.

The fix, line by line

Compute the minimum in a width that cannot overflow, and narrow only the result:

// compute in the address domain - wide enough that nothing wraps
logic [ADDR_WIDTH-1:0] bdry_beats_wide;
logic [REM_W-1:0]      sub_beats;

always_comb begin
  bdry_beats_wide = (BOUNDARY - (cur_addr & (BOUNDARY-1))) >> req_size;

  // reduce against MAX_LEN *before* narrowing: MAX_LEN <= 256 always fits in REM_W,
  // so the min is guaranteed representable and the cast below can never truncate.
  sub_beats = (bdry_beats_wide >= MAX_LEN) ? REM_W'(MAX_LEN)
                                           : REM_W'(bdry_beats_wide);
  if (remaining < sub_beats) sub_beats = remaining;       // last sub-burst is short
end

Two decisions worth pausing on. First, bdry_beats_wide lives in ADDR_WIDTH bits, the same domain as the address it came from, so the shift result is exact. Second, the cast to REM_W happens only after we know the value is <= MAX_LEN <= 256, which fits. The earlier guard against zero is now genuinely dead code for legal inputs, which is exactly where you want it: present for safety, never load-bearing.

The corner that is not a bug: unaligned starts

There is a tempting follow-up bug. What if the start address sits fewer than one beat below a 4 KB boundary? bdry_beats_wide could round to zero, and it looks like you cannot split without crossing. You can spend real time on this. Do not.

In AXI every beat lives in its 2**AxSIZE-aligned container. An unaligned start is rounded down to that container, and a container that size can never straddle a boundary as large as 4 KB. The 4 KB rule constrains the burst’s aligned span, never a lone beat. So “start address plus N times size” is the wrong arithmetic for the boundary check, and the apparent corner is an artifact of the wrong model. The right move is to state the precondition out loud - inputs are size-aligned - rather than code around a case the protocol already forbids.

Key Lesson: When a proof flags an “impossible” requirement, suspect your model before your design. The fix is often a precondition written down, not RTL.

Two ways to build it

There is more than one architecture, and the choice is a real tradeoff, not a detail.

A. Split on the fly. Hold the request in a few registers and emit one sub-burst per handshake, advancing a running address and remaining-beats counter.

• Pros: tiny (a handful of flops), constant area regardless of burst length, naturally back-pressured.
• Cons: one sub-burst per cycle of progress; the control FSM is where the subtle timing bugs live (see below).

B. Precompute the whole plan. On accept, compute every sub-burst’s address and length into a small FIFO, then stream the FIFO.

• Pros: the emit path is trivial and fast; the splitting math is isolated and easy to test in one place.
• Cons: more registers (the plan FIFO), a bounded worst case (a 256-beat INCR at MAX_LEN=1 is 256 entries), and you have moved, not removed, the hard part.

For a library cell that has to be small and composable, we took A. The price of that choice is the bug in the next section - which is precisely the kind of thing architecture B trades area to avoid.

Key Lesson: Pick the architecture whose failure mode you can afford. “Split on the fly” buys area back and pays for it in FSM timing bugs; “precompute the plan” pays in registers and buys back a trivial emit path.

Proving it

Simulation told us the naive splitter was fine. It was not. So the real question is what you can prove, and the answer is more than you might expect from a control block.

Sim does the obvious corners: every burst type crossed with size, length, and start offset; len = 0 and len = 255; MAX_LEN = 1 (the AXI4-Lite-adapter degenerate case). Useful, never sufficient.

Formal carries the guarantee. Bind a checker onto the cell - the RTL is never modified - and assert the obligation directly. Boundary legality is one line, and proving it for every legal request is categorically stronger than a few million random ones:

bind burst_splitter fv_burst_splitter fv (.*);

// no offered INCR sub-burst may cross the boundary
always_ff @(posedge clk)
  if (rst_n && sub_valid && sub_burst == INCR)
    bs001_no_cross: assert (
      (sub_addr & (BOUNDARY-1)) + ((sub_len + 1) << sub_size) <= BOUNDARY
    );

The throughput bug from earlier? It would survive this single property (one beat never crosses anything), which is why you also assert the quantity - that an aligned INCR emits MAX_LEN-beat sub-bursts, and that the sub-bursts’ lengths sum back to the original. Assert legality and conservation, not just legality.

Key Lesson: Assert the quantity, not just the legality - and prove it for every legal request, not the few thousand a simulation reaches. “No beat crosses” is true of the broken design too.

The bug only formal found

Here is the one that justifies the whole exercise. The splitter emits a small “group descriptor” (how many sub-bursts this request became) so the response side can recombine. Our FSM had an innocent shortcut: when the last sub-burst was accepted on the same cycle the descriptor channel was ready, it went straight back to idle and reopened the request port.

Walk two requests across that window:

cycle	splitter state	event	req port	descriptor
t	DECOMP	last sub-burst of group A accepted	reopens	A’s count not yet pushed
t+1	IDLE	group B accepted into the same slot	open	B overwrites A’s pending count

No single beat is malformed. The corruption is purely in the timing of two back-to-back groups - the exact interleaving a directed test, running one burst at a time, will never produce. Formal produces it on purpose, because it explores the adversarial schedule rather than a scripted one. The fix is a one-state detour that keeps the request port shut until the descriptor is actually consumed:

unique case (state)
  DECOMP:   if (sub_last && sub_valid && sub_ready) state <= GRP_EMIT;
  GRP_EMIT: if (grp_push && grp_ready)              state <= IDLE; // port reopens only here
endcase

Key Lesson: Freeing a resource and re-arming its input port in the same cycle, before the dependent handshake retires, is a race. Serialize on the handshake you depend on. Formal finds these because it drives the adversarial schedule you would never script.

From “it works” to “it ships”

A passing proof is not a production cell. The checklist that separates the two:

• Reset. Synchronous, active-low, and - critically for a split/join pair - the same reset domain across every cell, so a mid-transaction reset cannot leave a half-built group on one side. Control flops reset to known states; the proof pins the post-reset state explicitly.
• Parameterization, and proving across it. ADDR_WIDTH, MAX_LEN (1..256), BOUNDARY, DATA_WIDTH, sideband widths. A property proven at MAX_LEN = 16 says nothing about MAX_LEN = 1. Sweep the proof across the corners (1, 16, 256) and the degenerate widths, and state which corners closed unbounded and which only bounded.
• The input contract, written down. Size-aligned INCR is not a hope, it is a stated assumption: under strict mode the proof assumes it; under a defensive mode the cell detects a violation and terminates it with SLVERR instead of splitting wrong. Either way the contract is in the source, not in someone’s head.
• Lint and elaboration. Clean under both a synthesis-style linter and the formal frontend - they disagree often enough that passing one is not passing the other.
• CDC. This cell is single-clock by construction; the moment a design puts the splitter and its slave in different clock domains, the boundary moves to a synchronizer and that becomes its own proof. Know where your clock domains end.

Lessons

The splitter logic is about fifty lines. The confidence that it is correct took a multiple of that in properties, a parameter sweep, and a bug that only an adversarial scheduler could find. None of the real bugs were in the “interesting” arithmetic - they were a width that truncated one bit early, and a state machine that reopened a port one cycle too soon. That is where this class of block fails, and it is why “it simulates” and “it is correct” are different sentences.

The bundle, and where to go next

Every cell we publish ships with its proof bundle - the bound checker, the assumptions, the covers, the parameter sweep, and the exact sign-off (what closed unbounded, what is bounded-clean and to what depth, and how it scored under mutation testing). If you want to see what an honest formal record looks like rather than a green checkmark, that is on the evidence page, and the discipline behind grading the proof itself is in what a formal PASS has to earn.

The splitter is one third of a set. The natural next reads, building toward a full split/recombine path:

• burst_join - recombining the responses: worst-of RRESP/BRESP, one master-visible last per request, and why it is harder to prove unbounded than the splitter.
• burst_controller - regenerating WLAST on the write path, and the width bug we found in hand-written RTL that had shipped.
• Async FIFO and CDC - when the split and join live in different clock domains.

One block, one real failure, one correct build, one proof, one lesson. That is the deal: you should leave knowing how to build this, and how to know you built it right.