AXI Interfaces to USB

   addr 0x1000, 256 beats of 4 bytes   ->  one burst. Fits.

   addr 0x1F00, 256 beats of 4 bytes   ->  MUST BE SPLIT:
                                           64 beats to 0x2000,
                                           then 192 from there.

   what is LEFT          the descriptor does not go on for ever
   the 4 KB BOUNDARY     the protocol forbids crossing it
   MAX_BEATS             AXI4 INCR allows at most 256

// usb_axi_burst -- the one AXI rule a DMA engine has to obey and the one it
// is easiest to get away with breaking.
//
// A USB CONTROLLER IS TWO AXI PORTS WITH OPPOSITE REQUIREMENTS
//
//     the SLAVE port    registers. A handful of 32-bit accesses, and every
//                       one of them is a driver spinning on a status bit.
//                       It wants LATENCY.
//
//     the MASTER port   the DMA engine moving packet data. Kilobytes at a
//                       time, and nobody is waiting on any individual beat.
//                       It wants THROUGHPUT.
//
// Those are different ports for a reason. Putting both behind one bridge
// makes the register reads queue behind a 256-beat burst, and a driver that
// polls a status register then sees a millisecond of latency on an access
// that should take tens of nanoseconds.
//
// THE 4 KB RULE
//
// An AXI burst must not cross a 4 KB address boundary. Not "should not":
// the protocol forbids it, because 4 KB is the smallest page an interconnect
// is allowed to decode differently, and a burst that crossed one could be
// half in one slave and half in another.
//
// A DMA buffer is whatever address the operating system gave you. So:
//
//     addr 0x1000, 256 beats of 4 bytes   ->  one burst. Fits.
//     addr 0x1F00, 256 beats of 4 bytes   ->  MUST BE SPLIT:
//                                             64 beats to 0x2000, then 192.
//
// AND THIS IS WHY IT IS SO EASY TO SHIP BROKEN
//
// Many interconnects tolerate a crossing burst. Some split it for you, some
// route the whole thing on the first address and corrupt memory, some assert
// an error nobody has wired up. So an engine that ignores the rule works
// perfectly on the SoC it was developed on, and fails on the next one -- and
// the failure is memory corruption at an address that has nothing to do with
// USB.
//
//     It is not a bug you find by testing. It is a bug you find by
//     obeying the rule.
//
// THE OTHER LIMIT
//
// AXI4 allows at most 256 beats in an INCR burst, so a long transfer is
// split by the beat count as well as by the boundary. Both limits apply at
// once and the burst is the smaller of the three: what is left, what fits
// before the boundary, and what the protocol allows.
module usb_axi_burst #(
  parameter integer ADDR_W    = 32,
  parameter integer DATA_W    = 32,
  parameter integer BOUNDARY  = 4096,  // the AXI rule. 4 KB, always.
  parameter integer MAX_BEATS = 256    // AXI4 INCR limit
) (
  input  wire              clk,
  input  wire              rst_n,

  input  wire              start,
  input  wire [ADDR_W-1:0] addr,       // where the buffer begins
  input  wire [15:0]       beats,      // how many beats it is
  input  wire              burst_ack,  // the fabric accepted this burst
  input  wire              eot,

  output wire              busy,
  output wire              bv,         // a burst is offered this cycle
  output wire [ADDR_W-1:0] baddr,
  output wire [7:0]        blen,       // AXI AWLEN: beats - 1
  output wire [2:0]        bsize,      // AXI AWSIZE: log2(bytes per beat)
  output wire [15:0]       bbeats,     // the same count, not encoded
  output wire [15:0]       bindex,     // 0-based burst number
  output wire [15:0]       remaining,
  output wire              done_pulse,
  output wire              err_pulse,
  output wire [1:0]        err_code,

  output reg [31:0] n_start,
  output reg [31:0] n_burst,
  output reg [31:0] n_split_bound,   // split because of the 4 KB rule
  output reg [31:0] n_split_len,     // split because of the beat limit
  output reg [31:0] n_done,
  output reg [31:0] n_unaligned,
  output reg [31:0] n_zero,
  output reg [31:0] n_restart
);

  localparam [1:0] E_NONE      = 2'd0,
                   E_UNALIGNED = 2'd1,  // the address is not beat-aligned
                   E_ZERO      = 2'd2,  // a descriptor of no beats
                   E_RESTART   = 2'd3;  // a new one while a burst is running

  // Bytes per beat, and the AXI size encoding of it. Derived from DATA_W
  // rather than written as a constant, because the two must never drift:
  // an AWSIZE that disagrees with the data width is a burst the fabric will
  // happily accept and misinterpret.
  localparam integer BPB   = DATA_W / 8;
  localparam [2:0]   BSIZE = (BPB == 1) ? 3'd0 :
                             (BPB == 2) ? 3'd1 :
                             (BPB == 4) ? 3'd2 :
                             (BPB == 8) ? 3'd3 :
                             (BPB == 16) ? 3'd4 :
                             (BPB == 32) ? 3'd5 :
                             (BPB == 64) ? 3'd6 : 3'd7;

  localparam [15:0] BND16 = BOUNDARY;
  localparam [15:0] MAXB16 = MAX_BEATS;
  localparam [15:0] BPB16 = BPB;

  reg [ADDR_W-1:0] addr_r;
  reg [15:0]       rem_r, idx_r;
  reg              busy_r, dn_r, er_r;
  reg [1:0]        ec_r;

  // ---- How many beats this burst may carry. ----
  //
  // The smaller of three limits, and all three are real:
  //
  //   what is left        the descriptor does not go on for ever
  //   the 4 KB boundary   the protocol forbids crossing it
  //   MAX_BEATS           AXI4 INCR allows at most 256
  //
  // Dropping any one of them produces a burst that the fabric may accept
  // and misroute, which is the worst kind of wrong: no error anywhere.
  function [15:0] beats_to_boundary;
    input [ADDR_W-1:0] a;
    reg [15:0] off;
    begin
      off               = a[15:0] % BND16;
      beats_to_boundary = (BND16 - off) / BPB16;
    end
  endfunction

  function [15:0] this_burst;
    input [ADDR_W-1:0] a;
    input [15:0]       r;
    reg [15:0] lim_b, lim_l;
    begin
      lim_b = beats_to_boundary(a);
      lim_l = MAXB16;
      this_burst = r;
      if (lim_b < this_burst) this_burst = lim_b;
      if (lim_l < this_burst) this_burst = lim_l;
    end
  endfunction

  wire [15:0] tb = this_burst(addr_r, rem_r);

  assign busy       = busy_r;
  assign bv         = busy_r;
  assign baddr      = addr_r;
  // AXI encodes the beat count as length MINUS ONE. A burst of one beat has
  // AWLEN = 0, and there is no encoding for zero beats -- which is why a
  // descriptor of no beats is rejected rather than issued.
  assign blen       = busy_r ? (tb[7:0] - 8'd1) : 8'd0;
  assign bsize      = BSIZE;
  assign bbeats     = busy_r ? tb : 16'd0;
  assign bindex     = idx_r;
  assign remaining  = rem_r;
  assign done_pulse = dn_r;
  assign err_pulse  = er_r;
  assign err_code   = ec_r;

  reg [ADDR_W-1:0] addr_n;
  reg [15:0]       rem_n, idx_n;
  reg              busy_n, dn_n, er_n;
  reg [1:0]        ec_n;
  reg              st_n, bu_n, sb_n, sl_n, dn_c, un_n, zr_n, rs_n;

  always @* begin
    addr_n = addr_r;
    rem_n  = rem_r;
    idx_n  = idx_r;
    busy_n = busy_r;
    dn_n   = 1'b0; er_n = 1'b0; ec_n = E_NONE;
    st_n = 1'b0; bu_n = 1'b0; sb_n = 1'b0; sl_n = 1'b0;
    dn_c = 1'b0; un_n = 1'b0; zr_n = 1'b0; rs_n = 1'b0;

    if (eot) begin
      // Nothing: the counters are the report.
    end else if (start) begin
      if (busy_r) begin
        er_n = 1'b1; ec_n = E_RESTART;
        rs_n = 1'b1;
      end else if (beats == 16'd0) begin
        // AXI has no encoding for a zero-beat burst. A descriptor of no
        // beats is a software bug and issuing AWLEN = 0xFF for it -- which
        // is what `beats - 1` produces -- writes 256 beats of rubbish.
        er_n = 1'b1; ec_n = E_ZERO;
        zr_n = 1'b1;
      end else if ((addr[15:0] % BPB16) != 16'd0) begin
        // An INCR burst of this size must start on a beat boundary. An
        // unaligned start is legal AXI only with the narrow-transfer rules,
        // which a DMA engine has no reason to use and every reason to avoid.
        er_n = 1'b1; ec_n = E_UNALIGNED;
        un_n = 1'b1;
      end else begin
        addr_n = addr;
        rem_n  = beats;
        idx_n  = 16'd0;
        busy_n = 1'b1;
        st_n   = 1'b1;
      end
    end else if (burst_ack) begin
      if (busy_r) begin
        bu_n = 1'b1;
        // Which limit cut this burst short is worth counting separately: a
        // run of boundary splits says the buffer is badly aligned, and a run
        // of length splits says it is simply long. They lead to different
        // conversations with whoever allocates the buffers.
        if (tb < rem_r) begin
          if (tb == beats_to_boundary(addr_r)) sb_n = 1'b1;
          else                                 sl_n = 1'b1;
        end
        addr_n = addr_r + {{(ADDR_W-16){1'b0}}, tb} * BPB;
        rem_n  = rem_r - tb;
        idx_n  = idx_r + 16'd1;
        if (rem_n == 16'd0) begin
          busy_n = 1'b0;
          dn_n   = 1'b1;
          dn_c   = 1'b1;
        end
      end
    end
  end

  always @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      addr_r <= {ADDR_W{1'b0}};
      rem_r  <= 16'd0;
      idx_r  <= 16'd0;
      busy_r <= 1'b0;
      dn_r   <= 1'b0; er_r <= 1'b0; ec_r <= E_NONE;
      n_start       <= 32'd0;
      n_burst       <= 32'd0;
      n_split_bound <= 32'd0;
      n_split_len   <= 32'd0;
      n_done        <= 32'd0;
      n_unaligned   <= 32'd0;
      n_zero        <= 32'd0;
      n_restart     <= 32'd0;
    end else begin
      addr_r <= addr_n;
      rem_r  <= rem_n;
      idx_r  <= idx_n;
      busy_r <= busy_n;
      dn_r   <= dn_n; er_r <= er_n; ec_r <= ec_n;

      if (st_n) n_start       <= n_start       + 32'd1;
      if (bu_n) n_burst       <= n_burst       + 32'd1;
      if (sb_n) n_split_bound <= n_split_bound + 32'd1;
      if (sl_n) n_split_len   <= n_split_len   + 32'd1;
      if (dn_c) n_done        <= n_done        + 32'd1;
      if (un_n) n_unaligned   <= n_unaligned   + 32'd1;
      if (zr_n) n_zero        <= n_zero        + 32'd1;
      if (rs_n) n_restart     <= n_restart     + 32'd1;
    end
  end
endmodule

// usb_axi_burst -- the one AXI rule a DMA engine has to obey and the one it
// is easiest to get away with breaking.
//
// A USB CONTROLLER IS TWO AXI PORTS WITH OPPOSITE REQUIREMENTS
//
//     the SLAVE port    registers. A handful of 32-bit accesses, and every
//                       one of them is a driver spinning on a status bit.
//                       It wants LATENCY.
//
//     the MASTER port   the DMA engine moving packet data. Kilobytes at a
//                       time, and nobody is waiting on any individual beat.
//                       It wants THROUGHPUT.
//
// Those are different ports for a reason. Putting both behind one bridge
// makes the register reads queue behind a 256-beat burst, and a driver that
// polls a status register then sees a millisecond of latency on an access
// that should take tens of nanoseconds.
//
// THE 4 KB RULE
//
// An AXI burst must not cross a 4 KB address boundary. Not "should not":
// the protocol forbids it, because 4 KB is the smallest page an interconnect
// is allowed to decode differently, and a burst that crossed one could be
// half in one slave and half in another.
//
// A DMA buffer is whatever address the operating system gave you. So:
//
//     addr 0x1000, 256 beats of 4 bytes   ->  one burst. Fits.
//     addr 0x1F00, 256 beats of 4 bytes   ->  MUST BE SPLIT:
//                                             64 beats to 0x2000, then 192.
//
// AND THIS IS WHY IT IS SO EASY TO SHIP BROKEN
//
// Many interconnects tolerate a crossing burst. Some split it for you, some
// route the whole thing on the first address and corrupt memory, some assert
// an error nobody has wired up. So an engine that ignores the rule works
// perfectly on the SoC it was developed on, and fails on the next one -- and
// the failure is memory corruption at an address that has nothing to do with
// USB.
//
//     It is not a bug you find by testing. It is a bug you find by
//     obeying the rule.
//
// THE OTHER LIMIT
//
// AXI4 allows at most 256 beats in an INCR burst, so a long transfer is
// split by the beat count as well as by the boundary. Both limits apply at
// once and the burst is the smaller of the three: what is left, what fits
// before the boundary, and what the protocol allows.
package usb_axi_pkg;
  typedef enum logic [1:0] {
    E_NONE      = 2'd0,
    E_UNALIGNED = 2'd1,   // the address is not beat-aligned
    E_ZERO      = 2'd2,   // a descriptor of no beats
    E_RESTART   = 2'd3    // a new one while a burst is running
  } axi_err_e;
endpackage

module usb_axi_burst
  import usb_axi_pkg::*;
 #(
  parameter int ADDR_W    = 32,
  parameter int DATA_W    = 32,
  parameter int BOUNDARY  = 4096,      // the AXI rule. 4 KB, always.
  parameter int MAX_BEATS = 256        // AXI4 INCR limit
) (
  input  logic              clk,
  input  logic              rst_n,

  input  logic              start,
  input  logic [ADDR_W-1:0] addr,      // where the buffer begins
  input  logic [15:0]       beats,     // how many beats it is
  input  logic              burst_ack, // the fabric accepted this burst
  input  logic              eot,

  output logic              busy,
  output logic              bv,        // a burst is offered this cycle
  output logic [ADDR_W-1:0] baddr,
  output logic [7:0]        blen,      // AXI AWLEN: beats - 1
  output logic [2:0]        bsize,     // AXI AWSIZE: log2(bytes per beat)
  output logic [15:0]       bbeats,    // the same count, not encoded
  output logic [15:0]       bindex,    // 0-based burst number
  output logic [15:0]       remaining,
  output logic              done_pulse,
  output logic              err_pulse,
  output axi_err_e          err_code,

  output logic [31:0] n_start,
  output logic [31:0] n_burst,
  output logic [31:0] n_split_bound,   // split because of the 4 KB rule
  output logic [31:0] n_split_len,     // split because of the beat limit
  output logic [31:0] n_done,
  output logic [31:0] n_unaligned,
  output logic [31:0] n_zero,
  output logic [31:0] n_restart
);

  // Bytes per beat, and the AXI size encoding of it. Derived from DATA_W
  // rather than written as a constant, because the two must never drift:
  // an AWSIZE that disagrees with the data width is a burst the fabric will
  // happily accept and misinterpret.
  localparam int BPB   = DATA_W / 8;
  localparam [2:0]   BSIZE = (BPB == 1) ? 3'd0 :
                             (BPB == 2) ? 3'd1 :
                             (BPB == 4) ? 3'd2 :
                             (BPB == 8) ? 3'd3 :
                             (BPB == 16) ? 3'd4 :
                             (BPB == 32) ? 3'd5 :
                             (BPB == 64) ? 3'd6 : 3'd7;

  localparam logic [15:0] BND16  = 16'(BOUNDARY);
  localparam logic [15:0] MAXB16 = 16'(MAX_BEATS);
  localparam logic [15:0] BPB16  = 16'(BPB);

  logic [ADDR_W-1:0] addr_r;
  logic [15:0]       rem_r, idx_r;
  logic              busy_r, dn_r, er_r;
  axi_err_e          ec_r;

  // ---- How many beats this burst may carry. ----
  //
  // The smaller of three limits, and all three are real:
  //
  //   what is left        the descriptor does not go on for ever
  //   the 4 KB boundary   the protocol forbids crossing it
  //   MAX_BEATS           AXI4 INCR allows at most 256
  //
  // Dropping any one of them produces a burst that the fabric may accept
  // and misroute, which is the worst kind of wrong: no error anywhere.
  function automatic logic [15:0] beats_to_boundary(input logic [ADDR_W-1:0] a);
    logic [15:0] off;
    begin
      off               = a[15:0] % BND16;
      beats_to_boundary = (BND16 - off) / BPB16;
    end
  endfunction

  function automatic logic [15:0] this_burst(input logic [ADDR_W-1:0] a,
                                            input logic [15:0] r);
    logic [15:0] lim_b, lim_l;
    begin
      lim_b = beats_to_boundary(a);
      lim_l = MAXB16;
      this_burst = r;
      if (lim_b < this_burst) this_burst = lim_b;
      if (lim_l < this_burst) this_burst = lim_l;
    end
  endfunction

  logic [15:0] tb;
  assign tb = this_burst(addr_r, rem_r);

  assign busy       = busy_r;
  assign bv         = busy_r;
  assign baddr      = addr_r;
  // AXI encodes the beat count as length MINUS ONE. A burst of one beat has
  // AWLEN = 0, and there is no encoding for zero beats -- which is why a
  // descriptor of no beats is rejected rather than issued.
  assign blen       = busy_r ? (tb[7:0] - 8'd1) : 8'd0;
  assign bsize      = BSIZE;
  assign bbeats     = busy_r ? tb : 16'd0;
  assign bindex     = idx_r;
  assign remaining  = rem_r;
  assign done_pulse = dn_r;
  assign err_pulse  = er_r;
  assign err_code   = ec_r;

  logic [ADDR_W-1:0] addr_n;
  logic [15:0]       rem_n, idx_n;
  logic              busy_n, dn_n, er_n;
  axi_err_e          ec_n;
  logic              st_n, bu_n, sb_n, sl_n, dn_c, un_n, zr_n, rs_n;

  always_comb begin
    addr_n = addr_r;
    rem_n  = rem_r;
    idx_n  = idx_r;
    busy_n = busy_r;
    dn_n   = 1'b0; er_n = 1'b0; ec_n = E_NONE;
    st_n = 1'b0; bu_n = 1'b0; sb_n = 1'b0; sl_n = 1'b0;
    dn_c = 1'b0; un_n = 1'b0; zr_n = 1'b0; rs_n = 1'b0;

    if (eot) begin
      // Nothing: the counters are the report.
    end else if (start) begin
      if (busy_r) begin
        er_n = 1'b1; ec_n = E_RESTART;
        rs_n = 1'b1;
      end else if (beats == 16'd0) begin
        // AXI has no encoding for a zero-beat burst. A descriptor of no
        // beats is a software bug and issuing AWLEN = 0xFF for it -- which
        // is what `beats - 1` produces -- writes 256 beats of rubbish.
        er_n = 1'b1; ec_n = E_ZERO;
        zr_n = 1'b1;
      end else if ((addr[15:0] % BPB16) != 16'd0) begin
        // An INCR burst of this size must start on a beat boundary. An
        // unaligned start is legal AXI only with the narrow-transfer rules,
        // which a DMA engine has no reason to use and every reason to avoid.
        er_n = 1'b1; ec_n = E_UNALIGNED;
        un_n = 1'b1;
      end else begin
        addr_n = addr;
        rem_n  = beats;
        idx_n  = 16'd0;
        busy_n = 1'b1;
        st_n   = 1'b1;
      end
    end else if (burst_ack) begin
      if (busy_r) begin
        bu_n = 1'b1;
        // Which limit cut this burst short is worth counting separately: a
        // run of boundary splits says the buffer is badly aligned, and a run
        // of length splits says it is simply long. They lead to different
        // conversations with whoever allocates the buffers.
        if (tb < rem_r) begin
          if (tb == beats_to_boundary(addr_r)) sb_n = 1'b1;
          else                                 sl_n = 1'b1;
        end
        addr_n = addr_r + ADDR_W'({{(ADDR_W-16){1'b0}}, tb} * BPB);
        rem_n  = rem_r - tb;
        idx_n  = idx_r + 16'd1;
        if (rem_n == 16'd0) begin
          busy_n = 1'b0;
          dn_n   = 1'b1;
          dn_c   = 1'b1;
        end
      end
    end
  end

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      addr_r <= '0;
      rem_r  <= 16'd0;
      idx_r  <= 16'd0;
      busy_r <= 1'b0;
      dn_r   <= 1'b0; er_r <= 1'b0; ec_r <= E_NONE;
      n_start       <= 32'd0;
      n_burst       <= 32'd0;
      n_split_bound <= 32'd0;
      n_split_len   <= 32'd0;
      n_done        <= 32'd0;
      n_unaligned   <= 32'd0;
      n_zero        <= 32'd0;
      n_restart     <= 32'd0;
    end else begin
      addr_r <= addr_n;
      rem_r  <= rem_n;
      idx_r  <= idx_n;
      busy_r <= busy_n;
      dn_r   <= dn_n; er_r <= er_n; ec_r <= ec_n;

      if (st_n) n_start       <= n_start       + 32'd1;
      if (bu_n) n_burst       <= n_burst       + 32'd1;
      if (sb_n) n_split_bound <= n_split_bound + 32'd1;
      if (sl_n) n_split_len   <= n_split_len   + 32'd1;
      if (dn_c) n_done        <= n_done        + 32'd1;
      if (un_n) n_unaligned   <= n_unaligned   + 32'd1;
      if (zr_n) n_zero        <= n_zero        + 32'd1;
      if (rs_n) n_restart     <= n_restart     + 32'd1;
    end
  end
endmodule

-- usb_axi_burst -- the one AXI rule a DMA engine has to obey and the one it
-- is easiest to get away with breaking.
--
-- A USB CONTROLLER IS TWO AXI PORTS WITH OPPOSITE REQUIREMENTS
--
--     the SLAVE port    registers. A handful of 32-bit accesses, and every
--                       one of them is a driver spinning on a status bit.
--                       It wants LATENCY.
--
--     the MASTER port   the DMA engine moving packet data. Kilobytes at a
--                       time, and nobody is waiting on any individual beat.
--                       It wants THROUGHPUT.
--
-- Those are different ports for a reason. Putting both behind one bridge
-- makes the register reads queue behind a 256-beat burst, and a driver that
-- polls a status register then sees a millisecond of latency on an access
-- that should take tens of nanoseconds.
--
-- THE 4 KB RULE
--
-- An AXI burst must not cross a 4 KB address boundary. Not "should not": the
-- protocol forbids it, because 4 KB is the smallest page an interconnect is
-- allowed to decode differently, and a burst that crossed one could be half
-- in one slave and half in another.
--
-- A DMA buffer is whatever address the operating system gave you. So:
--
--     addr 0x1000, 256 beats of 4 bytes   ->  one burst. Fits.
--     addr 0x1F00, 256 beats of 4 bytes   ->  MUST BE SPLIT:
--                                             64 beats to 0x2000, then 192.
--
-- AND THIS IS WHY IT IS SO EASY TO SHIP BROKEN
--
-- Many interconnects tolerate a crossing burst. Some split it for you, some
-- route the whole thing on the first address and corrupt memory, some assert
-- an error nobody has wired up. So an engine that ignores the rule works
-- perfectly on the SoC it was developed on, and fails on the next one -- and
-- the failure is memory corruption at an address that has nothing to do with
-- USB.
--
--     It is not a bug you find by testing. It is a bug you find by
--     obeying the rule.
--
-- THE OTHER LIMIT
--
-- AXI4 allows at most 256 beats in an INCR burst, so a long transfer is split
-- by the beat count as well as by the boundary. Both limits apply at once and
-- the burst is the smaller of the three: what is left, what fits before the
-- boundary, and what the protocol allows.
library ieee;
use ieee.std_logic_1164.all;
use ieee.numeric_std.all;

package usb_axi_pkg is
  constant E_NONE      : std_logic_vector(1 downto 0) := "00";
  constant E_UNALIGNED : std_logic_vector(1 downto 0) := "01";
  constant E_ZERO      : std_logic_vector(1 downto 0) := "10";
  constant E_RESTART   : std_logic_vector(1 downto 0) := "11";
end package;

library ieee;
use ieee.std_logic_1164.all;
use ieee.numeric_std.all;
use work.usb_axi_pkg.all;

entity usb_axi_burst is
  generic (
    ADDR_W    : integer := 32;
    DATA_W    : integer := 32;
    BOUNDARY  : integer := 4096;   -- the AXI rule. 4 KB, always.
    MAX_BEATS : integer := 256     -- AXI4 INCR limit
  );
  port (
    clk       : in std_logic;
    rst_n     : in std_logic;

    start     : in std_logic;
    addr      : in unsigned(ADDR_W-1 downto 0);
    beats     : in unsigned(15 downto 0);
    burst_ack : in std_logic;
    eot       : in std_logic;

    busy       : out std_logic;
    bv         : out std_logic;
    baddr      : out unsigned(ADDR_W-1 downto 0);
    blen       : out unsigned(7 downto 0);   -- AXI AWLEN: beats - 1
    bsize      : out unsigned(2 downto 0);   -- AXI AWSIZE
    bbeats     : out unsigned(15 downto 0);
    bindex     : out unsigned(15 downto 0);
    remaining  : out unsigned(15 downto 0);
    done_pulse : out std_logic;
    err_pulse  : out std_logic;
    err_code   : out std_logic_vector(1 downto 0);

    n_start       : out unsigned(31 downto 0);
    n_burst       : out unsigned(31 downto 0);
    n_split_bound : out unsigned(31 downto 0);
    n_split_len   : out unsigned(31 downto 0);
    n_done        : out unsigned(31 downto 0);
    n_unaligned   : out unsigned(31 downto 0);
    n_zero        : out unsigned(31 downto 0);
    n_restart     : out unsigned(31 downto 0)
  );
end entity;

architecture rtl of usb_axi_burst is
  -- Bytes per beat, and the AXI size encoding of it. Derived from DATA_W
  -- rather than written as a constant, because the two must never drift: an
  -- AWSIZE that disagrees with the data width is a burst the fabric will
  -- happily accept and misinterpret.
  constant BPB : integer := DATA_W / 8;

  function size_enc (b : integer) return unsigned is
  begin
    case b is
      when 1  => return to_unsigned(0, 3);
      when 2  => return to_unsigned(1, 3);
      when 4  => return to_unsigned(2, 3);
      when 8  => return to_unsigned(3, 3);
      when 16 => return to_unsigned(4, 3);
      when 32 => return to_unsigned(5, 3);
      when 64 => return to_unsigned(6, 3);
      when others => return to_unsigned(7, 3);
    end case;
  end function;

  signal addr_r : unsigned(ADDR_W-1 downto 0) := (others => '0');
  signal rem_r, idx_r : unsigned(15 downto 0) := (others => '0');
  signal busy_r, dn_r, er_r : std_logic := '0';
  signal ec_r : std_logic_vector(1 downto 0) := E_NONE;

  signal st_c, bu_c, sb_c, sl_c : unsigned(31 downto 0) := (others => '0');
  signal dn_c, un_c, zr_c, rs_c : unsigned(31 downto 0) := (others => '0');

  signal tb : unsigned(15 downto 0) := (others => '0');

  -- ---- How many beats this burst may carry. ----
  --
  -- The smaller of three limits, and all three are real:
  --
  --   what is left        the descriptor does not go on for ever
  --   the 4 KB boundary   the protocol forbids crossing it
  --   MAX_BEATS           AXI4 INCR allows at most 256
  --
  -- Dropping any one of them produces a burst that the fabric may accept and
  -- misroute, which is the worst kind of wrong: no error anywhere.
  function beats_to_boundary (a : unsigned) return unsigned is
    variable off : unsigned(15 downto 0);
  begin
    off := a(15 downto 0) mod to_unsigned(BOUNDARY, 16);
    return (to_unsigned(BOUNDARY, 16) - off) / to_unsigned(BPB, 16);
  end function;

  function this_burst (a : unsigned; r : unsigned(15 downto 0))
    return unsigned is
    variable v : unsigned(15 downto 0);
    variable b : unsigned(15 downto 0);
  begin
    v := r;
    b := beats_to_boundary(a);
    if b < v then v := b; end if;
    if to_unsigned(MAX_BEATS, 16) < v then v := to_unsigned(MAX_BEATS, 16); end if;
    return v;
  end function;
begin
  tb <= this_burst(addr_r, rem_r);

  busy   <= busy_r;
  bv     <= busy_r;
  baddr  <= addr_r;
  -- AXI encodes the beat count as length MINUS ONE. A burst of one beat has
  -- AWLEN = 0, and there is no encoding for zero beats -- which is why a
  -- descriptor of no beats is rejected rather than issued.
  blen   <= (tb(7 downto 0) - 1) when busy_r = '1' else (others => '0');
  bsize  <= size_enc(BPB);
  bbeats <= tb when busy_r = '1' else (others => '0');
  bindex <= idx_r;
  remaining  <= rem_r;
  done_pulse <= dn_r;
  err_pulse  <= er_r;
  err_code   <= ec_r;

  n_start       <= st_c;
  n_burst       <= bu_c;
  n_split_bound <= sb_c;
  n_split_len   <= sl_c;
  n_done        <= dn_c;
  n_unaligned   <= un_c;
  n_zero        <= zr_c;
  n_restart     <= rs_c;

  process (clk, rst_n)
    variable addr_v : unsigned(ADDR_W-1 downto 0);
    variable rem_v, idx_v : unsigned(15 downto 0);
    variable busy_v, dn_v, er_v : std_logic;
    variable ec_v : std_logic_vector(1 downto 0);
    variable tb_v : unsigned(15 downto 0);
  begin
    if rst_n = '0' then
      addr_r <= (others => '0');
      rem_r  <= (others => '0');
      idx_r  <= (others => '0');
      busy_r <= '0';
      dn_r   <= '0'; er_r <= '0'; ec_r <= E_NONE;
      st_c <= (others => '0'); bu_c <= (others => '0');
      sb_c <= (others => '0'); sl_c <= (others => '0');
      dn_c <= (others => '0'); un_c <= (others => '0');
      zr_c <= (others => '0'); rs_c <= (others => '0');
    elsif rising_edge(clk) then
      addr_v := addr_r;
      rem_v  := rem_r;
      idx_v  := idx_r;
      busy_v := busy_r;
      dn_v := '0'; er_v := '0'; ec_v := E_NONE;
      tb_v := this_burst(addr_r, rem_r);

      if eot = '1' then
        -- Nothing: the counters are the report.
        null;
      elsif start = '1' then
        if busy_r = '1' then
          er_v := '1'; ec_v := E_RESTART;
          rs_c <= rs_c + 1;
        elsif beats = 0 then
          -- AXI has no encoding for a zero-beat burst. A descriptor of no
          -- beats is a software bug and issuing AWLEN = 0xFF for it -- which
          -- is what `beats - 1` produces -- writes 256 beats of rubbish.
          er_v := '1'; ec_v := E_ZERO;
          zr_c <= zr_c + 1;
        elsif (addr(15 downto 0) mod to_unsigned(BPB, 16)) /= 0 then
          -- An INCR burst of this size must start on a beat boundary. An
          -- unaligned start is legal AXI only with the narrow-transfer rules,
          -- which a DMA engine has no reason to use and every reason to
          -- avoid.
          er_v := '1'; ec_v := E_UNALIGNED;
          un_c <= un_c + 1;
        else
          addr_v := addr;
          rem_v  := beats;
          idx_v  := (others => '0');
          busy_v := '1';
          st_c   <= st_c + 1;
        end if;
      elsif burst_ack = '1' then
        if busy_r = '1' then
          bu_c <= bu_c + 1;
          -- Which limit cut this burst short is worth counting separately: a
          -- run of boundary splits says the buffer is badly aligned, and a
          -- run of length splits says it is simply long. They lead to
          -- different conversations with whoever allocates the buffers.
          if tb_v < rem_v then
            if tb_v = beats_to_boundary(addr_r) then
              sb_c <= sb_c + 1;
            else
              sl_c <= sl_c + 1;
            end if;
          end if;
          addr_v := addr_v + resize(tb_v * to_unsigned(BPB, 16), ADDR_W);
          rem_v  := rem_v - tb_v;
          idx_v  := idx_v + 1;
          if rem_v = 0 then
            busy_v := '0';
            dn_v   := '1';
            dn_c   <= dn_c + 1;
          end if;
        end if;
      end if;

      addr_r <= addr_v;
      rem_r  <= rem_v;
      idx_r  <= idx_v;
      busy_r <= busy_v;
      dn_r   <= dn_v; er_r <= er_v; ec_r <= ec_v;
    end if;
  end process;
end architecture;

   every aligned offset in a boundary window   (64)
 x every beat count from 1 to two windows      (128)
 = 8192 transfers, every burst of every one checked

`timescale 1ns/1ps
// Testbench for usb_axi_burst.
//
// THE CHECKS ARE PROTOCOL PROPERTIES, NOT EXPECTED VALUES
//
// A burst splitter is one of the few blocks where the specification states
// the acceptance criteria directly, so the testbench asserts those rather
// than a table of expected outputs:
//
//   1. no burst crosses a BOUNDARY-byte address boundary
//   2. no burst exceeds MAX_BEATS beats
//   3. every burst carries at least one beat
//   4. AWLEN is the beat count MINUS ONE, every time
//   5. consecutive bursts are contiguous -- no gap, no overlap
//   6. the beats delivered sum to exactly the beats requested
//
// Property 1 is the one this chapter is about and property 6 is the one that
// catches a splitter which obeys property 1 by dropping data.
//
// THE EXHAUSTIVE CLAIM
//
// The splitting arithmetic depends on two numbers: where in the boundary
// window the buffer starts, and how many beats it is. So both are swept, all
// the way across, as a product:
//
//     every aligned offset in a boundary window   (64)
//   x every beat count from 1 to 2 windows' worth (128)
//   = 8192 transfers, every burst of every one checked
//
// The DUT is instantiated with a SCALED boundary so that product is
// tractable. A second instance carries the real 4096/256 values and is
// driven by the directed cases, because a parameter that is never changed is
// a constant with extra steps -- chapter 25.4's retry budget again.
module tb_ab_v;

  localparam integer ADDR_W = 32;
  localparam integer DATA_W = 32;
  localparam integer BPB    = DATA_W / 8;

  // the scaled instance, for the exhaustive sweep
  localparam integer BND_S  = 256;
  localparam integer MAXB_S = 16;

  // the real instance, for the directed cases
  localparam integer BND_R  = 4096;
  localparam integer MAXB_R = 256;

  localparam [1:0] E_NONE = 2'd0, E_UNALIGNED = 2'd1, E_ZERO = 2'd2,
                   E_RESTART = 2'd3;

  reg               clk = 1'b0, rst_n = 1'b0;
  reg               start = 1'b0, burst_ack = 1'b0, eot = 1'b0;
  reg  [ADDR_W-1:0] addr = {ADDR_W{1'b0}};
  reg  [15:0]       beats = 16'd0;

  wire              busy, bv, done_pulse, err_pulse;
  wire [ADDR_W-1:0] baddr;
  wire [7:0]        blen;
  wire [2:0]        bsize;
  wire [15:0]       bbeats, bindex, remaining;
  wire [1:0]        err_code;
  wire [31:0] n_start, n_burst, n_split_bound, n_split_len, n_done,
              n_unaligned, n_zero, n_restart;

  usb_axi_burst #(.ADDR_W(ADDR_W), .DATA_W(DATA_W),
                  .BOUNDARY(BND_S), .MAX_BEATS(MAXB_S)) dut (
    .clk(clk), .rst_n(rst_n),
    .start(start), .addr(addr), .beats(beats), .burst_ack(burst_ack),
    .eot(eot),
    .busy(busy), .bv(bv), .baddr(baddr), .blen(blen), .bsize(bsize),
    .bbeats(bbeats), .bindex(bindex), .remaining(remaining),
    .done_pulse(done_pulse), .err_pulse(err_pulse), .err_code(err_code),
    .n_start(n_start), .n_burst(n_burst), .n_split_bound(n_split_bound),
    .n_split_len(n_split_len), .n_done(n_done),
    .n_unaligned(n_unaligned), .n_zero(n_zero), .n_restart(n_restart)
  );

  // ---- The same design with the REAL AXI numbers. ----
  //
  // Driven by the same stimulus and checked against the same properties. A
  // splitter whose boundary is hard-coded to whatever the test used passes
  // everything above and corrupts memory on the first real SoC.
  wire              busy4, bv4, done4;
  wire [ADDR_W-1:0] baddr4;
  wire [7:0]        blen4;
  wire [15:0]       bbeats4, bindex4;

  usb_axi_burst #(.ADDR_W(ADDR_W), .DATA_W(DATA_W),
                  .BOUNDARY(BND_R), .MAX_BEATS(MAXB_R)) dut4k (
    .clk(clk), .rst_n(rst_n),
    .start(start), .addr(addr), .beats(beats), .burst_ack(burst_ack),
    .eot(eot),
    .busy(busy4), .bv(bv4), .baddr(baddr4), .blen(blen4), .bsize(),
    .bbeats(bbeats4), .bindex(bindex4), .remaining(),
    .done_pulse(done4), .err_pulse(), .err_code(),
    .n_start(), .n_burst(), .n_split_bound(), .n_split_len(), .n_done(),
    .n_unaligned(), .n_zero(), .n_restart()
  );

  always #5 clk = ~clk;

  integer errors = 0, checks = 0, steps = 0;
  integer k;

  // reach: aligned offset (64) x beat count (128)
  reg [0:0] reach [0:8191];
  integer   n_reach;

  task ck;
    input [255:0] nm;
    input [31:0]  got, exp;
    begin
      checks = checks + 1;
      if (got !== exp) begin
        errors = errors + 1;
        if (errors < 25)
          $display("FAIL t=%0t step=%0d %0s got=%0d exp=%0d",
                   $time, steps, nm, got, exp);
      end
    end
  endtask

  task fail; input [255:0] nm;
    begin
      errors = errors + 1;
      if (errors < 25) $display("FAIL t=%0t step=%0d %0s", $time, steps, nm);
    end
  endtask

  task tickc;
    begin
      @(posedge clk); #1;
      steps = steps + 1;
    end
  endtask

  // ---- The six properties, checked on the burst being offered. ----
  task check_burst;
    input [ADDR_W-1:0] a;
    input [15:0]       nb;
    input [7:0]        ln;
    input integer      bnd;
    input integer      maxb;
    input [255:0]      who;
    reg [31:0] off;
    begin
      // 3. at least one beat
      checks = checks + 1;
      if (nb == 16'd0) begin
        errors = errors + 1;
        if (errors < 25) $display("FAIL %0s: a zero-beat burst", who);
      end
      // 2. the AXI4 INCR limit
      checks = checks + 1;
      if (nb > maxb[15:0]) begin
        errors = errors + 1;
        if (errors < 25)
          $display("FAIL %0s: %0d beats exceeds the %0d-beat limit",
                   who, nb, maxb);
      end
      // 4. AWLEN is beats minus one
      checks = checks + 1;
      if (ln !== (nb[7:0] - 8'd1)) begin
        errors = errors + 1;
        if (errors < 25)
          $display("FAIL %0s: AWLEN %0d for %0d beats", who, ln, nb);
      end
      // 1. THE RULE. The burst must not cross the boundary.
      off = a % bnd;
      checks = checks + 1;
      if ((off + nb * BPB) > bnd[31:0]) begin
        errors = errors + 1;
        if (errors < 25)
          $display("FAIL %0s: burst at 0x%0h (offset %0d) of %0d beats crosses the %0d-byte boundary",
                   who, a, off, nb, bnd);
      end
    end
  endtask

  // Run one whole transfer, checking every burst and the tiling.
  task run_xfer;
    input [ADDR_W-1:0] a0;
    input [15:0]       nb;
    integer            seen;
    reg [ADDR_W-1:0]   expect_addr;
    integer            guard;
    integer            max_ok;
    reg                stuck;
    begin
      start = 1'b1; burst_ack = 1'b0; eot = 1'b0; addr = a0; beats = nb;
      tickc;
      start = 1'b0;
      seen        = 0;
      expect_addr = a0;
      guard       = 0;
      // ---- PROPERTY 7: a bound on the NUMBER of bursts. ----
      //
      // Each limit can only cut a transfer so many times. Within one
      // boundary window the beat limit gives ceil(beats / MAX_BEATS) bursts,
      // and the transfer spans a known number of windows -- so a correct
      // splitter cannot need more than the sum of the two.
      //
      // It is a real property and it is also what keeps the suite usable: a
      // mutation that computes the distance to the boundary wrongly emits
      // ONE-BEAT bursts, which is correct-looking, terminating, and turns an
      // eight-second run into a ten-minute one. Bounding the loop at 4096
      // catches a design that hangs; bounding it at what the limits allow
      // catches a design that crawls.
      max_ok = ((nb + MAXB_S - 1) / MAXB_S)
             + (((a0 % BND_S) + nb * BPB + BND_S - 1) / BND_S) + 1;
      stuck = 1'b0;
      while (busy && (guard < max_ok) && !stuck) begin
        guard = guard + 1;
        check_burst(baddr, bbeats, blen, BND_S, MAXB_S, "scaled");
        // ---- FAIL FAST on a design that cannot progress. ----
        //
        // A zero-beat burst is not just wrong, it is unadvanceable: the
        // address never moves and the remaining count never falls, so the
        // loop below would run its full guard of 4096 for every one of the
        // 8192 transfers. One mutation then reports NINETY-SIX MILLION
        // failures and the other six are invisible beside it -- and the run
        // takes minutes instead of seconds.
        //
        // A mutation score is only comparable if no mutation is allowed to
        // spin. Bound the loop AND leave it on the first unadvanceable
        // burst.
        if (bbeats == 16'd0) stuck = 1'b1;
        // The 4 KB instance needs fewer splits for the same transfer, so it
        // finishes first and its outputs stop meaning anything. Checking a
        // burst that is not being offered is checking the idle value of a
        // bus, which is a property of the reset state and not of the
        // splitter.
        if (busy4)
          check_burst(baddr4, bbeats4, blen4, BND_R, MAXB_R, "real 4K");
        // 5. contiguous: no gap and no overlap between consecutive bursts
        checks = checks + 1;
        if (baddr !== expect_addr) begin
          errors = errors + 1;
          if (errors < 25)
            $display("FAIL burst %0d at 0x%0h, expected 0x%0h",
                     bindex, baddr, expect_addr);
        end
        expect_addr = baddr + bbeats * BPB;
        seen        = seen + bbeats;
        burst_ack = 1'b1;
        tickc;
        burst_ack = 1'b0;
      end
      // 6. THE TILING. Everything asked for was delivered, once.
      checks = checks + 1;
      if (!stuck && (seen != nb)) begin
        errors = errors + 1;
        if (errors < 25)
          $display("FAIL addr=0x%0h beats=%0d: delivered %0d", a0, nb, seen);
      end
      checks = checks + 1;
      if (guard >= max_ok) begin
        errors = errors + 1;
        if (errors < 25)
          $display("FAIL addr=0x%0h beats=%0d took %0d bursts; the limits allow at most %0d",
                   a0, nb, guard, max_ok - 1);
      end
      if (stuck) fail("a zero-beat burst: the transfer cannot progress");
      // ---- Leave the DUT clean for the next case. ----
      //
      // A transfer that was abandoned leaves the design BUSY, and every
      // subsequent descriptor is then refused as a restart -- so one failing
      // case reports itself 8192 more times under a different name, and the
      // real first failure is buried. Resetting here costs nothing on a
      // passing run, where the design is already idle.
      if (busy) reset_all;
    end
  endtask

  task reset_all;
    begin
      start = 1'b0; burst_ack = 1'b0; eot = 1'b0;
      rst_n = 1'b0;
      @(posedge clk); #1;
      rst_n = 1'b1;
      @(negedge clk);
    end
  endtask

  integer off, nb, i, w, base;
  integer max_bursts, tot_bursts;
  integer n_unal, n_zero_cases, n_rst;

  initial begin
    for (k = 0; k < 8192; k = k + 1) reach[k] = 1'b0;
    max_bursts = 0; tot_bursts = 0;
    n_unal = 0; n_zero_cases = 0; n_rst = 0;

    repeat (3) @(posedge clk);
    rst_n = 1'b1;
    @(negedge clk);

    // ================= PHASE 1 -- every offset x every length ============
    //
    // 64 aligned offsets across one boundary window, and every beat count
    // from 1 to two windows' worth. The bursts of every one of the 8192
    // transfers are checked against all six properties.
    for (off = 0; off < BND_S; off = off + BPB)
      for (nb = 1; nb <= 128; nb = nb + 1) begin
        run_xfer(32'h0001_0000 + off[31:0], nb[15:0]);
        reach[(off / BPB) * 128 + (nb - 1)] = 1'b1;
        if (n_burst - base > max_bursts) max_bursts = n_burst - base;
        base = n_burst;
      end

    // ================= PHASE 2 -- the worked example, at 4 KB ============
    //
    // The case from the header, driven against the instance with the real
    // AXI numbers: a buffer 256 bytes below a 4 KB boundary, 256 beats of 4
    // bytes. It must come out as 64 beats and then 192, and the first burst
    // must end exactly on the boundary.
    reset_all;
    start = 1'b1; addr = 32'h0000_1F00; beats = 16'd256; eot = 1'b0;
    tickc;
    start = 1'b0;
    if (bbeats4 !== 16'd64) begin
      errors = errors + 1;
      $display("FAIL 0x1F00: first burst is %0d beats, expected 64", bbeats4);
    end
    if ((baddr4 + bbeats4 * BPB) !== 32'h0000_2000) begin
      errors = errors + 1;
      $display("FAIL 0x1F00: the first burst does not end on the boundary");
    end
    burst_ack = 1'b1; tickc; burst_ack = 1'b0;
    if (baddr4 !== 32'h0000_2000) begin
      errors = errors + 1;
      $display("FAIL 0x1F00: the second burst starts at 0x%0h", baddr4);
    end
    if (bbeats4 !== 16'd192) begin
      errors = errors + 1;
      $display("FAIL 0x1F00: second burst is %0d beats, expected 192",
               bbeats4);
    end
    burst_ack = 1'b1; tickc; burst_ack = 1'b0;
    if (busy4) begin
      errors = errors + 1;
      $display("FAIL 0x1F00: the transfer did not finish in two bursts");
    end

    // ...and a buffer that IS 4 KB aligned needs no split at all.
    reset_all;
    start = 1'b1; addr = 32'h0000_2000; beats = 16'd256;
    tickc;
    start = 1'b0;
    if (bbeats4 !== 16'd256) begin
      errors = errors + 1;
      $display("FAIL aligned 256 beats split into %0d", bbeats4);
    end
    burst_ack = 1'b1; tickc; burst_ack = 1'b0;
    if (busy4) begin
      errors = errors + 1;
      $display("FAIL an aligned 256-beat transfer took more than one burst");
    end

    // ================= PHASE 3 -- the two limits are DIFFERENT ===========
    //
    // A long, perfectly aligned transfer is split by the beat limit and not
    // by the boundary. Counting them together loses the distinction between
    // "this buffer is badly aligned" and "this buffer is simply large",
    // which are different conversations with whoever allocates them.
    reset_all;
    base = n_split_bound;
    k    = n_split_len;
    run_xfer(32'h0002_0000, 16'd64);      // aligned; 64 beats, MAXB_S = 16
    if (n_split_len - k != 3) begin
      errors = errors + 1;
      $display("FAIL aligned long transfer: %0d length splits, expected 3",
               n_split_len - k);
    end
    if (n_split_bound != base) begin
      errors = errors + 1;
      $display("FAIL aligned long transfer produced a boundary split");
    end
    // ...and a short transfer that straddles a boundary is split by the
    // boundary and not by the length.
    base = n_split_bound;
    k    = n_split_len;
    run_xfer(32'h0002_00F8, 16'd4);       // 8 bytes below a 256-byte boundary
    if (n_split_bound - base != 1) begin
      errors = errors + 1;
      $display("FAIL straddling transfer: %0d boundary splits, expected 1",
               n_split_bound - base);
    end
    if (n_split_len != k) begin
      errors = errors + 1;
      $display("FAIL straddling transfer produced a length split");
    end

    // ================= PHASE 4 -- the rejections, EXHAUSTIVELY ============
    //
    // Three things must be refused, and each one is refused for a reason that
    // is quantified over something: every misaligned offset, every address,
    // every point in a running transfer. The first version of this phase drove
    // one case of each and the two mutations that accept them died on THREE
    // and FOUR checks -- correct, and one phase reordering from zero.
    //
    // An INCR burst of this size must start on a beat boundary, so every
    // non-zero offset within a beat is a rejection: BPB - 1 of them, at four
    // different base addresses.
    n_unal = 0;
    for (i = 0; i < 4; i = i + 1)
      for (off = 1; off < BPB; off = off + 1) begin
        reset_all;
        base = n_unaligned;
        start = 1'b1; eot = 1'b0;
        addr  = 32'h0003_0000 + (i[31:0] << 8) + off[31:0];
        beats = 16'd8;
        tickc;
        start = 1'b0;
        if (n_unaligned != base + 1) begin
          errors = errors + 1;
          $display("FAIL offset %0d at base %0d was accepted", off, i);
        end
        // ...and nothing started: no burst is offered and no address latched.
        if (busy) begin
          errors = errors + 1;
          $display("FAIL offset %0d started a transfer", off);
        end
        if (bv) begin
          errors = errors + 1;
          $display("FAIL offset %0d offered a burst", off);
        end
        if (err_code !== E_UNALIGNED) begin
          errors = errors + 1;
          $display("FAIL offset %0d reported code %0d", off, err_code);
        end
        n_unal = n_unal + 1;
      end
    if (n_unal != 4 * (BPB - 1)) begin
      errors = errors + 1;
      $display("FAIL unaligned cases %0d, expected %0d", n_unal, 4 * (BPB - 1));
    end

    // ...and a zero-beat descriptor, at every one of those base addresses.
    // AXI has no encoding for it: `beats - 1` is 0xFFFF, so accepting it
    // issues 256 beats of whatever was in the buffer.
    n_zero_cases = 0;
    for (i = 0; i < 4; i = i + 1) begin
      reset_all;
      base = n_zero;
      start = 1'b1; eot = 1'b0;
      addr  = 32'h0004_0000 + (i[31:0] << 12);
      beats = 16'd0;
      tickc;
      start = 1'b0;
      if (n_zero != base + 1) begin
        errors = errors + 1;
        $display("FAIL a zero-beat descriptor at base %0d was accepted", i);
      end
      if (busy || bv) begin
        errors = errors + 1;
        $display("FAIL a zero-beat descriptor started a transfer");
      end
      if (err_code !== E_ZERO) begin
        errors = errors + 1;
        $display("FAIL zero-beat reported code %0d", err_code);
      end
      // ...and an aligned, non-zero descriptor at the same address IS
      // accepted, so the rejection is about the beat count and not the
      // address.
      start = 1'b1; beats = 16'd8;
      tickc;
      start = 1'b0;
      if (!busy) begin
        errors = errors + 1;
        $display("FAIL a valid descriptor at base %0d was refused", i);
      end
      burst_ack = 1'b1; tickc; burst_ack = 1'b0;
      n_zero_cases = n_zero_cases + 1;
    end
    if (n_zero_cases != 4) begin
      errors = errors + 1;
      $display("FAIL zero-beat cases %0d, expected 4", n_zero_cases);
    end

    // ...and a restart, at every burst index of a multi-burst transfer. The
    // running descriptor must be untouched: its address, its remaining count
    // and its burst index all survive.
    n_rst = 0;
    for (i = 0; i < 4; i = i + 1) begin
      reset_all;
      start = 1'b1; eot = 1'b0;
      addr = 32'h0005_0000; beats = 16'd64;    // 4 bursts at MAXB_S = 16
      tickc;
      start = 1'b0;
      for (nb = 0; nb < i; nb = nb + 1) begin
        burst_ack = 1'b1; tickc; burst_ack = 1'b0;
      end
      base = n_restart;
      w    = baddr;
      nb   = remaining;
      start = 1'b1; addr = 32'h0006_0000; beats = 16'd8;
      tickc;
      start = 1'b0;
      if (n_restart != base + 1) begin
        errors = errors + 1;
        $display("FAIL a restart at burst %0d was not reported", i);
      end
      if (baddr !== w[31:0]) begin
        errors = errors + 1;
        $display("FAIL a restart at burst %0d moved the address", i);
      end
      if (remaining !== nb[15:0]) begin
        errors = errors + 1;
        $display("FAIL a restart at burst %0d changed the remaining count", i);
      end
      if (bindex !== i[15:0]) begin
        errors = errors + 1;
        $display("FAIL a restart at burst %0d moved the burst index", i);
      end
      // ...and the original transfer still completes. BOUNDED: an
      // unbounded `while (busy)` in a testbench is an infinite loop the
      // moment a mutation stops the design advancing, and the run never
      // reaches the summary that would have told you which mutation.
      off = 0;
      while (busy && (off < 4096)) begin
        burst_ack = 1'b1; tickc; burst_ack = 1'b0;
        off = off + 1;
      end
      if (busy) begin
        errors = errors + 1;
        if (errors < 25)
          $display("FAIL the transfer after a restart at burst %0d never finished", i);
        reset_all;
      end
      n_rst = n_rst + 1;
    end
    if (n_rst != 4) begin
      errors = errors + 1;
      $display("FAIL restart cases %0d, expected 4", n_rst);
    end

    // The random phase is switchable, because a mutation score is only
    // interesting once it is DECOMPOSED. The directed phases already reach
    // every situation the exhaustiveness proof requires, so nothing in that
    // claim depends on it.
`ifndef DIRECTED_ONLY
    // ================= PHASE 5 -- random =================================
    reset_all;
    for (i = 0; i < 4000; i = i + 1) begin
      w = ($unsigned($random) % 4096) & 32'hFFFF_FFFC;   // aligned
      run_xfer(32'h0010_0000 + w[31:0],
               ($unsigned($random) % 400) + 1);
    end

`endif

    // ================= the exhaustiveness proof ==========================
    n_reach = 0;
    for (k = 0; k < 8192; k = k + 1) n_reach = n_reach + reach[k];
    if (n_reach != 8192) begin
      errors = errors + 1;
      $display("FAIL offset x length reach %0d/8192", n_reach);
    end

    $display("steps=%0d checks=%0d reach=%0d/8192 errors=%0d",
             steps, checks, n_reach, errors);
    // The counters below cover the random phase only: each directed phase
    // resets the DUT so that its measurement starts from a known state, and
    // a counter that spans a reset is a counter nobody can interpret.
    $display("[random phase] start=%0d burst=%0d done=%0d",
             n_start, n_burst, n_done);
    $display("[random phase] split_boundary=%0d split_length=%0d",
             n_split_bound, n_split_len);
    $display("%0s: %0d errors in %0d checks",
             (errors == 0) ? "PASS" : "FAIL", errors, checks);
    $finish;
  end
endmodule

`timescale 1ns/1ps
// Testbench for usb_axi_burst.
//
// THE CHECKS ARE PROTOCOL PROPERTIES, NOT EXPECTED VALUES
//
// A burst splitter is one of the few blocks where the specification states
// the acceptance criteria directly, so the testbench asserts those rather
// than a table of expected outputs:
//
//   1. no burst crosses a BOUNDARY-byte address boundary
//   2. no burst exceeds MAX_BEATS beats
//   3. every burst carries at least one beat
//   4. AWLEN is the beat count MINUS ONE, every time
//   5. consecutive bursts are contiguous -- no gap, no overlap
//   6. the beats delivered sum to exactly the beats requested
//
// Property 1 is the one this chapter is about and property 6 is the one that
// catches a splitter which obeys property 1 by dropping data.
//
// THE EXHAUSTIVE CLAIM
//
// The splitting arithmetic depends on two numbers: where in the boundary
// window the buffer starts, and how many beats it is. So both are swept, all
// the way across, as a product:
//
//     every aligned offset in a boundary window   (64)
//   x every beat count from 1 to 2 windows' worth (128)
//   = 8192 transfers, every burst of every one checked
//
// The DUT is instantiated with a SCALED boundary so that product is
// tractable. A second instance carries the real 4096/256 values and is
// driven by the directed cases, because a parameter that is never changed is
// a constant with extra steps -- chapter 25.4's retry budget again.
module tb_ab_sv;
  import usb_axi_pkg::*;

  localparam int ADDR_W = 32;
  localparam int DATA_W = 32;
  localparam int BPB    = DATA_W / 8;

  // the scaled instance, for the exhaustive sweep
  localparam int BND_S  = 256;
  localparam int MAXB_S = 16;

  // the real instance, for the directed cases
  localparam int BND_R  = 4096;
  localparam int MAXB_R = 256;

  logic               clk = 1'b0, rst_n = 1'b0;
  logic               start = 1'b0, burst_ack = 1'b0, eot = 1'b0;
  logic [ADDR_W-1:0]  addr = '0;
  logic [15:0]        beats = 16'd0;

  logic               busy, bv, done_pulse, err_pulse;
  logic [ADDR_W-1:0]  baddr;
  logic [7:0]         blen;
  logic [2:0]         bsize;
  logic [15:0]        bbeats, bindex, remaining;
  axi_err_e           err_code;
  logic [31:0] n_start, n_burst, n_split_bound, n_split_len, n_done,
               n_unaligned, n_zero, n_restart;

  usb_axi_burst #(.ADDR_W(ADDR_W), .DATA_W(DATA_W),
                  .BOUNDARY(BND_S), .MAX_BEATS(MAXB_S)) dut (
    .clk(clk), .rst_n(rst_n),
    .start(start), .addr(addr), .beats(beats), .burst_ack(burst_ack),
    .eot(eot),
    .busy(busy), .bv(bv), .baddr(baddr), .blen(blen), .bsize(bsize),
    .bbeats(bbeats), .bindex(bindex), .remaining(remaining),
    .done_pulse(done_pulse), .err_pulse(err_pulse), .err_code(err_code),
    .n_start(n_start), .n_burst(n_burst), .n_split_bound(n_split_bound),
    .n_split_len(n_split_len), .n_done(n_done),
    .n_unaligned(n_unaligned), .n_zero(n_zero), .n_restart(n_restart)
  );

  // ---- The same design with the REAL AXI numbers. ----
  //
  // Driven by the same stimulus and checked against the same properties. A
  // splitter whose boundary is hard-coded to whatever the test used passes
  // everything above and corrupts memory on the first real SoC.
  logic              busy4, bv4, done4;
  logic [ADDR_W-1:0] baddr4;
  logic [7:0]        blen4;
  logic [15:0]       bbeats4, bindex4;

  usb_axi_burst #(.ADDR_W(ADDR_W), .DATA_W(DATA_W),
                  .BOUNDARY(BND_R), .MAX_BEATS(MAXB_R)) dut4k (
    .clk(clk), .rst_n(rst_n),
    .start(start), .addr(addr), .beats(beats), .burst_ack(burst_ack),
    .eot(eot),
    .busy(busy4), .bv(bv4), .baddr(baddr4), .blen(blen4), .bsize(),
    .bbeats(bbeats4), .bindex(bindex4), .remaining(),
    .done_pulse(done4), .err_pulse(), .err_code(),
    .n_start(), .n_burst(), .n_split_bound(), .n_split_len(), .n_done(),
    .n_unaligned(), .n_zero(), .n_restart()
  );

  always #5 clk = ~clk;

  int errors = 0, checks = 0, steps = 0;
  int k;

  // reach: aligned offset (64) x beat count (128)
  bit reach [8192];
  int n_reach;

  task automatic ck(string nm, int unsigned got, int unsigned exp);
    checks++;
    if (got !== exp) begin
      errors++;
      if (errors < 25)
        $display("FAIL t=%0t step=%0d %0s got=%0d exp=%0d",
                 $time, steps, nm, got, exp);
    end
  endtask

  task automatic fail(string nm);
    errors++;
    if (errors < 25) $display("FAIL t=%0t step=%0d %0s", $time, steps, nm);
  endtask

  task automatic tickc;
    begin
      @(posedge clk); #1;
      steps = steps + 1;
    end
  endtask

  // ---- The six properties, checked on the burst being offered. ----
  task automatic check_burst(logic [ADDR_W-1:0] a, logic [15:0] nb,
                             logic [7:0] ln, int bnd, int maxb, string who);
    logic [31:0] off;
    begin
      // 3. at least one beat
      checks = checks + 1;
      if (nb == 16'd0) begin
        errors = errors + 1;
        if (errors < 25) $display("FAIL %0s: a zero-beat burst", who);
      end
      // 2. the AXI4 INCR limit
      checks = checks + 1;
      if (nb > 16'(maxb)) begin
        errors = errors + 1;
        if (errors < 25)
          $display("FAIL %0s: %0d beats exceeds the %0d-beat limit",
                   who, nb, maxb);
      end
      // 4. AWLEN is beats minus one
      checks = checks + 1;
      if (ln !== (nb[7:0] - 8'd1)) begin
        errors = errors + 1;
        if (errors < 25)
          $display("FAIL %0s: AWLEN %0d for %0d beats", who, ln, nb);
      end
      // 1. THE RULE. The burst must not cross the boundary.
      off = a % 32'(bnd);
      checks = checks + 1;
      if ((off + 32'(nb) * BPB) > 32'(bnd)) begin
        errors = errors + 1;
        if (errors < 25)
          $display("FAIL %0s: burst at 0x%0h (offset %0d) of %0d beats crosses the %0d-byte boundary",
                   who, a, off, nb, bnd);
      end
    end
  endtask

  // Run one whole transfer, checking every burst and the tiling.
  task run_xfer;
    input [ADDR_W-1:0] a0;
    input [15:0]       nb;
    integer            seen;
    reg [ADDR_W-1:0]   expect_addr;
    integer            guard;
    int                max_ok;
    reg                stuck;
    begin
      start = 1'b1; burst_ack = 1'b0; eot = 1'b0; addr = a0; beats = nb;
      tickc;
      start = 1'b0;
      seen        = 0;
      expect_addr = a0;
      guard       = 0;
      // ---- PROPERTY 7: a bound on the NUMBER of bursts. ----
      //
      // Each limit can only cut a transfer so many times. Within one
      // boundary window the beat limit gives ceil(beats / MAX_BEATS) bursts,
      // and the transfer spans a known number of windows -- so a correct
      // splitter cannot need more than the sum of the two.
      //
      // It is a real property and it is also what keeps the suite usable: a
      // mutation that computes the distance to the boundary wrongly emits
      // ONE-BEAT bursts, which is correct-looking, terminating, and turns an
      // eight-second run into a ten-minute one. Bounding the loop at 4096
      // catches a design that hangs; bounding it at what the limits allow
      // catches a design that crawls.
      max_ok = ((int'(nb) + MAXB_S - 1) / MAXB_S)
             + (((int'(a0) % BND_S) + int'(nb) * BPB + BND_S - 1) / BND_S) + 1;
      stuck = 1'b0;
      while (busy && (guard < max_ok) && !stuck) begin
        guard = guard + 1;
        check_burst(baddr, bbeats, blen, BND_S, MAXB_S, "scaled");
        // ---- FAIL FAST on a design that cannot progress. ----
        //
        // A zero-beat burst is not just wrong, it is unadvanceable: the
        // address never moves and the remaining count never falls, so the
        // loop below would run its full guard of 4096 for every one of the
        // 8192 transfers. One mutation then reports NINETY-SIX MILLION
        // failures and the other six are invisible beside it -- and the run
        // takes minutes instead of seconds.
        //
        // A mutation score is only comparable if no mutation is allowed to
        // spin. Bound the loop AND leave it on the first unadvanceable
        // burst.
        if (bbeats == 16'd0) stuck = 1'b1;
        // The 4 KB instance needs fewer splits for the same transfer, so it
        // finishes first and its outputs stop meaning anything. Checking a
        // burst that is not being offered is checking the idle value of a
        // bus, which is a property of the reset state and not of the
        // splitter.
        if (busy4)
          check_burst(baddr4, bbeats4, blen4, BND_R, MAXB_R, "real 4K");
        // 5. contiguous: no gap and no overlap between consecutive bursts
        checks = checks + 1;
        if (baddr !== expect_addr) begin
          errors = errors + 1;
          if (errors < 25)
            $display("FAIL burst %0d at 0x%0h, expected 0x%0h",
                     bindex, baddr, expect_addr);
        end
        expect_addr = baddr + ADDR_W'(32'(bbeats) * BPB);
        seen        = seen + int'(bbeats);
        burst_ack = 1'b1;
        tickc;
        burst_ack = 1'b0;
      end
      // 6. THE TILING. Everything asked for was delivered, once.
      checks = checks + 1;
      if (!stuck && (seen != nb)) begin
        errors = errors + 1;
        if (errors < 25)
          $display("FAIL addr=0x%0h beats=%0d: delivered %0d", a0, nb, seen);
      end
      checks = checks + 1;
      if (guard >= max_ok) begin
        errors = errors + 1;
        if (errors < 25)
          $display("FAIL addr=0x%0h beats=%0d took %0d bursts; the limits allow at most %0d",
                   a0, nb, guard, max_ok - 1);
      end
      if (stuck) fail("a zero-beat burst: the transfer cannot progress");
      // ---- Leave the DUT clean for the next case. ----
      //
      // A transfer that was abandoned leaves the design BUSY, and every
      // subsequent descriptor is then refused as a restart -- so one failing
      // case reports itself 8192 more times under a different name, and the
      // real first failure is buried. Resetting here costs nothing on a
      // passing run, where the design is already idle.
      if (busy) reset_all;
    end
  endtask

  task automatic reset_all;
    begin
      start = 1'b0; burst_ack = 1'b0; eot = 1'b0;
      rst_n = 1'b0;
      @(posedge clk); #1;
      rst_n = 1'b1;
      @(negedge clk);
    end
  endtask

  int off, nb, i, w, base;
  int max_bursts, tot_bursts;
  integer n_unal, n_zero_cases, n_rst;

  initial begin
    foreach (reach[q]) reach[q] = 1'b0;
    max_bursts = 0; tot_bursts = 0;
    n_unal = 0; n_zero_cases = 0; n_rst = 0;

    repeat (3) @(posedge clk);
    rst_n = 1'b1;
    @(negedge clk);

    // ================= PHASE 1 -- every offset x every length ============
    //
    // 64 aligned offsets across one boundary window, and every beat count
    // from 1 to two windows' worth. The bursts of every one of the 8192
    // transfers are checked against all six properties.
    for (off = 0; off < BND_S; off = off + BPB)
      for (nb = 1; nb <= 128; nb = nb + 1) begin
        run_xfer(32'h0001_0000 + 32'(off), 16'(nb));
        reach[(off / BPB) * 128 + (nb - 1)] = 1'b1;
        if (int'(n_burst) - base > max_bursts) max_bursts = int'(n_burst) - base;
        base = int'(n_burst);
      end

    // ================= PHASE 2 -- the worked example, at 4 KB ============
    //
    // The case from the header, driven against the instance with the real
    // AXI numbers: a buffer 256 bytes below a 4 KB boundary, 256 beats of 4
    // bytes. It must come out as 64 beats and then 192, and the first burst
    // must end exactly on the boundary.
    reset_all;
    start = 1'b1; addr = 32'h0000_1F00; beats = 16'd256; eot = 1'b0;
    tickc;
    start = 1'b0;
    if (bbeats4 !== 16'd64) begin
      errors = errors + 1;
      $display("FAIL 0x1F00: first burst is %0d beats, expected 64", bbeats4);
    end
    if ((baddr4 + bbeats4 * BPB) !== 32'h0000_2000) begin
      errors = errors + 1;
      $display("FAIL 0x1F00: the first burst does not end on the boundary");
    end
    burst_ack = 1'b1; tickc; burst_ack = 1'b0;
    if (baddr4 !== 32'h0000_2000) begin
      errors = errors + 1;
      $display("FAIL 0x1F00: the second burst starts at 0x%0h", baddr4);
    end
    if (bbeats4 !== 16'd192) begin
      errors = errors + 1;
      $display("FAIL 0x1F00: second burst is %0d beats, expected 192",
               bbeats4);
    end
    burst_ack = 1'b1; tickc; burst_ack = 1'b0;
    if (busy4) begin
      errors = errors + 1;
      $display("FAIL 0x1F00: the transfer did not finish in two bursts");
    end

    // ...and a buffer that IS 4 KB aligned needs no split at all.
    reset_all;
    start = 1'b1; addr = 32'h0000_2000; beats = 16'd256;
    tickc;
    start = 1'b0;
    if (bbeats4 !== 16'd256) begin
      errors = errors + 1;
      $display("FAIL aligned 256 beats split into %0d", bbeats4);
    end
    burst_ack = 1'b1; tickc; burst_ack = 1'b0;
    if (busy4) begin
      errors = errors + 1;
      $display("FAIL an aligned 256-beat transfer took more than one burst");
    end

    // ================= PHASE 3 -- the two limits are DIFFERENT ===========
    //
    // A long, perfectly aligned transfer is split by the beat limit and not
    // by the boundary. Counting them together loses the distinction between
    // "this buffer is badly aligned" and "this buffer is simply large",
    // which are different conversations with whoever allocates them.
    reset_all;
    base = int'(n_split_bound);
    k    = int'(n_split_len);
    run_xfer(32'h0002_0000, 16'd64);      // aligned; 64 beats, MAXB_S = 16
    if (int'(n_split_len) - k != 3) begin
      errors = errors + 1;
      $display("FAIL aligned long transfer: %0d length splits, expected 3",
               int'(n_split_len) - k);
    end
    if (int'(n_split_bound) != base) begin
      errors = errors + 1;
      $display("FAIL aligned long transfer produced a boundary split");
    end
    // ...and a short transfer that straddles a boundary is split by the
    // boundary and not by the length.
    base = int'(n_split_bound);
    k    = int'(n_split_len);
    run_xfer(32'h0002_00F8, 16'd4);       // 8 bytes below a 256-byte boundary
    if (int'(n_split_bound) - base != 1) begin
      errors = errors + 1;
      $display("FAIL straddling transfer: %0d boundary splits, expected 1",
               int'(n_split_bound) - base);
    end
    if (int'(n_split_len) != k) begin
      errors = errors + 1;
      $display("FAIL straddling transfer produced a length split");
    end

    // ================= PHASE 4 -- the rejections, EXHAUSTIVELY ============
    //
    // Three things must be refused, and each one is refused for a reason that
    // is quantified over something: every misaligned offset, every address,
    // every point in a running transfer. The first version of this phase drove
    // one case of each and the two mutations that accept them died on THREE
    // and FOUR checks -- correct, and one phase reordering from zero.
    //
    // An INCR burst of this size must start on a beat boundary, so every
    // non-zero offset within a beat is a rejection: BPB - 1 of them, at four
    // different base addresses.
    n_unal = 0;
    for (i = 0; i < 4; i = i + 1)
      for (off = 1; off < BPB; off = off + 1) begin
        reset_all;
        base = int'(n_unaligned);
        start = 1'b1; eot = 1'b0;
        addr  = 32'h0003_0000 + 32'(i << 8) + 32'(off);
        beats = 16'd8;
        tickc;
        start = 1'b0;
        if (int'(n_unaligned) != base + 1) begin
          errors = errors + 1;
          $display("FAIL offset %0d at base %0d was accepted", off, i);
        end
        // ...and nothing started: no burst is offered and no address latched.
        if (busy) begin
          errors = errors + 1;
          $display("FAIL offset %0d started a transfer", off);
        end
        if (bv) begin
          errors = errors + 1;
          $display("FAIL offset %0d offered a burst", off);
        end
        if (err_code !== E_UNALIGNED) begin
          errors = errors + 1;
          $display("FAIL offset %0d reported code %0d", off, err_code);
        end
        n_unal = n_unal + 1;
      end
    if (n_unal != 4 * (BPB - 1)) begin
      errors = errors + 1;
      $display("FAIL unaligned cases %0d, expected %0d", n_unal, 4 * (BPB - 1));
    end

    // ...and a zero-beat descriptor, at every one of those base addresses.
    // AXI has no encoding for it: `beats - 1` is 0xFFFF, so accepting it
    // issues 256 beats of whatever was in the buffer.
    n_zero_cases = 0;
    for (i = 0; i < 4; i = i + 1) begin
      reset_all;
      base = int'(n_zero);
      start = 1'b1; eot = 1'b0;
      addr  = 32'h0004_0000 + 32'(i << 12);
      beats = 16'd0;
      tickc;
      start = 1'b0;
      if (int'(n_zero) != base + 1) begin
        errors = errors + 1;
        $display("FAIL a zero-beat descriptor at base %0d was accepted", i);
      end
      if (busy || bv) begin
        errors = errors + 1;
        $display("FAIL a zero-beat descriptor started a transfer");
      end
      if (err_code !== E_ZERO) begin
        errors = errors + 1;
        $display("FAIL zero-beat reported code %0d", err_code);
      end
      // ...and an aligned, non-zero descriptor at the same address IS
      // accepted, so the rejection is about the beat count and not the
      // address.
      start = 1'b1; beats = 16'd8;
      tickc;
      start = 1'b0;
      if (!busy) begin
        errors = errors + 1;
        $display("FAIL a valid descriptor at base %0d was refused", i);
      end
      burst_ack = 1'b1; tickc; burst_ack = 1'b0;
      n_zero_cases = n_zero_cases + 1;
    end
    if (n_zero_cases != 4) begin
      errors = errors + 1;
      $display("FAIL zero-beat cases %0d, expected 4", n_zero_cases);
    end

    // ...and a restart, at every burst index of a multi-burst transfer. The
    // running descriptor must be untouched: its address, its remaining count
    // and its burst index all survive.
    n_rst = 0;
    for (i = 0; i < 4; i = i + 1) begin
      reset_all;
      start = 1'b1; eot = 1'b0;
      addr = 32'h0005_0000; beats = 16'd64;    // 4 bursts at MAXB_S = 16
      tickc;
      start = 1'b0;
      for (nb = 0; nb < i; nb = nb + 1) begin
        burst_ack = 1'b1; tickc; burst_ack = 1'b0;
      end
      base = int'(n_restart);
      w    = int'(baddr);
      nb   = int'(remaining);
      start = 1'b1; addr = 32'h0006_0000; beats = 16'd8;
      tickc;
      start = 1'b0;
      if (int'(n_restart) != base + 1) begin
        errors = errors + 1;
        $display("FAIL a restart at burst %0d was not reported", i);
      end
      if (baddr !== 32'(w)) begin
        errors = errors + 1;
        $display("FAIL a restart at burst %0d moved the address", i);
      end
      if (remaining !== 16'(nb)) begin
        errors = errors + 1;
        $display("FAIL a restart at burst %0d changed the remaining count", i);
      end
      if (bindex !== 16'(i)) begin
        errors = errors + 1;
        $display("FAIL a restart at burst %0d moved the burst index", i);
      end
      // ...and the original transfer still completes. BOUNDED: an
      // unbounded `while (busy)` in a testbench is an infinite loop the
      // moment a mutation stops the design advancing, and the run never
      // reaches the summary that would have told you which mutation.
      off = 0;
      while (busy && (off < 4096)) begin
        burst_ack = 1'b1; tickc; burst_ack = 1'b0;
        off = off + 1;
      end
      if (busy) begin
        errors = errors + 1;
        if (errors < 25)
          $display("FAIL the transfer after a restart at burst %0d never finished", i);
        reset_all;
      end
      n_rst = n_rst + 1;
    end
    if (n_rst != 4) begin
      errors = errors + 1;
      $display("FAIL restart cases %0d, expected 4", n_rst);
    end

    // The random phase is switchable, because a mutation score is only
    // interesting once it is DECOMPOSED. The directed phases already reach
    // every situation the exhaustiveness proof requires, so nothing in that
    // claim depends on it.
`ifndef DIRECTED_ONLY
    // ================= PHASE 5 -- random =================================
    reset_all;
    for (i = 0; i < 4000; i = i + 1) begin
      w = int'(($unsigned($random) % 4096) & 32'hFFFF_FFFC);   // aligned
      run_xfer(32'h0010_0000 + 32'(w),
               16'(($unsigned($random) % 400) + 1));
    end

`endif

    // ================= the exhaustiveness proof ==========================
    n_reach = 0;
    for (k = 0; k < 8192; k = k + 1) n_reach = n_reach + reach[k];
    if (n_reach != 8192) begin
      errors = errors + 1;
      $display("FAIL offset x length reach %0d/8192", n_reach);
    end

    $display("steps=%0d checks=%0d reach=%0d/8192 errors=%0d",
             steps, checks, n_reach, errors);
    // The counters below cover the random phase only: each directed phase
    // resets the DUT so that its measurement starts from a known state, and
    // a counter that spans a reset is a counter nobody can interpret.
    $display("[random phase] start=%0d burst=%0d done=%0d",
             n_start, n_burst, n_done);
    $display("[random phase] split_boundary=%0d split_length=%0d",
             n_split_bound, n_split_len);
    $display("%0s: %0d errors in %0d checks",
             (errors == 0) ? "PASS" : "FAIL", errors, checks);
    $finish;
  end
endmodule