The Endpoints Question

   Indexed by NUMBER:              Indexed by (NUMBER, DIRECTION):

     table[4]                        table[4][2]
       halt(1) -> kills both           halt(1, IN) -> kills IN only
       toggle(1) shared                toggle(1, IN) independent
       maxp(1) shared                  maxp(1, IN) independent

   One of these is a device. The other is a device that
   works until somebody halts an endpoint.

// =====================================================================
//  usb_ep_table -- "Explain endpoints" answered in hardware.
//
//  The answer everybody gives is "a logical channel, numbered 0 to 15,
//  with a direction and a maximum packet size". All true, and it hides
//  the fact the question is actually about:
//
//      Endpoint 1 IN and endpoint 1 OUT are TWO DIFFERENT ENDPOINTS.
//
//  Separate buffers, separate data toggles, separate halt states,
//  separate max packet sizes. The number is not an identifier; the pair
//  (number, direction) is. A device with "four endpoints" may have four
//  or eight of them depending on what the descriptors say, and a table
//  indexed by number alone is a device where halting the IN direction
//  silently halts the OUT direction with it.
//
//  Endpoint 0 is the exception that proves the rule: it is the one
//  endpoint that is genuinely bidirectional, because control transfers
//  need both directions of the SAME conversation.
// =====================================================================
module usb_ep_table #(
  parameter N_NUM = 4            // endpoint numbers 0..N_NUM-1
) (
  input  wire        clk,
  input  wire        rst_n,

  // ---- a token, as it arrives off the bus ----
  input  wire        tok_valid,
  input  wire [3:0]  tok_ep,      // endpoint NUMBER
  input  wire        tok_in,      // direction: 1 = IN (device to host)

  // ---- configuration, from the descriptors ----
  input  wire        cfg_wr,
  input  wire [3:0]  cfg_ep,
  input  wire        cfg_in,
  input  wire        cfg_enable,
  input  wire [10:0] cfg_maxp,

  // ---- halt control, per (number, direction) ----
  input  wire        halt_wr,
  input  wire [3:0]  halt_ep,
  input  wire        halt_in,
  input  wire        halt_set,

  // ---- a transaction completing, which advances the toggle ----
  input  wire        xact_ack,

  // ---- lookup results for the token above ----
  output wire        ep_valid,    // this (number, direction) exists
  output wire        ep_halted,
  output wire [10:0] ep_maxp,
  output wire        ep_toggle,

  // ---- observability ----
  output wire [31:0] n_lookup,
  output wire [31:0] n_unknown_ep,
  output wire [31:0] n_halted_hit,
  output wire [31:0] n_toggle_flip,
  // Evidence that the two directions were driven INDEPENDENTLY: a halt
  // applied to one direction while the other stayed unhalted. This is a
  // coverage counter, not a self-check -- the design cannot detect its own
  // cross-direction leak, because a leak is indistinguishable from a
  // deliberate write from inside the module. The TESTBENCH does that, with
  // an independent shadow of both directions.
  output wire [31:0] n_split_halt
);

  // ---- the table is indexed by (number, direction), never by number ----
  //
  // Two separate arrays rather than one array of structs, so that an index
  // that forgets the direction cannot compile into something plausible.
  // IN and OUT are not two views of one endpoint; they are two endpoints.
  reg              en_in  [0:N_NUM-1];
  reg              en_out [0:N_NUM-1];
  reg              hl_in  [0:N_NUM-1];
  reg              hl_out [0:N_NUM-1];
  reg  [10:0]      mp_in  [0:N_NUM-1];
  reg  [10:0]      mp_out [0:N_NUM-1];
  reg              tg_in  [0:N_NUM-1];
  reg              tg_out [0:N_NUM-1];

  reg [31:0] look_c, unk_c, halt_c, flip_c, split_c;

  // ---- endpoint 0 is bidirectional, and it is the ONLY one ----
  //
  // A control transfer is one conversation that runs both ways, so EP0's
  // two directions share a halt state and a packet size by definition.
  // Every other endpoint number describes two independent pipes that
  // merely happen to be written with the same digit.
  wire in_range = tok_valid && (tok_ep < N_NUM);
  wire is_ep0   = (tok_ep == 4'd0);

  wire sel_in   = tok_in;

  // The lookup. Note that every read is indexed by BOTH tok_ep and the
  // direction -- there is no path in this module that reads a table entry
  // without having decided which direction it wants.
  wire       e_valid  = in_range && (sel_in ? en_in[tok_ep]  : en_out[tok_ep]);
  wire       e_halted = in_range && (sel_in ? hl_in[tok_ep]  : hl_out[tok_ep]);
  wire [10:0] e_maxp  = in_range ? (sel_in ? mp_in[tok_ep]   : mp_out[tok_ep])
                                 : 11'd0;
  wire       e_toggle = in_range && (sel_in ? tg_in[tok_ep]  : tg_out[tok_ep]);

  assign ep_valid  = e_valid;
  assign ep_halted = e_halted;
  assign ep_maxp   = e_valid ? e_maxp : 11'd0;
  assign ep_toggle = e_toggle;

  assign n_lookup      = look_c;
  assign n_unknown_ep  = unk_c;
  assign n_halted_hit  = halt_c;
  assign n_toggle_flip = flip_c;
  assign n_split_halt  = split_c;

  integer i;

  always @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      for (i = 0; i < N_NUM; i = i + 1) begin
        // Endpoint 0 exists in both directions from the moment the device
        // powers up -- it is how the host talks to a device it knows
        // nothing about. Every other endpoint exists only once a
        // descriptor has said so.
        en_in[i]  <= (i == 0);
        en_out[i] <= (i == 0);
        hl_in[i]  <= 1'b0;
        hl_out[i] <= 1'b0;
        mp_in[i]  <= (i == 0) ? 11'd64 : 11'd0;
        mp_out[i] <= (i == 0) ? 11'd64 : 11'd0;
        tg_in[i]  <= 1'b0;
        tg_out[i] <= 1'b0;
      end
      look_c  <= 32'd0;
      unk_c   <= 32'd0;
      halt_c  <= 32'd0;
      flip_c  <= 32'd0;
      split_c <= 32'd0;
    end else begin
      // ---- configuration writes one direction of one number ----
      if (cfg_wr && (cfg_ep < N_NUM)) begin
        if (cfg_ep == 4'd0) begin
          // EP0 is bidirectional: configuring it configures both halves,
          // because they are one conversation rather than two pipes.
          en_in[cfg_ep]  <= cfg_enable;
          en_out[cfg_ep] <= cfg_enable;
          mp_in[cfg_ep]  <= cfg_maxp;
          mp_out[cfg_ep] <= cfg_maxp;
        end else if (cfg_in) begin
          en_in[cfg_ep]  <= cfg_enable;
          mp_in[cfg_ep]  <= cfg_maxp;
        end else begin
          en_out[cfg_ep] <= cfg_enable;
          mp_out[cfg_ep] <= cfg_maxp;
        end
      end

      // ---- halt applies to ONE direction ----
      //
      // Except on EP0, where a halt would make the device unrecoverable:
      // clearing a halt is itself a control transfer, so EP0 is not
      // haltable at all.
      if (halt_wr && (halt_ep < N_NUM) && (halt_ep != 4'd0)) begin
        if (halt_in) hl_in[halt_ep]  <= halt_set;
        else         hl_out[halt_ep] <= halt_set;
      end

      // ---- a completed transaction flips ONE toggle ----
      if (tok_valid && in_range && e_valid && !e_halted && xact_ack) begin
        if (sel_in) tg_in[tok_ep]  <= ~tg_in[tok_ep];
        else        tg_out[tok_ep] <= ~tg_out[tok_ep];
        flip_c <= flip_c + 32'd1;
      end

      // ---- counters ----
      if (tok_valid) begin
        look_c <= look_c + 32'd1;
        if (!in_range || !e_valid) unk_c  <= unk_c  + 32'd1;
        if (e_halted)              halt_c <= halt_c + 32'd1;
      end

      // ---- coverage: the directions were driven SEPARATELY ----
      //
      // A halt set on one direction of a number whose other direction is
      // not halted. If this reads zero, every halt in the run moved both
      // directions together and the independence claim was never tested --
      // which is the whole point of the chapter, so the number is published.
      if (halt_wr && (halt_ep < N_NUM) && (halt_ep != 4'd0) && halt_set) begin
        if (halt_in && !hl_out[halt_ep]) split_c <= split_c + 32'd1;
        if (!halt_in && !hl_in[halt_ep]) split_c <= split_c + 32'd1;
      end
    end
  end

endmodule

// =====================================================================
//  usb_ep_table -- SystemVerilog.
//
//  The eight parallel arrays of the Verilog become ONE array of a struct
//  indexed by direction, which is the right shape: an endpoint's state
//  belongs together, and the direction is part of its address rather
//  than a reason to duplicate every field.
//
//  It also makes the central claim structural. `ep[num][dir]` cannot be
//  written without naming a direction, so the cross-direction leak this
//  chapter is about becomes a thing you have to go out of your way to
//  write rather than a thing you can do by forgetting an index.
//
//  The answer everybody gives is "a logical channel, numbered 0 to 15,
//  with a direction and a maximum packet size". All true, and it hides
//  the fact the question is actually about:
//
//      Endpoint 1 IN and endpoint 1 OUT are TWO DIFFERENT ENDPOINTS.
//
//  Separate buffers, separate data toggles, separate halt states,
//  separate max packet sizes. The number is not an identifier; the pair
//  (number, direction) is. A device with "four endpoints" may have four
//  or eight of them depending on what the descriptors say, and a table
//  indexed by number alone is a device where halting the IN direction
//  silently halts the OUT direction with it.
//
//  Endpoint 0 is the exception that proves the rule: it is the one
//  endpoint that is genuinely bidirectional, because control transfers
//  need both directions of the SAME conversation.
// =====================================================================
module usb_ep_table #(
  parameter int N_NUM = 4            // endpoint numbers 0..N_NUM-1
) (
  input  logic       clk,
  input  logic       rst_n,

  // ---- a token, as it arrives off the bus ----
  input  logic       tok_valid,
  input  logic [3:0] tok_ep,      // endpoint NUMBER
  input  logic       tok_in,      // direction: 1 = IN (device to host)

  // ---- configuration, from the descriptors ----
  input  logic       cfg_wr,
  input  logic [3:0] cfg_ep,
  input  logic       cfg_in,
  input  logic       cfg_enable,
  input  logic [10:0]cfg_maxp,

  // ---- halt control, per (number, direction) ----
  input  logic       halt_wr,
  input  logic [3:0] halt_ep,
  input  logic       halt_in,
  input  logic       halt_set,

  // ---- a transaction completing, which advances the toggle ----
  input  logic       xact_ack,

  // ---- lookup results for the token above ----
  output logic       ep_valid,    // this (number, direction) exists
  output logic       ep_halted,
  output logic [10:0]ep_maxp,
  output logic       ep_toggle,

  // ---- observability ----
  output logic [31:0]n_lookup,
  output logic [31:0]n_unknown_ep,
  output logic [31:0]n_halted_hit,
  output logic [31:0]n_toggle_flip,
  // Evidence that the two directions were driven INDEPENDENTLY: a halt
  // applied to one direction while the other stayed unhalted. This is a
  // coverage counter, not a self-check -- the design cannot detect its own
  // cross-direction leak, because a leak is indistinguishable from a
  // deliberate write from inside the module. The TESTBENCH does that, with
  // an independent shadow of both directions.
  output logic [31:0]n_split_halt
);

  // ---- the table is indexed by (number, direction), never by number ----
  //
  // Two separate arrays rather than one array of structs, so that an index
  // that forgets the direction cannot compile into something plausible.
  // IN and OUT are not two views of one endpoint; they are two endpoints.
  // Every field is indexed [number][direction]. Writing one of these
  // without naming a direction is a compile error, which is exactly the
  // property this chapter is about: the cross-direction leak becomes
  // something you have to go out of your way to write.
  //
  // DIR_OUT is 0 and DIR_IN is 1, matching the token's direction bit, so
  // the token's own field is the index with no translation.
  //
  // A packed struct would read better still, and Icarus Verilog 13 aborts
  // its elaborator on a variable field-select into a 2-D unpacked array of
  // one -- so the fields are separate arrays that share an index shape.
  localparam int DIR_OUT = 0, DIR_IN = 1;
  logic        st_en [N_NUM][2];
  logic        st_hl [N_NUM][2];
  logic [10:0] st_mp [N_NUM][2];
  logic        st_tg [N_NUM][2];

  logic [31:0] look_c, unk_c, halt_c, flip_c, split_c;

  // ---- endpoint 0 is bidirectional, and it is the ONLY one ----
  //
  // A control transfer is one conversation that runs both ways, so EP0's
  // two directions share a halt state and a packet size by definition.
  // Every other endpoint number describes two independent pipes that
  // merely happen to be written with the same digit.
  wire in_range = tok_valid && (tok_ep < N_NUM);
  wire is_ep0   = (tok_ep == 4'd0);

  wire sel_in   = tok_in;
  wire [0:0] d  = tok_in;   // the direction index

  // The lookup. Note that every read is indexed by BOTH tok_ep and the
  // direction -- there is no path in this module that reads a table entry
  // without having decided which direction it wants.
  wire       e_valid  = in_range && st_en[tok_ep][d];
  wire       e_halted = in_range && st_hl[tok_ep][d];
  wire [10:0] e_maxp  = in_range ? st_mp[tok_ep][d] : 11'd0;
  wire       e_toggle = in_range && st_tg[tok_ep][d];

  assign ep_valid  = e_valid;
  assign ep_halted = e_halted;
  assign ep_maxp   = e_valid ? e_maxp : 11'd0;
  assign ep_toggle = e_toggle;

  assign n_lookup      = look_c;
  assign n_unknown_ep  = unk_c;
  assign n_halted_hit  = halt_c;
  assign n_toggle_flip = flip_c;
  assign n_split_halt  = split_c;


  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      for (int i = 0; i < N_NUM; i++) begin
        // Endpoint 0 exists in both directions from the moment the device
        // powers up -- it is how the host talks to a device it knows
        // nothing about. Every other endpoint exists only once a
        // descriptor has said so.
        for (int j = 0; j < 2; j++) begin
          st_en[i][j]     <= (i == 0);
          st_hl[i][j] <= 1'b0;
          st_mp[i][j]   <= (i == 0) ? 11'd64 : 11'd0;
          st_tg[i][j] <= 1'b0;
        end
      end
      look_c  <= 32'd0;
      unk_c   <= 32'd0;
      halt_c  <= 32'd0;
      flip_c  <= 32'd0;
      split_c <= 32'd0;
    end else begin
      // ---- configuration writes one direction of one number ----
      if (cfg_wr && (cfg_ep < N_NUM)) begin
        if (cfg_ep == 4'd0) begin
          // EP0 is bidirectional: configuring it configures both halves,
          // because they are one conversation rather than two pipes.
          for (int j = 0; j < 2; j++) begin
            st_en[cfg_ep][j]   <= cfg_enable;
            st_mp[cfg_ep][j] <= cfg_maxp;
          end
        end else begin
          st_en[cfg_ep][cfg_in]   <= cfg_enable;
          st_mp[cfg_ep][cfg_in] <= cfg_maxp;
        end
      end

      // ---- halt applies to ONE direction ----
      //
      // Except on EP0, where a halt would make the device unrecoverable:
      // clearing a halt is itself a control transfer, so EP0 is not
      // haltable at all.
      if (halt_wr && (halt_ep < N_NUM) && (halt_ep != 4'd0)) begin
        st_hl[halt_ep][halt_in] <= halt_set;
      end

      // ---- a completed transaction flips ONE toggle ----
      if (tok_valid && in_range && e_valid && !e_halted && xact_ack) begin
        st_tg[tok_ep][d] <= ~st_tg[tok_ep][d];
        flip_c <= flip_c + 32'd1;
      end

      // ---- counters ----
      if (tok_valid) begin
        look_c <= look_c + 32'd1;
        if (!in_range || !e_valid) unk_c  <= unk_c  + 32'd1;
        if (e_halted)              halt_c <= halt_c + 32'd1;
      end

      // ---- coverage: the directions were driven SEPARATELY ----
      //
      // A halt set on one direction of a number whose other direction is
      // not halted. If this reads zero, every halt in the run moved both
      // directions together and the independence claim was never tested --
      // which is the whole point of the chapter, so the number is published.
      if (halt_wr && (halt_ep < N_NUM) && (halt_ep != 4'd0) && halt_set) begin
        if (!st_hl[halt_ep][!halt_in]) split_c <= split_c + 32'd1;
      end
    end
  end

endmodule

-- =====================================================================
--  usb_ep_table -- VHDL-2008.
--
--  VHDL gets the shape the SystemVerilog wanted: a record per endpoint
--  state, in a two-dimensional array indexed by (number, direction).
--  There is no way to write an entry without naming a direction, which
--  is the property this chapter is about -- a cross-direction leak has
--  to be written deliberately rather than by forgetting an index.
--
--  The Verilog carries eight parallel one-dimensional arrays instead,
--  because Verilog-2005 has neither records nor multi-dimensional
--  arrays of them. Eight arrays that must be kept in step is exactly
--  the situation in which a direction gets forgotten.
-- =====================================================================
library ieee;
use ieee.std_logic_1164.all;
use ieee.numeric_std.all;

package ep_pkg is
  -- DIR_OUT is 0 and DIR_IN is 1, matching the token's direction bit, so
  -- the token's own field indexes the table with no translation.
  constant DIR_OUT : natural := 0;
  constant DIR_IN  : natural := 1;

  type ep_state_t is record
    en     : std_logic;
    halted : std_logic;
    maxp   : unsigned(10 downto 0);
    toggle : std_logic;
  end record;

  type ep_table_t is array (natural range <>, natural range <>) of ep_state_t;
end package;

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

entity usb_ep_table is
  generic (
    N_NUM : natural := 4
  );
  port (
    clk        : in  std_logic;
    rst_n      : in  std_logic;

    tok_valid  : in  std_logic;
    tok_ep     : in  std_logic_vector(3 downto 0);
    tok_in     : in  std_logic;

    cfg_wr     : in  std_logic;
    cfg_ep     : in  std_logic_vector(3 downto 0);
    cfg_in     : in  std_logic;
    cfg_enable : in  std_logic;
    cfg_maxp   : in  std_logic_vector(10 downto 0);

    halt_wr    : in  std_logic;
    halt_ep    : in  std_logic_vector(3 downto 0);
    halt_in    : in  std_logic;
    halt_set   : in  std_logic;

    xact_ack   : in  std_logic;

    ep_valid   : out std_logic;
    ep_halted  : out std_logic;
    ep_maxp    : out std_logic_vector(10 downto 0);
    ep_toggle  : out std_logic;

    n_lookup      : out std_logic_vector(31 downto 0);
    n_unknown_ep  : out std_logic_vector(31 downto 0);
    n_halted_hit  : out std_logic_vector(31 downto 0);
    n_toggle_flip : out std_logic_vector(31 downto 0);
    n_split_halt  : out std_logic_vector(31 downto 0)
  );
end entity;

architecture rtl of usb_ep_table is
  signal tbl : ep_table_t(0 to N_NUM-1, 0 to 1);

  signal look_c, unk_c, halt_c, flip_c, split_c : unsigned(31 downto 0)
    := (others => '0');

  signal in_range : std_logic;
  signal e_valid, e_halted, e_toggle : std_logic;
  signal e_maxp : unsigned(10 downto 0);

  -- The direction index, derived once from the token's own bit.
  function dir_of(b : std_logic) return natural is
  begin
    if b = '1' then return DIR_IN; else return DIR_OUT; end if;
  end function;
begin

  in_range <= '1' when (tok_valid = '1' and
                        to_integer(unsigned(tok_ep)) < N_NUM) else '0';

  -- Every read names BOTH the number and the direction. There is no path
  -- through this architecture that reads a table entry without one.
  -- The bound check is made INSIDE this process, from tok_ep directly.
  -- Gating on the separate `in_range` signal is a crash rather than a
  -- mis-read: a signal lags its inputs within a delta cycle, so tok_ep can
  -- already be 13 while in_range is still '1' from the previous value, and
  -- VHDL's range checking then aborts the run rather than returning
  -- rubbish the way Verilog would.
  lookup : process(all)
    variable n, d : natural;
  begin
    n := to_integer(unsigned(tok_ep));
    if tok_valid = '1' and n < N_NUM then
      d := dir_of(tok_in);
      e_valid  <= tbl(n, d).en;
      e_halted <= tbl(n, d).halted;
      e_maxp   <= tbl(n, d).maxp;
      e_toggle <= tbl(n, d).toggle;
    else
      e_valid  <= '0';
      e_halted <= '0';
      e_maxp   <= (others => '0');
      e_toggle <= '0';
    end if;
  end process;

  ep_valid  <= e_valid;
  ep_halted <= e_halted;
  ep_toggle <= e_toggle;
  ep_maxp   <= std_logic_vector(e_maxp) when e_valid = '1'
               else (others => '0');

  n_lookup      <= std_logic_vector(look_c);
  n_unknown_ep  <= std_logic_vector(unk_c);
  n_halted_hit  <= std_logic_vector(halt_c);
  n_toggle_flip <= std_logic_vector(flip_c);
  n_split_halt  <= std_logic_vector(split_c);

  main : process(clk, rst_n)
    variable cn, hn, tn, cd, hd, td : natural;
  begin
    if rst_n = '0' then
      for i in 0 to N_NUM-1 loop
        for j in 0 to 1 loop
          -- Endpoint 0 exists in both directions from power-up: it is how
          -- the host talks to a device it knows nothing about. Every other
          -- endpoint exists only once a descriptor has said so.
          if i = 0 then
            tbl(i, j).en   <= '1';
            tbl(i, j).maxp <= to_unsigned(64, 11);
          else
            tbl(i, j).en   <= '0';
            tbl(i, j).maxp <= (others => '0');
          end if;
          tbl(i, j).halted <= '0';
          tbl(i, j).toggle <= '0';
        end loop;
      end loop;
      look_c  <= (others => '0');
      unk_c   <= (others => '0');
      halt_c  <= (others => '0');
      flip_c  <= (others => '0');
      split_c <= (others => '0');

    elsif rising_edge(clk) then
      -- ---- configuration writes one direction of one number ----
      if cfg_wr = '1' and to_integer(unsigned(cfg_ep)) < N_NUM then
        cn := to_integer(unsigned(cfg_ep));
        cd := dir_of(cfg_in);
        if cn = 0 then
          -- EP0 is bidirectional: configuring it configures both halves,
          -- because they are one conversation rather than two pipes.
          for j in 0 to 1 loop
            tbl(cn, j).en   <= cfg_enable;
            tbl(cn, j).maxp <= unsigned(cfg_maxp);
          end loop;
        else
          tbl(cn, cd).en   <= cfg_enable;
          tbl(cn, cd).maxp <= unsigned(cfg_maxp);
        end if;
      end if;

      -- ---- halt applies to ONE direction ----
      --
      -- Except on EP0, where a halt would make the device unrecoverable:
      -- clearing a halt is itself a control transfer.
      if halt_wr = '1' and to_integer(unsigned(halt_ep)) < N_NUM
         and to_integer(unsigned(halt_ep)) /= 0 then
        hn := to_integer(unsigned(halt_ep));
        hd := dir_of(halt_in);
        tbl(hn, hd).halted <= halt_set;
      end if;

      -- ---- coverage: the directions were driven SEPARATELY ----
      --
      -- A halt SET on one direction whose other direction is not halted.
      -- Zero here means every halt in the run moved both directions
      -- together and the independence claim was never tested.
      --
      -- Deliberately its OWN block with its own endpoint-0 exclusion, so
      -- that it matches the Verilog statement for statement: folding it
      -- inside the halt-write block above gave mutation D4 an extra effect
      -- in VHDL that it does not have in Verilog, and the two directed
      -- columns then read 296 against 319.
      if halt_wr = '1' and to_integer(unsigned(halt_ep)) < N_NUM
         and to_integer(unsigned(halt_ep)) /= 0 and halt_set = '1' then
        hn := to_integer(unsigned(halt_ep));
        hd := dir_of(halt_in);
        if tbl(hn, 1 - hd).halted = '0' then
          split_c <= split_c + 1;
        end if;
      end if;

      -- ---- a completed transaction flips ONE toggle ----
      if tok_valid = '1' and in_range = '1' and e_valid = '1'
         and e_halted = '0' and xact_ack = '1' then
        tn := to_integer(unsigned(tok_ep));
        td := dir_of(tok_in);
        tbl(tn, td).toggle <= not tbl(tn, td).toggle;
        flip_c <= flip_c + 1;
      end if;

      -- ---- counters ----
      if tok_valid = '1' then
        look_c <= look_c + 1;
        if in_range = '0' or e_valid = '0' then unk_c  <= unk_c  + 1; end if;
        if e_halted = '1' then                  halt_c <= halt_c + 1; end if;
      end if;
    end if;
  end process;

end architecture;

   Checking only the targeted direction:

     halt(1, IN);  check halted(1, IN) == 1   -- PASSES

   A design that halts both directions passes that check
   perfectly. The write landed correctly. It also landed
   somewhere nobody looked.

   Checking every direction of every number:

     halt(1, IN);
     for n in 0..3: for d in {IN, OUT}:
        compare against an INDEPENDENT shadow   -- FAILS

// =====================================================================
//  Testbench for usb_ep_table.
//
//  The headline property is a NEGATIVE one about independence: touching
//  one direction of an endpoint number must never move the other. So the
//  shadow keeps the two directions in completely separate arrays and, after
//  every single operation, compares BOTH directions of EVERY number --
//  not only the one that was targeted.
//
//  Checking only the targeted direction is how a cross-direction leak
//  survives a testbench: the write landed correctly, and it also landed
//  somewhere nobody looked.
// =====================================================================
`timescale 1ns/1ps
module tb_ep_v;

  localparam N_NUM = 4;

  reg         clk = 1'b0, rst_n = 1'b0;
  reg         tok_valid = 1'b0;
  reg  [3:0]  tok_ep = 4'd0;
  reg         tok_in = 1'b0;
  reg         cfg_wr = 1'b0;
  reg  [3:0]  cfg_ep = 4'd0;
  reg         cfg_in = 1'b0;
  reg         cfg_enable = 1'b0;
  reg  [10:0] cfg_maxp = 11'd0;
  reg         halt_wr = 1'b0;
  reg  [3:0]  halt_ep = 4'd0;
  reg         halt_in = 1'b0;
  reg         halt_set = 1'b0;
  reg         xact_ack = 1'b0;

  wire        ep_valid, ep_halted, ep_toggle;
  wire [10:0] ep_maxp;
  wire [31:0] n_lookup, n_unknown_ep, n_halted_hit, n_toggle_flip, n_split_halt;

  usb_ep_table #(.N_NUM(N_NUM)) dut (
    .clk(clk), .rst_n(rst_n),
    .tok_valid(tok_valid), .tok_ep(tok_ep), .tok_in(tok_in),
    .cfg_wr(cfg_wr), .cfg_ep(cfg_ep), .cfg_in(cfg_in),
    .cfg_enable(cfg_enable), .cfg_maxp(cfg_maxp),
    .halt_wr(halt_wr), .halt_ep(halt_ep), .halt_in(halt_in),
    .halt_set(halt_set),
    .xact_ack(xact_ack),
    .ep_valid(ep_valid), .ep_halted(ep_halted),
    .ep_maxp(ep_maxp), .ep_toggle(ep_toggle),
    .n_lookup(n_lookup), .n_unknown_ep(n_unknown_ep),
    .n_halted_hit(n_halted_hit), .n_toggle_flip(n_toggle_flip),
    .n_split_halt(n_split_halt)
  );

  always #5 clk = ~clk;

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

  // ---- $random is SIGNED: mask the sign bit before any modulo ----
  function [31:0] urand;
    input dummy;
    begin urand = $random(seed) & 32'h3FFF_FFFF; end
  endfunction

  // ---- the shadow: two directions, two sets of arrays, never merged ----
  reg         s_en_in  [0:N_NUM-1];
  reg         s_en_out [0:N_NUM-1];
  reg         s_hl_in  [0:N_NUM-1];
  reg         s_hl_out [0:N_NUM-1];
  reg [10:0]  s_mp_in  [0:N_NUM-1];
  reg [10:0]  s_mp_out [0:N_NUM-1];
  reg         s_tg_in  [0:N_NUM-1];
  reg         s_tg_out [0:N_NUM-1];
  reg [31:0]  x_look, x_unk, x_halt, x_flip, x_split;
  // Run-wide totals. The DUT's counters are cleared by every reset, so a
  // summary printed from them describes the last window rather than the run.
  integer g_look = 0, g_unk = 0, g_halt = 0, g_flip = 0, g_split = 0;

  // ---- the headline counter ----
  //
  // Every cycle in which any direction of any number disagreed with the
  // shadow. A cross-direction leak shows up here and nowhere else, because
  // the direction that was written is always correct.
  integer n_cross = 0;

  // ---- exhaustive reach over (number, dir, enabled, halted, toggle) ----
  reg reach [0:63];
  integer ri, n_reach;

  task ck(input cond, input [255:0] what);
    begin
      checks = checks + 1;
      if (!cond) begin
        errors = errors + 1;
        if (errors <= 20)
          $display("  ERROR @%0t step=%0d: %0s", $time, steps, what);
      end
    end
  endtask

  // ---------------------------------------------------------------
  //  Compare EVERY direction of EVERY number against the shadow.
  //
  //  Called after every operation. This is the expensive way to do it
  //  and it is the only way that can see a leak.
  // ---------------------------------------------------------------
  task audit_all;
    integer a;
    begin
      for (a = 0; a < N_NUM; a = a + 1) begin
        // drive a lookup at (a, IN) and check it, then (a, OUT)
        tok_valid = 1'b1; tok_ep = a[3:0]; tok_in = 1'b1;
        #1;
        if (ep_valid  !== s_en_in[a]) n_cross = n_cross + 1;
        if (ep_halted !== s_hl_in[a]) n_cross = n_cross + 1;
        if (ep_toggle !== s_tg_in[a]) n_cross = n_cross + 1;
        ck(ep_valid  === s_en_in[a], "IN  enable  disagrees");
        ck(ep_halted === s_hl_in[a], "IN  halt    disagrees");
        ck(ep_toggle === s_tg_in[a], "IN  toggle  disagrees");
        ck(ep_maxp   === (s_en_in[a] ? s_mp_in[a] : 11'd0),
           "IN  maxp    disagrees");

        tok_in = 1'b0;
        #1;
        if (ep_valid  !== s_en_out[a]) n_cross = n_cross + 1;
        if (ep_halted !== s_hl_out[a]) n_cross = n_cross + 1;
        if (ep_toggle !== s_tg_out[a]) n_cross = n_cross + 1;
        ck(ep_valid  === s_en_out[a], "OUT enable  disagrees");
        ck(ep_halted === s_hl_out[a], "OUT halt    disagrees");
        ck(ep_toggle === s_tg_out[a], "OUT toggle  disagrees");
        ck(ep_maxp   === (s_en_out[a] ? s_mp_out[a] : 11'd0),
           "OUT maxp    disagrees");
      end
      tok_valid = 1'b0;
      ck(n_cross == 0, "a direction changed that nothing touched");
    end
  endtask

  // ---------------------------------------------------------------
  //  A combinational lookup with NO clocked side effect.
  //
  //  Positioned at a negedge deliberately. Driving tok_valid and then
  //  waiting #1 lands exactly on the next posedge once the preceding audit
  //  has consumed its 8 ns -- the DUT then counts a lookup the shadow knows
  //  nothing about. Two errors, entirely a testbench timing accident.
  // ---------------------------------------------------------------
  task peek(input [3:0] e, input d);
    begin
      @(negedge clk);
      tok_valid = 1'b1; tok_ep = e; tok_in = d;
      #1;
    end
  endtask

  // ---------------------------------------------------------------
  //  One clocked operation, then a full audit.
  // ---------------------------------------------------------------
  task op(input cw, input [3:0] ce, input ci, input cen, input [10:0] cm,
          input hw, input [3:0] he, input hi, input hs,
          input tv, input [3:0] te, input ti, input xa);
    begin
      cfg_wr = cw;  cfg_ep = ce;  cfg_in = ci;
      cfg_enable = cen;  cfg_maxp = cm;
      halt_wr = hw; halt_ep = he; halt_in = hi; halt_set = hs;
      tok_valid = tv; tok_ep = te; tok_in = ti; xact_ack = xa;

      // ---- advance the shadow ----
      //
      // The LOOKUP is evaluated first, because the design's lookup is a
      // combinational read of REGISTERED table entries -- it sees the
      // values as they stood before this edge. A shadow that applies the
      // configuration write first sees the new values and disagrees on
      // every cycle that configures and looks up at once.
      if (tv && (te < N_NUM)) begin
        x_look = x_look + 1;  g_look = g_look + 1;
        if (ti) begin
          if (!s_en_in[te])  begin x_unk = x_unk + 1; g_unk = g_unk + 1; end
          if (s_hl_in[te])   begin x_halt = x_halt + 1; g_halt = g_halt + 1; end
          if (s_en_in[te] && !s_hl_in[te] && xa) begin
            s_tg_in[te] = ~s_tg_in[te];
            x_flip = x_flip + 1;  g_flip = g_flip + 1;
          end
        end else begin
          if (!s_en_out[te]) begin x_unk = x_unk + 1; g_unk = g_unk + 1; end
          if (s_hl_out[te])  begin x_halt = x_halt + 1; g_halt = g_halt + 1; end
          if (s_en_out[te] && !s_hl_out[te] && xa) begin
            s_tg_out[te] = ~s_tg_out[te];
            x_flip = x_flip + 1;  g_flip = g_flip + 1;
          end
        end
      end else if (tv) begin
        x_look = x_look + 1;  g_look = g_look + 1;
        x_unk  = x_unk + 1;  g_unk = g_unk + 1;
      end

      if (cw && (ce < N_NUM)) begin
        if (ce == 4'd0) begin
          // EP0 is bidirectional: one conversation, both halves
          s_en_in[ce]  = cen;  s_en_out[ce] = cen;
          s_mp_in[ce]  = cm;   s_mp_out[ce] = cm;
        end else if (ci) begin
          s_en_in[ce]  = cen;  s_mp_in[ce]  = cm;
        end else begin
          s_en_out[ce] = cen;  s_mp_out[ce] = cm;
        end
      end

      if (hw && (he < N_NUM) && (he != 4'd0)) begin
        // The design counts a SPLIT HALT only when a halt is being SET,
        // not when it is cleared. Omitting `hs` here made the shadow count
        // clears as well -- 3202 errors, none of them the design.
        if (hs) begin
          if (hi && !s_hl_out[he]) begin x_split = x_split + 1; g_split = g_split + 1; end
          if (!hi && !s_hl_in[he]) begin x_split = x_split + 1; g_split = g_split + 1; end
        end
        if (hi) s_hl_in[he]  = hs;
        else    s_hl_out[he] = hs;
      end

      @(posedge clk);
      #1;
      steps = steps + 1;

      cfg_wr = 1'b0; halt_wr = 1'b0; tok_valid = 1'b0; xact_ack = 1'b0;

      ck(n_lookup      === x_look,  "lookup count disagrees");
      ck(n_unknown_ep  === x_unk,   "unknown-endpoint count disagrees");
      ck(n_halted_hit  === x_halt,  "halted-hit count disagrees");
      ck(n_toggle_flip === x_flip,  "toggle-flip count disagrees");
      ck(n_split_halt  === x_split, "split-halt count disagrees");

      audit_all;
    end
  endtask

  task reset_dut;
    integer a;
    begin
      rst_n = 1'b0;
      cfg_wr = 0; halt_wr = 0; tok_valid = 0; xact_ack = 0;
      @(posedge clk); @(posedge clk);
      rst_n = 1'b1;
      for (a = 0; a < N_NUM; a = a + 1) begin
        s_en_in[a]  = (a == 0);  s_en_out[a] = (a == 0);
        s_hl_in[a]  = 1'b0;      s_hl_out[a] = 1'b0;
        s_mp_in[a]  = (a == 0) ? 11'd64 : 11'd0;
        s_mp_out[a] = (a == 0) ? 11'd64 : 11'd0;
        s_tg_in[a]  = 1'b0;      s_tg_out[a] = 1'b0;
      end
      x_look = 0; x_unk = 0; x_halt = 0; x_flip = 0; x_split = 0;
      @(posedge clk); #1;
    end
  endtask

  integer ei, di, en, hl, tg, k, a2;

  initial begin
    for (ri = 0; ri < 64; ri = ri + 1) reach[ri] = 1'b0;
    seed = 32'd27004;

    // =============================================================
    //  PHASE 1 (DIRECTED, EXHAUSTIVE) -- every (number, direction) in
    //  every (enabled, halted, toggle) state. 4 x 2 x 2 x 2 x 2 = 64.
    // =============================================================
    for (ei = 0; ei < N_NUM; ei = ei + 1)
    for (di = 0; di < 2; di = di + 1)
    for (en = 0; en < 2; en = en + 1)
    for (hl = 0; hl < 2; hl = hl + 1)
    for (tg = 0; tg < 2; tg = tg + 1) begin
      reset_dut;
      // configure this direction
      op(1'b1, ei[3:0], di[0], en[0], 11'd512,
         1'b0, 4'd0, 1'b0, 1'b0,  1'b0, 4'd0, 1'b0, 1'b0);
      // halt it if wanted
      if (hl) op(1'b0, 4'd0, 1'b0, 1'b0, 11'd0,
                 1'b1, ei[3:0], di[0], 1'b1,  1'b0, 4'd0, 1'b0, 1'b0);
      // flip the toggle if wanted
      if (tg) op(1'b0, 4'd0, 1'b0, 1'b0, 11'd0,
                 1'b0, 4'd0, 1'b0, 1'b0,  1'b1, ei[3:0], di[0], 1'b1);
      // and look it up
      op(1'b0, 4'd0, 1'b0, 1'b0, 11'd0,
         1'b0, 4'd0, 1'b0, 1'b0,  1'b1, ei[3:0], di[0], 1'b0);

      ri = (ei << 4) | (di << 3) | (en << 2) | (hl << 1) | tg;
      reach[ri] = 1'b1;
    end

    // =============================================================
    //  PHASE 2 (DIRECTED, EXHAUSTIVE) -- THE CHAPTER'S POINT.
    //
    //  For every endpoint number except 0, enable BOTH directions, then
    //  halt exactly ONE of them, and prove the other is untouched --
    //  enable, halt, max packet size and toggle all independently.
    //
    //  Both orders, both directions: 3 numbers x 2 directions x 2 orders.
    // =============================================================
    for (ei = 1; ei < N_NUM; ei = ei + 1)
    for (di = 0; di < 2; di = di + 1)
    for (k = 0; k < 2; k = k + 1) begin
      reset_dut;
      // both directions exist, with DIFFERENT packet sizes so a shared
      // field cannot pass by accident
      op(1'b1, ei[3:0], 1'b1, 1'b1, 11'd64,
         1'b0, 4'd0, 1'b0, 1'b0,  1'b0, 4'd0, 1'b0, 1'b0);
      op(1'b1, ei[3:0], 1'b0, 1'b1, 11'd512,
         1'b0, 4'd0, 1'b0, 1'b0,  1'b0, 4'd0, 1'b0, 1'b0);

      if (k == 0) begin
        // advance one toggle, then halt one direction
        op(1'b0, 4'd0, 1'b0, 1'b0, 11'd0,
           1'b0, 4'd0, 1'b0, 1'b0,  1'b1, ei[3:0], di[0], 1'b1);
        op(1'b0, 4'd0, 1'b0, 1'b0, 11'd0,
           1'b1, ei[3:0], di[0], 1'b1,  1'b0, 4'd0, 1'b0, 1'b0);
      end else begin
        // halt one direction, then try to use the OTHER
        op(1'b0, 4'd0, 1'b0, 1'b0, 11'd0,
           1'b1, ei[3:0], di[0], 1'b1,  1'b0, 4'd0, 1'b0, 1'b0);
        op(1'b0, 4'd0, 1'b0, 1'b0, 11'd0,
           1'b0, 4'd0, 1'b0, 1'b0,  1'b1, ei[3:0], ~di[0], 1'b1);
      end

      // the untouched direction must still work
      peek(ei[3:0], ~di[0]);
      ck(ep_valid === 1'b1, "the other direction stopped existing");
      ck(ep_halted === 1'b0, "halting one direction halted the other");
      tok_valid = 1'b0;

      // and clearing the halt leaves the other alone too
      op(1'b0, 4'd0, 1'b0, 1'b0, 11'd0,
         1'b1, ei[3:0], di[0], 1'b0,  1'b0, 4'd0, 1'b0, 1'b0);
    end

    // =============================================================
    //  PHASE 3 (DIRECTED) -- endpoint 0 is the exception.
    //
    //  It is bidirectional, it exists from reset, and it is not
    //  haltable: clearing a halt is itself a control transfer, so a
    //  device that could halt EP0 would be unrecoverable.
    // =============================================================
    reset_dut;
    for (di = 0; di < 2; di = di + 1) begin
      // it exists in both directions before anything configures it
      peek(4'd0, di[0]);
      ck(ep_valid === 1'b1, "EP0 did not exist at reset");
      ck(ep_maxp  === 11'd64, "EP0 had no default packet size");
      tok_valid = 1'b0;
      // and a halt attempt does nothing
      op(1'b0, 4'd0, 1'b0, 1'b0, 11'd0,
         1'b1, 4'd0, di[0], 1'b1,  1'b0, 4'd0, 1'b0, 1'b0);
      peek(4'd0, di[0]);
      ck(ep_halted === 1'b0, "EP0 was halted, which is unrecoverable");
      tok_valid = 1'b0;
    end
    // configuring EP0 configures both halves
    op(1'b1, 4'd0, 1'b1, 1'b1, 11'd8,
       1'b0, 4'd0, 1'b0, 1'b0,  1'b0, 4'd0, 1'b0, 1'b0);
    for (di = 0; di < 2; di = di + 1) begin
      peek(4'd0, di[0]);
      ck(ep_maxp === 11'd8, "configuring EP0 did not apply to both directions");
      tok_valid = 1'b0;
    end

    // =============================================================
    //  PHASE 4 (DIRECTED) -- an endpoint number that does not exist.
    // =============================================================
    reset_dut;
    for (k = N_NUM; k < 16; k = k + 1)
    for (di = 0; di < 2; di = di + 1) begin
      peek(k[3:0], di[0]);
      ck(ep_valid === 1'b0, "an out-of-range endpoint reported valid");
      ck(ep_maxp  === 11'd0, "an out-of-range endpoint reported a packet size");
      tok_valid = 1'b0;
      @(posedge clk); #1;
    end

    // =============================================================
    //  PHASE 5 (RANDOM) -- a driver configuring and halting freely.
    // =============================================================
`ifndef DIRECTED_ONLY
    reset_dut;
    for (k = 0; k < 8000; k = k + 1) begin
      op((urand(0) % 4) == 0, urand(0) % 16, (urand(0) % 2) == 0,
         (urand(0) % 4) != 0, (urand(0) % 2) ? 11'd64 : 11'd512,
         (urand(0) % 5) == 0, urand(0) % 16, (urand(0) % 2) == 0,
         (urand(0) % 3) != 0,
         (urand(0) % 2) == 0, urand(0) % 16, (urand(0) % 2) == 0,
         (urand(0) % 3) != 0);
      if ((k % 128) == 127) reset_dut;
    end
`endif

    n_reach = 0;
    for (ri = 0; ri < 64; ri = ri + 1) if (reach[ri]) n_reach = n_reach + 1;

    $display("steps=%0d checks=%0d reach=%0d/64 errors=%0d",
             steps, checks, n_reach, errors);
    $display("[ep] lookups=%0d unknown=%0d halted_hits=%0d toggles=%0d split_halts=%0d",
             g_look, g_unk, g_halt, g_flip, g_split);
    $display("[the whole point] cross-direction leaks = %0d", n_cross);
    if (n_reach != 64) begin
      $display("FAIL: exhaustive sweep incomplete"); errors = errors + 1;
    end
    if (errors == 0) $display("PASS: 0 errors in %0d checks", checks);
    else             $display("FAIL: %0d errors in %0d checks", errors, checks);
    $finish;
  end

endmodule

// =====================================================================
//  Testbench for usb_ep_table.
//
//  The headline property is a NEGATIVE one about independence: touching
//  one direction of an endpoint number must never move the other. So the
//  shadow keeps the two directions in completely separate arrays and, after
//  every single operation, compares BOTH directions of EVERY number --
//  not only the one that was targeted.
//
//  Checking only the targeted direction is how a cross-direction leak
//  survives a testbench: the write landed correctly, and it also landed
//  somewhere nobody looked.
// =====================================================================
`timescale 1ns/1ps
module tb_ep_sv;

  localparam N_NUM = 4;

  logic       clk = 1'b0, rst_n = 1'b0;
  logic       tok_valid = 1'b0;
  logic [3:0] tok_ep = 4'd0;
  logic       tok_in = 1'b0;
  logic       cfg_wr = 1'b0;
  logic [3:0] cfg_ep = 4'd0;
  logic       cfg_in = 1'b0;
  logic       cfg_enable = 1'b0;
  logic [10:0] cfg_maxp = 11'd0;
  logic       halt_wr = 1'b0;
  logic [3:0] halt_ep = 4'd0;
  logic       halt_in = 1'b0;
  logic       halt_set = 1'b0;
  logic       xact_ack = 1'b0;

  logic       ep_valid, ep_halted, ep_toggle;
  logic [10:0] ep_maxp;
  logic [31:0] n_lookup, n_unknown_ep, n_halted_hit, n_toggle_flip, n_split_halt;

  usb_ep_table #(.N_NUM(N_NUM)) dut (
    .clk(clk), .rst_n(rst_n),
    .tok_valid(tok_valid), .tok_ep(tok_ep), .tok_in(tok_in),
    .cfg_wr(cfg_wr), .cfg_ep(cfg_ep), .cfg_in(cfg_in),
    .cfg_enable(cfg_enable), .cfg_maxp(cfg_maxp),
    .halt_wr(halt_wr), .halt_ep(halt_ep), .halt_in(halt_in),
    .halt_set(halt_set),
    .xact_ack(xact_ack),
    .ep_valid(ep_valid), .ep_halted(ep_halted),
    .ep_maxp(ep_maxp), .ep_toggle(ep_toggle),
    .n_lookup(n_lookup), .n_unknown_ep(n_unknown_ep),
    .n_halted_hit(n_halted_hit), .n_toggle_flip(n_toggle_flip),
    .n_split_halt(n_split_halt)
  );

  always #5 clk = ~clk;

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

  // ---- $random is SIGNED: mask the sign bit before any modulo ----
  function automatic logic [31:0] urand(bit dummy);
    return $random(seed) & 32'h3FFF_FFFF;
  endfunction

  // ---- the shadow: two directions, two sets of arrays, never merged ----
  logic       s_en_in  [0:N_NUM-1];
  logic       s_en_out [0:N_NUM-1];
  logic       s_hl_in  [0:N_NUM-1];
  logic       s_hl_out [0:N_NUM-1];
  logic [10:0] s_mp_in  [0:N_NUM-1];
  logic [10:0] s_mp_out [0:N_NUM-1];
  logic       s_tg_in  [0:N_NUM-1];
  logic       s_tg_out [0:N_NUM-1];
  logic [31:0] x_look, x_unk, x_halt, x_flip, x_split;
  // Run-wide totals. The DUT's counters are cleared by every reset, so a
  // summary printed from them describes the last window rather than the run.
  integer g_look = 0, g_unk = 0, g_halt = 0, g_flip = 0, g_split = 0;

  // ---- the headline counter ----
  //
  // Every cycle in which any direction of any number disagreed with the
  // shadow. A cross-direction leak shows up here and nowhere else, because
  // the direction that was written is always correct.
  integer n_cross = 0;

  // ---- exhaustive reach over (number, dir, enabled, halted, toggle) ----
  logic reach [0:63];
  integer ri, n_reach;

  task ck(input logic cond, input logic [255:0] what);
    begin
      checks = checks + 1;
      if (!cond) begin
        errors = errors + 1;
        if (errors <= 20)
          $display("  ERROR @%0t step=%0d: %0s", $time, steps, what);
      end
    end
  endtask

  // ---------------------------------------------------------------
  //  Compare EVERY direction of EVERY number against the shadow.
  //
  //  Called after every operation. This is the expensive way to do it
  //  and it is the only way that can see a leak.
  // ---------------------------------------------------------------
  task audit_all;
    integer a;
    begin
      for (a = 0; a < N_NUM; a = a + 1) begin
        // drive a lookup at (a, IN) and check it, then (a, OUT)
        tok_valid = 1'b1; tok_ep = a[3:0]; tok_in = 1'b1;
        #1;
        if (ep_valid  !== s_en_in[a]) n_cross = n_cross + 1;
        if (ep_halted !== s_hl_in[a]) n_cross = n_cross + 1;
        if (ep_toggle !== s_tg_in[a]) n_cross = n_cross + 1;
        ck(ep_valid  === s_en_in[a], "IN  enable  disagrees");
        ck(ep_halted === s_hl_in[a], "IN  halt    disagrees");
        ck(ep_toggle === s_tg_in[a], "IN  toggle  disagrees");
        ck(ep_maxp   === (s_en_in[a] ? s_mp_in[a] : 11'd0),
           "IN  maxp    disagrees");

        tok_in = 1'b0;
        #1;
        if (ep_valid  !== s_en_out[a]) n_cross = n_cross + 1;
        if (ep_halted !== s_hl_out[a]) n_cross = n_cross + 1;
        if (ep_toggle !== s_tg_out[a]) n_cross = n_cross + 1;
        ck(ep_valid  === s_en_out[a], "OUT enable  disagrees");
        ck(ep_halted === s_hl_out[a], "OUT halt    disagrees");
        ck(ep_toggle === s_tg_out[a], "OUT toggle  disagrees");
        ck(ep_maxp   === (s_en_out[a] ? s_mp_out[a] : 11'd0),
           "OUT maxp    disagrees");
      end
      tok_valid = 1'b0;
      ck(n_cross == 0, "a direction changed that nothing touched");
    end
  endtask

  // ---------------------------------------------------------------
  //  A combinational lookup with NO clocked side effect.
  //
  //  Positioned at a negedge deliberately. Driving tok_valid and then
  //  waiting #1 lands exactly on the next posedge once the preceding audit
  //  has consumed its 8 ns -- the DUT then counts a lookup the shadow knows
  //  nothing about. Two errors, entirely a testbench timing accident.
  // ---------------------------------------------------------------
  task peek(input logic [3:0] e, input logic d);
    begin
      @(negedge clk);
      tok_valid = 1'b1; tok_ep = e; tok_in = d;
      #1;
    end
  endtask

  // ---------------------------------------------------------------
  //  One clocked operation, then a full audit.
  // ---------------------------------------------------------------
  task op(input logic cw, input logic [3:0] ce, input logic ci, input logic cen,
          input logic [10:0] cm,
          input logic hw, input logic [3:0] he, input logic hi, input logic hs,
          input logic tv, input logic [3:0] te, input logic ti, input logic xa);
    begin
      cfg_wr = cw;  cfg_ep = ce;  cfg_in = ci;
      cfg_enable = cen;  cfg_maxp = cm;
      halt_wr = hw; halt_ep = he; halt_in = hi; halt_set = hs;
      tok_valid = tv; tok_ep = te; tok_in = ti; xact_ack = xa;

      // ---- advance the shadow ----
      //
      // The LOOKUP is evaluated first, because the design's lookup is a
      // combinational read of REGISTERED table entries -- it sees the
      // values as they stood before this edge. A shadow that applies the
      // configuration write first sees the new values and disagrees on
      // every cycle that configures and looks up at once.
      if (tv && (te < N_NUM)) begin
        x_look = x_look + 1;  g_look = g_look + 1;
        if (ti) begin
          if (!s_en_in[te])  begin x_unk = x_unk + 1; g_unk = g_unk + 1; end
          if (s_hl_in[te])   begin x_halt = x_halt + 1; g_halt = g_halt + 1; end
          if (s_en_in[te] && !s_hl_in[te] && xa) begin
            s_tg_in[te] = ~s_tg_in[te];
            x_flip = x_flip + 1;  g_flip = g_flip + 1;
          end
        end else begin
          if (!s_en_out[te]) begin x_unk = x_unk + 1; g_unk = g_unk + 1; end
          if (s_hl_out[te])  begin x_halt = x_halt + 1; g_halt = g_halt + 1; end
          if (s_en_out[te] && !s_hl_out[te] && xa) begin
            s_tg_out[te] = ~s_tg_out[te];
            x_flip = x_flip + 1;  g_flip = g_flip + 1;
          end
        end
      end else if (tv) begin
        x_look = x_look + 1;  g_look = g_look + 1;
        x_unk  = x_unk + 1;  g_unk = g_unk + 1;
      end

      if (cw && (ce < N_NUM)) begin
        if (ce == 4'd0) begin
          // EP0 is bidirectional: one conversation, both halves
          s_en_in[ce]  = cen;  s_en_out[ce] = cen;
          s_mp_in[ce]  = cm;   s_mp_out[ce] = cm;
        end else if (ci) begin
          s_en_in[ce]  = cen;  s_mp_in[ce]  = cm;
        end else begin
          s_en_out[ce] = cen;  s_mp_out[ce] = cm;
        end
      end

      if (hw && (he < N_NUM) && (he != 4'd0)) begin
        // The design counts a SPLIT HALT only when a halt is being SET,
        // not when it is cleared. Omitting `hs` here made the shadow count
        // clears as well -- 3202 errors, none of them the design.
        if (hs) begin
          if (hi && !s_hl_out[he]) begin x_split = x_split + 1; g_split = g_split + 1; end
          if (!hi && !s_hl_in[he]) begin x_split = x_split + 1; g_split = g_split + 1; end
        end
        if (hi) s_hl_in[he]  = hs;
        else    s_hl_out[he] = hs;
      end

      @(posedge clk);
      #1;
      steps = steps + 1;

      cfg_wr = 1'b0; halt_wr = 1'b0; tok_valid = 1'b0; xact_ack = 1'b0;

      ck(n_lookup      === x_look,  "lookup count disagrees");
      ck(n_unknown_ep  === x_unk,   "unknown-endpoint count disagrees");
      ck(n_halted_hit  === x_halt,  "halted-hit count disagrees");
      ck(n_toggle_flip === x_flip,  "toggle-flip count disagrees");
      ck(n_split_halt  === x_split, "split-halt count disagrees");

      audit_all;
    end
  endtask

  task reset_dut;
    integer a;
    begin
      rst_n = 1'b0;
      cfg_wr = 0; halt_wr = 0; tok_valid = 0; xact_ack = 0;
      @(posedge clk); @(posedge clk);
      rst_n = 1'b1;
      for (a = 0; a < N_NUM; a = a + 1) begin
        s_en_in[a]  = (a == 0);  s_en_out[a] = (a == 0);
        s_hl_in[a]  = 1'b0;      s_hl_out[a] = 1'b0;
        s_mp_in[a]  = (a == 0) ? 11'd64 : 11'd0;
        s_mp_out[a] = (a == 0) ? 11'd64 : 11'd0;
        s_tg_in[a]  = 1'b0;      s_tg_out[a] = 1'b0;
      end
      x_look = 0; x_unk = 0; x_halt = 0; x_flip = 0; x_split = 0;
      @(posedge clk); #1;
    end
  endtask

  integer ei, di, en, hl, tg, k, a2;

  initial begin
    for (ri = 0; ri < 64; ri = ri + 1) reach[ri] = 1'b0;
    seed = 32'd27004;

    // =============================================================
    //  PHASE 1 (DIRECTED, EXHAUSTIVE) -- every (number, direction) in
    //  every (enabled, halted, toggle) state. 4 x 2 x 2 x 2 x 2 = 64.
    // =============================================================
    for (ei = 0; ei < N_NUM; ei = ei + 1)
    for (di = 0; di < 2; di = di + 1)
    for (en = 0; en < 2; en = en + 1)
    for (hl = 0; hl < 2; hl = hl + 1)
    for (tg = 0; tg < 2; tg = tg + 1) begin
      reset_dut;
      // configure this direction
      op(1'b1, ei[3:0], di[0], en[0], 11'd512,
         1'b0, 4'd0, 1'b0, 1'b0,  1'b0, 4'd0, 1'b0, 1'b0);
      // halt it if wanted
      if (hl) op(1'b0, 4'd0, 1'b0, 1'b0, 11'd0,
                 1'b1, ei[3:0], di[0], 1'b1,  1'b0, 4'd0, 1'b0, 1'b0);
      // flip the toggle if wanted
      if (tg) op(1'b0, 4'd0, 1'b0, 1'b0, 11'd0,
                 1'b0, 4'd0, 1'b0, 1'b0,  1'b1, ei[3:0], di[0], 1'b1);
      // and look it up
      op(1'b0, 4'd0, 1'b0, 1'b0, 11'd0,
         1'b0, 4'd0, 1'b0, 1'b0,  1'b1, ei[3:0], di[0], 1'b0);

      ri = (ei << 4) | (di << 3) | (en << 2) | (hl << 1) | tg;
      reach[ri] = 1'b1;
    end

    // =============================================================
    //  PHASE 2 (DIRECTED, EXHAUSTIVE) -- THE CHAPTER'S POINT.
    //
    //  For every endpoint number except 0, enable BOTH directions, then
    //  halt exactly ONE of them, and prove the other is untouched --
    //  enable, halt, max packet size and toggle all independently.
    //
    //  Both orders, both directions: 3 numbers x 2 directions x 2 orders.
    // =============================================================
    for (ei = 1; ei < N_NUM; ei = ei + 1)
    for (di = 0; di < 2; di = di + 1)
    for (k = 0; k < 2; k = k + 1) begin
      reset_dut;
      // both directions exist, with DIFFERENT packet sizes so a shared
      // field cannot pass by accident
      op(1'b1, ei[3:0], 1'b1, 1'b1, 11'd64,
         1'b0, 4'd0, 1'b0, 1'b0,  1'b0, 4'd0, 1'b0, 1'b0);
      op(1'b1, ei[3:0], 1'b0, 1'b1, 11'd512,
         1'b0, 4'd0, 1'b0, 1'b0,  1'b0, 4'd0, 1'b0, 1'b0);

      if (k == 0) begin
        // advance one toggle, then halt one direction
        op(1'b0, 4'd0, 1'b0, 1'b0, 11'd0,
           1'b0, 4'd0, 1'b0, 1'b0,  1'b1, ei[3:0], di[0], 1'b1);
        op(1'b0, 4'd0, 1'b0, 1'b0, 11'd0,
           1'b1, ei[3:0], di[0], 1'b1,  1'b0, 4'd0, 1'b0, 1'b0);
      end else begin
        // halt one direction, then try to use the OTHER
        op(1'b0, 4'd0, 1'b0, 1'b0, 11'd0,
           1'b1, ei[3:0], di[0], 1'b1,  1'b0, 4'd0, 1'b0, 1'b0);
        op(1'b0, 4'd0, 1'b0, 1'b0, 11'd0,
           1'b0, 4'd0, 1'b0, 1'b0,  1'b1, ei[3:0], ~di[0], 1'b1);
      end

      // the untouched direction must still work
      peek(ei[3:0], ~di[0]);
      ck(ep_valid === 1'b1, "the other direction stopped existing");
      ck(ep_halted === 1'b0, "halting one direction halted the other");
      tok_valid = 1'b0;

      // and clearing the halt leaves the other alone too
      op(1'b0, 4'd0, 1'b0, 1'b0, 11'd0,
         1'b1, ei[3:0], di[0], 1'b0,  1'b0, 4'd0, 1'b0, 1'b0);
    end

    // =============================================================
    //  PHASE 3 (DIRECTED) -- endpoint 0 is the exception.
    //
    //  It is bidirectional, it exists from reset, and it is not
    //  haltable: clearing a halt is itself a control transfer, so a
    //  device that could halt EP0 would be unrecoverable.
    // =============================================================
    reset_dut;
    for (di = 0; di < 2; di = di + 1) begin
      // it exists in both directions before anything configures it
      peek(4'd0, di[0]);
      ck(ep_valid === 1'b1, "EP0 did not exist at reset");
      ck(ep_maxp  === 11'd64, "EP0 had no default packet size");
      tok_valid = 1'b0;
      // and a halt attempt does nothing
      op(1'b0, 4'd0, 1'b0, 1'b0, 11'd0,
         1'b1, 4'd0, di[0], 1'b1,  1'b0, 4'd0, 1'b0, 1'b0);
      peek(4'd0, di[0]);
      ck(ep_halted === 1'b0, "EP0 was halted, which is unrecoverable");
      tok_valid = 1'b0;
    end
    // configuring EP0 configures both halves
    op(1'b1, 4'd0, 1'b1, 1'b1, 11'd8,
       1'b0, 4'd0, 1'b0, 1'b0,  1'b0, 4'd0, 1'b0, 1'b0);
    for (di = 0; di < 2; di = di + 1) begin
      peek(4'd0, di[0]);
      ck(ep_maxp === 11'd8, "configuring EP0 did not apply to both directions");
      tok_valid = 1'b0;
    end

    // =============================================================
    //  PHASE 4 (DIRECTED) -- an endpoint number that does not exist.
    // =============================================================
    reset_dut;
    for (k = N_NUM; k < 16; k = k + 1)
    for (di = 0; di < 2; di = di + 1) begin
      peek(k[3:0], di[0]);
      ck(ep_valid === 1'b0, "an out-of-range endpoint reported valid");
      ck(ep_maxp  === 11'd0, "an out-of-range endpoint reported a packet size");
      tok_valid = 1'b0;
      @(posedge clk); #1;
    end

    // =============================================================
    //  PHASE 5 (RANDOM) -- a driver configuring and halting freely.
    // =============================================================
`ifndef DIRECTED_ONLY
    reset_dut;
    for (k = 0; k < 8000; k = k + 1) begin
      op((urand(0) % 4) == 0, urand(0) % 16, (urand(0) % 2) == 0,
         (urand(0) % 4) != 0, (urand(0) % 2) ? 11'd64 : 11'd512,
         (urand(0) % 5) == 0, urand(0) % 16, (urand(0) % 2) == 0,
         (urand(0) % 3) != 0,
         (urand(0) % 2) == 0, urand(0) % 16, (urand(0) % 2) == 0,
         (urand(0) % 3) != 0);
      if ((k % 128) == 127) reset_dut;
    end
`endif

    n_reach = 0;
    for (ri = 0; ri < 64; ri = ri + 1) if (reach[ri]) n_reach = n_reach + 1;

    $display("steps=%0d checks=%0d reach=%0d/64 errors=%0d",
             steps, checks, n_reach, errors);
    $display("[ep] lookups=%0d unknown=%0d halted_hits=%0d toggles=%0d split_halts=%0d",
             g_look, g_unk, g_halt, g_flip, g_split);
    $display("[the whole point] cross-direction leaks = %0d", n_cross);
    if (n_reach != 64) begin
      $display("FAIL: exhaustive sweep incomplete"); errors = errors + 1;
    end
    if (errors == 0) $display("PASS: 0 errors in %0d checks", checks);
    else             $display("FAIL: %0d errors in %0d checks", errors, checks);
    $finish;
  end

endmodule