xHCI Overview

   given ONE array and TWO agents, how does the consumer know
   which entries the producer has finished writing?

   a TRB belongs to HARDWARE   <=>   TRB.Cycle == CCS

  xhci_trb_ring  #(RING_N = 8, PTRW = 3)

  from the fetch engine         to the transfer engine
  ---------------------         ----------------------
  run                           owned / consume
  trb_valid                     is_transfer / follow_link / toggle
  trb_cycle                     action   IDLE / TRANSFER / LINK /
  trb_is_link                            LINK_TOG / UNOWNED
  trb_toggle_cycle
  trb_link_target [2:0]         deq_ptr [2:0]
  doorbell                      ccs
                                ring_empty / stopped

  n_transfers / n_links / n_toggles / n_empty / n_restarts

// xhci_trb_ring -- how two agents share a circular buffer without ever
// telling each other where they have got to.
//
// THE PROBLEM EHCI'S LINKED LIST DOES NOT SOLVE WELL
//
// Chapter 22.1's asynchronous schedule is a ring of Queue Heads that software
// edits while hardware walks it. It works, but every edit is a pointer
// update that has to be safe against a concurrent reader, and finding out
// whether there is anything to do costs a full lap.
//
// xHCI replaced all of it with RINGS: fixed arrays of 16-byte Transfer
// Request Blocks, written by software and read by hardware. Which immediately
// raises the classic producer/consumer question:
//
//     given one array and two agents, how does the consumer know
//     which entries the producer has finished writing?
//
// The textbook answer is a head pointer and a tail pointer, exchanged through
// registers or through memory. xHCI does not do that either. Exchanging
// pointers means every enqueue costs a write the other side has to see, and
// on a PCIe device that write is a round trip.
//
// THE CYCLE BIT
//
// Every TRB carries one bit -- the Cycle bit -- and each side keeps one bit
// of its own:
//
//     software holds PCS, the Producer Cycle State
//     hardware holds CCS, the Consumer Cycle State
//
// and the rule is a single comparison:
//
//     a TRB belongs to HARDWARE  <=>  TRB.Cycle == CCS
//
// Software writes a TRB with Cycle = PCS, which hands it over. Hardware
// consumes TRBs while they match CCS and STOPS at the first one that does
// not -- because that TRB is one software has not written yet, and the stale
// contents of the array are the previous lap's TRBs, which carry the OPPOSITE
// cycle value.
//
// That is the whole mechanism. No pointer is exchanged, no register is
// written on the fast path, and "is there work?" is answered by reading one
// bit of one TRB.
//
// WRAPPING, AND WHY THE TOGGLE IS NOT AUTOMATIC
//
// The trick only works if the value written on one lap differs from the value
// left by the previous lap. So both sides invert their cycle state each time
// they wrap -- and the wrap is not implicit. Every ring ENDS with a LINK TRB,
// which carries the address of the next segment and a Toggle Cycle flag:
//
//     Link TRB with TC = 1   ->  follow the pointer AND invert CCS
//     Link TRB with TC = 0   ->  follow the pointer, cycle state UNCHANGED
//
// TC is set on the link that closes the ring and clear on links that merely
// join one segment to the next. A controller that inverts on every link
// desynchronises any multi-segment ring; one that never inverts stops dead
// after one lap, because everything then looks unowned.
//
// AND THE LINK TRB IS ITSELF A TRB
//
// It has a Cycle bit and it obeys the same ownership rule. A Link TRB that
// software has not yet handed over must NOT be followed -- it is the end of
// what has been produced, exactly like any other unowned TRB. Following it
// reads a pointer software has not written.
module xhci_trb_ring #(
  parameter RING_N = 8,          // TRBs per segment
  parameter PTRW   = 3           // pointer width: must hold 0 .. RING_N-1
) (
  input  wire            clk,
  input  wire            rst_n,

  input  wire            run,              // the endpoint is running
  input  wire            trb_valid,        // a TRB has been fetched
  input  wire            trb_cycle,        // its Cycle bit
  input  wire            trb_is_link,      // it is a Link TRB
  input  wire            trb_toggle_cycle, // ...with the Toggle Cycle flag
  input  wire [PTRW-1:0] trb_link_target,  // ...and this is where it points
  input  wire            doorbell,         // software: "I enqueued something"

  output wire            owned,            // TRB.Cycle == CCS
  output wire            consume,          // take this TRB
  output wire            is_transfer,      // ...and it is real work, not a link
  output wire            follow_link,
  output wire            toggle,           // invert CCS this cycle
  output wire [2:0]      action,           // the same decision, named

  output wire [PTRW-1:0] deq_ptr,
  output wire            ccs,              // Consumer Cycle State
  output wire            ring_empty,       // an unowned TRB: nothing to do
  output wire            stopped,          // ...latched, until the doorbell

  output reg  [31:0]     n_transfers,
  output reg  [31:0]     n_links,
  output reg  [31:0]     n_toggles,
  output reg  [31:0]     n_empty,
  output reg  [31:0]     n_restarts
);
  reg [PTRW-1:0] deq_r;
  reg            ccs_r;
  reg            stopped_r;

  assign deq_ptr = deq_r;
  assign ccs     = ccs_r;
  assign stopped = stopped_r;

  wire running = run && !stopped_r;

  // ---- THE OWNERSHIP TEST. One comparison, and everything follows. ----
  //
  // A TRB whose Cycle bit differs from CCS is one software has not handed
  // over. What is physically in memory there is the PREVIOUS lap's TRB --
  // real-looking data, with a real-looking type and a real-looking pointer,
  // that must not be acted on.
  assign owned      = running && trb_valid && (trb_cycle == ccs_r);
  assign ring_empty = running && trb_valid && (trb_cycle != ccs_r);

  assign consume     = owned;
  assign follow_link = owned &&  trb_is_link;
  assign is_transfer = owned && !trb_is_link;

  // The toggle is NOT implicit in wrapping. Only a Link TRB carrying the
  // Toggle Cycle flag inverts the consumer's cycle state.
  assign toggle = follow_link && trb_toggle_cycle;

  // The same decision as one named value. TRB_IDLE, TRB_UNOWNED and a
  // consumed TRB that happens to be a plain link all look like "the pointer
  // did not move much" on a waveform, and they are three different states of
  // the world.
  localparam [2:0] TRB_IDLE     = 3'd0,  // not running, or no TRB fetched
                   TRB_TRANSFER = 3'd1,  // owned, not a link: real work
                   TRB_LINK     = 3'd2,  // owned link, cycle state unchanged
                   TRB_LINK_TOG = 3'd3,  // owned link with Toggle Cycle
                   TRB_UNOWNED  = 3'd4;  // software has not handed it over

  assign action = (!running || !trb_valid) ? TRB_IDLE
                : !owned                   ? TRB_UNOWNED
                : !trb_is_link             ? TRB_TRANSFER
                : trb_toggle_cycle         ? TRB_LINK_TOG
                                           : TRB_LINK;

  // ---- Next state, as priority chains ----
  //
  // A Link TRB moves the dequeue pointer to the link's target; an ordinary
  // consumed TRB advances it by one. A correct ring always ends in a Link
  // TRB, so the increment never has to wrap -- but it wraps anyway, because
  // a controller must not walk off the end of an array software got wrong.
  // RING_N itself does not fit in PTRW bits -- RING_N-1 does. Comparing
  // against the last index rather than against the count is what keeps this
  // correct for any RING_N, including a power of two where the truncated
  // count reads as zero.
  localparam [PTRW-1:0] LAST_IDX = RING_N - 1;

  wire [PTRW-1:0] deq_inc = (deq_r == LAST_IDX) ? {PTRW{1'b0}}
                                                : deq_r + {{(PTRW-1){1'b0}}, 1'b1};

  wire [PTRW-1:0] deq_next = !run        ? {PTRW{1'b0}}
                           : follow_link ? trb_link_target
                           : consume     ? deq_inc
                                         : deq_r;

  // CCS resets to ONE, not zero. Software's PCS also starts at 1, and a ring
  // is zeroed before use -- so every TRB initially reads Cycle = 0, which is
  // "not owned by hardware". An empty ring is therefore empty by
  // construction, with no initialisation handshake at all.
  wire ccs_next = !run   ? 1'b1
                : toggle ? ~ccs_r
                         :  ccs_r;

  // Same pattern as the EHCI walker in chapter 22.1: the condition that
  // stops the consumer evaporates the moment it stops, so it has to be
  // latched, and software has to ring a doorbell to say the ring is no
  // longer empty.
  wire stopped_next = !run      ? 1'b0
                    : doorbell  ? 1'b0
                    : ring_empty ? 1'b1
                                 : stopped_r;

  always @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      deq_r       <= {PTRW{1'b0}};
      ccs_r       <= 1'b1;
      stopped_r   <= 1'b0;
      n_transfers <= 32'd0;
      n_links     <= 32'd0;
      n_toggles   <= 32'd0;
      n_empty     <= 32'd0;
      n_restarts  <= 32'd0;
    end else begin
      deq_r     <= deq_next;
      ccs_r     <= ccs_next;
      stopped_r <= stopped_next;

      if (is_transfer)  n_transfers <= n_transfers + 32'd1;
      if (follow_link)  n_links     <= n_links + 32'd1;
      if (toggle)       n_toggles   <= n_toggles + 32'd1;
      if (ring_empty)   n_empty     <= n_empty + 32'd1;
      // Doorbells that actually RELEASED a stopped consumer -- as distinct
      // from doorbells rung while it was already running, which are the
      // common case and cost nothing. A high restart count against a low
      // transfer count is software enqueueing one TRB at a time.
      if (run && doorbell && stopped_r)
                        n_restarts  <= n_restarts + 32'd1;
    end
  end
endmodule

// xhci_trb_ring -- how two agents share a circular buffer without ever
// telling each other where they have got to.
//
// THE PROBLEM EHCI'S LINKED LIST DOES NOT SOLVE WELL
//
// Chapter 22.1's asynchronous schedule is a ring of Queue Heads that software
// edits while hardware walks it. It works, but every edit is a pointer
// update that has to be safe against a concurrent reader, and finding out
// whether there is anything to do costs a full lap.
//
// xHCI replaced all of it with RINGS: fixed arrays of 16-byte Transfer
// Request Blocks, written by software and read by hardware. Which immediately
// raises the classic producer/consumer question:
//
//     given one array and two agents, how does the consumer know
//     which entries the producer has finished writing?
//
// The textbook answer is a head pointer and a tail pointer, exchanged through
// registers or through memory. xHCI does not do that either. Exchanging
// pointers means every enqueue costs a write the other side has to see, and
// on a PCIe device that write is a round trip.
//
// THE CYCLE BIT
//
// Every TRB carries one bit -- the Cycle bit -- and each side keeps one bit
// of its own:
//
//     software holds PCS, the Producer Cycle State
//     hardware holds CCS, the Consumer Cycle State
//
// and the rule is a single comparison:
//
//     a TRB belongs to HARDWARE  <=>  TRB.Cycle == CCS
//
// Software writes a TRB with Cycle = PCS, which hands it over. Hardware
// consumes TRBs while they match CCS and STOPS at the first one that does
// not -- because that TRB is one software has not written yet, and the stale
// contents of the array are the previous lap's TRBs, which carry the OPPOSITE
// cycle value.
//
// That is the whole mechanism. No pointer is exchanged, no register is
// written on the fast path, and "is there work?" is answered by reading one
// bit of one TRB.
//
// WRAPPING, AND WHY THE TOGGLE IS NOT AUTOMATIC
//
// The trick only works if the value written on one lap differs from the value
// left by the previous lap. So both sides invert their cycle state each time
// they wrap -- and the wrap is not implicit. Every ring ENDS with a LINK TRB,
// which carries the address of the next segment and a Toggle Cycle flag:
//
//     Link TRB with TC = 1   ->  follow the pointer AND invert CCS
//     Link TRB with TC = 0   ->  follow the pointer, cycle state UNCHANGED
//
// TC is set on the link that closes the ring and clear on links that merely
// join one segment to the next. A controller that inverts on every link
// desynchronises any multi-segment ring; one that never inverts stops dead
// after one lap, because everything then looks unowned.
//
// AND THE LINK TRB IS ITSELF A TRB
//
// It has a Cycle bit and it obeys the same ownership rule. A Link TRB that
// software has not yet handed over must NOT be followed -- it is the end of
// what has been produced, exactly like any other unowned TRB. Following it
// reads a pointer software has not written.
package xhci_ring_pkg;
  // What the consumer decided about the TRB in front of it. Naming the
  // outcomes matters here because THREE of them look like "nothing
  // happened" on a waveform and mean entirely different things.
  typedef enum logic [2:0] {
    TRB_IDLE     = 3'd0,  // not running, or no TRB fetched
    TRB_TRANSFER = 3'd1,  // owned, not a link: real work
    TRB_LINK     = 3'd2,  // owned Link TRB, cycle state unchanged
    TRB_LINK_TOG = 3'd3,  // owned Link TRB with Toggle Cycle: CCS inverts
    TRB_UNOWNED  = 3'd4   // software has not handed this one over
  } trb_action_e;
endpackage

module xhci_trb_ring
  import xhci_ring_pkg::*;
#(
  parameter int RING_N = 8,      // TRBs per segment
  parameter int PTRW   = 3       // pointer width: must hold 0 .. RING_N-1
) (
  input  logic            clk,
  input  logic            rst_n,

  input  logic            run,              // the endpoint is running
  input  logic            trb_valid,        // a TRB has been fetched
  input  logic            trb_cycle,        // its Cycle bit
  input  logic            trb_is_link,      // it is a Link TRB
  input  logic            trb_toggle_cycle, // ...with the Toggle Cycle flag
  input  logic [PTRW-1:0] trb_link_target,  // ...and where it points
  input  logic            doorbell,         // software: "I enqueued something"

  output logic            owned,            // TRB.Cycle == CCS
  output logic            consume,          // take this TRB
  output logic            is_transfer,      // ...real work, not a link
  output logic            follow_link,
  output logic            toggle,           // invert CCS this cycle
  output trb_action_e     action,           // the same decision, named

  output logic [PTRW-1:0] deq_ptr,
  output logic            ccs,              // Consumer Cycle State
  output logic            ring_empty,       // an unowned TRB: nothing to do
  output logic            stopped,          // ...latched, until the doorbell

  output logic [31:0]     n_transfers,
  output logic [31:0]     n_links,
  output logic [31:0]     n_toggles,
  output logic [31:0]     n_empty,
  output logic [31:0]     n_restarts
);
  logic [PTRW-1:0] deq_r;
  logic            ccs_r;
  logic            stopped_r;

  assign deq_ptr = deq_r;
  assign ccs     = ccs_r;
  assign stopped = stopped_r;

  logic running;
  assign running = run && !stopped_r;

  // ---- THE OWNERSHIP TEST. One comparison, and everything follows. ----
  //
  // A TRB whose Cycle bit differs from CCS is one software has not handed
  // over. What is physically in memory there is the PREVIOUS lap's TRB --
  // real-looking data, with a real-looking type and a real-looking pointer,
  // that must not be acted on.
  assign owned      = running && trb_valid && (trb_cycle == ccs_r);
  assign ring_empty = running && trb_valid && (trb_cycle != ccs_r);

  assign consume     = owned;
  assign follow_link = owned &&  trb_is_link;
  assign is_transfer = owned && !trb_is_link;

  // The toggle is NOT implicit in wrapping. Only a Link TRB carrying the
  // Toggle Cycle flag inverts the consumer's cycle state.
  assign toggle = follow_link && trb_toggle_cycle;

  // The same decision as one named value. TRB_IDLE, TRB_UNOWNED and a
  // consumed TRB that happens to be a plain link all look like "the pointer
  // did not move much" on a waveform, and they are three different states of
  // the world.
  always_comb begin
    if      (!running || !trb_valid)  action = TRB_IDLE;
    else if (!owned)                  action = TRB_UNOWNED;
    else if (!trb_is_link)            action = TRB_TRANSFER;
    else if (trb_toggle_cycle)        action = TRB_LINK_TOG;
    else                              action = TRB_LINK;
  end

  // ---- Next state, as priority chains ----
  //
  // A Link TRB moves the dequeue pointer to the link's target; an ordinary
  // consumed TRB advances it by one. A correct ring always ends in a Link
  // TRB, so the increment never has to wrap -- but it wraps anyway, because
  // a controller must not walk off the end of an array software got wrong.
  // RING_N itself does not fit in PTRW bits -- RING_N-1 does. Comparing
  // against the last index rather than against the count is what keeps this
  // correct for any RING_N, including a power of two where the truncated
  // count reads as zero.
  localparam logic [PTRW-1:0] LAST_IDX = PTRW'(RING_N - 1);

  logic [PTRW-1:0] deq_inc;
  assign deq_inc = (deq_r == LAST_IDX) ? {PTRW{1'b0}}
                                                : deq_r + {{(PTRW-1){1'b0}}, 1'b1};

  logic [PTRW-1:0] deq_next;
  assign deq_next = !run        ? {PTRW{1'b0}}
                           : follow_link ? trb_link_target
                           : consume     ? deq_inc
                                         : deq_r;

  // CCS resets to ONE, not zero. Software's PCS also starts at 1, and a ring
  // is zeroed before use -- so every TRB initially reads Cycle = 0, which is
  // "not owned by hardware". An empty ring is therefore empty by
  // construction, with no initialisation handshake at all.
  logic ccs_next;
  assign ccs_next = !run   ? 1'b1
                : toggle ? ~ccs_r
                         :  ccs_r;

  // Same pattern as the EHCI walker in chapter 22.1: the condition that
  // stops the consumer evaporates the moment it stops, so it has to be
  // latched, and software has to ring a doorbell to say the ring is no
  // longer empty.
  logic stopped_next;
  assign stopped_next = !run      ? 1'b0
                    : doorbell  ? 1'b0
                    : ring_empty ? 1'b1
                                 : stopped_r;

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      deq_r       <= {PTRW{1'b0}};
      ccs_r       <= 1'b1;
      stopped_r   <= 1'b0;
      n_transfers <= '0;
      n_links     <= '0;
      n_toggles   <= '0;
      n_empty     <= '0;
      n_restarts  <= '0;
    end else begin
      deq_r     <= deq_next;
      ccs_r     <= ccs_next;
      stopped_r <= stopped_next;

      if (is_transfer)  n_transfers <= n_transfers + 1;
      if (follow_link)  n_links     <= n_links + 1;
      if (toggle)       n_toggles   <= n_toggles + 1;
      if (ring_empty)   n_empty     <= n_empty + 1;
      // Doorbells that actually RELEASED a stopped consumer -- as distinct
      // from doorbells rung while it was already running, which are the
      // common case and cost nothing. A high restart count against a low
      // transfer count is software enqueueing one TRB at a time.
      if (run && doorbell && stopped_r)
                        n_restarts  <= n_restarts + 1;
    end
  end
endmodule

-- xhci_trb_ring -- how two agents share a circular buffer without ever
-- telling each other where they have got to.
--
-- THE PROBLEM EHCI'S LINKED LIST DOES NOT SOLVE WELL
--
-- Chapter 22.1's asynchronous schedule is a ring of Queue Heads that software
-- edits while hardware walks it. It works, but every edit is a pointer update
-- that has to be safe against a concurrent reader, and finding out whether
-- there is anything to do costs a full lap.
--
-- xHCI replaced all of it with RINGS: fixed arrays of 16-byte Transfer
-- Request Blocks, written by software and read by hardware. Which immediately
-- raises the classic producer/consumer question:
--
--     given one array and two agents, how does the consumer know
--     which entries the producer has finished writing?
--
-- The textbook answer is a head pointer and a tail pointer, exchanged through
-- registers or through memory. xHCI does not do that either: exchanging
-- pointers means every enqueue costs a write the other side has to see, and
-- on a PCIe device that write is a round trip.
--
-- THE CYCLE BIT
--
-- Every TRB carries one bit -- the Cycle bit -- and each side keeps one bit
-- of its own:
--
--     software holds PCS, the Producer Cycle State
--     hardware holds CCS, the Consumer Cycle State
--
-- and the rule is a single comparison:
--
--     a TRB belongs to HARDWARE  <=>  TRB.Cycle = CCS
--
-- Software writes a TRB with Cycle = PCS, which hands it over. Hardware
-- consumes TRBs while they match CCS and STOPS at the first one that does
-- not -- because that TRB is one software has not written yet, and the stale
-- contents there are the previous lap's TRBs, which carry the OPPOSITE cycle
-- value.
--
-- No pointer is exchanged, no register is written on the fast path, and "is
-- there work?" is answered by reading one bit of one TRB.
--
-- WRAPPING, AND WHY THE TOGGLE IS NOT AUTOMATIC
--
-- The trick only works if the value written on one lap differs from the value
-- left by the previous lap. So both sides invert their cycle state each time
-- they wrap -- and the wrap is not implicit. Every ring ENDS with a LINK TRB,
-- which carries the address of the next segment and a Toggle Cycle flag:
--
--     Link TRB with TC = '1'  ->  follow the pointer AND invert CCS
--     Link TRB with TC = '0'  ->  follow the pointer, cycle state UNCHANGED
--
-- TC is set on the link that closes the ring and clear on links that merely
-- join one segment to the next. A controller that inverts on every link
-- desynchronises any multi-segment ring; one that never inverts stops dead
-- after one lap, because everything then looks unowned.
--
-- AND THE LINK TRB IS ITSELF A TRB
--
-- It has a Cycle bit and obeys the same ownership rule. A Link TRB software
-- has not yet handed over must NOT be followed -- it is the end of what has
-- been produced, exactly like any other unowned TRB, and following it reads a
-- pointer software never wrote.
library ieee;
use ieee.std_logic_1164.all;
use ieee.numeric_std.all;

package xhci_ring_pkg is
  -- What the consumer decided about the TRB in front of it. Naming the
  -- outcomes matters here because THREE of them look like "nothing happened"
  -- on a waveform and mean entirely different things.
  type trb_action_t is (
    TRB_IDLE,      -- not running, or no TRB fetched
    TRB_TRANSFER,  -- owned, not a link: real work
    TRB_LINK,      -- owned Link TRB, cycle state unchanged
    TRB_LINK_TOG,  -- owned Link TRB with Toggle Cycle: CCS inverts
    TRB_UNOWNED    -- software has not handed this one over
  );

  function act_code(a : trb_action_t) return std_logic_vector;
end package;

package body xhci_ring_pkg is
  function act_code(a : trb_action_t) return std_logic_vector is
  begin
    return std_logic_vector(to_unsigned(trb_action_t'pos(a), 3));
  end function;
end package body;

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

entity xhci_trb_ring is
  generic (
    RING_N : natural := 8;          -- TRBs per segment
    PTRW   : natural := 3           -- pointer width: holds 0 .. RING_N-1
  );
  port (
    clk              : in  std_logic;
    rst_n            : in  std_logic;

    run              : in  std_logic;   -- the endpoint is running
    trb_valid        : in  std_logic;   -- a TRB has been fetched
    trb_cycle        : in  std_logic;   -- its Cycle bit
    trb_is_link      : in  std_logic;   -- it is a Link TRB
    trb_toggle_cycle : in  std_logic;   -- ...with the Toggle Cycle flag
    trb_link_target  : in  std_logic_vector(PTRW-1 downto 0);
    doorbell         : in  std_logic;   -- software: "I enqueued something"

    owned            : out std_logic;   -- TRB.Cycle = CCS
    consume          : out std_logic;
    is_transfer      : out std_logic;   -- real work, not a link
    follow_link      : out std_logic;
    toggle           : out std_logic;   -- invert CCS this cycle
    action           : out std_logic_vector(2 downto 0);

    deq_ptr          : out std_logic_vector(PTRW-1 downto 0);
    ccs              : out std_logic;   -- Consumer Cycle State
    ring_empty       : out std_logic;
    stopped          : out std_logic;   -- latched, until the doorbell

    n_transfers      : out std_logic_vector(31 downto 0);
    n_links          : out std_logic_vector(31 downto 0);
    n_toggles        : out std_logic_vector(31 downto 0);
    n_empty          : out std_logic_vector(31 downto 0);
    n_restarts       : out std_logic_vector(31 downto 0)
  );
end entity;

architecture rtl of xhci_trb_ring is
  signal deq_r     : natural range 0 to RING_N-1 := 0;
  signal ccs_r     : std_logic := '1';
  signal stopped_r : std_logic := '0';

  signal running, own_s, empty_s, fol_s, xfer_s, tog_s : std_logic;
  signal act_s : trb_action_t;

  signal deq_n : natural range 0 to RING_N-1;
  signal ccs_n, stopped_n : std_logic;

  signal tr_c, lk_c, tg_c, em_c, rs_c : unsigned(31 downto 0)
       := (others => '0');
begin
  deq_ptr <= std_logic_vector(to_unsigned(deq_r, PTRW));
  ccs     <= ccs_r;
  stopped <= stopped_r;

  running <= run and (not stopped_r);

  -- ---- THE OWNERSHIP TEST. One comparison, and everything follows. ----
  --
  -- A TRB whose Cycle bit differs from CCS is one software has not handed
  -- over. What is physically in memory there is the PREVIOUS lap's TRB --
  -- real-looking data, with a real-looking type and a real-looking pointer,
  -- that must not be acted on.
  own_s   <= '1' when (running = '1' and trb_valid = '1'
                       and trb_cycle = ccs_r) else '0';
  empty_s <= '1' when (running = '1' and trb_valid = '1'
                       and trb_cycle /= ccs_r) else '0';

  fol_s  <= own_s and trb_is_link;
  xfer_s <= own_s and (not trb_is_link);

  -- The toggle is NOT implicit in wrapping. Only a Link TRB carrying the
  -- Toggle Cycle flag inverts the consumer's cycle state.
  tog_s <= fol_s and trb_toggle_cycle;

  owned       <= own_s;
  consume     <= own_s;
  is_transfer <= xfer_s;
  follow_link <= fol_s;
  toggle      <= tog_s;
  ring_empty  <= empty_s;

  -- The same decision as one named value. TRB_IDLE, TRB_UNOWNED and a
  -- consumed TRB that happens to be a plain link all look like "the pointer
  -- did not move much" on a waveform, and they are three different states of
  -- the world.
  classify : process (running, trb_valid, own_s, trb_is_link,
                      trb_toggle_cycle)
  begin
    if running = '0' or trb_valid = '0' then
      act_s <= TRB_IDLE;
    elsif own_s = '0' then
      act_s <= TRB_UNOWNED;
    elsif trb_is_link = '0' then
      act_s <= TRB_TRANSFER;
    elsif trb_toggle_cycle = '1' then
      act_s <= TRB_LINK_TOG;
    else
      act_s <= TRB_LINK;
    end if;
  end process;

  action <= act_code(act_s);

  -- ---- Next state, as priority chains ----
  --
  -- A Link TRB moves the dequeue pointer to the link's target; an ordinary
  -- consumed TRB advances it by one. A correct ring always ends in a Link
  -- TRB, so the increment never has to wrap -- but it wraps anyway, because a
  -- controller must not walk off the end of an array software got wrong.
  nextptr : process (run, fol_s, own_s, deq_r, trb_link_target)
  begin
    if run = '0' then
      deq_n <= 0;
    elsif fol_s = '1' then
      deq_n <= to_integer(unsigned(trb_link_target));
    elsif own_s = '1' then
      if deq_r = RING_N - 1 then
        deq_n <= 0;
      else
        deq_n <= deq_r + 1;
      end if;
    else
      deq_n <= deq_r;
    end if;
  end process;

  -- CCS resets to ONE, not zero. Software's PCS also starts at 1, and a ring
  -- is zeroed before use -- so every TRB initially reads Cycle = '0', which
  -- is "not owned by hardware". An empty ring is therefore empty by
  -- construction, with no initialisation handshake at all.
  ccs_n <= '1' when run = '0'
      else (not ccs_r) when tog_s = '1'
      else ccs_r;

  -- Same pattern as the EHCI walker in chapter 22.1: the condition that stops
  -- the consumer evaporates the moment it stops, so it has to be latched, and
  -- software has to ring a doorbell to say the ring is no longer empty.
  stopped_n <= '0' when run = '0'
          else '0' when doorbell = '1'
          else '1' when empty_s = '1'
          else stopped_r;

  regs : process (clk, rst_n)
  begin
    if rst_n = '0' then
      deq_r     <= 0;
      ccs_r     <= '1';
      stopped_r <= '0';
      tr_c <= (others => '0');
      lk_c <= (others => '0');
      tg_c <= (others => '0');
      em_c <= (others => '0');
      rs_c <= (others => '0');
    elsif rising_edge(clk) then
      deq_r     <= deq_n;
      ccs_r     <= ccs_n;
      stopped_r <= stopped_n;

      if xfer_s = '1' then
        tr_c <= tr_c + 1;
      end if;
      if fol_s = '1' then
        lk_c <= lk_c + 1;
      end if;
      if tog_s = '1' then
        tg_c <= tg_c + 1;
      end if;
      if empty_s = '1' then
        em_c <= em_c + 1;
      end if;
      -- Doorbells that actually RELEASED a stopped consumer -- as distinct
      -- from doorbells rung while it was already running, which are the
      -- common case and cost nothing.
      if run = '1' and doorbell = '1' and stopped_r = '1' then
        rs_c <= rs_c + 1;
      end if;
    end if;
  end process;

  n_transfers <= std_logic_vector(tr_c);
  n_links     <= std_logic_vector(lk_c);
  n_toggles   <= std_logic_vector(tg_c);
  n_empty     <= std_logic_vector(em_c);
  n_restarts  <= std_logic_vector(rs_c);
end architecture;

`timescale 1ns/1ps
module tb_tr_v;
  localparam RING_N = 8, PTRW = 3;
  reg clk=0, rst_n=0;
  reg run=0, trb_valid=0, trb_cycle=0, trb_is_link=0, trb_toggle_cycle=0;
  reg doorbell=0;
  reg [PTRW-1:0] trb_link_target=0;
  wire owned, consume, is_transfer, follow_link, toggle;
  wire ccs, ring_empty, stopped;
  wire [PTRW-1:0] deq_ptr;
  wire [2:0] action;
  wire [31:0] n_transfers, n_links, n_toggles, n_empty, n_restarts;
  always #5 clk=~clk;

  xhci_trb_ring #(.RING_N(RING_N), .PTRW(PTRW)) dut (
    .clk(clk), .rst_n(rst_n), .run(run), .trb_valid(trb_valid),
    .trb_cycle(trb_cycle), .trb_is_link(trb_is_link),
    .trb_toggle_cycle(trb_toggle_cycle), .trb_link_target(trb_link_target),
    .doorbell(doorbell), .owned(owned), .consume(consume),
    .is_transfer(is_transfer), .follow_link(follow_link), .toggle(toggle),
    .action(action),
    .deq_ptr(deq_ptr), .ccs(ccs), .ring_empty(ring_empty),
    .stopped(stopped), .n_transfers(n_transfers), .n_links(n_links),
    .n_toggles(n_toggles), .n_empty(n_empty), .n_restarts(n_restarts));

  // ---- SHADOW MODEL of all three registers ----
  integer s_deq, s_ccs, s_stopped;
  integer m_tr, m_lk, m_tg, m_em, m_rs;

  integer errors=0, i, a, b, c, d, e, f, g, p;
  integer n_exh=0, n_lnk_exh=0;
  integer n_deq [0:7];
  integer n_owned=0, n_unowned=0, n_link=0, n_tog=0, n_notog=0;

  task check(input cond, input [639:0] msg);
    begin if (!cond) begin errors=errors+1;
      if (errors <= 25)
        $display("  FAIL: %0s (run=%b vld=%b cyc=%b link=%b tc=%b tgt=%0d db=%b | own=%b cons=%b xfer=%b fol=%b tog=%b deq=%0d ccs=%b empty=%b stop=%b || model deq=%0d ccs=%0d stop=%0d, t=%0t)",
                 msg, run, trb_valid, trb_cycle, trb_is_link,
                 trb_toggle_cycle, trb_link_target, doorbell, owned, consume,
                 is_transfer, follow_link, toggle, deq_ptr, ccs, ring_empty,
                 stopped, s_deq, s_ccs, s_stopped, $time);
    end end
  endtask

  localparam [2:0] TRB_IDLE=0, TRB_TRANSFER=1, TRB_LINK=2, TRB_LINK_TOG=3,
                   TRB_UNOWNED=4;

  task check_comb;
    reg e_running, e_own, e_empty, e_fol, e_xfer, e_tog;
    reg [2:0] e_act;
    begin
      // The model states the ownership test as an XNOR of the two bits where
      // the design compares them -- a different route to the same answer.
      e_running = run && (s_stopped == 0);
      e_own   = e_running && trb_valid && ~(trb_cycle ^ s_ccs[0]);
      e_empty = e_running && trb_valid && (trb_cycle ^ s_ccs[0]);
      e_fol   = e_own && trb_is_link;
      e_xfer  = e_own && !trb_is_link;
      e_tog   = e_fol && trb_toggle_cycle;

      check(owned       === e_own,   "owned matches the model");
      check(consume     === e_own,   "consume matches the model");
      check(ring_empty  === e_empty, "ring_empty matches the model");
      check(follow_link === e_fol,   "follow_link matches the model");
      check(is_transfer === e_xfer,  "is_transfer matches the model");
      check(toggle      === e_tog,   "toggle matches the model");

      if      (!e_running || !trb_valid) e_act = TRB_IDLE;
      else if (!e_own)                   e_act = TRB_UNOWNED;
      else if (!trb_is_link)             e_act = TRB_TRANSFER;
      else if (trb_toggle_cycle)         e_act = TRB_LINK_TOG;
      else                               e_act = TRB_LINK;
      check(action === e_act, "action matches the model");
      // The named decision must agree with the booleans it summarises.
      check((action === TRB_TRANSFER) === is_transfer,
            "action disagrees with is_transfer");
      check((action === TRB_LINK_TOG) === toggle,
            "action disagrees with toggle");
      check((action === TRB_UNOWNED) === ring_empty,
            "action disagrees with ring_empty");
      check(deq_ptr     === s_deq[PTRW-1:0], "deq_ptr matches the model");
      check(ccs         === s_ccs[0],        "ccs matches the model");
      check(stopped     === (s_stopped != 0),"stopped matches the model");

      // ---- SAFETY PROPERTIES, independent of the model ----
      // 1. THE property. A TRB whose cycle bit differs from CCS belongs to
      //    software and must not be touched -- what is there is the previous
      //    lap's contents, which look exactly like real TRBs.
      if (trb_valid && (trb_cycle !== ccs)) begin
        check(!consume,
              "an unowned TRB was consumed -- that is last lap's data, not software's");
        check(!follow_link,
              "an unowned Link TRB was followed -- that pointer was never written");
        check(!is_transfer, "an unowned TRB was run as a transfer");
      end
      // 2. Owned and empty are exactly complementary while running.
      check(!(owned && ring_empty),
            "a TRB was both owned and not owned");
      // 3. Consuming and the two kinds of TRB partition cleanly.
      check(!(is_transfer && follow_link),
            "a TRB was both a transfer and a link");
      if (consume) check(is_transfer || follow_link,
                         "a TRB was consumed as neither a transfer nor a link");
      // 4. THE toggle rule. Only a Link TRB carrying Toggle Cycle may invert
      //    the cycle state. Anything else desynchronises the ring for ever.
      if (toggle) begin
        check(follow_link,
              "the cycle state was inverted on something that is not a Link TRB");
        check(trb_toggle_cycle,
              "the cycle state was inverted on a Link TRB with Toggle Cycle CLEAR");
      end
      // 5. A Link TRB without Toggle Cycle never inverts.
      if (follow_link && !trb_toggle_cycle)
        check(!toggle,
              "a plain segment link inverted the cycle state");
      // 6. Nothing happens while the endpoint is not running.
      if (!run) begin
        check(!consume && !ring_empty && !toggle,
              "the ring was consumed with the endpoint stopped");
      end
      // 7. A stopped consumer consumes nothing.
      if (stopped) check(!consume, "a stopped consumer took a TRB");
      // 8. The dequeue pointer moves only for a reason: a consumed TRB
      //    advances it, a followed link relocates it, and nothing else
      //    touches it. (Its RANGE is structural -- a PTRW-bit pointer into a
      //    2**PTRW-entry segment cannot leave it -- so range is not the
      //    property worth asserting here; provenance is.)
      if (!consume && run && (s_stopped == 0))
        check(deq_ptr === s_deq[PTRW-1:0],
              "the dequeue pointer moved with no TRB consumed");

      if (s_deq >= 0 && s_deq < 8) n_deq[s_deq] = n_deq[s_deq] + 1;
      if (e_own)   n_owned   = n_owned + 1;
      if (e_empty) n_unowned = n_unowned + 1;
      if (e_fol)   n_link    = n_link + 1;
      if (e_tog)   n_tog     = n_tog + 1;
      if (e_fol && !trb_toggle_cycle) n_notog = n_notog + 1;
    end
  endtask

  task model_step;
    reg e_running, e_own, e_empty, e_fol, e_xfer, e_tog;
    integer nd;
    begin
      e_running = run && (s_stopped == 0);
      e_own   = e_running && trb_valid && (trb_cycle == s_ccs[0]);
      e_empty = e_running && trb_valid && (trb_cycle != s_ccs[0]);
      e_fol   = e_own && trb_is_link;
      e_xfer  = e_own && !trb_is_link;
      e_tog   = e_fol && trb_toggle_cycle;

      if (e_xfer)  m_tr = m_tr + 1;
      if (e_fol)   m_lk = m_lk + 1;
      if (e_tog)   m_tg = m_tg + 1;
      if (e_empty) m_em = m_em + 1;
      if (run && doorbell && (s_stopped != 0)) m_rs = m_rs + 1;

      // next dequeue pointer
      if (!run)         nd = 0;
      else if (e_fol)   nd = trb_link_target;
      else if (e_own)   nd = (s_deq == RING_N-1) ? 0 : s_deq + 1;
      else              nd = s_deq;
      s_deq = nd;

      if (!run)       s_ccs = 1;
      else if (e_tog) s_ccs = 1 - s_ccs;

      if (!run)        s_stopped = 0;
      else if (doorbell) s_stopped = 0;
      else if (e_empty)  s_stopped = 1;
    end
  endtask

  task step;
    begin
      #1;
      check_comb;
      model_step;
      @(posedge clk); #1;
      check(deq_ptr === s_deq[PTRW-1:0],   "deq_ptr tracked the model");
      check(ccs     === s_ccs[0],          "ccs tracked the model");
      check(stopped === (s_stopped != 0),  "stopped tracked the model");
      check(n_transfers === m_tr[31:0], "n_transfers matches the model");
      check(n_links     === m_lk[31:0], "n_links matches the model");
      check(n_toggles   === m_tg[31:0], "n_toggles matches the model");
      check(n_empty     === m_em[31:0], "n_empty matches the model");
      check(n_restarts  === m_rs[31:0], "n_restarts matches the model");
    end
  endtask

  task idle_in;
    begin
      trb_valid=0; trb_is_link=0; trb_toggle_cycle=0; doorbell=0;
    end
  endtask

  task hard_reset;
    begin
      rst_n=0; run=0; idle_in; trb_cycle=0; trb_link_target=0;
      @(posedge clk); #1; @(posedge clk); #1; rst_n=1; #1;
      s_deq=0; s_ccs=1; s_stopped=0;
      m_tr=0; m_lk=0; m_tg=0; m_em=0; m_rs=0;
    end
  endtask

  // Walk the consumer to a chosen (deq_ptr, ccs, stopped) using only legal
  // transitions: consuming owned transfer TRBs advances the pointer, a Link
  // TRB with Toggle Cycle inverts the cycle state, and an unowned TRB stops.
  task goto_state(input [PTRW-1:0] want_deq, input want_ccs,
                  input want_stopped);
    begin
      hard_reset;
      run=1; step; idle_in;
      if (!want_ccs) begin
        // one Link TRB with Toggle Cycle, pointing back at entry 0
        trb_valid=1; trb_cycle=1; trb_is_link=1; trb_toggle_cycle=1;
        trb_link_target=0; step; idle_in;
      end
      // advance by consuming owned transfer TRBs
      for (p=0; p<want_deq; p=p+1) begin
        trb_valid=1; trb_cycle=want_ccs; trb_is_link=0; step; idle_in;
      end
      if (want_stopped) begin
        // an unowned TRB stops the consumer without moving the pointer
        trb_valid=1; trb_cycle=~want_ccs; trb_is_link=0; step; idle_in;
      end
      #1;
      check(deq_ptr === want_deq, "goto_state reached the dequeue pointer");
      check(ccs === want_ccs,     "goto_state reached the cycle state");
      check(stopped === want_stopped, "goto_state reached the stop latch");
    end
  endtask

  initial begin
    for (i=0;i<8;i=i+1) n_deq[i]=0;
    hard_reset;
    check(ccs === 1'b1,
          "CCS resets to ONE -- a zeroed ring then reads as unowned");
    check(deq_ptr === 3'd0, "and the dequeue pointer to zero");

    // ===== A. EXHAUSTIVE sweep of the ownership and toggle rules =====
    // 8 (deq_ptr) x 2 (ccs) x 2 (run) x 2 (trb_valid) x 2 (trb_cycle)
    //   x 2 (is_link) x 2 (toggle_cycle) x 2 (doorbell)
    // = 1024 one-step transitions, with the link target fixed; the target is
    // swept separately below because it only matters on a followed link.
    for (a=0; a<8; a=a+1)          // deq_ptr
     for (b=0; b<2; b=b+1)         // ccs
      for (c=0; c<2; c=c+1)        // run
       for (d=0; d<2; d=d+1)       // trb_valid
        for (e=0; e<2; e=e+1)      // trb_cycle
         for (f=0; f<2; f=f+1)     // is_link
          for (g=0; g<2; g=g+1)    // toggle_cycle
           for (i=0; i<2; i=i+1) begin   // doorbell
             goto_state(a[PTRW-1:0], b[0], 1'b0);
             run=c[0]; trb_valid=d[0]; trb_cycle=e[0];
             trb_is_link=f[0]; trb_toggle_cycle=g[0];
             trb_link_target=3'd5; doorbell=i[0];
             step;
             n_exh = n_exh + 1;
             idle_in;
           end
    $display("  exhaustive ownership sweep: %0d of %0d transitions verified",
             n_exh, 8*2*2*2*2*2*2*2);

    // ===== B. EXHAUSTIVE link-target sweep =====
    // Every starting pointer against every link target: 8 x 8 = 64 followed
    // links, which is the whole of the pointer-update domain.
    for (a=0; a<8; a=a+1)
     for (b=0; b<8; b=b+1) begin
       goto_state(a[PTRW-1:0], 1'b1, 1'b0);
       trb_valid=1; trb_cycle=1; trb_is_link=1; trb_toggle_cycle=0;
       trb_link_target=b[PTRW-1:0];
       step; idle_in;
       #1;
       check(deq_ptr === b[PTRW-1:0],
             "a followed Link TRB moves the dequeue pointer to its target");
       check(ccs === 1'b1,
             "and leaves the cycle state alone when Toggle Cycle is clear");
       n_lnk_exh = n_lnk_exh + 1;
     end
    $display("  exhaustive link-target sweep: %0d of 64 followed links verified",
             n_lnk_exh);

    // ===== C. directed: one full lap of a ring =====
    hard_reset; run=1; step; idle_in;
    check(ccs === 1'b1, "CCS starts at 1");

    // 1. A zeroed ring reads as unowned: every TRB has Cycle = 0 and CCS is
    //    1, so an untouched ring is empty with no handshake at all.
    trb_valid=1; trb_cycle=0; trb_is_link=0; #1;
    check(!owned, "a zeroed TRB is NOT owned by hardware");
    check(ring_empty, "so the ring reads empty");
    step; idle_in;
    #1; check(stopped, "and the consumer stops");

    // 2. Software enqueues: writes a TRB with Cycle = PCS = 1, then rings.
    doorbell=1; step; idle_in;
    #1; check(!stopped, "the doorbell restarts the consumer");
    check(n_restarts === 32'd1, "and that restart was counted");

    trb_valid=1; trb_cycle=1; trb_is_link=0; step; idle_in;
    check(n_transfers === 32'd1, "the TRB is taken as a transfer");
    #1; check(deq_ptr === 3'd1, "and the pointer advances by one");

    // 3. Three more transfers.
    for (i=0;i<3;i=i+1) begin
      trb_valid=1; trb_cycle=1; trb_is_link=0; step; idle_in;
    end
    #1; check(deq_ptr === 3'd4, "four transfers consumed");
    check(n_transfers === 32'd4, "and counted");

    // 4. A Link TRB that merely joins segments: follow it, do NOT toggle.
    trb_valid=1; trb_cycle=1; trb_is_link=1; trb_toggle_cycle=0;
    trb_link_target=3'd6; #1;
    check(follow_link, "an owned Link TRB is followed");
    check(!is_transfer, "and is NOT counted as a transfer");
    check(!toggle, "and with Toggle Cycle clear it does not invert CCS");
    step; idle_in;
    #1;
    check(deq_ptr === 3'd6, "the pointer moved to the link's target");
    check(ccs === 1'b1, "and the cycle state is unchanged");
    check(n_links === 32'd1, "one link followed");
    check(n_transfers === 32'd4, "and still four transfers");

    // 5. THE case. The Link TRB that closes the ring carries Toggle Cycle.
    trb_valid=1; trb_cycle=1; trb_is_link=1; trb_toggle_cycle=1;
    trb_link_target=3'd0; #1;
    check(toggle, "the closing link inverts the cycle state");
    step; idle_in;
    #1;
    check(deq_ptr === 3'd0, "back to the start of the segment");
    check(ccs === 1'b0, "with CCS now ZERO -- the next lap uses the other value");
    check(n_toggles === 32'd1, "one toggle");

    // 6. And now the OLD TRBs -- the ones from the first lap, still
    //    physically in memory with Cycle = 1 -- read as unowned.
    trb_valid=1; trb_cycle=1; trb_is_link=0; #1;
    check(!owned,
          "last lap's TRB is not owned this lap -- that is the whole mechanism");
    check(ring_empty, "so the ring reads empty");
    step; idle_in;

    // 7. Software's next enqueue writes Cycle = 0, matching the new CCS.
    doorbell=1; step; idle_in;
    trb_valid=1; trb_cycle=0; trb_is_link=0; #1;
    check(owned, "a TRB written with the NEW cycle value is owned");
    step; idle_in;
    check(n_transfers === 32'd5, "and consumed");

    // 8. An unowned LINK TRB is not followed either -- it is the end of what
    //    software has produced, exactly like any other unowned TRB.
    trb_valid=1; trb_cycle=1; trb_is_link=1; trb_toggle_cycle=1;
    trb_link_target=3'd3; #1;
    check(!owned, "an unowned Link TRB is still unowned");
    check(!follow_link, "so it is NOT followed");
    check(!toggle, "and does NOT invert the cycle state");
    step; idle_in;
    #1; check(ccs === 1'b0, "the cycle state survived intact");

    // ===== D. randomised =====
    hard_reset; run=1;
    for (i=0;i<40000;i=i+1) begin
      run              = ({$random}%32)!=0;
      trb_valid        = ({$random}%4)!=0;
      // bias toward OWNED TRBs -- a ring that is mostly unowned never
      // exercises the consume path
      trb_cycle        = (({$random}%4)!=0) ? ccs : ~ccs;
      trb_is_link      = ({$random}%6)==0;
      trb_toggle_cycle = ({$random}%2);
      trb_link_target  = {$random}%8;
      doorbell         = ({$random}%8)==0;
      step;
    end

    for (i=0;i<8;i=i+1)
      check(n_deq[i] > 200, "every dequeue position was occupied many times");
    check(n_owned   > 5000, "owned TRBs were seen many times");
    check(n_unowned > 1000, "unowned TRBs were seen many times");
    check(n_link    > 1000, "Link TRBs were followed many times");
    check(n_tog     > 400,  "the cycle state was toggled many times");
    check(n_notog   > 400,  "and plain segment links were followed many times");

    $display("");
    $display("  REACH: ownership=%0d link-target=%0d | dequeue positions: %0d %0d %0d %0d %0d %0d %0d %0d",
             n_exh, n_lnk_exh, n_deq[0], n_deq[1], n_deq[2], n_deq[3], n_deq[4],
             n_deq[5], n_deq[6], n_deq[7]);
    $display("  CASES: owned=%0d unowned=%0d links-followed=%0d toggling=%0d plain=%0d",
             n_owned, n_unowned, n_link, n_tog, n_notog);
    $display("  COUNTERS: transfers=%0d links=%0d toggles=%0d empty=%0d restarts=%0d",
             n_transfers, n_links, n_toggles, n_empty, n_restarts);
    $display("  [Verilog] xhci_trb_ring: %0d errors", errors);
    $display("  [Verilog] %0s", errors==0 ? "PASS" : "FAIL");
    $display("");
    $finish;
  end
endmodule

`timescale 1ns/1ps
module tb_tr_sv;
  import xhci_ring_pkg::*;

  localparam RING_N = 8, PTRW = 3;
  logic clk=0, rst_n=0;
  logic run=0, trb_valid=0, trb_cycle=0, trb_is_link=0, trb_toggle_cycle=0;
  logic doorbell=0;
  logic [PTRW-1:0] trb_link_target=0;
  logic owned, consume, is_transfer, follow_link, toggle;
  logic ccs, ring_empty, stopped;
  logic [PTRW-1:0] deq_ptr;
  trb_action_e action;
  logic [31:0] n_transfers, n_links, n_toggles, n_empty, n_restarts;

  // Icarus seeds $random and $urandom identically, so an unseeded run would
  // replay the Verilog suite's stimulus exactly. See chapter 20.5 section 9.2.
  int urandom_seed = 22202;
  always #5 clk=~clk;

  xhci_trb_ring #(.RING_N(RING_N), .PTRW(PTRW)) dut (
    .clk, .rst_n, .run, .trb_valid, .trb_cycle, .trb_is_link,
    .trb_toggle_cycle, .trb_link_target, .doorbell, .owned, .consume,
    .is_transfer, .follow_link, .toggle, .action, .deq_ptr, .ccs,
    .ring_empty, .stopped, .n_transfers, .n_links, .n_toggles, .n_empty,
    .n_restarts);

  // ---- SHADOW MODEL of all three registers ----
  int s_deq, s_ccs, s_stopped;
  int m_tr, m_lk, m_tg, m_em, m_rs;

  int errors=0, i, a, b, c, d, e, f, g, p;
  int n_exh=0, n_lnk_exh=0;
  int n_deq [8];
  int n_owned=0, n_unowned=0, n_link=0, n_tog=0, n_notog=0;

  task automatic check(input bit cond, input string msg);
    // Icarus will not call .name() on a net, so the enum output is copied
    // into a variable of the same type before being printed.
    trb_action_e ac_v;
    if (!cond) begin
      errors++;
      ac_v = action;
      if (errors <= 25)
        $display("  FAIL: %0s (run=%b vld=%b cyc=%b link=%b tc=%b tgt=%0d db=%b | act=%s own=%b tog=%b deq=%0d ccs=%b empty=%b stop=%b || model deq=%0d ccs=%0d stop=%0d, t=%0t)",
                 msg, run, trb_valid, trb_cycle, trb_is_link,
                 trb_toggle_cycle, trb_link_target, doorbell, ac_v.name(),
                 owned, toggle, deq_ptr, ccs, ring_empty, stopped, s_deq,
                 s_ccs, s_stopped, $time);
    end
  endtask

  task automatic check_comb;
    bit e_running, e_own, e_empty, e_fol, e_xfer, e_tog;
    trb_action_e e_act;
    begin
      // The model states the ownership test as an XNOR of the two bits where
      // the design compares them -- a different route to the same answer.
      e_running = run && (s_stopped == 0);
      e_own   = e_running && trb_valid && ~(trb_cycle ^ 1'(s_ccs));
      e_empty = e_running && trb_valid && (trb_cycle ^ 1'(s_ccs));
      e_fol   = e_own && trb_is_link;
      e_xfer  = e_own && !trb_is_link;
      e_tog   = e_fol && trb_toggle_cycle;

      check(owned       === e_own,   "owned matches the model");
      check(consume     === e_own,   "consume matches the model");
      check(ring_empty  === e_empty, "ring_empty matches the model");
      check(follow_link === e_fol,   "follow_link matches the model");
      check(is_transfer === e_xfer,  "is_transfer matches the model");
      check(toggle      === e_tog,   "toggle matches the model");

      if      (!e_running || !trb_valid) e_act = TRB_IDLE;
      else if (!e_own)                   e_act = TRB_UNOWNED;
      else if (!trb_is_link)             e_act = TRB_TRANSFER;
      else if (trb_toggle_cycle)         e_act = TRB_LINK_TOG;
      else                               e_act = TRB_LINK;
      check(action === e_act, "action matches the model");
      // The named decision must agree with the booleans it summarises.
      check((action === TRB_TRANSFER) === is_transfer,
            "action disagrees with is_transfer");
      check((action === TRB_LINK_TOG) === toggle,
            "action disagrees with toggle");
      check((action === TRB_UNOWNED) === ring_empty,
            "action disagrees with ring_empty");
      check(deq_ptr     === PTRW'(s_deq), "deq_ptr matches the model");
      check(ccs         === 1'(s_ccs),        "ccs matches the model");
      check(stopped     === (s_stopped != 0),"stopped matches the model");

      // ---- SAFETY PROPERTIES, independent of the model ----
      // 1. THE property. A TRB whose cycle bit differs from CCS belongs to
      //    software and must not be touched -- what is there is the previous
      //    lap's contents, which look exactly like real TRBs.
      if (trb_valid && (trb_cycle !== ccs)) begin
        check(!consume,
              "an unowned TRB was consumed -- that is last lap's data, not software's");
        check(!follow_link,
              "an unowned Link TRB was followed -- that pointer was never written");
        check(!is_transfer, "an unowned TRB was run as a transfer");
      end
      // 2. Owned and empty are exactly complementary while running.
      check(!(owned && ring_empty),
            "a TRB was both owned and not owned");
      // 3. Consuming and the two kinds of TRB partition cleanly.
      check(!(is_transfer && follow_link),
            "a TRB was both a transfer and a link");
      if (consume) check(is_transfer || follow_link,
                         "a TRB was consumed as neither a transfer nor a link");
      // 4. THE toggle rule. Only a Link TRB carrying Toggle Cycle may invert
      //    the cycle state. Anything else desynchronises the ring for ever.
      if (toggle) begin
        check(follow_link,
              "the cycle state was inverted on something that is not a Link TRB");
        check(trb_toggle_cycle,
              "the cycle state was inverted on a Link TRB with Toggle Cycle CLEAR");
      end
      // 5. A Link TRB without Toggle Cycle never inverts.
      if (follow_link && !trb_toggle_cycle)
        check(!toggle,
              "a plain segment link inverted the cycle state");
      // 6. Nothing happens while the endpoint is not running.
      if (!run) begin
        check(!consume && !ring_empty && !toggle,
              "the ring was consumed with the endpoint stopped");
      end
      // 7. A stopped consumer consumes nothing.
      if (stopped) check(!consume, "a stopped consumer took a TRB");
      // 8. The dequeue pointer moves only for a reason: a consumed TRB
      //    advances it, a followed link relocates it, and nothing else
      //    touches it. (Its RANGE is structural -- a PTRW-bit pointer into a
      //    2**PTRW-entry segment cannot leave it -- so range is not the
      //    property worth asserting here; provenance is.)
      if (!consume && run && (s_stopped == 0))
        check(deq_ptr === PTRW'(s_deq),
              "the dequeue pointer moved with no TRB consumed");

      n_deq[s_deq] = n_deq[s_deq] + 1;
      if (e_own)   n_owned   = n_owned + 1;
      if (e_empty) n_unowned = n_unowned + 1;
      if (e_fol)   n_link    = n_link + 1;
      if (e_tog)   n_tog     = n_tog + 1;
      if (e_fol && !trb_toggle_cycle) n_notog = n_notog + 1;
    end
  endtask

  task automatic model_step;
    bit e_running, e_own, e_empty, e_fol, e_xfer, e_tog;
    int nd;
    begin
      e_running = run && (s_stopped == 0);
      e_own   = e_running && trb_valid && (trb_cycle == 1'(s_ccs));
      e_empty = e_running && trb_valid && (trb_cycle != 1'(s_ccs));
      e_fol   = e_own && trb_is_link;
      e_xfer  = e_own && !trb_is_link;
      e_tog   = e_fol && trb_toggle_cycle;

      if (e_xfer)  m_tr = m_tr + 1;
      if (e_fol)   m_lk = m_lk + 1;
      if (e_tog)   m_tg = m_tg + 1;
      if (e_empty) m_em = m_em + 1;
      if (run && doorbell && (s_stopped != 0)) m_rs = m_rs + 1;

      // next dequeue pointer
      if (!run)         nd = 0;
      else if (e_fol)   nd = trb_link_target;
      else if (e_own)   nd = (s_deq == RING_N-1) ? 0 : s_deq + 1;
      else              nd = s_deq;
      s_deq = nd;

      if (!run)       s_ccs = 1;
      else if (e_tog) s_ccs = 1 - s_ccs;

      if (!run)        s_stopped = 0;
      else if (doorbell) s_stopped = 0;
      else if (e_empty)  s_stopped = 1;
    end
  endtask

  task automatic step;
    begin
      #1;
      check_comb;
      model_step;
      @(posedge clk); #1;
      check(deq_ptr === PTRW'(s_deq),   "deq_ptr tracked the model");
      check(ccs     === 1'(s_ccs),          "ccs tracked the model");
      check(stopped === (s_stopped != 0),  "stopped tracked the model");
      check(n_transfers === 32'(m_tr), "n_transfers matches the model");
      check(n_links     === 32'(m_lk), "n_links matches the model");
      check(n_toggles   === 32'(m_tg), "n_toggles matches the model");
      check(n_empty     === 32'(m_em), "n_empty matches the model");
      check(n_restarts  === 32'(m_rs), "n_restarts matches the model");
    end
  endtask

  task automatic idle_in;
    begin
      trb_valid=0; trb_is_link=0; trb_toggle_cycle=0; doorbell=0;
    end
  endtask

  task automatic hard_reset;
    begin
      rst_n=0; run=0; idle_in; trb_cycle=0; trb_link_target=0;
      @(posedge clk); #1; @(posedge clk); #1; rst_n=1; #1;
      s_deq=0; s_ccs=1; s_stopped=0;
      m_tr=0; m_lk=0; m_tg=0; m_em=0; m_rs=0;
    end
  endtask

  // Walk the consumer to a chosen (deq_ptr, ccs, stopped) using only legal
  // transitions: consuming owned transfer TRBs advances the pointer, a Link
  // TRB with Toggle Cycle inverts the cycle state, and an unowned TRB stops.
  task automatic goto_state(input logic [PTRW-1:0] want_deq,
                            input bit want_ccs, input bit want_stopped);
    begin
      hard_reset;
      run=1; step; idle_in;
      if (!want_ccs) begin
        // one Link TRB with Toggle Cycle, pointing back at entry 0
        trb_valid=1; trb_cycle=1; trb_is_link=1; trb_toggle_cycle=1;
        trb_link_target=0; step; idle_in;
      end
      // advance by consuming owned transfer TRBs
      for (p=0; p<want_deq; p=p+1) begin
        trb_valid=1; trb_cycle=want_ccs; trb_is_link=0; step; idle_in;
      end
      if (want_stopped) begin
        // an unowned TRB stops the consumer without moving the pointer
        trb_valid=1; trb_cycle=~want_ccs; trb_is_link=0; step; idle_in;
      end
      #1;
      check(deq_ptr === want_deq, "goto_state reached the dequeue pointer");
      check(ccs === want_ccs,     "goto_state reached the cycle state");
      check(stopped === want_stopped, "goto_state reached the stop latch");
    end
  endtask

  initial begin
    void'($urandom(urandom_seed));
    foreach (n_deq[i]) n_deq[i]=0;
    hard_reset;
    check(ccs === 1'b1,
          "CCS resets to ONE -- a zeroed ring then reads as unowned");
    check(deq_ptr === 3'd0, "and the dequeue pointer to zero");

    // ===== A. EXHAUSTIVE sweep of the ownership and toggle rules =====
    // 8 (deq_ptr) x 2 (ccs) x 2 (run) x 2 (trb_valid) x 2 (trb_cycle)
    //   x 2 (is_link) x 2 (toggle_cycle) x 2 (doorbell)
    // = 1024 one-step transitions, with the link target fixed; the target is
    // swept separately below because it only matters on a followed link.
    for (a=0; a<8; a=a+1)          // deq_ptr
     for (b=0; b<2; b=b+1)         // ccs
      for (c=0; c<2; c=c+1)        // run
       for (d=0; d<2; d=d+1)       // trb_valid
        for (e=0; e<2; e=e+1)      // trb_cycle
         for (f=0; f<2; f=f+1)     // is_link
          for (g=0; g<2; g=g+1)    // toggle_cycle
           for (i=0; i<2; i=i+1) begin   // doorbell
             goto_state(PTRW'(a), b[0], 1'b0);
             run=c[0]; trb_valid=d[0]; trb_cycle=e[0];
             trb_is_link=f[0]; trb_toggle_cycle=g[0];
             trb_link_target=3'd5; doorbell=i[0];
             step;
             n_exh = n_exh + 1;
             idle_in;
           end
    $display("  exhaustive ownership sweep: %0d of %0d transitions verified",
             n_exh, 8*2*2*2*2*2*2*2);

    // ===== B. EXHAUSTIVE link-target sweep =====
    // Every starting pointer against every link target: 8 x 8 = 64 followed
    // links, which is the whole of the pointer-update domain.
    for (a=0; a<8; a=a+1)
     for (b=0; b<8; b=b+1) begin
       goto_state(PTRW'(a), 1'b1, 1'b0);
       trb_valid=1; trb_cycle=1; trb_is_link=1; trb_toggle_cycle=0;
       trb_link_target=PTRW'(b);
       step; idle_in;
       #1;
       check(deq_ptr === PTRW'(b),
             "a followed Link TRB moves the dequeue pointer to its target");
       check(ccs === 1'b1,
             "and leaves the cycle state alone when Toggle Cycle is clear");
       n_lnk_exh = n_lnk_exh + 1;
     end
    $display("  exhaustive link-target sweep: %0d of 64 followed links verified",
             n_lnk_exh);

    // ===== C. directed: one full lap of a ring =====
    hard_reset; run=1; step; idle_in;
    check(ccs === 1'b1, "CCS starts at 1");

    // 1. A zeroed ring reads as unowned: every TRB has Cycle = 0 and CCS is
    //    1, so an untouched ring is empty with no handshake at all.
    trb_valid=1; trb_cycle=0; trb_is_link=0; #1;
    check(!owned, "a zeroed TRB is NOT owned by hardware");
    check(ring_empty, "so the ring reads empty");
    step; idle_in;
    #1; check(stopped, "and the consumer stops");

    // 2. Software enqueues: writes a TRB with Cycle = PCS = 1, then rings.
    doorbell=1; step; idle_in;
    #1; check(!stopped, "the doorbell restarts the consumer");
    check(n_restarts === 32'd1, "and that restart was counted");

    trb_valid=1; trb_cycle=1; trb_is_link=0; step; idle_in;
    check(n_transfers === 32'd1, "the TRB is taken as a transfer");
    #1; check(deq_ptr === 3'd1, "and the pointer advances by one");

    // 3. Three more transfers.
    for (i=0;i<3;i=i+1) begin
      trb_valid=1; trb_cycle=1; trb_is_link=0; step; idle_in;
    end
    #1; check(deq_ptr === 3'd4, "four transfers consumed");
    check(n_transfers === 32'd4, "and counted");

    // 4. A Link TRB that merely joins segments: follow it, do NOT toggle.
    trb_valid=1; trb_cycle=1; trb_is_link=1; trb_toggle_cycle=0;
    trb_link_target=3'd6; #1;
    check(follow_link, "an owned Link TRB is followed");
    check(!is_transfer, "and is NOT counted as a transfer");
    check(!toggle, "and with Toggle Cycle clear it does not invert CCS");
    step; idle_in;
    #1;
    check(deq_ptr === 3'd6, "the pointer moved to the link's target");
    check(ccs === 1'b1, "and the cycle state is unchanged");
    check(n_links === 32'd1, "one link followed");
    check(n_transfers === 32'd4, "and still four transfers");

    // 5. THE case. The Link TRB that closes the ring carries Toggle Cycle.
    trb_valid=1; trb_cycle=1; trb_is_link=1; trb_toggle_cycle=1;
    trb_link_target=3'd0; #1;
    check(toggle, "the closing link inverts the cycle state");
    step; idle_in;
    #1;
    check(deq_ptr === 3'd0, "back to the start of the segment");
    check(ccs === 1'b0, "with CCS now ZERO -- the next lap uses the other value");
    check(n_toggles === 32'd1, "one toggle");

    // 6. And now the OLD TRBs -- the ones from the first lap, still
    //    physically in memory with Cycle = 1 -- read as unowned.
    trb_valid=1; trb_cycle=1; trb_is_link=0; #1;
    check(!owned,
          "last lap's TRB is not owned this lap -- that is the whole mechanism");
    check(ring_empty, "so the ring reads empty");
    step; idle_in;

    // 7. Software's next enqueue writes Cycle = 0, matching the new CCS.
    doorbell=1; step; idle_in;
    trb_valid=1; trb_cycle=0; trb_is_link=0; #1;
    check(owned, "a TRB written with the NEW cycle value is owned");
    step; idle_in;
    check(n_transfers === 32'd5, "and consumed");

    // 8. An unowned LINK TRB is not followed either -- it is the end of what
    //    software has produced, exactly like any other unowned TRB.
    trb_valid=1; trb_cycle=1; trb_is_link=1; trb_toggle_cycle=1;
    trb_link_target=3'd3; #1;
    check(!owned, "an unowned Link TRB is still unowned");
    check(!follow_link, "so it is NOT followed");
    check(!toggle, "and does NOT invert the cycle state");
    step; idle_in;
    #1; check(ccs === 1'b0, "the cycle state survived intact");

    // ===== D. randomised =====
    hard_reset; run=1;
    for (i=0;i<40000;i=i+1) begin
      run              = ($urandom%32)!=0;
      trb_valid        = ($urandom%4)!=0;
      // bias toward OWNED TRBs -- a ring that is mostly unowned never
      // exercises the consume path
      trb_cycle        = (($urandom%4)!=0) ? ccs : ~ccs;
      trb_is_link      = ($urandom%6)==0;
      trb_toggle_cycle = $urandom%2;
      trb_link_target  = PTRW'($urandom%8);
      doorbell         = ($urandom%8)==0;
      step;
    end

    foreach (n_deq[i])
      check(n_deq[i] > 200, "every dequeue position was occupied many times");
    check(n_owned   > 5000, "owned TRBs were seen many times");
    check(n_unowned > 1000, "unowned TRBs were seen many times");
    check(n_link    > 1000, "Link TRBs were followed many times");
    check(n_tog     > 400,  "the cycle state was toggled many times");
    check(n_notog   > 400,  "and plain segment links were followed many times");

    $display("");
    $display("  REACH: ownership=%0d link-target=%0d | dequeue positions: %0d %0d %0d %0d %0d %0d %0d %0d",
             n_exh, n_lnk_exh, n_deq[0], n_deq[1], n_deq[2], n_deq[3], n_deq[4],
             n_deq[5], n_deq[6], n_deq[7]);
    $display("  CASES: owned=%0d unowned=%0d links-followed=%0d toggling=%0d plain=%0d",
             n_owned, n_unowned, n_link, n_tog, n_notog);
    $display("  COUNTERS: transfers=%0d links=%0d toggles=%0d empty=%0d restarts=%0d",
             n_transfers, n_links, n_toggles, n_empty, n_restarts);
    $display("  [SystemVerilog] xhci_trb_ring: %0d errors", errors);
    $display("  [SystemVerilog] %0s", errors==0 ? "PASS" : "FAIL");
    $display("");
    $finish;
  end
endmodule

library ieee;
use ieee.std_logic_1164.all;
use ieee.numeric_std.all;
use ieee.math_real.all;
use work.xhci_ring_pkg.all;

entity tb_tr_vhdl is
end entity;

architecture sim of tb_tr_vhdl is
  constant RING_N : natural := 8;
  constant PTRW   : natural := 3;

  signal clk   : std_logic := '0';
  signal rst_n : std_logic := '0';
  signal run, trb_valid, trb_cycle, trb_is_link : std_logic := '0';
  signal trb_toggle_cycle, doorbell : std_logic := '0';
  signal trb_link_target : std_logic_vector(PTRW-1 downto 0)
       := (others => '0');

  signal owned, consume, is_transfer, follow_link, toggle : std_logic;
  signal ccs, ring_empty, stopped : std_logic;
  signal deq_ptr : std_logic_vector(PTRW-1 downto 0);
  signal action  : std_logic_vector(2 downto 0);
  signal n_transfers, n_links, n_toggles, n_empty, n_restarts
       : std_logic_vector(31 downto 0);

  signal running_sim : boolean := true;

  type cnt8_t is array (0 to 7) of integer;
begin
  clk <= not clk after 5 ns when running_sim else '0';

  dut : entity work.xhci_trb_ring
    generic map (RING_N => RING_N, PTRW => PTRW)
    port map (clk => clk, rst_n => rst_n, run => run,
              trb_valid => trb_valid, trb_cycle => trb_cycle,
              trb_is_link => trb_is_link,
              trb_toggle_cycle => trb_toggle_cycle,
              trb_link_target => trb_link_target, doorbell => doorbell,
              owned => owned, consume => consume, is_transfer => is_transfer,
              follow_link => follow_link, toggle => toggle, action => action,
              deq_ptr => deq_ptr, ccs => ccs, ring_empty => ring_empty,
              stopped => stopped, n_transfers => n_transfers,
              n_links => n_links, n_toggles => n_toggles, n_empty => n_empty,
              n_restarts => n_restarts);

  stim : process
    variable seed1 : positive := 6473;
    variable seed2 : positive := 1987;
    variable r1    : real;

    -- VHDL-2008 requires a shared variable to have a protected type, so the
    -- bookkeeping lives inside the single stimulus process instead.
    variable errors : integer := 0;

    -- SHADOW MODEL of all three registers.
    variable s_deq : integer := 0;
    variable s_ccs : std_logic := '1';
    variable s_stopped : integer := 0;
    variable m_tr, m_lk, m_tg, m_em, m_rs : integer := 0;

    variable n_exh, n_lnk_exh : integer := 0;
    variable n_deq : cnt8_t := (others => 0);
    variable n_owned, n_unowned, n_link, n_tog, n_notog : integer := 0;

    procedure check(cond : boolean; msg : string) is
    begin
      if not cond then
        errors := errors + 1;
        if errors <= 25 then
          report "  FAIL: " & msg
               & " (run=" & std_logic'image(run)(2)
               & " vld=" & std_logic'image(trb_valid)(2)
               & " cyc=" & std_logic'image(trb_cycle)(2)
               & " link=" & std_logic'image(trb_is_link)(2)
               & " tc=" & std_logic'image(trb_toggle_cycle)(2)
               & " tgt=" & integer'image(to_integer(unsigned(trb_link_target)))
               & " db=" & std_logic'image(doorbell)(2)
               & " | act=" & integer'image(to_integer(unsigned(action)))
               & " own=" & std_logic'image(owned)(2)
               & " tog=" & std_logic'image(toggle)(2)
               & " deq=" & integer'image(to_integer(unsigned(deq_ptr)))
               & " ccs=" & std_logic'image(ccs)(2)
               & " empty=" & std_logic'image(ring_empty)(2)
               & " stop=" & std_logic'image(stopped)(2)
               & " || model deq=" & integer'image(s_deq)
               & " ccs=" & std_logic'image(s_ccs)(2)
               & " stop=" & integer'image(s_stopped)
               & ")" severity note;
        end if;
      end if;
    end procedure;

    procedure rnd(variable v : out integer; m : integer) is
    begin
      uniform(seed1, seed2, r1);
      v := integer(floor(r1 * real(m)));
    end procedure;

    procedure check_comb is
      variable e_running, e_own, e_empty, e_fol, e_xfer, e_tog : boolean;
      variable e_act : trb_action_t;
    begin
      -- The model states the ownership test as "not different" where the
      -- design compares for equality -- a different route to the same answer.
      e_running := run = '1' and s_stopped = 0;
      e_own   := e_running and trb_valid = '1' and not (trb_cycle /= s_ccs);
      e_empty := e_running and trb_valid = '1' and (trb_cycle /= s_ccs);
      e_fol   := e_own and trb_is_link = '1';
      e_xfer  := e_own and trb_is_link = '0';
      e_tog   := e_fol and trb_toggle_cycle = '1';

      check((owned = '1') = e_own,          "owned matches the model");
      check((consume = '1') = e_own,        "consume matches the model");
      check((ring_empty = '1') = e_empty,   "ring_empty matches the model");
      check((follow_link = '1') = e_fol,    "follow_link matches the model");
      check((is_transfer = '1') = e_xfer,   "is_transfer matches the model");
      check((toggle = '1') = e_tog,         "toggle matches the model");
      check(to_integer(unsigned(deq_ptr)) = s_deq, "deq_ptr matches the model");
      check(ccs = s_ccs,                    "ccs matches the model");
      check((stopped = '1') = (s_stopped /= 0), "stopped matches the model");

      if not e_running or trb_valid = '0' then e_act := TRB_IDLE;
      elsif not e_own then                     e_act := TRB_UNOWNED;
      elsif trb_is_link = '0' then             e_act := TRB_TRANSFER;
      elsif trb_toggle_cycle = '1' then        e_act := TRB_LINK_TOG;
      else                                     e_act := TRB_LINK;
      end if;
      check(action = act_code(e_act), "action matches the model");
      -- The named decision must agree with the booleans it summarises.
      check((action = act_code(TRB_TRANSFER)) = (is_transfer = '1'),
            "action disagrees with is_transfer");
      check((action = act_code(TRB_LINK_TOG)) = (toggle = '1'),
            "action disagrees with toggle");
      check((action = act_code(TRB_UNOWNED)) = (ring_empty = '1'),
            "action disagrees with ring_empty");

      -- ---- SAFETY PROPERTIES, independent of the model ----
      -- 1. THE property. A TRB whose cycle bit differs from CCS belongs to
      --    software and must not be touched.
      if trb_valid = '1' and trb_cycle /= ccs then
        check(consume = '0',
              "an unowned TRB was consumed -- that is last lap's data, not software's");
        check(follow_link = '0',
              "an unowned Link TRB was followed -- that pointer was never written");
        check(is_transfer = '0', "an unowned TRB was run as a transfer");
      end if;
      -- 2. Owned and empty are exactly complementary while running.
      check(not (owned = '1' and ring_empty = '1'),
            "a TRB was both owned and not owned");
      -- 3. Consuming and the two kinds of TRB partition cleanly.
      check(not (is_transfer = '1' and follow_link = '1'),
            "a TRB was both a transfer and a link");
      if consume = '1' then
        check(is_transfer = '1' or follow_link = '1',
              "a TRB was consumed as neither a transfer nor a link");
      end if;
      -- 4. THE toggle rule. Only a Link TRB carrying Toggle Cycle may invert
      --    the cycle state.
      if toggle = '1' then
        check(follow_link = '1',
              "the cycle state was inverted on something that is not a Link TRB");
        check(trb_toggle_cycle = '1',
              "the cycle state was inverted on a Link TRB with Toggle Cycle CLEAR");
      end if;
      -- 5. A Link TRB without Toggle Cycle never inverts.
      if follow_link = '1' and trb_toggle_cycle = '0' then
        check(toggle = '0', "a plain segment link inverted the cycle state");
      end if;
      -- 6. Nothing happens while the endpoint is not running.
      if run = '0' then
        check(consume = '0' and ring_empty = '0' and toggle = '0',
              "the ring was consumed with the endpoint stopped");
      end if;
      -- 7. A stopped consumer consumes nothing.
      if stopped = '1' then
        check(consume = '0', "a stopped consumer took a TRB");
      end if;
      -- 8. The dequeue pointer moves only for a reason.
      if consume = '0' and run = '1' and s_stopped = 0 then
        check(to_integer(unsigned(deq_ptr)) = s_deq,
              "the dequeue pointer moved with no TRB consumed");
      end if;

      n_deq(s_deq) := n_deq(s_deq) + 1;
      if e_own   then n_owned   := n_owned + 1;   end if;
      if e_empty then n_unowned := n_unowned + 1; end if;
      if e_fol   then n_link    := n_link + 1;    end if;
      if e_tog   then n_tog     := n_tog + 1;     end if;
      if e_fol and trb_toggle_cycle = '0' then n_notog := n_notog + 1; end if;
    end procedure;

    procedure model_step is
      variable e_running, e_own, e_empty, e_fol, e_xfer, e_tog : boolean;
      variable nd : integer;
    begin
      e_running := run = '1' and s_stopped = 0;
      e_own   := e_running and trb_valid = '1' and trb_cycle = s_ccs;
      e_empty := e_running and trb_valid = '1' and trb_cycle /= s_ccs;
      e_fol   := e_own and trb_is_link = '1';
      e_xfer  := e_own and trb_is_link = '0';
      e_tog   := e_fol and trb_toggle_cycle = '1';

      if e_xfer  then m_tr := m_tr + 1; end if;
      if e_fol   then m_lk := m_lk + 1; end if;
      if e_tog   then m_tg := m_tg + 1; end if;
      if e_empty then m_em := m_em + 1; end if;
      if run = '1' and doorbell = '1' and s_stopped /= 0 then
        m_rs := m_rs + 1;
      end if;

      if run = '0' then    nd := 0;
      elsif e_fol then     nd := to_integer(unsigned(trb_link_target));
      elsif e_own then
        if s_deq = RING_N - 1 then nd := 0; else nd := s_deq + 1; end if;
      else                 nd := s_deq;
      end if;
      s_deq := nd;

      if run = '0' then    s_ccs := '1';
      elsif e_tog then     s_ccs := not s_ccs;
      end if;

      if run = '0' then        s_stopped := 0;
      elsif doorbell = '1' then s_stopped := 0;
      elsif e_empty then       s_stopped := 1;
      end if;
    end procedure;

    procedure step is
    begin
      wait for 1 ns;
      check_comb;
      model_step;
      wait until rising_edge(clk);
      wait for 1 ns;
      check(to_integer(unsigned(deq_ptr)) = s_deq, "deq_ptr tracked the model");
      check(ccs = s_ccs, "ccs tracked the model");
      check((stopped = '1') = (s_stopped /= 0), "stopped tracked the model");
      check(n_transfers = std_logic_vector(to_unsigned(m_tr, 32)),
            "n_transfers matches the model");
      check(n_links = std_logic_vector(to_unsigned(m_lk, 32)),
            "n_links matches the model");
      check(n_toggles = std_logic_vector(to_unsigned(m_tg, 32)),
            "n_toggles matches the model");
      check(n_empty = std_logic_vector(to_unsigned(m_em, 32)),
            "n_empty matches the model");
      check(n_restarts = std_logic_vector(to_unsigned(m_rs, 32)),
            "n_restarts matches the model");
    end procedure;

    procedure idle_in is
    begin
      trb_valid <= '0'; trb_is_link <= '0'; trb_toggle_cycle <= '0';
      doorbell <= '0';
    end procedure;

    procedure hard_reset is
    begin
      rst_n <= '0'; run <= '0'; idle_in; trb_cycle <= '0';
      trb_link_target <= (others => '0');
      wait until rising_edge(clk); wait for 1 ns;
      wait until rising_edge(clk); wait for 1 ns;
      rst_n <= '1'; wait for 1 ns;
      s_deq := 0; s_ccs := '1'; s_stopped := 0;
      m_tr := 0; m_lk := 0; m_tg := 0; m_em := 0; m_rs := 0;
    end procedure;

    -- Walk the consumer to a chosen (deq_ptr, ccs, stopped) using only legal
    -- transitions: consuming owned transfer TRBs advances the pointer, a Link
    -- TRB with Toggle Cycle inverts the cycle state, and an unowned TRB stops.
    procedure goto_state(want_deq : integer; want_ccs : std_logic;
                         want_stopped : std_logic) is
    begin
      hard_reset;
      run <= '1'; step; idle_in;
      if want_ccs = '0' then
        trb_valid <= '1'; trb_cycle <= '1'; trb_is_link <= '1';
        trb_toggle_cycle <= '1'; trb_link_target <= (others => '0');
        step; idle_in;
      end if;
      for p in 0 to want_deq - 1 loop
        trb_valid <= '1'; trb_cycle <= want_ccs; trb_is_link <= '0';
        step; idle_in;
      end loop;
      if want_stopped = '1' then
        trb_valid <= '1'; trb_cycle <= not want_ccs; trb_is_link <= '0';
        step; idle_in;
      end if;
      wait for 1 ns;
      check(to_integer(unsigned(deq_ptr)) = want_deq,
            "goto_state reached the dequeue pointer");
      check(ccs = want_ccs, "goto_state reached the cycle state");
      check(stopped = want_stopped, "goto_state reached the stop latch");
    end procedure;

    variable iv : integer;
    variable bb, bc, bd, be, bf, bg, bi : std_logic;
  begin
    hard_reset;
    check(ccs = '1',
          "CCS resets to ONE -- a zeroed ring then reads as unowned");
    check(to_integer(unsigned(deq_ptr)) = 0,
          "and the dequeue pointer to zero");

    -- ===== A. EXHAUSTIVE sweep of the ownership and toggle rules =====
    -- 8 (deq_ptr) x 2 (ccs) x 2 (run) x 2 (trb_valid) x 2 (trb_cycle)
    --   x 2 (is_link) x 2 (toggle_cycle) x 2 (doorbell)
    -- = 1024 one-step transitions, with the link target fixed; the target is
    -- swept separately below because it only matters on a followed link.
    for a in 0 to 7 loop
      for b in 0 to 1 loop
        if b = 1 then bb := '1'; else bb := '0'; end if;
        for c in 0 to 1 loop
          if c = 1 then bc := '1'; else bc := '0'; end if;
          for d in 0 to 1 loop
            if d = 1 then bd := '1'; else bd := '0'; end if;
            for e in 0 to 1 loop
              if e = 1 then be := '1'; else be := '0'; end if;
              for f in 0 to 1 loop
                if f = 1 then bf := '1'; else bf := '0'; end if;
                for g in 0 to 1 loop
                  if g = 1 then bg := '1'; else bg := '0'; end if;
                  for i2 in 0 to 1 loop
                    if i2 = 1 then bi := '1'; else bi := '0'; end if;
                    goto_state(a, bb, '0');
                    run <= bc; trb_valid <= bd; trb_cycle <= be;
                    trb_is_link <= bf; trb_toggle_cycle <= bg;
                    trb_link_target <= std_logic_vector(to_unsigned(5, PTRW));
                    doorbell <= bi;
                    step;
                    n_exh := n_exh + 1;
                    idle_in;
                  end loop;
                end loop;
              end loop;
            end loop;
          end loop;
        end loop;
      end loop;
    end loop;
    report "  exhaustive ownership sweep: " & integer'image(n_exh)
         & " of 1024 transitions verified" severity note;

    -- ===== B. EXHAUSTIVE link-target sweep =====
    -- Every starting pointer against every link target: 8 x 8 = 64 followed
    -- links, which is the whole of the pointer-update domain.
    for a in 0 to 7 loop
      for b in 0 to 7 loop
        goto_state(a, '1', '0');
        trb_valid <= '1'; trb_cycle <= '1'; trb_is_link <= '1';
        trb_toggle_cycle <= '0';
        trb_link_target <= std_logic_vector(to_unsigned(b, PTRW));
        step; idle_in;
        wait for 1 ns;
        check(to_integer(unsigned(deq_ptr)) = b,
              "a followed Link TRB moves the dequeue pointer to its target");
        check(ccs = '1',
              "and leaves the cycle state alone when Toggle Cycle is clear");
        n_lnk_exh := n_lnk_exh + 1;
      end loop;
    end loop;
    report "  exhaustive link-target sweep: " & integer'image(n_lnk_exh)
         & " of 64 followed links verified" severity note;

    -- ===== C. directed: one full lap of a ring =====
    hard_reset; run <= '1'; step; idle_in;
    check(ccs = '1', "CCS starts at 1");

    -- 1. A zeroed ring reads as unowned.
    trb_valid <= '1'; trb_cycle <= '0'; trb_is_link <= '0';
    wait for 1 ns;
    check(owned = '0', "a zeroed TRB is NOT owned by hardware");
    check(ring_empty = '1', "so the ring reads empty");
    step; idle_in;
    wait for 1 ns;
    check(stopped = '1', "and the consumer stops");

    -- 2. Software enqueues: writes a TRB with Cycle = PCS = 1, then rings.
    doorbell <= '1'; step; idle_in;
    wait for 1 ns;
    check(stopped = '0', "the doorbell restarts the consumer");
    check(n_restarts = std_logic_vector(to_unsigned(1, 32)),
          "and that restart was counted");

    trb_valid <= '1'; trb_cycle <= '1'; trb_is_link <= '0'; step; idle_in;
    check(n_transfers = std_logic_vector(to_unsigned(1, 32)),
          "the TRB is taken as a transfer");
    wait for 1 ns;
    check(to_integer(unsigned(deq_ptr)) = 1,
          "and the pointer advances by one");

    -- 3. Three more transfers.
    for i in 0 to 2 loop
      trb_valid <= '1'; trb_cycle <= '1'; trb_is_link <= '0'; step; idle_in;
    end loop;
    wait for 1 ns;
    check(to_integer(unsigned(deq_ptr)) = 4, "four transfers consumed");
    check(n_transfers = std_logic_vector(to_unsigned(4, 32)), "and counted");

    -- 4. A Link TRB that merely joins segments: follow it, do NOT toggle.
    trb_valid <= '1'; trb_cycle <= '1'; trb_is_link <= '1';
    trb_toggle_cycle <= '0';
    trb_link_target <= std_logic_vector(to_unsigned(6, PTRW));
    wait for 1 ns;
    check(follow_link = '1', "an owned Link TRB is followed");
    check(is_transfer = '0', "and is NOT counted as a transfer");
    check(toggle = '0',
          "and with Toggle Cycle clear it does not invert CCS");
    step; idle_in;
    wait for 1 ns;
    check(to_integer(unsigned(deq_ptr)) = 6,
          "the pointer moved to the link's target");
    check(ccs = '1', "and the cycle state is unchanged");
    check(n_links = std_logic_vector(to_unsigned(1, 32)),
          "one link followed");
    check(n_transfers = std_logic_vector(to_unsigned(4, 32)),
          "and still four transfers");

    -- 5. THE case. The Link TRB that closes the ring carries Toggle Cycle.
    trb_valid <= '1'; trb_cycle <= '1'; trb_is_link <= '1';
    trb_toggle_cycle <= '1';
    trb_link_target <= (others => '0');
    wait for 1 ns;
    check(toggle = '1', "the closing link inverts the cycle state");
    step; idle_in;
    wait for 1 ns;
    check(to_integer(unsigned(deq_ptr)) = 0,
          "back to the start of the segment");
    check(ccs = '0',
          "with CCS now ZERO -- the next lap uses the other value");
    check(n_toggles = std_logic_vector(to_unsigned(1, 32)), "one toggle");

    -- 6. And now the OLD TRBs read as unowned.
    trb_valid <= '1'; trb_cycle <= '1'; trb_is_link <= '0';
    wait for 1 ns;
    check(owned = '0',
          "last lap's TRB is not owned this lap -- that is the whole mechanism");
    check(ring_empty = '1', "so the ring reads empty");
    step; idle_in;

    -- 7. Software's next enqueue writes Cycle = 0, matching the new CCS.
    doorbell <= '1'; step; idle_in;
    trb_valid <= '1'; trb_cycle <= '0'; trb_is_link <= '0';
    wait for 1 ns;
    check(owned = '1', "a TRB written with the NEW cycle value is owned");
    step; idle_in;
    check(n_transfers = std_logic_vector(to_unsigned(5, 32)), "and consumed");

    -- 8. An unowned LINK TRB is not followed either.
    trb_valid <= '1'; trb_cycle <= '1'; trb_is_link <= '1';
    trb_toggle_cycle <= '1';
    trb_link_target <= std_logic_vector(to_unsigned(3, PTRW));
    wait for 1 ns;
    check(owned = '0', "an unowned Link TRB is still unowned");
    check(follow_link = '0', "so it is NOT followed");
    check(toggle = '0', "and does NOT invert the cycle state");
    step; idle_in;
    wait for 1 ns;
    check(ccs = '0', "the cycle state survived intact");

    -- ===== D. randomised =====
    -- ieee.math_real.uniform is a genuinely different generator from either
    -- Verilog builtin, which is what makes this column independent evidence.
    hard_reset; run <= '1';
    for i in 0 to 39999 loop
      rnd(iv, 32); if iv /= 0 then run <= '1'; else run <= '0'; end if;
      rnd(iv, 4);  if iv /= 0 then trb_valid <= '1';
                   else trb_valid <= '0'; end if;
      -- bias toward OWNED TRBs -- a ring that is mostly unowned never
      -- exercises the consume path
      rnd(iv, 4);
      if iv /= 0 then trb_cycle <= ccs; else trb_cycle <= not ccs; end if;
      rnd(iv, 6);  if iv = 0 then trb_is_link <= '1';
                   else trb_is_link <= '0'; end if;
      rnd(iv, 2);  if iv = 1 then trb_toggle_cycle <= '1';
                   else trb_toggle_cycle <= '0'; end if;
      rnd(iv, 8);  trb_link_target <= std_logic_vector(to_unsigned(iv, PTRW));
      rnd(iv, 8);  if iv = 0 then doorbell <= '1';
                   else doorbell <= '0'; end if;
      step;
    end loop;

    for i in 0 to 7 loop
      check(n_deq(i) > 200, "every dequeue position was occupied many times");
    end loop;
    check(n_owned   > 5000, "owned TRBs were seen many times");
    check(n_unowned > 1000, "unowned TRBs were seen many times");
    check(n_link    > 1000, "Link TRBs were followed many times");
    check(n_tog     > 400,  "the cycle state was toggled many times");
    check(n_notog   > 400,  "and plain segment links were followed many times");

    report "  REACH: ownership=" & integer'image(n_exh)
         & " link-target=" & integer'image(n_lnk_exh)
         & " | dequeue positions: " & integer'image(n_deq(0))
         & " " & integer'image(n_deq(1)) & " " & integer'image(n_deq(2))
         & " " & integer'image(n_deq(3)) & " " & integer'image(n_deq(4))
         & " " & integer'image(n_deq(5)) & " " & integer'image(n_deq(6))
         & " " & integer'image(n_deq(7)) severity note;
    report "  CASES: owned=" & integer'image(n_owned)
         & " unowned=" & integer'image(n_unowned)
         & " links-followed=" & integer'image(n_link)
         & " toggling=" & integer'image(n_tog)
         & " plain=" & integer'image(n_notog) severity note;
    report "  COUNTERS: transfers="
         & integer'image(to_integer(unsigned(n_transfers)))
         & " links=" & integer'image(to_integer(unsigned(n_links)))
         & " toggles=" & integer'image(to_integer(unsigned(n_toggles)))
         & " empty=" & integer'image(to_integer(unsigned(n_empty)))
         & " restarts=" & integer'image(to_integer(unsigned(n_restarts)))
         severity note;
    report "  [VHDL] xhci_trb_ring: " & integer'image(errors) & " errors"
         severity note;
    if errors = 0 then
      report "  [VHDL] PASS" severity note;
    else
      report "  [VHDL] FAIL" severity failure;
    end if;
    running_sim <= false;
    wait;
  end process;
end architecture;