The AXI protocol checker

`timescale 1ns/1ns
// axi_pkg.sv: the arithmetic of a burst (read-only).
// Every transfer n of a burst has an address and a set of byte lanes, computed from the start
// address, the burst length, the transfer size and the burst type exactly as the AXI specification
// defines them. The memory, the manager tasks and the checker all use these functions, so they
// never disagree about where a byte lands.
package axi_pkg;
  localparam logic [1:0] FIXED = 2'b00, INCR = 2'b01, WRAP = 2'b10;
  localparam logic [1:0] OKAY = 2'b00, EXOKAY = 2'b01, SLVERR = 2'b10, DECERR = 2'b11;

  function automatic string burst_name(input logic [1:0] b);
    case (b) FIXED: return "FIXED"; INCR: return "INCR"; WRAP: return "WRAP"; default: return "RESERVED"; endcase
  endfunction
  function automatic string resp_name(input logic [1:0] r);
    case (r) OKAY: return "OKAY"; EXOKAY: return "EXOKAY"; SLVERR: return "SLVERR"; default: return "DECERR"; endcase
  endfunction

  // Bytes in one transfer: 1, 2, 4, ... 128.
  function automatic int bytes_of(input logic [2:0] size);
    return 1 << size;
  endfunction

  // The address of transfer n (n counts from 0).
  //   transfer 0 uses the start address as given, aligned or not;
  //   later transfers use the start address aligned down to the transfer size, plus n transfers;
  //   a WRAP burst returns to its wrap boundary (the start aligned down to the whole burst) when
  //   it reaches the end of that window; a FIXED burst repeats the start address.
  function automatic int unsigned beat_addr(input int unsigned start, input int len, input logic [2:0] size,
                                            input logic [1:0] burst, input int n);
    int unsigned nb = 1 << size;
    int unsigned aligned = (start / nb) * nb;
    int unsigned window = nb * (len + 1);
    int unsigned boundary = (start / window) * window;
    int unsigned a;
    if (burst == FIXED || n == 0) return start;
    a = aligned + n * nb;
    if (burst == WRAP && a >= boundary + window) a = a - window;
    return a;
  endfunction

  // The byte lanes transfer n uses on a bus of bus_bytes bytes, packed as {upper, lower}.
  // Transfer 0 of an unaligned burst (and every transfer of a FIXED burst) uses only the lanes from
  // its address up to the end of its aligned transfer; every other transfer uses all the lanes of
  // its size.
  function automatic logic [15:0] beat_lanes(input int unsigned start, input int len, input logic [2:0] size,
                                             input logic [1:0] burst, input int n, input int bus_bytes);
    int unsigned nb = 1 << size;
    int unsigned a = beat_addr(start, len, size, burst, n);
    int unsigned aligned = (a / nb) * nb;
    int unsigned word = (a / bus_bytes) * bus_bytes;
    int lower = a - word;
    int upper = (n == 0 || burst == FIXED) ? (aligned + nb - 1 - word) : (lower + nb - 1);
    return {upper[7:0], lower[7:0]};
  endfunction

  // The strobe of transfer n: a 1 for every lane it uses (bit l is lane l).
  function automatic logic [63:0] beat_strb(input int unsigned start, input int len, input logic [2:0] size,
                                            input logic [1:0] burst, input int n, input int bus_bytes);
    logic [15:0] lanes = beat_lanes(start, len, size, burst, n, bus_bytes);
    logic [63:0] s = 0;
    for (int l = lanes[7:0]; l <= lanes[15:8]; l++) s[l] = 1'b1;
    return s;
  endfunction

  // True when the burst crosses a 4 KB boundary (only an INCR burst can).
  function automatic bit crosses_4k(input int unsigned start, input int len, input logic [2:0] size, input logic [1:0] burst);
    if (burst != INCR) return 0;
    return (beat_addr(start, len, size, burst, 0) / 4096) != ((beat_addr(start, len, size, burst, len) + (1 << size) - 1) / 4096);
  endfunction
endpackage

`timescale 1ns/1ns
// axi_mem.sv: an AXI4 subordinate with a byte-addressed memory behind it (read-only in this lesson).
// It accepts requests on AW and AR, write beats on W (before or after their AW), writes the bytes a
// burst addresses using the strobes, and answers on B and R after a latency. The switches below are
// plain variables: the stimulus sets them by name (mem.reorder = 1;) before it starts.
//   rd_latency, wr_latency   cycles from a request (or its last write beat) to its first response
//   slow_latency, slow_above addresses at or above slow_above answer after slow_latency instead
//   err_above                addresses at or above err_above get SLVERR (and are not written)
//   reorder                  answer transactions with DIFFERENT IDs as soon as each is ready;
//                            transactions with the same ID still answer in order
//   interleave               interleave the read data beats of ready transactions with different IDs
//   excl_on                  support exclusive access (one monitor per ID), else answer OKAY
//   posted                   apply a write to the memory only when its response is sent, so a read
//                            that arrives between the last beat and B still sees the old bytes
//   trace                    print every byte the memory writes
// Broken twins, each off by default: early_b (B before the last write beat and before AW),
// ignore_strobes (write every lane of the bus word), drop_hold (RDATA changes while RVALID waits
// for RREADY), reorder_same_id (a later transaction with the same ID may answer first),
// wrap_bug (a WRAP burst addressed like INCR).
module axi_mem #(parameter int DATA_W = 32, parameter int ID_W = 4, parameter int DEPTH = 65536) (
  input  logic              aclk,
  input  logic              aresetn,
  input  logic [ID_W-1:0]   awid,
  input  logic [31:0]       awaddr,
  input  logic [7:0]        awlen,
  input  logic [2:0]        awsize,
  input  logic [1:0]        awburst,
  input  logic              awlock,
  input  logic [3:0]        awcache,
  input  logic [2:0]        awprot,
  input  logic              awvalid,
  output logic              awready,
  input  logic [DATA_W-1:0] wdata,
  input  logic [DATA_W/8-1:0] wstrb,
  input  logic              wlast,
  input  logic              wvalid,
  output logic              wready,
  output logic [ID_W-1:0]   bid,
  output logic [1:0]        bresp,
  output logic              bvalid,
  input  logic              bready,
  input  logic [ID_W-1:0]   arid,
  input  logic [31:0]       araddr,
  input  logic [7:0]        arlen,
  input  logic [2:0]        arsize,
  input  logic [1:0]        arburst,
  input  logic              arlock,
  input  logic [3:0]        arcache,
  input  logic [2:0]        arprot,
  input  logic              arvalid,
  output logic              arready,
  output logic [ID_W-1:0]   rid,
  output logic [DATA_W-1:0] rdata,
  output logic [1:0]        rresp,
  output logic              rlast,
  output logic              rvalid,
  input  logic              rready
);
  import axi_pkg::*;
  localparam int BUS = DATA_W / 8;
  localparam int N = 16;                      // transactions in flight per direction

  // ---- switches ----
  int rd_latency = 2, wr_latency = 2, slow_latency = 8;
  int unsigned slow_above = 32'hffff_ffff, err_above = 32'hffff_ffff;
  bit reorder = 0, interleave = 0, excl_on = 0, posted = 0, trace = 0;
  bit early_b = 0, ignore_strobes = 0, drop_hold = 0, reorder_same_id = 0, wrap_bug = 0;

  // ---- the memory ----
  logic [7:0] mem [0:DEPTH-1];
  initial for (int i = 0; i < DEPTH; i++) mem[i] = 8'h00;

  int cycle = -1;
  int seq = 0;                                // every request gets a sequence number: issue order

  // ---- write side: accepted AW requests (a ring) and write beats (a ring) ----
  logic [ID_W-1:0] aw_id [0:N-1];
  int unsigned     aw_addr [0:N-1];
  int              aw_len [0:N-1];
  logic [2:0]      aw_size [0:N-1];
  logic [1:0]      aw_burst [0:N-1];
  logic            aw_lock [0:N-1];
  int aw_head = 0, aw_tail = 0, aw_count = 0;
  localparam int WQ = 1024;
  logic [DATA_W-1:0] w_data [0:WQ-1];
  logic [BUS-1:0]    w_strb [0:WQ-1];
  logic              w_last [0:WQ-1];
  int w_head = 0, w_tail = 0, w_count = 0, w_bursts = 0;   // w_bursts: complete bursts in the ring

  // ---- write responses waiting for their latency ----
  logic            b_use [0:N-1];
  logic [ID_W-1:0] b_id [0:N-1];
  logic [1:0]      b_rsp [0:N-1];
  int              b_at [0:N-1], b_seq [0:N-1];
  logic            b_driving = 0;
  logic            early_done = 0;            // the early_b twin answers once per burst
  // posted writes: the beats of a write kept until its response goes out
  logic [DATA_W-1:0] p_data [0:N-1][0:255];
  logic [BUS-1:0]    p_strb [0:N-1][0:255];
  int unsigned       p_addr [0:N-1];
  int                p_len [0:N-1];
  logic [2:0]        p_size [0:N-1];
  logic [1:0]        p_burst [0:N-1];
  logic              p_pending [0:N-1];

  // ---- read side: accepted AR requests with their progress ----
  logic            r_use [0:N-1];
  logic [ID_W-1:0] r_id [0:N-1];
  int unsigned     r_addr [0:N-1];
  int              r_len [0:N-1];
  logic [2:0]      r_size [0:N-1];
  logic [1:0]      r_burst [0:N-1];
  logic            r_lock [0:N-1];
  int              r_at [0:N-1], r_seq [0:N-1], r_beat [0:N-1], r_served [0:N-1];
  int              r_cur = -1;                // the transaction whose beat is on the wires
  logic            r_driving = 0;

  // ---- exclusive monitors, one per ID ----
  logic        mon_use [0:(1<<ID_W)-1];
  int unsigned mon_addr [0:(1<<ID_W)-1];
  int unsigned mon_bytes [0:(1<<ID_W)-1];

  initial begin
    for (int i = 0; i < N; i++) begin b_use[i] = 0; r_use[i] = 0; p_pending[i] = 0; end
    for (int i = 0; i < (1 << ID_W); i++) mon_use[i] = 0;
    awready = 0; wready = 0; arready = 0; bvalid = 0; rvalid = 0; bid = 0; bresp = 0; rid = 0; rresp = 0; rlast = 0; rdata = 0;
  end

  function automatic int latency_of(input int unsigned a, input int base);
    return (a >= slow_above) ? slow_latency : base;
  endfunction
  function automatic logic [1:0] burst_used(input logic [1:0] b);
    return (wrap_bug && b == WRAP) ? INCR : b;
  endfunction

  // ---- selection policies ----
  // The oldest of all pending entries, or the oldest of its ID: the in-order rule of the protocol.
  function automatic bit b_oldest(input int i, input bit same_id_only);
    for (int j = 0; j < N; j++)
      if (b_use[j] && j != i && b_seq[j] < b_seq[i] && (!same_id_only || b_id[j] == b_id[i])) return 0;
    return 1;
  endfunction
  function automatic bit r_oldest(input int i, input bit same_id_only);
    for (int j = 0; j < N; j++)
      if (r_use[j] && j != i && r_seq[j] < r_seq[i] && (!same_id_only || r_id[j] == r_id[i])) return 0;
    return 1;
  endfunction
  function automatic bit b_eligible(input int i);
    if (!b_use[i] || b_at[i] > cycle) return 0;
    if (!reorder) return b_oldest(i, 0);
    return reorder_same_id ? 1 : b_oldest(i, 1);
  endfunction
  function automatic bit r_eligible(input int i);
    if (!r_use[i] || r_at[i] > cycle) return 0;
    if (!reorder) return r_oldest(i, 0);
    return reorder_same_id ? 1 : r_oldest(i, 1);
  endfunction
  function automatic int free_b();
    for (int i = 0; i < N; i++) if (!b_use[i]) return i;
    return -1;
  endfunction
  function automatic int free_r();
    for (int i = 0; i < N; i++) if (!r_use[i]) return i;
    return -1;
  endfunction
  function automatic int pick_b();
    int best = -1;
    for (int i = 0; i < N; i++) if (b_eligible(i) && (best < 0 || b_seq[i] < b_seq[best])) best = i;
    return best;
  endfunction
  function automatic int pick_r();
    int best = -1;
    for (int i = 0; i < N; i++) if (r_eligible(i)) begin
      if (best < 0) best = i;
      else if (interleave ? (r_served[i] < r_served[best]) : (r_seq[i] < r_seq[best])) best = i;
    end
    return best;
  endfunction

  // ---- the bytes of one read beat, as the bus word that holds them ----
  function automatic logic [DATA_W-1:0] read_word(input int unsigned a);
    logic [DATA_W-1:0] d = 0;
    int unsigned word = (a / BUS) * BUS;
    for (int l = 0; l < BUS; l++) d[8*l +: 8] = (word + l < DEPTH) ? mem[word + l] : 8'h00;
    return d;
  endfunction

  // ---- the write of one complete burst into the memory ----
  task automatic write_burst(input int e);
    logic [1:0]  rsp = OKAY;
    logic        do_write = 1, ended = 0;
    int unsigned a, word;
    logic [15:0] lanes;
    int          n = 0, slot;
    int unsigned total = (1 << aw_size[e]) * (aw_len[e] + 1);
    slot = free_b();
    if (aw_lock[e] && excl_on) begin
      if (mon_use[aw_id[e]] && mon_addr[aw_id[e]] == aw_addr[e]) begin
        rsp = EXOKAY;
        $display("mem e%0d: exclusive write id=%0d at 0x%0h: the monitor matched, EXOKAY", cycle, aw_id[e], aw_addr[e]);
      end else begin
        do_write = 0;
        $display("mem e%0d: exclusive write id=%0d at 0x%0h: no monitor, OKAY and nothing written", cycle, aw_id[e], aw_addr[e]);
      end
    end
    while (!ended && n <= aw_len[e]) begin
      a = beat_addr(aw_addr[e], aw_len[e], aw_size[e], burst_used(aw_burst[e]), n);
      lanes = beat_lanes(aw_addr[e], aw_len[e], aw_size[e], burst_used(aw_burst[e]), n, BUS);
      word = (a / BUS) * BUS;
      if (a >= err_above) rsp = SLVERR;
      else if (do_write && posted && slot >= 0) begin
        p_data[slot][n] = w_data[w_head]; p_strb[slot][n] = w_strb[w_head];
      end else if (do_write) begin
        for (int l = 0; l < BUS; l++)
          if ((w_strb[w_head][l] || ignore_strobes) && word + l < DEPTH) begin
            mem[word + l] = w_data[w_head][8*l +: 8];
            if (trace) $display("mem e%0d: beat %0d writes 0x%02h to 0x%0h (lane %0d)", cycle, n, w_data[w_head][8*l +: 8], word + l, l);
          end
      end
      ended = w_last[w_head];                      // a burst ends at its WLAST, whatever AWLEN said
      w_head = (w_head + 1) % WQ; w_count = w_count - 1;
      n = n + 1;
    end
    while (!ended) begin                           // beats past AWLEN (a broken manager) are dropped
      ended = w_last[w_head];
      w_head = (w_head + 1) % WQ; w_count = w_count - 1;
    end
    // A write clears every monitor that watches a byte it touched.
    if (do_write)
      for (int i = 0; i < (1 << ID_W); i++)
        if (mon_use[i] && mon_addr[i] < aw_addr[e] + total && aw_addr[e] < mon_addr[i] + mon_bytes[i]) mon_use[i] = 0;
    if (slot >= 0) begin
      b_use[slot] = 1; b_id[slot] = aw_id[e]; b_rsp[slot] = rsp; b_seq[slot] = seq; seq = seq + 1;
      b_at[slot] = cycle + latency_of(aw_addr[e], wr_latency);
      if (posted && do_write) begin
        p_pending[slot] = 1; p_addr[slot] = aw_addr[e]; p_len[slot] = n - 1; p_size[slot] = aw_size[e]; p_burst[slot] = aw_burst[e];
      end
    end
  endtask

  // A posted write reaches the memory when its response goes out.
  task automatic apply_posted(input int i);
    int unsigned a, word;
    for (int n = 0; n <= p_len[i]; n++) begin
      a = beat_addr(p_addr[i], p_len[i], p_size[i], burst_used(p_burst[i]), n);
      word = (a / BUS) * BUS;
      if (a < err_above)
        for (int l = 0; l < BUS; l++)
          if ((p_strb[i][n][l] || ignore_strobes) && word + l < DEPTH) begin
            mem[word + l] = p_data[i][n][8*l +: 8];
            if (trace) $display("mem e%0d: posted beat %0d writes 0x%02h to 0x%0h (lane %0d)", cycle, n, p_data[i][n][8*l +: 8], word + l, l);
          end
    end
    p_pending[i] = 0;
  endtask

  int pick, extra;
  always @(posedge aclk) begin
    cycle = cycle + 1;
    if (!aresetn) begin
      aw_head = 0; aw_tail = 0; aw_count = 0; w_head = 0; w_tail = 0; w_count = 0; w_bursts = 0;
      for (int i = 0; i < N; i++) begin b_use[i] = 0; r_use[i] = 0; end
      b_driving = 0; r_driving = 0; r_cur = -1;
      awready <= 0; wready <= 0; arready <= 0; bvalid <= 0; rvalid <= 0;
    end else begin
      // -- AW: take a request while there is room --
      if (awvalid && awready) begin
        aw_id[aw_tail] = awid; aw_addr[aw_tail] = awaddr; aw_len[aw_tail] = awlen; aw_size[aw_tail] = awsize;
        aw_burst[aw_tail] = awburst; aw_lock[aw_tail] = awlock;
        aw_tail = (aw_tail + 1) % N; aw_count = aw_count + 1;
      end
      // -- W: take a beat while there is room --
      if (wvalid && wready) begin
        w_data[w_tail] = wdata; w_strb[w_tail] = wstrb; w_last[w_tail] = wlast;
        w_tail = (w_tail + 1) % WQ; w_count = w_count + 1;
        if (wlast) w_bursts = w_bursts + 1;
      end
      // -- a complete burst with its request: write it and schedule B --
      if (aw_count > 0 && w_bursts > 0) begin
        write_burst(aw_head);
        aw_head = (aw_head + 1) % N; aw_count = aw_count - 1; w_bursts = w_bursts - 1;
        early_done = 0;
      end else if (early_b && !early_done && w_count > 0 && w_bursts == 0) begin
        // The broken twin: a response as soon as the first write beat arrived, before WLAST and,
        // when the data came first, before the address.
        pick = free_b();
        if (pick >= 0) begin
          b_use[pick] = 1; b_id[pick] = (aw_count > 0) ? aw_id[aw_head] : awid; b_rsp[pick] = OKAY; b_seq[pick] = seq; seq = seq + 1; b_at[pick] = cycle;
          early_done = 1;
        end
      end
      // -- B: finish a handshake, then put the next response on the wires --
      if (b_driving && bready) b_driving = 0;
      if (!b_driving) begin
        pick = pick_b();
        if (pick >= 0) begin
          if (p_pending[pick]) apply_posted(pick);
          b_driving = 1; bid <= b_id[pick]; bresp <= b_rsp[pick]; b_use[pick] = 0;
        end
      end
      bvalid <= b_driving;
      // -- AR: take a request while there is room --
      if (arvalid && arready) begin
        pick = free_r();
        if (pick >= 0) begin
          r_use[pick] = 1; r_id[pick] = arid; r_addr[pick] = araddr; r_len[pick] = arlen; r_size[pick] = arsize; r_burst[pick] = arburst;
          r_lock[pick] = arlock; r_beat[pick] = 0; r_seq[pick] = seq; seq = seq + 1; r_served[pick] = -1;
          r_at[pick] = cycle + latency_of(araddr, rd_latency);
          if (arlock && excl_on) begin
            mon_use[arid] = 1; mon_addr[arid] = araddr; mon_bytes[arid] = (1 << arsize) * (arlen + 1);
            $display("mem e%0d: exclusive read id=%0d at 0x%0h: monitor set", cycle, arid, araddr);
          end
        end
      end
      // -- R: finish a handshake, then put the next beat on the wires --
      if (r_driving && !rready && drop_hold) rdata <= rdata + 1;   // the broken twin: data not held
      if (r_driving && rready) begin
        r_driving = 0;
        if (r_beat[r_cur] > r_len[r_cur]) begin r_use[r_cur] = 0; r_cur = -1; end
        else if (interleave) r_cur = -1;
      end
      if (!r_driving) begin
        pick = (r_cur >= 0) ? r_cur : pick_r();
        if (pick >= 0) begin
          r_cur = pick; r_driving = 1; r_served[pick] = cycle;
          extra = r_beat[pick];
          rid <= r_id[pick];
          rdata <= read_word(beat_addr(r_addr[pick], r_len[pick], r_size[pick], burst_used(r_burst[pick]), extra));
          rresp <= (beat_addr(r_addr[pick], r_len[pick], r_size[pick], burst_used(r_burst[pick]), extra) >= err_above) ? SLVERR
                 : ((r_lock[pick] && excl_on) ? EXOKAY : OKAY);
          rlast <= (extra == r_len[pick]);
          r_beat[pick] = extra + 1;
        end
      end
      rvalid <= r_driving;
      awready <= (aw_count < N - 1);
      wready  <= (w_count < WQ - 2);
      arready <= 1;
    end
  end
endmodule

`timescale 1ns/1ns
// axi_checker.sv: the rules of an AXI4 interface, checked at every rising edge (read-only).
// Each broken rule is named with the channel and the edge where it was seen:
//   reset      a VALID is 1 while reset is active;
//   hold       a VALID dropped before its READY: the offer was withdrawn;
//   stable     a channel's payload changed while its offer waited;
//   known      a payload is x while its VALID is 1;
//   len        a FIXED or WRAP burst longer than 16 beats;
//   wrap       a WRAP burst whose length is not 2, 4, 8 or 16 beats or whose address is not aligned;
//   boundary   a burst that crosses a 4 KB boundary;
//   size       a transfer wider than the data bus;
//   strobe     a write strobe on a lane the beat does not address;
//   wlast      WLAST on the wrong beat (not AWLEN), or missing after it;
//   rlast      RLAST on the wrong beat of the oldest read with that ID, or missing after it;
//   border     BVALID before any outstanding write has its last beat, or before its AW;
//   bid, rid   a response ID with no outstanding request of that ID;
//   exokay     EXOKAY for a request that was not exclusive;
//   exclusive  an exclusive request whose bytes are not a power of two up to 128, or not aligned to them.
// The rules no checker can see on the wires (VALID must not wait for READY; same-ID responses
// in the order of their requests) are checked by the data the tasks compare (lessons P2.2, P2.10).
module axi_checker #(parameter int DATA_W = 32, parameter int ID_W = 4) (
  input logic              aclk,
  input logic              aresetn,
  input logic [ID_W-1:0]   awid,
  input logic [31:0]       awaddr,
  input logic [7:0]        awlen,
  input logic [2:0]        awsize,
  input logic [1:0]        awburst,
  input logic              awlock,
  input logic              awvalid,
  input logic              awready,
  input logic [DATA_W-1:0] wdata,
  input logic [DATA_W/8-1:0] wstrb,
  input logic              wlast,
  input logic              wvalid,
  input logic              wready,
  input logic [ID_W-1:0]   bid,
  input logic [1:0]        bresp,
  input logic              bvalid,
  input logic              bready,
  input logic [ID_W-1:0]   arid,
  input logic [31:0]       araddr,
  input logic [7:0]        arlen,
  input logic [2:0]        arsize,
  input logic [1:0]        arburst,
  input logic              arlock,
  input logic              arvalid,
  input logic              arready,
  input logic [ID_W-1:0]   rid,
  input logic [DATA_W-1:0] rdata,
  input logic [1:0]        rresp,
  input logic              rlast,
  input logic              rvalid,
  input logic              rready
);
  import axi_pkg::*;
  localparam int BUS = DATA_W / 8;
  localparam int Q = 64;
  int cycle = -1, writes = 0, reads = 0, stalls = 0, broken = 0;
  logic [DATA_W-1:0] used;

  function void report(input string rule, input string what);
    broken++;
    $display("RULE %s broken at edge %0d: %s", rule, cycle, what);
  endfunction

  // Previous values of every channel, for hold and stable.
  logic p_awv = 0, p_awr = 0, p_wv = 0, p_wr = 0, p_bv = 0, p_br = 0, p_arv = 0, p_arr = 0, p_rv = 0, p_rr = 0;
  logic [31:0] p_awaddr, p_araddr;
  logic [7:0] p_awlen, p_arlen;
  logic [2:0] p_awsize, p_arsize;
  logic [1:0] p_awburst, p_arburst, p_bresp, p_rresp;
  logic [ID_W-1:0] p_awid, p_arid, p_bid, p_rid;
  logic [DATA_W-1:0] p_wdata, p_rdata;
  logic [BUS-1:0] p_wstrb;
  logic p_wlast, p_rlast, p_awlock, p_arlock;

  // Write requests in order (AXI4 write data follows the order of the addresses).
  int unsigned q_addr [0:Q-1];
  int q_len [0:Q-1];
  logic [2:0] q_size [0:Q-1];
  logic [1:0] q_burst [0:Q-1];
  int aw_n = 0;                 // requests accepted
  int wb_n = 0;                 // write bursts started
  int wb_done = 0;              // write bursts ended (WLAST seen)
  int w_beat = 0;               // beats so far in the current burst
  int b_n = 0;                  // responses given
  // Beats recorded for bursts that ran ahead of their AW: strobes and count, checked when AW arrives.
  logic [BUS-1:0] rec_strb [0:Q-1][0:255];
  int rec_beats [0:Q-1];
  logic rec_open [0:Q-1];
  // Outstanding requests per ID, and the read requests per ID in order.
  int aw_out [0:(1<<ID_W)-1], ar_out [0:(1<<ID_W)-1], aw_excl [0:(1<<ID_W)-1], ar_excl [0:(1<<ID_W)-1];
  int rq_len [0:(1<<ID_W)-1][0:15];
  int rq_head [0:(1<<ID_W)-1], rq_tail [0:(1<<ID_W)-1], r_beat [0:(1<<ID_W)-1];
  initial for (int i = 0; i < (1 << ID_W); i++) begin aw_out[i] = 0; ar_out[i] = 0; aw_excl[i] = 0; ar_excl[i] = 0; rq_head[i] = 0; rq_tail[i] = 0; r_beat[i] = 0; end
  initial for (int i = 0; i < Q; i++) begin rec_beats[i] = 0; rec_open[i] = 0; end

  function automatic bit pow2_le128(input int unsigned n);
    return (n == 1 || n == 2 || n == 4 || n == 8 || n == 16 || n == 32 || n == 64 || n == 128);
  endfunction

  task automatic check_request(input string ch, input int unsigned addr, input int len, input logic [2:0] size, input logic [1:0] burst, input logic lock);
    int unsigned bytes = (1 << size) * (len + 1);
    if ((burst == FIXED || burst == WRAP) && len > 15) report("len", $sformatf("%s: a %s burst of %0d beats (16 at most)", ch, burst_name(burst), len + 1));
    if (burst == WRAP && !(len == 1 || len == 3 || len == 7 || len == 15)) report("wrap", $sformatf("%s: a WRAP burst of %0d beats (2, 4, 8 or 16)", ch, len + 1));
    if (burst == WRAP && (addr % (1 << size)) != 0) report("wrap", $sformatf("%s: WRAP burst at 0x%0h is not aligned to its %0d-byte transfers", ch, addr, 1 << size));
    if (burst == 2'b11) report("len", $sformatf("%s: burst type 2'b11 is reserved", ch));
    if ((1 << size) > BUS) report("size", $sformatf("%s: %0d-byte transfers on a %0d-byte bus", ch, 1 << size, BUS));
    if (crosses_4k(addr, len, size, burst)) report("boundary", $sformatf("%s: burst at 0x%0h, %0d beats of %0d bytes, crosses a 4 KB boundary", ch, addr, len + 1, 1 << size));
    if (lock && (!pow2_le128(bytes) || (addr % bytes) != 0)) report("exclusive", $sformatf("%s: exclusive access of %0d bytes at 0x%0h (a power of two up to 128, aligned)", ch, bytes, addr));
  endtask

  task automatic check_strobe(input int k, input int n, input logic [BUS-1:0] strb);
    logic [63:0] allowed = beat_strb(q_addr[k % Q], q_len[k % Q], q_size[k % Q], q_burst[k % Q], n, BUS);
    if ((strb & ~allowed[BUS-1:0]) != 0)
      report("strobe", $sformatf("W beat %0d of write %0d: strobe %b on lanes outside %b", n, k, strb, allowed[BUS-1:0]));
  endtask

  always @(posedge aclk) begin
    cycle++;
    if (!aresetn) begin
      if (awvalid === 1 || wvalid === 1 || arvalid === 1) report("reset", "a manager VALID is 1 during reset");
      if (bvalid === 1 || rvalid === 1) report("reset", "a subordinate VALID is 1 during reset");
    end else begin
      // hold, stable and known, per channel
      if (p_awv && !p_awr && awvalid !== 1) report("hold", "AWVALID dropped before AWREADY");
      if (p_awv && !p_awr && awvalid === 1 && (awaddr !== p_awaddr || awlen !== p_awlen || awsize !== p_awsize || awburst !== p_awburst || awid !== p_awid || awlock !== p_awlock)) report("stable", "AW payload changed while the request waited");
      if (p_wv && !p_wr && wvalid !== 1) report("hold", "WVALID dropped before WREADY");
      if (p_wv && !p_wr && wvalid === 1 && (wdata !== p_wdata || wstrb !== p_wstrb || wlast !== p_wlast)) report("stable", "W payload changed while the beat waited");
      if (p_bv && !p_br && bvalid !== 1) report("hold", "BVALID dropped before BREADY");
      if (p_bv && !p_br && bvalid === 1 && (bresp !== p_bresp || bid !== p_bid)) report("stable", "B payload changed while the response waited");
      if (p_arv && !p_arr && arvalid !== 1) report("hold", "ARVALID dropped before ARREADY");
      if (p_arv && !p_arr && arvalid === 1 && (araddr !== p_araddr || arlen !== p_arlen || arsize !== p_arsize || arburst !== p_arburst || arid !== p_arid || arlock !== p_arlock)) report("stable", "AR payload changed while the request waited");
      if (p_rv && !p_rr && rvalid !== 1) report("hold", "RVALID dropped before RREADY");
      if (p_rv && !p_rr && rvalid === 1 && (rdata !== p_rdata || rresp !== p_rresp || rid !== p_rid || rlast !== p_rlast)) report("stable", "R payload changed while the beat waited");
      if (awvalid === 1 && ($isunknown(awaddr) || $isunknown(awlen) || $isunknown(awsize) || $isunknown(awburst) || $isunknown(awid))) report("known", "AW payload is x while AWVALID is 1");
      if (wvalid === 1 && ($isunknown(wstrb) || $isunknown(wlast))) report("known", "W strobe or last is x while WVALID is 1");
      else if (wvalid === 1) begin
        used = '0;
        for (int l = 0; l < BUS; l++) if (wstrb[l] === 1) used[8*l +: 8] = 8'hff;
        if ($isunknown(wdata & used)) report("known", "W data is x on a strobed lane while WVALID is 1");
      end
      if (arvalid === 1 && ($isunknown(araddr) || $isunknown(arlen) || $isunknown(arsize) || $isunknown(arburst) || $isunknown(arid))) report("known", "AR payload is x while ARVALID is 1");
      if (bvalid === 1 && ($isunknown(bresp) || $isunknown(bid))) report("known", "B payload is x while BVALID is 1");
      if (rvalid === 1 && ($isunknown(rresp) || $isunknown(rid) || $isunknown(rlast))) report("known", "R payload is x while RVALID is 1");
      if ((awvalid === 1 && awready !== 1) || (wvalid === 1 && wready !== 1) || (arvalid === 1 && arready !== 1) ||
          (bvalid === 1 && bready !== 1) || (rvalid === 1 && rready !== 1)) stalls++;
      // AW accepted
      if (awvalid === 1 && awready === 1) begin
        check_request("AW", awaddr, awlen, awsize, awburst, awlock);
        q_addr[aw_n % Q] = awaddr; q_len[aw_n % Q] = awlen; q_size[aw_n % Q] = awsize; q_burst[aw_n % Q] = awburst;
        aw_out[awid]++; if (awlock) aw_excl[awid]++;
        // beats of this write that arrived before its address: check them now
        if (rec_beats[aw_n % Q] > 0) begin
          for (int n = 0; n < rec_beats[aw_n % Q]; n++) check_strobe(aw_n, n, rec_strb[aw_n % Q][n]);
          if (!rec_open[aw_n % Q] && rec_beats[aw_n % Q] != awlen + 1)
            report("wlast", $sformatf("write %0d sent %0d beats before its AW said AWLEN=%0d", aw_n, rec_beats[aw_n % Q], awlen));
          if (!rec_open[aw_n % Q]) rec_beats[aw_n % Q] = 0;
        end
        aw_n++;
      end
      // W beat accepted
      if (wvalid === 1 && wready === 1) begin
        if (w_beat == 0) begin wb_n++; rec_beats[(wb_n - 1) % Q] = 0; rec_open[(wb_n - 1) % Q] = 1; end
        if (wb_n <= aw_n) begin
          check_strobe(wb_n - 1, w_beat, wstrb);
          if (wlast === 1 && w_beat != q_len[(wb_n - 1) % Q]) report("wlast", $sformatf("WLAST on beat %0d of write %0d, AWLEN=%0d", w_beat, wb_n - 1, q_len[(wb_n - 1) % Q]));
          if (wlast !== 1 && w_beat == q_len[(wb_n - 1) % Q]) report("wlast", $sformatf("beat %0d of write %0d is AWLEN=%0d but WLAST is 0", w_beat, wb_n - 1, q_len[(wb_n - 1) % Q]));
        end else begin
          rec_strb[(wb_n - 1) % Q][w_beat] = wstrb;
        end
        rec_beats[(wb_n - 1) % Q] = w_beat + 1;
        w_beat++;
        if (wlast === 1) begin w_beat = 0; wb_done++; rec_open[(wb_n - 1) % Q] = 0; if (wb_n <= aw_n) rec_beats[(wb_n - 1) % Q] = 0; end
      end
      // B offered or accepted
      if (bvalid === 1 && !p_bv) begin
        if (b_n >= aw_n && b_n >= wb_done) report("border", "BVALID with no write to answer: neither an AW nor a WLAST is outstanding");
        else if (b_n >= wb_done) report("border", "BVALID before the last beat of the write it answers");
        else if (b_n >= aw_n) report("border", "BVALID before the AW of the write it answers was accepted");
      end
      if (bvalid === 1 && bready === 1) begin
        if (aw_out[bid] == 0) report("bid", $sformatf("B with id %0d, which has no outstanding write", bid));
        else begin
          aw_out[bid]--; writes++;
          if (bresp === EXOKAY && aw_excl[bid] == 0) report("exokay", $sformatf("EXOKAY for write id %0d, which was not exclusive", bid));
          if (aw_excl[bid] > 0 && aw_excl[bid] > aw_out[bid]) aw_excl[bid] = aw_out[bid];
        end
        b_n++;
      end
      // AR accepted
      if (arvalid === 1 && arready === 1) begin
        check_request("AR", araddr, arlen, arsize, arburst, arlock);
        rq_len[arid][rq_tail[arid]] = arlen; rq_tail[arid] = (rq_tail[arid] + 1) % 16;
        ar_out[arid]++; if (arlock) ar_excl[arid]++;
      end
      // R beat accepted
      if (rvalid === 1 && rready === 1) begin
        if (ar_out[rid] == 0) report("rid", $sformatf("R with id %0d, which has no outstanding read", rid));
        else begin
          if (rlast === 1 && r_beat[rid] != rq_len[rid][rq_head[rid]])
            report("rlast", $sformatf("RLAST on beat %0d of the oldest read with id %0d, whose ARLEN is %0d", r_beat[rid], rid, rq_len[rid][rq_head[rid]]));
          if (rlast !== 1 && r_beat[rid] == rq_len[rid][rq_head[rid]])
            report("rlast", $sformatf("beat %0d of the oldest read with id %0d is its ARLEN but RLAST is 0", r_beat[rid], rid));
          if (rresp === EXOKAY && ar_excl[rid] == 0) report("exokay", $sformatf("EXOKAY for read id %0d, which was not exclusive", rid));
          r_beat[rid]++;
          if (rlast === 1) begin
            r_beat[rid] = 0; rq_head[rid] = (rq_head[rid] + 1) % 16; ar_out[rid]--; reads++;
            if (ar_excl[rid] > ar_out[rid]) ar_excl[rid] = ar_out[rid];
          end
        end
      end
    end
    p_awv = (awvalid === 1); p_awr = (awready === 1); p_wv = (wvalid === 1); p_wr = (wready === 1);
    p_bv = (bvalid === 1); p_br = (bready === 1); p_arv = (arvalid === 1); p_arr = (arready === 1);
    p_rv = (rvalid === 1); p_rr = (rready === 1);
    p_awaddr = awaddr; p_awlen = awlen; p_awsize = awsize; p_awburst = awburst; p_awid = awid; p_awlock = awlock;
    p_wdata = wdata; p_wstrb = wstrb; p_wlast = wlast; p_bresp = bresp; p_bid = bid;
    p_araddr = araddr; p_arlen = arlen; p_arsize = arsize; p_arburst = arburst; p_arid = arid; p_arlock = arlock;
    p_rdata = rdata; p_rresp = rresp; p_rid = rid; p_rlast = rlast;
  end
  final $display("checker: %0d writes, %0d reads, %0d stalled edges, %0d rules broken", writes, reads, stalls, broken);
endmodule

// axi_tasks.svh: the manager side of the bench, as tasks for the stimulus (read-only).
// Data for a write burst goes in wd[0], wd[1], ... (one entry per beat, the lowest byte at the
// lowest address); the data of a read comes back in rd[0], rd[1], ... with its responses in rr[].
// Every task prints the beat log: one line per handshake, with the edge where it happened.
// `cycle` counts rising edges from 0.
int cycle = -1;
always @(posedge aclk) cycle = cycle + 1;

logic [63:0] wd [0:255];
logic [63:0] rd [0:255];
logic [1:0]  rr [0:255];
logic [63:0] rdq [0:15][0:255];     // read data per ID, for reads collected out of order
logic [1:0]  rrq [0:15][0:255];
int          rdn [0:15];            // beats received per ID
logic [1:0]  last_bresp = 0;
int          last_beats = 0;
// What the task is driving right now, for the waveform scenes: the address and lanes of the beat.
int unsigned beat_a = 0;
logic [7:0]  beat_m = 0;
// quiet = 1 silences the beat log (a predict item can then ask for a dump line instead).
bit          quiet = 0;
// Strobe override: when strb_force is 1, every write beat uses strb_val as it is.
bit          strb_force = 0;
logic [7:0]  strb_val = 8'hff;
// Outstanding read requests per ID, so the tasks know the lanes of the beats that come back.
int unsigned arq_addr [0:15][0:7];
int          arq_len [0:15][0:7];
logic [2:0]  arq_size [0:15][0:7];
logic [1:0]  arq_burst [0:15][0:7];
int          arq_head [0:15], arq_tail [0:15];
initial for (int i = 0; i < 16; i++) begin arq_head[i] = 0; arq_tail[i] = 0; rdn[i] = 0; end
// READY patterns for the response channels: bit (cycle % 16) of the pattern drives the signal.
bit          rpat_on = 0, bpat_on = 0;
logic [15:0] rpat = 16'hffff, bpat = 16'hffff;
always @(posedge aclk) begin
  #1;
  if (rpat_on) rready = rpat[cycle % 16];
  if (bpat_on) bready = bpat[cycle % 16];
end

// A text waveform for the lesson's trace blocks: with watch = 1, one line per rising edge with the
// values sampled at that edge (cycle k of a trace is what edge k sees).
bit watch = 0;
int wave_edge = -1;
always @(posedge aclk) begin
  wave_edge = wave_edge + 1;
  if (watch) $display("wave e%0d: aw=%b%b w=%b%b b=%b%b ar=%b%b r=%b%b awaddr=%h wdata=%h wstrb=%b wlast=%b bid=%h bresp=%b araddr=%h rid=%h rdata=%h rresp=%b rlast=%b",
                      wave_edge, awvalid, awready, wvalid, wready, bvalid, bready, arvalid, arready, rvalid, rready,
                      awaddr, wdata, wstrb, wlast, bid, bresp, araddr, rid, rdata, rresp, rlast);
end

// Drive RREADY (ch = 0) or BREADY (ch = 1) from a 16-bit pattern; 16'hffff restores always ready.
task automatic ready_pattern(input int ch, input logic [15:0] pat);
  if (ch == 0) begin rpat = pat; rpat_on = 1; rready = pat[cycle % 16]; end
  else begin bpat = pat; bpat_on = 1; bready = pat[cycle % 16]; end
endtask

// The write address channel: offer the request and hold it until it is taken.
task automatic aw_issue(input logic [ID_W-1:0] id, input int unsigned addr, input int len, input logic [2:0] size,
                        input logic [1:0] burst, input logic lock = 0);
  awid = id; awaddr = addr; awlen = len[7:0]; awsize = size; awburst = burst; awlock = lock; awvalid = 1;
  do @(posedge aclk); while (!awready);
  #1 if (!quiet) $display("e%0d AW id=%0d addr=0x%0h len=%0d size=%0d %0s%0s", cycle, id, addr, len, size, burst_name(burst), lock ? " exclusive" : "");
  awvalid = 0; awaddr = 'x; awlen = 'x; awsize = 'x; awburst = 'x; awid = 'x; awlock = 0;
endtask

// The write data channel: the beats of one burst from wd[first..], each placed in its lanes.
task automatic w_burst(input int unsigned addr, input int len, input logic [2:0] size, input logic [1:0] burst, input int first = 0);
  logic [15:0] lanes;
  for (int n = 0; n <= len; n++) begin
    lanes = beat_lanes(addr, len, size, burst, n, BUS_BYTES);
    beat_a = beat_addr(addr, len, size, burst, n);
    beat_m = strb_force ? strb_val : beat_strb(addr, len, size, burst, n, BUS_BYTES);
    wdata = wd[first + n] << (8 * lanes[7:0]);
    wstrb = beat_m[BUS_BYTES-1:0];
    wlast = (n == len);
    wvalid = 1;
    do @(posedge aclk); while (!wready);
    #1 if (!quiet) $display("e%0d W  beat %0d data=0x%0h strb=%b last=%0d  addr 0x%0h lanes %0d-%0d", cycle, n, wdata, wstrb, wlast, beat_a, lanes[7:0], lanes[15:8]);
  end
  wvalid = 0; wdata = 'x; wstrb = 'x; wlast = 0; beat_m = 0;
endtask

// Wait for the write response of one transaction with this ID.
task automatic b_wait(input logic [ID_W-1:0] id);
  do @(posedge aclk); while (!(bvalid && bready && bid == id));
  last_bresp = bresp;                       // sampled at the edge, before the subordinate moves on
  #1 if (!quiet) $display("e%0d B  id=%0d %0s", cycle, id, resp_name(last_bresp));
endtask

// A complete write. order 0 offers the address, then the first beat one cycle later whether or
// not the address has been taken yet (a manager must never make WVALID wait for AWREADY); 1 offers
// the beats first and the address after beat 0; 2 offers the address and beat 0 in the same cycle.
// Returns after B, with the response in last_bresp.
task automatic axi_write(input logic [ID_W-1:0] id, input int unsigned addr, input int len, input logic [2:0] size,
                         input logic [1:0] burst, input int order = 0, input logic lock = 0);
  case (order)
    1: fork
         w_burst(addr, len, size, burst);
         begin @(posedge aclk); #1 aw_issue(id, addr, len, size, burst, lock); end
       join
    2: fork
         aw_issue(id, addr, len, size, burst, lock);
         w_burst(addr, len, size, burst);
       join
    default: fork
         aw_issue(id, addr, len, size, burst, lock);
         begin @(posedge aclk); #1 w_burst(addr, len, size, burst); end
       join
  endcase
  b_wait(id);
endtask

// The read address channel: offer the request and remember it for the beats that come back.
task automatic ar_issue(input logic [ID_W-1:0] id, input int unsigned addr, input int len, input logic [2:0] size,
                        input logic [1:0] burst, input logic lock = 0);
  arq_addr[id][arq_tail[id]] = addr; arq_len[id][arq_tail[id]] = len; arq_size[id][arq_tail[id]] = size;
  arq_burst[id][arq_tail[id]] = burst; arq_tail[id] = (arq_tail[id] + 1) % 8;
  arid = id; araddr = addr; arlen = len[7:0]; arsize = size; arburst = burst; arlock = lock; arvalid = 1;
  do @(posedge aclk); while (!arready);
  #1 if (!quiet) $display("e%0d AR id=%0d addr=0x%0h len=%0d size=%0d %0s%0s", cycle, id, addr, len, size, burst_name(burst), lock ? " exclusive" : "");
  arvalid = 0; araddr = 'x; arlen = 'x; arsize = 'x; arburst = 'x; arid = 'x; arlock = 0;
endtask

// Collect read beats until n transactions have ended (their RLAST). Each beat lands in rdq[rid][k]
// with only the bytes of the transfer (lane-shifted down), and rd[] holds the last transaction.
task automatic r_collect(input int n);
  int done = 0, h;
  logic [15:0] lanes;
  logic [63:0] bytes;
  logic [ID_W-1:0] id;
  logic [DATA_W-1:0] data;
  logic [1:0] resp;
  logic last;
  while (done < n) begin
    do @(posedge aclk); while (!(rvalid && rready));
    id = rid; data = rdata; resp = rresp; last = rlast;   // sampled at the edge, before the subordinate moves on
    h = arq_head[id];
    lanes = beat_lanes(arq_addr[id][h], arq_len[id][h], arq_size[id][h], arq_burst[id][h], rdn[id], BUS_BYTES);
    beat_a = beat_addr(arq_addr[id][h], arq_len[id][h], arq_size[id][h], arq_burst[id][h], rdn[id]);
    beat_m = beat_strb(arq_addr[id][h], arq_len[id][h], arq_size[id][h], arq_burst[id][h], rdn[id], BUS_BYTES);
    bytes = (data >> (8 * lanes[7:0])) & ((64'h1 << (8 * (lanes[15:8] - lanes[7:0] + 1))) - 1);
    rdq[id][rdn[id]] = bytes; rrq[id][rdn[id]] = resp;
    #1 if (!quiet) $display("e%0d R  id=%0d beat %0d data=0x%0h %0s%0s  addr 0x%0h lanes %0d-%0d", cycle, id, rdn[id], bytes, resp_name(resp),
                last ? " last" : "", beat_a, lanes[7:0], lanes[15:8]);
    rdn[id] = rdn[id] + 1;
    if (last) begin
      for (int k = 0; k < rdn[id]; k++) begin rd[k] = rdq[id][k]; rr[k] = rrq[id][k]; end
      last_beats = rdn[id]; rdn[id] = 0; arq_head[id] = (h + 1) % 8; done = done + 1;
    end
  end
  beat_m = 0;
endtask

// A complete read: AR, then every beat, into rd[] and rr[].
task automatic axi_read(input logic [ID_W-1:0] id, input int unsigned addr, input int len, input logic [2:0] size,
                        input logic [1:0] burst, input logic lock = 0);
  ar_issue(id, addr, len, size, burst, lock);
  r_collect(1);
endtask

// The table of a burst before it runs: the address, lanes and strobe of every beat.
task automatic beat_table(input int unsigned addr, input int len, input logic [2:0] size, input logic [1:0] burst);
  logic [15:0] lanes;
  logic [63:0] s;
  int unsigned a;
  $display("burst at 0x%0h: %0d beat%0s of %0d byte%0s, %0s, bus %0d bytes", addr, len + 1, len ? "s" : "", 1 << size, size ? "s" : "",
           burst_name(burst), BUS_BYTES);
  $display("  beat  address  lanes  strobe");
  for (int n = 0; n <= len; n++) begin
    lanes = beat_lanes(addr, len, size, burst, n, BUS_BYTES);
    s = beat_strb(addr, len, size, burst, n, BUS_BYTES);
    a = beat_addr(addr, len, size, burst, n);
    $display("  %4d  0x%05h  %0d-%0d    %b", n, a[19:0], lanes[7:0], lanes[15:8], s[BUS_BYTES-1:0]);
  end
  if (crosses_4k(addr, len, size, burst)) $display("  this burst crosses a 4 KB boundary");
endtask

// One byte of the memory that owns an address (the fabric's second memory above 0x8000).
function automatic logic [7:0] mem_byte(input int unsigned a);
`ifdef AXI_MEM1
  if (a >= 32'h8000) return `AXI_MEM1.mem[a];
`endif
  return `AXI_MEM.mem[a];
endfunction
task automatic set_byte(input int unsigned a, input logic [7:0] v);
`ifdef AXI_MEM1
  if (a >= 32'h8000) `AXI_MEM1.mem[a] = v;
  else `AXI_MEM.mem[a] = v;
`else
  `AXI_MEM.mem[a] = v;
`endif
endtask

// The memory, n bytes from addr, one bus word per group.
task automatic dump(input int unsigned addr, input int n);
  string line;
  int unsigned a = (addr / 16) * 16;
  while (a < addr + n) begin
    line = $sformatf("0x%05h ", a[19:0]);
    for (int i = 0; i < 16; i++) begin
      if (i % BUS_BYTES == 0) line = {line, " "};
      line = {line, $sformatf(" %02h", mem_byte(a + i))};
    end
    $display("%s", line);
    a = a + 16;
  end
endtask

// Fill n bytes from addr with first, first+1, ... so untouched bytes stay recognisable.
task automatic mem_fill(input int unsigned addr, input int n, input logic [7:0] first = 8'h00);
  for (int i = 0; i < n; i++) set_byte(addr + i, first + i[7:0]);
endtask

// Drive nothing for n cycles.
task automatic idle(input int n);
  repeat (n) @(posedge aclk);
  #1;
endtask

`timescale 1ns/1ps
// axi_props.sv: the rules of an AXI4 interface as properties (read-only in this lesson).
// One spec sentence, one property, named like the rule of axi_checker.sv it mirrors. The
// bookkeeping block below keeps what the sentences refer to (requests outstanding per ID, the
// write bursts in order); every property samples those counters the way it samples the wires,
// before the edge. A property reports with $display, so a failure never stops the run.
module axi_props #(parameter int DATA_W = 32, parameter int ID_W = 4) (
  input logic              aclk,
  input logic              aresetn,
  input logic [ID_W-1:0]   awid,
  input logic [31:0]       awaddr,
  input logic [7:0]        awlen,
  input logic [2:0]        awsize,
  input logic [1:0]        awburst,
  input logic              awlock,
  input logic              awvalid,
  input logic              awready,
  input logic [DATA_W-1:0] wdata,
  input logic [DATA_W/8-1:0] wstrb,
  input logic              wlast,
  input logic              wvalid,
  input logic              wready,
  input logic [ID_W-1:0]   bid,
  input logic [1:0]        bresp,
  input logic              bvalid,
  input logic              bready,
  input logic [ID_W-1:0]   arid,
  input logic [31:0]       araddr,
  input logic [7:0]        arlen,
  input logic [2:0]        arsize,
  input logic [1:0]        arburst,
  input logic              arlock,
  input logic              arvalid,
  input logic              arready,
  input logic [ID_W-1:0]   rid,
  input logic [DATA_W-1:0] rdata,
  input logic [1:0]        rresp,
  input logic              rlast,
  input logic              rvalid,
  input logic              rready
);
  import axi_pkg::*;
  localparam int BUS = DATA_W / 8;
  int edge_n = -1, fails = 0;
  always @(posedge aclk) edge_n++;

  // ---- what the sentences refer to ----
  int aw_out [0:(1<<ID_W)-1], ar_out [0:(1<<ID_W)-1], aw_excl [0:(1<<ID_W)-1], ar_excl [0:(1<<ID_W)-1];
  int rq_len [0:(1<<ID_W)-1][0:15];
  int rq_head [0:(1<<ID_W)-1], rq_tail [0:(1<<ID_W)-1], r_beat [0:(1<<ID_W)-1];
  int q_len [0:63];
  int unsigned q_addr [0:63];
  logic [2:0] q_size [0:63];
  logic [1:0] q_burst [0:63];
  int aw_n = 0, w_n = 0, w_beat = 0, wl_n = 0, b_n = 0;
  initial for (int i = 0; i < (1 << ID_W); i++) begin
    aw_out[i] = 0; ar_out[i] = 0; aw_excl[i] = 0; ar_excl[i] = 0; rq_head[i] = 0; rq_tail[i] = 0; r_beat[i] = 0;
  end
  always @(posedge aclk) if (aresetn) begin
    if (awvalid && awready) begin
      q_len[aw_n % 64] = awlen; q_addr[aw_n % 64] = awaddr; q_size[aw_n % 64] = awsize; q_burst[aw_n % 64] = awburst;
      aw_n++; aw_out[awid]++; if (awlock) aw_excl[awid]++;
    end
    if (wvalid && wready) begin
      w_beat++;
      if (wlast) begin w_beat = 0; w_n++; wl_n++; end
    end
    if (bvalid && bready) begin b_n++; if (aw_out[bid] > 0) aw_out[bid]--; if (aw_excl[bid] > aw_out[bid]) aw_excl[bid] = aw_out[bid]; end
    if (arvalid && arready) begin rq_len[arid][rq_tail[arid]] = arlen; rq_tail[arid] = (rq_tail[arid] + 1) % 16; ar_out[arid]++; if (arlock) ar_excl[arid]++; end
    if (rvalid && rready && ar_out[rid] > 0) begin
      r_beat[rid]++;
      if (rlast) begin r_beat[rid] = 0; rq_head[rid] = (rq_head[rid] + 1) % 16; ar_out[rid]--; if (ar_excl[rid] > ar_out[rid]) ar_excl[rid] = ar_out[rid]; end
    end
  end
  function automatic bit pow2_le128(input int unsigned n);
    return (n == 1 || n == 2 || n == 4 || n == 8 || n == 16 || n == 32 || n == 64 || n == 128);
  endfunction
  // The lanes the next write beat may strobe, from the request the bookkeeping kept (all of them
  // while the beat's AW has not arrived yet).
  logic [63:0] allowed_now = '1;
  always @(posedge aclk) if (aresetn)
    allowed_now = (w_n < aw_n) ? beat_strb(q_addr[w_n % 64], q_len[w_n % 64], q_size[w_n % 64], q_burst[w_n % 64], w_beat, BUS) : '1;

  // Sentence: once VALID is asserted it must remain asserted until the handshake occurs.
  hold_aw: assert property (@(posedge aclk) disable iff (!aresetn) awvalid && !awready |=> awvalid) else begin fails = fails + 1; $display("property hold_aw failed at edge %0d: AWVALID withdrawn", edge_n); end
  hold_w:  assert property (@(posedge aclk) disable iff (!aresetn) wvalid && !wready |=> wvalid)    else begin fails = fails + 1; $display("property hold_w failed at edge %0d: WVALID withdrawn", edge_n); end
  hold_b:  assert property (@(posedge aclk) disable iff (!aresetn) bvalid && !bready |=> bvalid)    else begin fails = fails + 1; $display("property hold_b failed at edge %0d: BVALID withdrawn", edge_n); end
  hold_ar: assert property (@(posedge aclk) disable iff (!aresetn) arvalid && !arready |=> arvalid) else begin fails = fails + 1; $display("property hold_ar failed at edge %0d: ARVALID withdrawn", edge_n); end
  hold_r:  assert property (@(posedge aclk) disable iff (!aresetn) rvalid && !rready |=> rvalid)    else begin fails = fails + 1; $display("property hold_r failed at edge %0d: RVALID withdrawn", edge_n); end
  // Sentence: the payload of a channel is held while its offer waits.
  stable_aw: assert property (@(posedge aclk) disable iff (!aresetn) awvalid && !awready |=> $stable({awid, awaddr, awlen, awsize, awburst, awlock})) else begin fails = fails + 1; $display("property stable_aw failed at edge %0d: AW payload changed while waiting", edge_n); end
  stable_w:  assert property (@(posedge aclk) disable iff (!aresetn) wvalid && !wready |=> $stable({wdata, wstrb, wlast})) else begin fails = fails + 1; $display("property stable_w failed at edge %0d: W payload changed while waiting", edge_n); end
  stable_b:  assert property (@(posedge aclk) disable iff (!aresetn) bvalid && !bready |=> $stable({bid, bresp})) else begin fails = fails + 1; $display("property stable_b failed at edge %0d: B payload changed while waiting", edge_n); end
  stable_ar: assert property (@(posedge aclk) disable iff (!aresetn) arvalid && !arready |=> $stable({arid, araddr, arlen, arsize, arburst, arlock})) else begin fails = fails + 1; $display("property stable_ar failed at edge %0d: AR payload changed while waiting", edge_n); end
  stable_r:  assert property (@(posedge aclk) disable iff (!aresetn) rvalid && !rready |=> $stable({rid, rdata, rresp, rlast})) else begin fails = fails + 1; $display("property stable_r failed at edge %0d: R payload changed while waiting", edge_n); end
  // Sentence: during reset the manager drives its VALIDs low, and so does the subordinate.
  reset_m: assert property (@(posedge aclk) !aresetn |-> !awvalid && !wvalid && !arvalid) else begin fails = fails + 1; $display("property reset_m failed at edge %0d: a manager VALID is 1 in reset", edge_n); end
  reset_s: assert property (@(posedge aclk) !aresetn |-> !bvalid && !rvalid) else begin fails = fails + 1; $display("property reset_s failed at edge %0d: a subordinate VALID is 1 in reset", edge_n); end
  // Sentences about the request: burst length by type, WRAP alignment, the 4 KB boundary, the size.
  len_aw: assert property (@(posedge aclk) disable iff (!aresetn) awvalid && awready && awburst != INCR |-> awlen <= 15) else begin fails = fails + 1; $display("property len failed at edge %0d: a FIXED or WRAP write burst longer than 16 beats", edge_n); end
  len_ar: assert property (@(posedge aclk) disable iff (!aresetn) arvalid && arready && arburst != INCR |-> arlen <= 15) else begin fails = fails + 1; $display("property len failed at edge %0d: a FIXED or WRAP read burst longer than 16 beats", edge_n); end
  wrap_aw: assert property (@(posedge aclk) disable iff (!aresetn) awvalid && awready && awburst == WRAP |-> (awlen == 1 || awlen == 3 || awlen == 7 || awlen == 15) && (awaddr % (1 << awsize)) == 0) else begin fails = fails + 1; $display("property wrap failed at edge %0d: a WRAP write of the wrong length or not aligned", edge_n); end
  wrap_ar: assert property (@(posedge aclk) disable iff (!aresetn) arvalid && arready && arburst == WRAP |-> (arlen == 1 || arlen == 3 || arlen == 7 || arlen == 15) && (araddr % (1 << arsize)) == 0) else begin fails = fails + 1; $display("property wrap failed at edge %0d: a WRAP read of the wrong length or not aligned", edge_n); end
  boundary_aw: assert property (@(posedge aclk) disable iff (!aresetn) awvalid && awready |-> !crosses_4k(awaddr, awlen, awsize, awburst)) else begin fails = fails + 1; $display("property boundary failed at edge %0d: a write burst crosses a 4 KB boundary", edge_n); end
  boundary_ar: assert property (@(posedge aclk) disable iff (!aresetn) arvalid && arready |-> !crosses_4k(araddr, arlen, arsize, arburst)) else begin fails = fails + 1; $display("property boundary failed at edge %0d: a read burst crosses a 4 KB boundary", edge_n); end
  size_aw: assert property (@(posedge aclk) disable iff (!aresetn) awvalid && awready |-> (1 << awsize) <= BUS) else begin fails = fails + 1; $display("property size failed at edge %0d: a write transfer wider than the bus", edge_n); end
  size_ar: assert property (@(posedge aclk) disable iff (!aresetn) arvalid && arready |-> (1 << arsize) <= BUS) else begin fails = fails + 1; $display("property size failed at edge %0d: a read transfer wider than the bus", edge_n); end
  // Sentence: an exclusive access is a power of two bytes up to 128, aligned to its size.
  excl_aw: assert property (@(posedge aclk) disable iff (!aresetn) awvalid && awready && awlock |-> pow2_le128((1 << awsize) * (awlen + 1)) && (awaddr % ((1 << awsize) * (awlen + 1))) == 0) else begin fails = fails + 1; $display("property exclusive failed at edge %0d: an exclusive write of the wrong size or alignment", edge_n); end
  // Sentences about the beats: strobes only on the lanes the beat addresses; WLAST on beat AWLEN.
  strobe: assert property (@(posedge aclk) disable iff (!aresetn) wvalid && wready && w_n < aw_n |-> (wstrb & ~allowed_now[BUS-1:0]) == 0) else begin fails = fails + 1; $display("property strobe failed at edge %0d: a strobe on a lane the beat does not address", edge_n); end
  wlast_ok: assert property (@(posedge aclk) disable iff (!aresetn) wvalid && wready && w_n < aw_n |-> wlast == (w_beat == q_len[w_n % 64])) else begin fails = fails + 1; $display("property wlast failed at edge %0d: WLAST on the wrong beat", edge_n); end
  // Sentences about the responses: B only after the last beat and the AW; IDs with a request;
  // RLAST on the last beat of the oldest read with that ID; EXOKAY only for exclusive requests.
  border: assert property (@(posedge aclk) disable iff (!aresetn) bvalid && !$past(bvalid) |-> wl_n > b_n && aw_n > b_n) else begin fails = fails + 1; $display("property border failed at edge %0d: BVALID before the last write beat or before the AW", edge_n); end
  bid_ok: assert property (@(posedge aclk) disable iff (!aresetn) bvalid && bready |-> aw_out[bid] > 0) else begin fails = fails + 1; $display("property bid failed at edge %0d: a write response with no outstanding write of that ID", edge_n); end
  rid_ok: assert property (@(posedge aclk) disable iff (!aresetn) rvalid |-> ar_out[rid] > 0) else begin fails = fails + 1; $display("property rid failed at edge %0d: read data with no outstanding read of that ID", edge_n); end
  rlast_ok: assert property (@(posedge aclk) disable iff (!aresetn) rvalid && rready && ar_out[rid] > 0 |-> rlast == (r_beat[rid] == rq_len[rid][rq_head[rid]])) else begin fails = fails + 1; $display("property rlast failed at edge %0d: RLAST on the wrong beat of the oldest read with that ID", edge_n); end
  exokay_b: assert property (@(posedge aclk) disable iff (!aresetn) bvalid && bready && bresp == EXOKAY |-> aw_excl[bid] > 0) else begin fails = fails + 1; $display("property exokay failed at edge %0d: EXOKAY for a write that was not exclusive", edge_n); end
  exokay_r: assert property (@(posedge aclk) disable iff (!aresetn) rvalid && rready && rresp == EXOKAY |-> ar_excl[rid] > 0) else begin fails = fails + 1; $display("property exokay failed at edge %0d: EXOKAY for a read that was not exclusive", edge_n); end

  final $display("properties: %0d failure(s)", fails);
endmodule