The AHB checker

`timescale 1ns/1ns
// ahb_pkg.sv: the encodings and the arithmetic of a burst (read-only).
// The memory, the driver, the checker and the lesson text all use these functions, so they never
// disagree about the address of a beat or the lanes it uses.
package ahb_pkg;
  localparam logic [1:0] IDLE = 2'b00, BUSY = 2'b01, NONSEQ = 2'b10, SEQ = 2'b11;
  localparam logic [2:0] SINGLE = 3'b000, INCR = 3'b001, WRAP4 = 3'b010, INCR4 = 3'b011,
                         WRAP8 = 3'b100, INCR8 = 3'b101, WRAP16 = 3'b110, INCR16 = 3'b111;
  localparam logic OKAY = 1'b0, ERROR = 1'b1;

  function automatic string trans_name(input logic [1:0] t);
    case (t) IDLE: return "IDLE"; BUSY: return "BUSY"; NONSEQ: return "NONSEQ"; default: return "SEQ"; endcase
  endfunction
  function automatic string burst_name(input logic [2:0] b);
    case (b)
      SINGLE: return "SINGLE"; INCR: return "INCR"; WRAP4: return "WRAP4"; INCR4: return "INCR4";
      WRAP8: return "WRAP8"; INCR8: return "INCR8"; WRAP16: return "WRAP16"; default: return "INCR16";
    endcase
  endfunction
  function automatic string resp_name(input logic r);
    return r ? "ERROR" : "OKAY";
  endfunction
  // s when c is 1, else the empty string (a string-typed result prints the same on every simulator).
  function automatic string opt(input bit c, input string s);
    if (c) return s;
    return "";
  endfunction

  // Beats in a burst: 1 for SINGLE, 4, 8 or 16 for the fixed bursts, 0 for INCR (undefined length).
  function automatic int beats_of(input logic [2:0] b);
    case (b) SINGLE: return 1; INCR: return 0; WRAP4, INCR4: return 4; WRAP8, INCR8: return 8; default: return 16; endcase
  endfunction
  function automatic bit is_wrap(input logic [2:0] b);
    return b == WRAP4 || b == WRAP8 || b == WRAP16;
  endfunction

  // The address of the beat after the one at a: the size in bytes further on; a wrapping burst
  // returns to the start of its window (beats x size bytes, aligned to that total) at the window's end.
  function automatic int unsigned next_addr(input int unsigned a, input logic [2:0] size, input logic [2:0] b);
    int unsigned nb = 1 << size;
    int unsigned window = nb * beats_of(b);
    int unsigned base;
    if (!is_wrap(b)) return a + nb;
    base = (a / window) * window;
    if (a + nb >= base + window) return base;
    return a + nb;
  endfunction

  // The address of beat n of a burst that starts at start.
  function automatic int unsigned beat_addr(input int unsigned start, input logic [2:0] size, input logic [2:0] b, input int n);
    int unsigned a = start;
    for (int k = 0; k < n; k++) a = next_addr(a, size, b);
    return a;
  endfunction

  // The lanes a transfer at address a uses on a bus of bus_bytes bytes, packed as {upper, lower}.
  // Every AHB transfer is aligned to its size, so it uses size bytes from its own lane upwards.
  function automatic logic [15:0] beat_lanes(input int unsigned a, input logic [2:0] size, input int bus_bytes);
    int lower = a % bus_bytes;
    int upper = lower + (1 << size) - 1;
    if (upper > bus_bytes - 1) upper = bus_bytes - 1;
    return {upper[7:0], lower[7:0]};
  endfunction

  // The strobe of a transfer: a 1 for every lane it uses (bit l is lane l).
  function automatic logic [63:0] beat_strb(input int unsigned a, input logic [2:0] size, input int bus_bytes);
    logic [15:0] lanes = beat_lanes(a, size, 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

  function automatic bit aligned(input int unsigned a, input logic [2:0] size);
    return (a % (1 << size)) == 0;
  endfunction

  // True when an incrementing burst of n beats (n is used only for INCR) crosses a 1 KB boundary.
  function automatic bit crosses_1k(input int unsigned start, input logic [2:0] size, input logic [2:0] b, input int n);
    int beats = beats_of(b) ? beats_of(b) : n;
    if (is_wrap(b) || beats < 2) return 0;
    return (start / 1024) != ((start + beats * (1 << size) - 1) / 1024);
  endfunction
endpackage

`timescale 1ns/1ns
// ahb_mem.sv: an AHB subordinate with a byte-addressed memory behind it (read-only in this lesson).
// It registers an address phase at an edge where HSEL is 1, HTRANS is NONSEQ or SEQ and HREADY is 1,
// then runs the data phase: wait states with HREADYOUT low, a write takes HWDATA (and HWSTRB) at the
// edge that ends the data phase, a read drives HRDATA for the cycle that ends it. IDLE and BUSY get a
// zero-wait OKAY and change nothing. The switches below are plain variables: the stimulus sets them by
// name (mem.waits = 2;).
//   waits          wait states inserted in every data phase
//   waits_at[k]    wait states for the k-th transfer this memory takes (from 0; -1 = use waits)
//   err_above      transfers at or above this address get the two-cycle ERROR (and write nothing)
//   excl_on        AHB5 exclusive access: one monitor per HMASTER, HEXOKAY on success
//   trace          print every transfer the memory takes and every byte it writes
// Broken twins, each off by default:
//   ignore_hready    registers an address phase while HREADY is low (another subordinate is stretching),
//                    so it acts on a transfer the manager may still change or cancel
//   wdata_in_addr    takes HWDATA in the address phase, so a write stores the previous transfer's data
//   act_on_idle      treats IDLE and BUSY as transfers (waits, reads, writes HWDATA); this twin is an
//                    AHB-Lite design without an HWSTRB input, so it writes the lanes HSIZE selects
//   one_cycle_error  answers ERROR in one cycle (HRESP high with HREADYOUT high)
//   ignore_size      writes every lane of the bus word, whatever HSIZE and HWSTRB say
module ahb_mem #(parameter int DATA_W = 32, parameter int DEPTH = 65536) (
  input  logic              hclk,
  input  logic              hresetn,
  input  logic              hsel,
  input  logic [31:0]       haddr,
  input  logic [1:0]        htrans,
  input  logic              hwrite,
  input  logic [2:0]        hsize,
  input  logic [2:0]        hburst,
  input  logic [3:0]        hprot,
  input  logic              hmastlock,
  input  logic [DATA_W-1:0] hwdata,
  input  logic [DATA_W/8-1:0] hwstrb,
  input  logic              hexcl,
  input  logic [3:0]        hmaster,
  input  logic              hready,
  output logic              hreadyout,
  output logic              hresp,
  output logic [DATA_W-1:0] hrdata,
  output logic              hexokay
);
  import ahb_pkg::*;
  localparam int BUS = DATA_W / 8;

  // ---- switches ----
  int waits = 0;
  int waits_at [0:63];
  int unsigned err_above = 32'hffff_ffff;
  bit excl_on = 0, trace = 0;
  bit ignore_hready = 0, wdata_in_addr = 0, act_on_idle = 0, one_cycle_error = 0, ignore_size = 0;

  // ---- the memory ----
  logic [7:0] mem [0:DEPTH-1];
  int cycle = -1;
  int taken = 0;                              // transfers taken so far

  // ---- the data phase in progress ----
  bit              d_valid = 0, d_write = 0, d_err = 0, d_exok = 0, d_xfail = 0;
  int unsigned     d_addr = 0;
  logic [2:0]      d_size = 0;
  logic [1:0]      d_trans = 0;
  logic [DATA_W-1:0] d_wd = 0;                // HWDATA seen in the address phase (the wdata_in_addr twin)
  int              d_cnt = 0;                 // wait states still to insert
  bit              e_two = 0;                 // the ERROR response is in its second cycle

  // ---- exclusive monitors, one per HMASTER ----
  bit          mon_use [0:15];
  int unsigned mon_addr [0:15];
  int          mon_bytes [0:15];

  initial begin
    for (int i = 0; i < DEPTH; i++) mem[i] = 8'h00;
    for (int k = 0; k < 64; k++) waits_at[k] = -1;
    for (int m = 0; m < 16; m++) mon_use[m] = 0;
    hreadyout = 1; hresp = 0; hrdata = 0; hexokay = 0;
  end

  function automatic logic [DATA_W-1:0] read_word(input int unsigned a);
    logic [DATA_W-1:0] w = 0;
    int unsigned word = (a / BUS) * BUS;
    for (int l = 0; l < BUS; l++) w[8*l +: 8] = mem[(word + l) % DEPTH];
    return w;
  endfunction

  // Write the lanes of one transfer: the lanes its address and size select, where the strobe is 1.
  task automatic write_bytes(input int unsigned a, input logic [2:0] size, input logic [DATA_W-1:0] data, input logic [BUS-1:0] strb);
    logic [15:0] lanes = beat_lanes(a, size, BUS);
    int unsigned word = (a / BUS) * BUS;
    int lo = ignore_size ? 0 : lanes[7:0];
    int hi = ignore_size ? BUS - 1 : lanes[15:8];
    for (int l = lo; l <= hi; l++)
      if (ignore_size || act_on_idle || strb[l]) begin
        mem[(word + l) % DEPTH] = data[8*l +: 8];
        if (trace) $display("mem e%0d:   byte 0x%0h <= %02h (lane %0d)", cycle, word + l, data[8*l +: 8], l);
      end
    // any write ends the exclusive monitors that cover one of its bytes
    for (int m = 0; m < 16; m++)
      if (mon_use[m] && a < mon_addr[m] + mon_bytes[m] && mon_addr[m] < a + (1 << size)) mon_use[m] = 0;
  endtask

  always @(posedge hclk) begin
    cycle = cycle + 1;
    if (!hresetn) begin
      d_valid = 0; e_two = 0;
      hreadyout <= 1; hresp <= 0; hexokay <= 0;
    end else begin
      // 1. the data phase that ends or waits at this edge
      if (d_valid) begin
        if (hreadyout && hready) begin
          if (d_write && !d_err && !d_xfail)
            write_bytes(d_addr, d_size, wdata_in_addr ? d_wd : hwdata, hwstrb);
          d_valid = 0;
        end else if (!hreadyout) begin
          if (d_cnt > 0) d_cnt = d_cnt - 1;
          else if (d_err) e_two = 1;
        end
      end
      // 2. the address phase on the wires at this edge
      if (hsel && (htrans[1] || act_on_idle) && (hready || (ignore_hready && !d_valid))) begin
        d_valid = 1; d_addr = haddr; d_write = hwrite; d_size = hsize; d_trans = htrans; d_wd = hwdata;
        d_cnt = (taken < 64 && waits_at[taken] >= 0) ? waits_at[taken] : waits;
        taken = taken + 1;
        d_err = (haddr >= err_above); e_two = 0;
        d_exok = 0; d_xfail = 0;
        if (excl_on && hexcl && htrans[1] && !d_err) begin
          if (!hwrite) begin
            mon_use[hmaster] = 1; mon_addr[hmaster] = haddr; mon_bytes[hmaster] = 1 << hsize; d_exok = 1;
          end else if (mon_use[hmaster] && mon_addr[hmaster] == haddr && mon_bytes[hmaster] == (1 << hsize)) begin
            d_exok = 1; mon_use[hmaster] = 0;
          end else d_xfail = 1;
        end
        if (trace) $display("mem e%0d: %0s %0s 0x%0h size %0d%0s%0s%0s", cycle, trans_name(htrans), hwrite ? "write" : "read", haddr, hsize,
                            opt(!hready, " (taken while HREADY is low)"), opt(d_err, " -> ERROR"),
                            opt(d_xfail, " -> exclusive failed"));
      end
      // 3. the response for the cycle that starts now
      if (d_valid && d_cnt > 0) begin
        hreadyout <= 0; hresp <= 0; hexokay <= 0;
      end else if (d_valid && d_err) begin
        hreadyout <= one_cycle_error ? 1'b1 : e_two; hresp <= 1; hexokay <= 0;
      end else begin
        hreadyout <= 1; hresp <= 0; hexokay <= d_valid && d_exok;
      end
      if (d_valid && !d_write) hrdata <= d_err ? '0 : read_word(d_addr);
    end
  end
endmodule

`timescale 1ns/1ns
// ahb_checker.sv: the rules of an AHB interface, checked at every rising edge (read-only).
// Each broken rule is named with the edge where it was seen:
//   reset         HTRANS is not IDLE, or HREADY is low, while reset is active;
//   hold          the address or control changed during a wait state (HREADY low), outside the
//                 changes the protocol allows;
//   trans_change  HTRANS changed during a wait state other than IDLE to NONSEQ, BUSY to SEQ (fixed
//                 bursts) or BUSY to anything (INCR); or SEQ/BUSY with no burst in progress;
//   seq_addr      a SEQ or BUSY address that is not the previous beat's address plus the size
//                 (wrapped for a WRAP burst);
//   burst_ctrl    HSIZE, HBURST, HWRITE or HPROT changed inside a burst;
//   align         a transfer not aligned to its size;
//   size_bus      a transfer wider than the data bus;
//   kb1           an incrementing burst that crosses a 1 KB boundary;
//   burst_len     a fixed-length burst that ends early or runs long, BUSY after a SINGLE, or BUSY
//                 after the last beat of a fixed-length burst;
//   idle_okay     an IDLE or BUSY transfer that did not get a zero-wait OKAY;
//   err_shape     an ERROR that is not two cycles (HREADY low then high, HRESP high in both);
//   exokay        HEXOKAY with HREADY low, with an ERROR, or for a transfer that was not exclusive;
//   known         x on the address, control, or the active lanes of the data.
// A NOTE (not a broken rule) marks a transfer kept after the first cycle of an ERROR: the protocol
// allows it, most managers cancel.
module ahb_checker #(parameter int DATA_W = 32) (
  input logic              hclk,
  input logic              hresetn,
  input logic [31:0]       haddr,
  input logic [1:0]        htrans,
  input logic              hwrite,
  input logic [2:0]        hsize,
  input logic [2:0]        hburst,
  input logic [3:0]        hprot,
  input logic              hmastlock,
  input logic [DATA_W-1:0] hwdata,
  input logic              hexcl,
  input logic              hready,
  input logic              hresp,
  input logic [DATA_W-1:0] hrdata,
  input logic              hexokay
);
  import ahb_pkg::*;
  localparam int BUS = DATA_W / 8;
  int cycle = -1, transfers = 0, waits = 0, errors = 0, broken = 0, notes = 0;

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

  function automatic logic [DATA_W-1:0] lane_mask(input int unsigned a, input logic [2:0] size);
    logic [15:0] lanes = beat_lanes(a, size, BUS);
    logic [DATA_W-1:0] m = '0;
    for (int l = lanes[7:0]; l <= lanes[15:8]; l++) m[8*l +: 8] = 8'hff;
    return m;
  endfunction

  // The previous edge.
  bit          p_on = 0;
  logic        p_ready = 1, p_resp = 0, p_write = 0, p_lock = 0;
  logic [1:0]  p_trans = 0;
  logic [31:0] p_addr = 0;
  logic [2:0]  p_size = 0, p_burst = 0;
  logic [3:0]  p_prot = 0;
  bit          e_first = 0;           // the previous edge was the first cycle of an ERROR
  // The data phase in progress.
  bit          d_on = 0, d_idle = 0, d_write = 0, d_excl = 0;
  int unsigned d_addr = 0;
  logic [2:0]  d_size = 0;
  // The burst in progress.
  bit          b_on = 0, b_err = 0, b_write = 0, b_kb = 0;
  logic [2:0]  b_burst = 0, b_size = 0;
  logic [3:0]  b_prot = 0;
  int unsigned b_first = 0, b_last = 0;
  int          b_count = 0;
  int unsigned exp_a;

  task automatic end_burst();
    if (b_on && beats_of(b_burst) > 1 && b_count < beats_of(b_burst) && !b_err)
      report("burst_len", $sformatf("%0s burst at 0x%0h ended after %0d of %0d beats", burst_name(b_burst), b_first, b_count, beats_of(b_burst)));
    b_on = 0;
  endtask

  task automatic check_beat();
    if ((1 << hsize) > BUS) report("size_bus", $sformatf("a %0d-byte transfer on a %0d-byte bus", 1 << hsize, BUS));
    if (!aligned(haddr, hsize)) report("align", $sformatf("a %0d-byte transfer at 0x%0h is not aligned to its size", 1 << hsize, haddr));
  endtask

  task automatic check_ctrl(input string what);
    if (hsize !== b_size || hburst !== b_burst || hwrite !== b_write || hprot !== b_prot)
      report("burst_ctrl", $sformatf("%0s at 0x%0h changed HSIZE, HBURST, HWRITE or HPROT inside the burst", what, haddr));
  endtask

  always @(posedge hclk) begin
    cycle++;
    if (!hresetn) begin
      if (htrans !== IDLE) report("reset", "HTRANS is not IDLE during reset");
      if (hready !== 1) report("reset", "HREADY is low during reset");
      p_on = 0; d_on = 0; b_on = 0; e_first = 0;
    end else begin
      // ---- the data phase that ends or waits at this edge ----
      if (hready === 0) waits++;
      if (e_first) begin
        if (hresp !== 1 || hready !== 1) report("err_shape", "the second cycle of an ERROR must have HRESP high and HREADY high");
      end else if (hresp === 1 && hready === 1)
        report("err_shape", "ERROR with HREADY high in its first cycle: an ERROR takes two cycles");
      if (hresp === 1 && b_on) b_err = 1;
      if (d_on && d_idle) begin
        if (hready !== 1 || hresp !== 0) report("idle_okay", "an IDLE or BUSY transfer must get a zero-wait OKAY");
        d_on = 0;
      end
      if (hexokay === 1) begin
        if (hready !== 1) report("exokay", "HEXOKAY while HREADY is low");
        else if (hresp === 1) report("exokay", "HEXOKAY together with an ERROR");
        else if (!(d_on && d_excl)) report("exokay", "HEXOKAY for a transfer that was not exclusive");
      end
      if (hready === 1 && d_on && !d_idle) begin
        if (d_write && $isunknown(hwdata & lane_mask(d_addr, d_size))) report("known", "HWDATA is x on an active lane");
        if (!d_write && hresp === 0 && $isunknown(hrdata & lane_mask(d_addr, d_size))) report("known", "HRDATA is x on an active lane");
        transfers++;
        if (hresp === 1) errors++;
        d_on = 0;
      end
      if (e_first && hready === 1 && (htrans === NONSEQ || htrans === SEQ)) begin
        notes++;
        $display("NOTE cancel at edge %0d: the %0s at 0x%0h behind an ERROR was kept, not cancelled (allowed; most managers cancel)", cycle, trans_name(htrans), haddr);
      end
      // ---- the address phase on the wires at this edge ----
      if (htrans !== IDLE && ($isunknown(haddr) || $isunknown(hwrite) || $isunknown(hsize) || $isunknown(hburst)))
        report("known", "address or control is x while HTRANS is not IDLE");
      if ($isunknown(htrans)) report("known", "HTRANS is x");
      if (p_on && p_ready === 0 && !e_first) begin
        // a wait state at the previous edge: only the allowed changes
        if (p_trans == IDLE) begin
          if (htrans === BUSY || htrans === SEQ) report("trans_change", $sformatf("IDLE changed to %0s during a wait state (only NONSEQ may follow)", trans_name(htrans)));
        end else if (p_trans == BUSY) begin
          if (p_burst != INCR) begin
            if (htrans !== BUSY && htrans !== SEQ) report("trans_change", $sformatf("BUSY in a %0s burst changed to %0s during a wait state (only SEQ may follow)", burst_name(p_burst), trans_name(htrans)));
            else if (haddr !== p_addr) report("hold", $sformatf("HADDR changed from 0x%0h to 0x%0h during a wait state", p_addr, haddr));
          end
        end else begin
          if (htrans !== p_trans) report("trans_change", $sformatf("%0s changed to %0s during a wait state", trans_name(p_trans), trans_name(htrans)));
          else if (haddr !== p_addr) report("hold", $sformatf("HADDR changed from 0x%0h to 0x%0h during a wait state", p_addr, haddr));
          else if (hwrite !== p_write || hsize !== p_size || hburst !== p_burst || hprot !== p_prot || hmastlock !== p_lock)
            report("hold", "HWRITE, HSIZE, HBURST, HPROT or HMASTLOCK changed during a wait state");
        end
      end
      if (hready === 1) begin
        // the address phase is accepted at this edge
        if (htrans === IDLE) begin
          end_burst();
          d_on = 1; d_idle = 1;
        end else if (htrans === NONSEQ) begin
          end_burst();
          check_beat();
          b_on = 1; b_err = 0; b_kb = 0; b_first = haddr; b_last = haddr; b_count = 1;
          b_burst = hburst; b_size = hsize; b_write = hwrite; b_prot = hprot;
          d_on = 1; d_idle = 0; d_write = hwrite; d_addr = haddr; d_size = hsize; d_excl = hexcl;
        end else if (htrans === SEQ) begin
          if (!b_on) report("trans_change", $sformatf("SEQ at 0x%0h with no burst in progress", haddr));
          else begin
            exp_a = next_addr(b_last, b_size, b_burst);
            if (haddr !== exp_a) report("seq_addr", $sformatf("SEQ at 0x%0h; the beat after 0x%0h in a %0s burst of %0d-byte transfers is 0x%0h", haddr, b_last, burst_name(b_burst), 1 << b_size, exp_a));
            check_ctrl("SEQ");
            if (!is_wrap(b_burst) && !b_kb && (haddr / 1024) != (b_first / 1024)) begin
              b_kb = 1;
              report("kb1", $sformatf("SEQ at 0x%0h crosses the 1 KB boundary of the burst that started at 0x%0h", haddr, b_first));
            end
            b_count++;
            if (beats_of(b_burst) > 0 && b_count > beats_of(b_burst))
              report("burst_len", $sformatf("beat %0d of a %0s burst, which has %0d beats", b_count, burst_name(b_burst), beats_of(b_burst)));
            b_last = haddr;
          end
          check_beat();
          d_on = 1; d_idle = 0; d_write = hwrite; d_addr = haddr; d_size = hsize; d_excl = hexcl;
        end else if (htrans === BUSY) begin
          if (!b_on) report("trans_change", $sformatf("BUSY at 0x%0h with no burst in progress", haddr));
          else if (b_burst == SINGLE) report("burst_len", "BUSY after a SINGLE transfer");
          else begin
            exp_a = next_addr(b_last, b_size, b_burst);
            if (beats_of(b_burst) > 1 && b_count == beats_of(b_burst))
              report("burst_len", $sformatf("BUSY after the last beat of the %0s burst (a fixed-length burst ends with SEQ)", burst_name(b_burst)));
            else if (haddr !== exp_a) report("seq_addr", $sformatf("BUSY at 0x%0h must show the next beat's address 0x%0h", haddr, exp_a));
            check_ctrl("BUSY");
          end
          d_on = 1; d_idle = 1;
        end
      end
      e_first = (hresp === 1 && hready === 0);
    end
    p_on = hresetn; p_ready = hready; p_resp = hresp; p_trans = htrans; p_addr = haddr; p_write = hwrite;
    p_size = hsize; p_burst = hburst; p_prot = hprot; p_lock = hmastlock;
  end
  final $display("checker: %0d transfers, %0d wait edges, %0d errors, %0d rules broken", transfers, waits, errors, broken);
endmodule

// ahb_tasks.svh: the manager side of the bench, as tasks for the stimulus (read-only).
// ahb_write, ahb_read and ahb_burst queue transfers; go() puts the queue on the bus and returns when
// the last data phase has ended. The driver below issues the next address phase at the same edge where
// the previous one is accepted, so the address of transfer N+1 is on the wires during the data phase
// of transfer N. Write data for a burst goes in wd[0], wd[1], ... (one entry per beat, the lowest byte
// at the lowest address); the data of every read comes back in rd[0], rd[1], ... in issue order, with
// the responses in rr[].
// The beat log has one line per accepted address phase (A), per ended data phase (D) and per transfer
// the manager cancels (X), each with the edge where it happened; watch = 1 adds one line per edge.
int cycle = -1;
always @(posedge hclk) cycle = cycle + 1;

localparam int QN = 512;
int unsigned q_addr [0:QN-1];
logic        q_write [0:QN-1];
logic [2:0]  q_size [0:QN-1];
logic [2:0]  q_burst [0:QN-1];
logic [1:0]  q_trans [0:QN-1];
logic [63:0] q_data [0:QN-1];
logic        q_lock [0:QN-1], q_excl [0:QN-1], q_sforce [0:QN-1];
logic [3:0]  q_prot [0:QN-1], q_master [0:QN-1];
logic [7:0]  q_strb [0:QN-1];
int          q_bn [0:QN-1], q_beat [0:QN-1], q_state [0:QN-1];   // burst number, beat, 0 queued 1 done 2 cancelled
logic [63:0] q_rdata [0:QN-1];
logic        q_resp [0:QN-1], q_exok [0:QN-1];
int q_n = 0, q_next = 0, bn = 0, last_start = 0, last_bn = 0;

logic [63:0] wd [0:255];
logic [63:0] rd [0:255];
logic        rr [0:255];
int          n_rd = 0;
logic        last_resp = 0, last_exokay = 0;
// quiet = 1 silences the beat log; watch = 1 prints the bus at every edge.
bit quiet = 0, watch = 0, running = 0, drv_done = 0;
// Driver switches (broken twins, off by default):
//   move_in_wait  the address moves on by one transfer size during a wait state
//   no_cancel     the transfer behind an ERROR is not cancelled (allowed, but the checker notes it)
// After the first cycle of an ERROR the driver cancels the transfer already in its address phase: the
// rest of the same burst is dropped; a separate transfer is issued again afterwards (reissue = 0 drops it).
//   busy_end      a BUSY after the last beat of every fixed-length burst
//   cross_1k      incrementing bursts are issued across a 1 KB boundary instead of being split
//   unaligned     transfers not aligned to their size are issued instead of refused
//   wrap_bug      a WRAP8 burst's addresses wrap inside 16 bytes, as if it were WRAP4
bit reissue = 1;
bit move_in_wait = 0, no_cancel = 0, busy_end = 0, cross_1k = 0, unaligned = 0, wrap_bug = 0;
// Attributes of the transfers queued next.
logic       lock = 0, excl = 0;
logic [3:0] prot = 4'b0011, master = 0;
bit         strb_force = 0;
logic [7:0] strb_val = 8'hff;
// What the bus is carrying in the data phase, for the waveform scenes: the address and lanes of the beat.
int unsigned beat_a = 0;
logic [7:0]  beat_m = 0;

function automatic int unsigned m_next(input int unsigned a, input logic [2:0] size, input logic [2:0] b);
  if (wrap_bug && b == WRAP8) return next_addr(a, size, WRAP4);
  return next_addr(a, size, b);
endfunction

task automatic q_push(input int unsigned a, input logic w, input logic [2:0] size, input logic [2:0] b, input logic [1:0] t,
                      input logic [63:0] data, input int burst_no, input int beat);
  q_addr[q_n] = a; q_write[q_n] = w; q_size[q_n] = size; q_burst[q_n] = b; q_trans[q_n] = t; q_data[q_n] = data;
  q_lock[q_n] = lock; q_excl[q_n] = excl; q_prot[q_n] = prot; q_master[q_n] = master;
  q_sforce[q_n] = strb_force; q_strb[q_n] = strb_val;
  q_bn[q_n] = burst_no; q_beat[q_n] = beat; q_state[q_n] = 0; q_resp[q_n] = 0; q_exok[q_n] = 0; q_rdata[q_n] = 0;
  q_n = q_n + 1;
endtask

task automatic q_copy(input int dst, input int src);
  q_addr[dst] = q_addr[src]; q_write[dst] = q_write[src]; q_size[dst] = q_size[src]; q_burst[dst] = q_burst[src];
  q_trans[dst] = q_trans[src]; q_data[dst] = q_data[src]; q_lock[dst] = q_lock[src]; q_excl[dst] = q_excl[src];
  q_prot[dst] = q_prot[src]; q_master[dst] = q_master[src]; q_sforce[dst] = q_sforce[src]; q_strb[dst] = q_strb[src];
  q_bn[dst] = q_bn[src]; q_beat[dst] = q_beat[src]; q_state[dst] = q_state[src];
endtask

// One write of size bytes (0 = byte, 1 = halfword, 2 = word) at addr; data holds the bytes, lowest first.
task automatic ahb_write(input int unsigned addr, input logic [2:0] size, input logic [63:0] data);
  if (!unaligned && !aligned(addr, size))
    $display("refused: a %0d-byte transfer at 0x%0h is not aligned (every AHB transfer is aligned to its size)", 1 << size, addr);
  else begin
    bn = bn + 1; last_start = q_n; last_bn = bn;
    q_push(addr, 1, size, SINGLE, NONSEQ, data, bn, 0);
  end
endtask

// One read of size bytes at addr; the bytes come back in rd[] in issue order.
task automatic ahb_read(input int unsigned addr, input logic [2:0] size);
  if (!unaligned && !aligned(addr, size))
    $display("refused: a %0d-byte transfer at 0x%0h is not aligned (every AHB transfer is aligned to its size)", 1 << size, addr);
  else begin
    bn = bn + 1; last_start = q_n; last_bn = bn;
    q_push(addr, 0, size, SINGLE, NONSEQ, 0, bn, 0);
  end
endtask

// A burst: hburst SINGLE, INCR (beats gives its length), WRAP4, INCR4, ... INCR16. Write data from wd[].
// An incrementing burst that would cross a 1 KB boundary is issued as two INCR bursts split at the
// boundary (unless cross_1k is set).
task automatic ahb_burst(input logic w, input logic [2:0] hb, input int unsigned addr, input logic [2:0] size, input int beats = 0);
  int n;
  int unsigned a;
  logic [2:0] b;
  logic [1:0] t;
  bit split;
  n = beats_of(hb) ? beats_of(hb) : (beats > 0 ? beats : 1);
  a = addr; b = hb; split = 0;
  if (!unaligned && !aligned(addr, size))
    $display("refused: a %0d-byte burst at 0x%0h is not aligned (every AHB transfer is aligned to its size)", 1 << size, addr);
  else begin
    if (!cross_1k && crosses_1k(addr, size, hb, n)) begin
      split = 1; b = INCR;
      $display("note: %0s at 0x%0h would cross a 1 KB boundary; issued as INCR bursts split at the boundary", burst_name(hb), addr);
    end
    bn = bn + 1; last_start = q_n; last_bn = bn;
    for (int k = 0; k < n; k++) begin
      t = (k == 0) ? NONSEQ : SEQ;
      if (k > 0 && split && (a % 1024) == 0) begin t = NONSEQ; bn = bn + 1; end
      q_push(a, w, size, b, t, w ? wd[k] : 64'h0, bn, k);
      a = m_next(a, size, b);
    end
    if (busy_end && beats_of(b) > 1) q_push(a, w, size, b, BUSY, 64'h0, bn, n);
  end
endtask

// n BUSY cycles before beat k of the burst queued last (k = its length: after the last beat).
task automatic busy_at(input int k, input int n = 1);
  int idx, src;
  idx = q_n;
  for (int j = q_n - 1; j >= last_start; j--)
    if (q_trans[j][1] && q_beat[j] == k) idx = j;
  src = (idx < q_n) ? idx : q_n - 1;           // the beat the BUSY announces, or the last beat
  for (int j = q_n - 1; j >= idx; j--) q_copy(j + n, j);
  for (int j = 0; j < n; j++) begin
    q_copy(idx + j, src >= idx ? src + n : src);
    q_trans[idx + j] = BUSY; q_data[idx + j] = 0; q_beat[idx + j] = k;
    if (src < idx) q_addr[idx + j] = m_next(q_addr[src], q_size[src], q_burst[src]);
  end
  q_n = q_n + n;
endtask

// n IDLE cycles in the queue (the address and control keep their last values).
task automatic idle_q(input int n);
  for (int j = 0; j < n; j++)
    if (q_n > 0) q_push(q_addr[q_n - 1], q_write[q_n - 1], q_size[q_n - 1], q_burst[q_n - 1], IDLE, 64'h0, 0, 0);
    else q_push(0, 0, 0, SINGLE, IDLE, 64'h0, 0, 0);
endtask

// The driver: pick, hold, cancel.
int a_idx = -1, d_idx = -1;       // queue entries in the address phase and in the data phase (-1: none)
bit moved = 0;
logic        s_ready, s_resp, s_exok, s_write;
logic [DATA_W-1:0] s_rdata;
logic [31:0] s_addr;
logic [1:0]  s_trans;
logic [2:0]  s_size, s_burst;
int          s_done, s_acc, s_cfrom, s_cto, s_cmode;

task automatic complete(input int i);
  logic [15:0] lanes;
  logic [63:0] bytes;
  q_state[i] = 1; q_resp[i] = s_resp; q_exok[i] = s_exok; last_resp = s_resp; last_exokay = s_exok;
  if (!q_write[i]) begin
    lanes = beat_lanes(q_addr[i], q_size[i], BUS_BYTES);
    bytes = (s_rdata >> (8 * lanes[7:0])) & ((64'h1 << (8 * (lanes[15:8] - lanes[7:0] + 1))) - 1);
    q_rdata[i] = bytes; rd[n_rd] = bytes; rr[n_rd] = s_resp; n_rd = n_rd + 1;
  end
  if (!quiet) $display("e%0d D  %0s addr=0x%0h data=0x%0h %0s%0s", cycle, q_write[i] ? "write" : "read ", q_addr[i],
                       q_write[i] ? q_data[i] : q_rdata[i], resp_name(s_resp),
                       opt(q_excl[i], s_exok ? " EXOKAY" : " (HEXOKAY low: exclusive failed)"));
endtask

task automatic drive();
  logic [15:0] lanes;
  logic [63:0] s;
  int e;
  if (a_idx >= 0) begin
    e = a_idx;
    htrans = q_trans[e]; haddr = q_addr[e] + (moved ? (1 << q_size[e]) : 0); hwrite = q_write[e]; hsize = q_size[e];
    hburst = q_burst[e]; hprot = q_prot[e]; hmastlock = q_lock[e]; hexcl = q_excl[e]; hmaster = q_master[e];
  end else begin
    htrans = IDLE; hmastlock = 0; hexcl = 0;      // address and control keep their last values
  end
  if (d_idx >= 0 && q_write[d_idx]) begin
    lanes = beat_lanes(q_addr[d_idx], q_size[d_idx], BUS_BYTES);
    s = beat_strb(q_addr[d_idx], q_size[d_idx], BUS_BYTES);
    hwdata = q_data[d_idx] << (8 * lanes[7:0]);
    hwstrb = q_sforce[d_idx] ? q_strb[d_idx][BUS_BYTES-1:0] : s[BUS_BYTES-1:0];
    beat_a = q_addr[d_idx]; beat_m = hwstrb;
  end else begin
    hwdata = '0; hwstrb = '0; beat_m = 0;
  end
endtask

always @(posedge hclk) begin
  s_ready = hready; s_resp = hresp; s_exok = hexokay; s_rdata = hrdata; s_addr = haddr; s_trans = htrans;
  s_write = hwrite; s_size = hsize; s_burst = hburst;
  s_done = -1; s_acc = -1; s_cmode = 0;
  if (hresetn) begin
    if (s_ready === 1'b1) begin
      s_done = d_idx; d_idx = -1;
      if (a_idx >= 0 && moved) q_addr[a_idx] = s_addr;   // the address the subordinate took
      if (a_idx >= 0 && q_trans[a_idx] != IDLE) s_acc = a_idx;
      if (a_idx >= 0 && q_trans[a_idx][1]) d_idx = a_idx;
      a_idx = -1; moved = 0;
      if (running && q_next < q_n) begin a_idx = q_next; q_next = q_next + 1; end
    end else if (s_resp === 1'b1 && !no_cancel && a_idx >= 0 && q_trans[a_idx] != IDLE) begin
      // the first cycle of an ERROR: the transfer already on the wires is cancelled (IHI 0033C 5.1.3)
      s_cfrom = a_idx;
      if (d_idx >= 0 && q_bn[a_idx] == q_bn[d_idx]) begin
        s_cto = a_idx;
        while (s_cto < q_n && q_bn[s_cto] == q_bn[d_idx]) begin q_state[s_cto] = 2; s_cto = s_cto + 1; end
        q_next = s_cto; s_cmode = 1;               // the rest of the burst is dropped
      end else if (reissue) begin
        q_next = a_idx; s_cmode = 2;               // a separate transfer: issued again after the ERROR
      end else begin
        q_state[a_idx] = 2; s_cto = a_idx + 1; s_cmode = 3;   // a separate transfer, dropped
      end
      a_idx = -1;
    end else if (move_in_wait && a_idx >= 0 && q_trans[a_idx][1]) moved = 1;
  end
  #1;
  if (s_done >= 0) complete(s_done);
  if (s_acc >= 0 && !quiet)
    $display("e%0d A  %0s %0s addr=0x%0h size=%0d %0s%0s%0s", cycle, trans_name(s_trans), s_write ? "WRITE" : "READ", s_addr, s_size,
             burst_name(s_burst), opt(q_lock[s_acc], " locked"), opt(q_excl[s_acc], " exclusive"));
  if (s_cmode == 1 && !quiet)
    for (int j = s_cfrom; j < s_cto; j++)
      if (q_trans[j][1]) $display("e%0d X  cancelled %0s %0s addr=0x%0h (the rest of the burst is dropped)", cycle, trans_name(q_trans[j]), q_write[j] ? "WRITE" : "READ", q_addr[j]);
  if (s_cmode == 3 && !quiet)
    $display("e%0d X  cancelled %0s %0s addr=0x%0h", cycle, trans_name(q_trans[s_cfrom]), q_write[s_cfrom] ? "WRITE" : "READ", q_addr[s_cfrom]);
  if (s_cmode == 2 && !quiet)
    $display("e%0d X  withdrew %0s %0s addr=0x%0h (issued again after the ERROR)", cycle, trans_name(q_trans[s_cfrom]), q_write[s_cfrom] ? "WRITE" : "READ", q_addr[s_cfrom]);
  drive();
  drv_done = running && q_next >= q_n && a_idx < 0 && d_idx < 0;   // go() returns after this edge's log
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).
int wave_edge = -1;
always @(posedge hclk) begin
  wave_edge = wave_edge + 1;
  if (watch) $display("wave e%0d: htrans=%0s haddr=%h hwrite=%b hsize=%0d hburst=%0s hwdata=%h hready=%b hresp=%b hrdata=%h",
                      wave_edge, trans_name(htrans), haddr, hwrite, hsize, burst_name(hburst), hwdata, hready, hresp, hrdata);
end

// Put the queue on the bus and wait until every transfer in it has ended; then empty the queue.
task automatic go();
  n_rd = 0; drv_done = 0; running = 1;
  wait (drv_done);
  running = 0; drv_done = 0; q_n = 0; q_next = 0;
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 logic [2:0] size, input logic [2:0] hb, input int beats = 0);
  int n;
  int unsigned a, window, base;
  logic [15:0] lanes;
  logic [63:0] s;
  n = beats_of(hb) ? beats_of(hb) : (beats > 0 ? beats : 1);
  a = addr;
  $display("%0s at 0x%0h: %0d beat%0s of %0d byte%0s, bus %0d bytes", burst_name(hb), addr, n, opt(n > 1, "s"), 1 << size, opt(size != 0, "s"), BUS_BYTES);
  if (is_wrap(hb)) begin
    window = (1 << size) * beats_of(hb); base = (addr / window) * window;
    $display("  wraps inside 0x%0h-0x%0h (%0d beats x %0d bytes)", base, base + window - 1, beats_of(hb), 1 << size);
  end
  $display("  beat  address  lanes  strobe");
  for (int k = 0; k < n; k++) begin
    lanes = beat_lanes(a, size, BUS_BYTES);
    s = beat_strb(a, size, BUS_BYTES);
    $display("  %4d  0x%05h  %0d-%0d    %b", k, a[19:0], lanes[7:0], lanes[15:8], s[BUS_BYTES-1:0]);
    a = m_next(a, size, hb);
  end
  if (crosses_1k(addr, size, hb, n)) $display("  this burst crosses a 1 KB boundary");
  if (!aligned(addr, size)) $display("  0x%0h is not aligned to %0d bytes: AHB does not allow it", addr, 1 << size);
endtask

// One byte of the memory that owns an address (the fabric's second memory from 0x1000).
function automatic logic [7:0] mem_byte(input int unsigned a);
`ifdef AHB_MEM1
  if (a >= 32'h1000 && a < 32'h2000) return `AHB_MEM1.mem[a % `AHB_DEPTH];
  if (a >= 32'h1000) return 8'h00;
`endif
  return `AHB_MEM.mem[a % `AHB_DEPTH];
endfunction
task automatic set_byte(input int unsigned a, input logic [7:0] v);
`ifdef AHB_MEM1
  if (a >= 32'h1000 && a < 32'h2000) `AHB_MEM1.mem[a % `AHB_DEPTH] = v;
  else if (a < 32'h1000) `AHB_MEM.mem[a % `AHB_DEPTH] = v;
`else
  `AHB_MEM.mem[a % `AHB_DEPTH] = 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 new for n cycles.
task automatic idle(input int n);
  repeat (n) @(posedge hclk);
  #1;
endtask

`timescale 1ns/1ps
// ahb_props.sv: the rules of an AHB interface as properties (read-only in this lesson).
// One spec sentence, one property, named like the rule of ahb_checker.sv it mirrors. The
// bookkeeping block below keeps what the sentences refer to (the burst in progress, the transfer
// in its data phase); every property samples those variables the way it samples the wires, before
// the edge. A property reports with $display, so a failure never stops the run.
module ahb_props #(parameter int DATA_W = 32) (
  input logic        hclk,
  input logic        hresetn,
  input logic [31:0] haddr,
  input logic [1:0]  htrans,
  input logic        hwrite,
  input logic [2:0]  hsize,
  input logic [2:0]  hburst,
  input logic [3:0]  hprot,
  input logic        hmastlock,
  input logic        hexcl,
  input logic        hready,
  input logic        hresp,
  input logic        hexokay
);
  import ahb_pkg::*;
  localparam int BUS = DATA_W / 8;
  int edge_n = -1, fails = 0;
  always @(posedge hclk) edge_n++;

  // ---- what the sentences refer to: the burst in progress and the transfer in its data phase ----
  bit          b_on = 0, b_err = 0, b_kb = 0, b_write = 0, d_x = 0;
  logic [2:0]  b_burst = 0, b_size = 0;
  logic [3:0]  b_prot = 0;
  int unsigned b_first = 0, b_last = 0;
  int          b_count = 0;
  always @(posedge hclk) begin
    if (!hresetn) begin b_on = 0; d_x = 0; end
    else begin
      if (hresp && b_on) b_err = 1;
      if (hready) begin                                   // an address phase is accepted at this edge
        if (htrans == IDLE) begin b_on = 0; d_x = 0; end
        else if (htrans == NONSEQ) begin
          b_on = 1; b_err = 0; b_kb = 0; b_first = haddr; b_last = haddr; b_count = 1;
          b_burst = hburst; b_size = hsize; b_write = hwrite; b_prot = hprot; d_x = hexcl;
        end else if (htrans == SEQ) begin
          if (b_on) begin
            if (!is_wrap(b_burst) && (haddr / 1024) != (b_first / 1024)) b_kb = 1;
            b_count++; b_last = haddr;
          end
          d_x = hexcl;
        end else d_x = 0;                                 // BUSY
      end
    end
  end
  // The beat after the last one of the burst in progress.
  logic [31:0] exp_a;
  assign exp_a = next_addr(b_last, b_size, b_burst);

  // Sentence: during reset the manager drives IDLE and every subordinate drives HREADYOUT high.
  reset_bus: assert property (@(posedge hclk) !hresetn |-> htrans == IDLE && hready) else begin fails = fails + 1; $display("property reset failed at edge %0d: a transfer or a wait state during reset", edge_n); end
  // Sentence: while a subordinate inserts wait states, the transfer waiting in its address phase
  // keeps its address and control (the first cycle of an ERROR is the exception).
  hold: assert property (@(posedge hclk) disable iff (!hresetn) !hready && !hresp && htrans[1] |=> $stable({haddr, hwrite, hsize, hburst, hprot, hmastlock})) else begin fails = fails + 1; $display("property hold failed at edge %0d: address or control changed during a wait state", edge_n); end
  // Sentence: during a wait state HTRANS may change only from IDLE to NONSEQ, from BUSY to SEQ in a
  // fixed-length burst, or from BUSY to anything in an INCR burst.
  trans_hold: assert property (@(posedge hclk) disable iff (!hresetn) !hready && !hresp && htrans[1] |=> $stable(htrans)) else begin fails = fails + 1; $display("property trans_change failed at edge %0d: NONSEQ or SEQ changed during a wait state", edge_n); end
  trans_idle: assert property (@(posedge hclk) disable iff (!hresetn) !hready && !hresp && htrans == IDLE |=> htrans != BUSY && htrans != SEQ) else begin fails = fails + 1; $display("property trans_change failed at edge %0d: IDLE changed to BUSY or SEQ during a wait state", edge_n); end
  trans_busy: assert property (@(posedge hclk) disable iff (!hresetn) !hready && !hresp && htrans == BUSY && hburst != INCR |=> (htrans == BUSY || htrans == SEQ) && $stable(haddr)) else begin fails = fails + 1; $display("property trans_change failed at edge %0d: BUSY in a fixed burst changed to something other than SEQ", edge_n); end
  // Sentence: SEQ and BUSY exist only inside a burst.
  trans_burst: assert property (@(posedge hclk) disable iff (!hresetn) hready && (htrans == SEQ || htrans == BUSY) |-> b_on) else begin fails = fails + 1; $display("property trans_change failed at edge %0d: SEQ or BUSY with no burst in progress", edge_n); end
  // Sentence: the address of a SEQ (and of a BUSY, which shows the next beat) is the previous
  // beat's address plus the size, wrapped at the window of a WRAP burst.
  seq_addr: assert property (@(posedge hclk) disable iff (!hresetn) hready && htrans == SEQ && b_on |-> haddr == exp_a) else begin fails = fails + 1; $display("property seq_addr failed at edge %0d: SEQ at 0x%0h, the next beat is 0x%0h", edge_n, haddr, exp_a); end
  busy_addr: assert property (@(posedge hclk) disable iff (!hresetn) hready && htrans == BUSY && b_on && b_burst != SINGLE && !(beats_of(b_burst) > 1 && b_count == beats_of(b_burst)) |-> haddr == exp_a) else begin fails = fails + 1; $display("property seq_addr failed at edge %0d: BUSY must show the next beat's address", edge_n); end
  // Sentence: HSIZE, HBURST, HWRITE and HPROT stay constant through a burst.
  burst_ctrl: assert property (@(posedge hclk) disable iff (!hresetn) hready && (htrans == SEQ || (htrans == BUSY && b_burst != SINGLE)) && b_on |-> hsize == b_size && hburst == b_burst && hwrite == b_write && hprot == b_prot) else begin fails = fails + 1; $display("property burst_ctrl failed at edge %0d: control changed inside a burst", edge_n); end
  // Sentences: every transfer is aligned to its size, and no wider than the data bus.
  align: assert property (@(posedge hclk) disable iff (!hresetn) hready && htrans[1] |-> aligned(haddr, hsize)) else begin fails = fails + 1; $display("property align failed at edge %0d: a %0d-byte transfer at 0x%0h", edge_n, 1 << hsize, haddr); end
  size_bus: assert property (@(posedge hclk) disable iff (!hresetn) hready && htrans[1] |-> (1 << hsize) <= BUS) else begin fails = fails + 1; $display("property size_bus failed at edge %0d: a transfer wider than the bus", edge_n); end
  // Sentence: an incrementing burst never crosses a 1 KB boundary.
  kb1: assert property (@(posedge hclk) disable iff (!hresetn) hready && htrans == SEQ && b_on && !is_wrap(b_burst) && !b_kb |-> (haddr / 1024) == (b_first / 1024)) else begin fails = fails + 1; $display("property kb1 failed at edge %0d: SEQ at 0x%0h crosses the 1 KB boundary", edge_n, haddr); end
  // Sentences: a fixed-length burst has exactly its beats (unless an ERROR ends it) and ends with
  // SEQ; no BUSY after a SINGLE.
  burst_short: assert property (@(posedge hclk) disable iff (!hresetn) hready && !hresp && (htrans == NONSEQ || htrans == IDLE) && b_on && beats_of(b_burst) > 1 && !b_err |-> b_count >= beats_of(b_burst)) else begin fails = fails + 1; $display("property burst_len failed at edge %0d: a fixed-length burst ended early", edge_n); end
  burst_long: assert property (@(posedge hclk) disable iff (!hresetn) hready && htrans == SEQ && b_on && beats_of(b_burst) > 0 |-> b_count < beats_of(b_burst)) else begin fails = fails + 1; $display("property burst_len failed at edge %0d: a SEQ beyond the burst's length", edge_n); end
  burst_busy: assert property (@(posedge hclk) disable iff (!hresetn) hready && htrans == BUSY && b_on |-> b_burst != SINGLE && !(beats_of(b_burst) > 1 && b_count == beats_of(b_burst))) else begin fails = fails + 1; $display("property burst_len failed at edge %0d: BUSY after a SINGLE or after the last beat of a fixed burst", edge_n); end
  // Sentence: IDLE and BUSY get a zero-wait OKAY.
  idle_okay: assert property (@(posedge hclk) disable iff (!hresetn) hready && (htrans == IDLE || htrans == BUSY) |=> hready && !hresp) else begin fails = fails + 1; $display("property idle_okay failed at edge %0d: IDLE or BUSY did not get a zero-wait OKAY", edge_n); end
  // Sentence: ERROR takes two cycles: HRESP high with HREADY low, then HRESP high with HREADY high.
  err_two: assert property (@(posedge hclk) disable iff (!hresetn) hresp && !hready |=> hresp && hready) else begin fails = fails + 1; $display("property err_shape failed at edge %0d: the ERROR did not end in its second cycle", edge_n); end
  err_first: assert property (@(posedge hclk) disable iff (!hresetn) hresp && hready |-> $past(hresp && !hready)) else begin fails = fails + 1; $display("property err_shape failed at edge %0d: ERROR with HREADY high in its first cycle", edge_n); end
  // Sentence: HEXOKAY only with HREADY, never with ERROR, and only for an exclusive transfer.
  exokay: assert property (@(posedge hclk) disable iff (!hresetn) hexokay |-> hready && !hresp && d_x) else begin fails = fails + 1; $display("property exokay failed at edge %0d: HEXOKAY where it is not allowed", edge_n); end

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