Dual-Bus Architecture

   D+  / D-       the USB 2 bus, exactly as Modules 1 to 19 described it
   SSTX+ / SSTX-  SuperSpeed, device to host
   SSRX+ / SSRX-  SuperSpeed, host to device

// usb3_dual_bus_arbiter -- two complete buses in one cable, and the decision
// between them.
//
// A USB 3 cable does not carry a faster version of the USB 2 wires. It
// carries the USB 2 wires UNCHANGED, plus two additional differential pairs:
//
//     D+ / D-        the USB 2 bus, exactly as Modules 1 to 19 described it
//     SSTX+ / SSTX-  SuperSpeed, device to host
//     SSRX+ / SSRX-  SuperSpeed, host to device
//
// Two things follow immediately, and they pull in opposite directions.
//
// FULL DUPLEX. SuperSpeed has a pair in each direction, so both ends may
// transmit at once. Chapter 18.1's repeater asymmetry -- broadcast down,
// select one up -- was forced by a SINGLE shared path; with two, it is not
// a constraint any more.
//
// AND MUTUAL EXCLUSION. A device operates at SuperSpeed OR at USB 2, never
// both at once for data. A device answering on both buses would answer every
// transaction twice, and the host has no way to tell which reply is real.
// The two buses are physically parallel and logically exclusive, and the
// interesting hardware is not either bus -- it is the decision between them.
//
// THE PULL-UP IS THE EXCEPTION, AND IT IS NOT AN OVERSIGHT
//
// The USB 2 attach detection runs whenever the port is powered, EVEN WHILE
// SuperSpeed is active. It has to: a USB 3 device plugged into a USB-2-only
// host must still be seen, and the only way the host can see it is the D+
// pull-up of chapter 19.2. So:
//
//     DATA      exclusive -- exactly one bus at a time
//     PRESENCE  always -- the USB 2 pull-up is independent of the decision
//
// A design that gates the pull-up on "not using SuperSpeed" makes a USB 3
// device invisible to every USB 2 host, which is the single most expensive
// way to fail this block.
//
// FALLBACK IS ONE-WAY
//
// SuperSpeed is attempted first. If training fails, the device falls back to
// USB 2 -- and STAYS there until a reset. It does not spontaneously retry,
// because a device that oscillated between buses would present and withdraw
// itself repeatedly, and the host would see a device that will not enumerate
// rather than one that is slow.
module usb3_dual_bus_arbiter (
  input  wire       clk,
  input  wire       rst_n,

  input  wire       vbus_present,
  input  wire       ss_rx_detect,     // a SuperSpeed partner is out there
  input  wire       ss_training_ok,   // the SuperSpeed link trained (20.3)
  input  wire       ss_training_fail,
  input  wire       ss_link_down,     // an established link was lost
  input  wire       host_reset,       // the only way back to SuperSpeed

  output wire [1:0] active_bus,
  output wire       ss_data_enable,   // SuperSpeed carries data
  output wire       usb2_data_enable, // the USB 2 pair carries data
  output wire       usb2_pullup,      // PRESENCE -- not gated on the above
  output wire       training,

  output reg [31:0] fallbacks,
  output reg [31:0] training_attempts,
  output reg        ever_fell_back
);
  localparam [1:0] BUS_NONE = 2'd0,   // no VBUS: nothing is running
                   BUS_SS   = 2'd1,   // SuperSpeed carries the data
                   BUS_USB2 = 2'd2,   // the USB 2 pair carries the data
                   BUS_TRAIN = 2'd3;  // deciding -- neither carries data yet

  reg [1:0] state;

  // THE MUTUAL EXCLUSION, structural. Both enables are decodes of one state
  // register, so there is no sequence of events that asserts both -- which
  // is a stronger guarantee than checking that they never are.
  //
  // AND BOTH ARE GATED ON VBUS, combinationally. The state register is
  // sequential: on the cycle VBUS disappears it still reads BUS_SS, and a
  // decode of it alone would drive a SuperSpeed transmitter into a host
  // that has just been unpowered. That is chapter 19.2's back-powering in
  // its SuperSpeed form, and the fix is the same one gate.
  assign active_bus       = state;
  assign ss_data_enable   = (state == BUS_SS)    && vbus_present;
  assign usb2_data_enable = (state == BUS_USB2)  && vbus_present;
  assign training         = (state == BUS_TRAIN) && vbus_present;

  // THE EXCEPTION. Presence detection is NOT part of the exclusion: the
  // pull-up follows VBUS and nothing else, so a USB 3 device remains
  // visible to a USB 2 host that will never speak SuperSpeed to it.
  // Chapter 19.2's guard still applies -- no VBUS, no pull-up, ever.
  assign usb2_pullup = vbus_present;

  always @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      state             <= BUS_NONE;
      fallbacks         <= 32'd0;
      training_attempts <= 32'd0;
      ever_fell_back    <= 1'b0;
    end else if (!vbus_present) begin
      // Physical reality first, as everywhere in this track. No VBUS, no
      // bus of either kind.
      state <= BUS_NONE;
    end else if (host_reset) begin
      // THE ONLY WAY BACK. A reset returns the device to the undecided
      // state, where SuperSpeed will be attempted again. Without this the
      // fallback of the next branch would be permanent for the life of the
      // attachment.
      state <= BUS_NONE;
    end else begin
      case (state)
        BUS_NONE: begin
          if (ss_rx_detect) begin
            // A SuperSpeed partner is present: try SuperSpeed FIRST.
            state             <= BUS_TRAIN;
            training_attempts <= training_attempts + 32'd1;
          end else begin
            // No SuperSpeed partner -- a USB 2 host, or a USB 2 cable.
            // Fall straight to USB 2 without attempting to train.
            state <= BUS_USB2;
          end
        end

        BUS_TRAIN: begin
          // Note the precedence: FAILURE outranks success. If both arrive
          // in one cycle the link is not trustworthy, and treating it as
          // trained would bring a bad link up rather than fall back.
          if (ss_training_fail) begin
            state          <= BUS_USB2;
            fallbacks      <= fallbacks + 32'd1;
            ever_fell_back <= 1'b1;
          end else if (ss_training_ok) begin
            state <= BUS_SS;
          end
        end

        BUS_SS: begin
          if (ss_link_down) begin
            // A trained link that was lost gets ONE more attempt, not an
            // immediate fallback: a transient is not a reason to spend the
            // rest of the attachment at a twentieth of the bandwidth.
            state             <= BUS_TRAIN;
            training_attempts <= training_attempts + 32'd1;
          end
        end

        BUS_USB2: begin
          // FALLBACK IS ONE-WAY. Nothing here moves to SuperSpeed --
          // ss_rx_detect asserting again does not, ss_training_ok does not.
          // Only the host_reset branch above escapes, and only by going
          // through BUS_NONE first.
          state <= BUS_USB2;
        end

        default: state <= BUS_NONE;
      endcase
    end
  end
endmodule

package usb3_dualbus_pkg;
  // Which bus is carrying data. BUS_TRAIN is a state in its own right and
  // not a flavour of "none": a link that is training has a SuperSpeed
  // partner and has not given up on it, which is entirely different from a
  // port with nothing attached.
  typedef enum logic [1:0] {
    BUS_NONE,    // no VBUS: nothing is running
    BUS_SS,      // SuperSpeed carries the data
    BUS_USB2,    // the USB 2 pair carries the data
    BUS_TRAIN    // deciding -- neither carries data yet
  } active_bus_e;
endpackage

// usb3_dual_bus_arbiter_sv -- two complete buses in one cable, and the decision
// between them.
//
// A USB 3 cable does not carry a faster version of the USB 2 wires. It
// carries the USB 2 wires UNCHANGED, plus two additional differential pairs:
//
//     D+ / D-        the USB 2 bus, exactly as Modules 1 to 19 described it
//     SSTX+ / SSTX-  SuperSpeed, device to host
//     SSRX+ / SSRX-  SuperSpeed, host to device
//
// Two things follow immediately, and they pull in opposite directions.
//
// FULL DUPLEX. SuperSpeed has a pair in each direction, so both ends may
// transmit at once. Chapter 18.1's repeater asymmetry -- broadcast down,
// select one up -- was forced by a SINGLE shared path; with two, it is not
// a constraint any more.
//
// AND MUTUAL EXCLUSION. A device operates at SuperSpeed OR at USB 2, never
// both at once for data. A device answering on both buses would answer every
// transaction twice, and the host has no way to tell which reply is real.
// The two buses are physically parallel and logically exclusive, and the
// interesting hardware is not either bus -- it is the decision between them.
//
// THE PULL-UP IS THE EXCEPTION, AND IT IS NOT AN OVERSIGHT
//
// The USB 2 attach detection runs whenever the port is powered, EVEN WHILE
// SuperSpeed is active. It has to: a USB 3 device plugged into a USB-2-only
// host must still be seen, and the only way the host can see it is the D+
// pull-up of chapter 19.2. So:
//
//     DATA      exclusive -- exactly one bus at a time
//     PRESENCE  always -- the USB 2 pull-up is independent of the decision
//
// A design that gates the pull-up on "not using SuperSpeed" makes a USB 3
// device invisible to every USB 2 host, which is the single most expensive
// way to fail this block.
//
// FALLBACK IS ONE-WAY
//
// SuperSpeed is attempted first. If training fails, the device falls back to
// USB 2 -- and STAYS there until a reset. It does not spontaneously retry,
// because a device that oscillated between buses would present and withdraw
// itself repeatedly, and the host would see a device that will not enumerate
// rather than one that is slow.
module usb3_dual_bus_arbiter_sv
  import usb3_dualbus_pkg::*;
(
  input  logic      clk,
  input  logic      rst_n,

  input  logic      vbus_present,
  input  logic      ss_rx_detect,     // a SuperSpeed partner is out there
  input  logic      ss_training_ok,   // the SuperSpeed link trained (20.3)
  input  logic      ss_training_fail,
  input  logic      ss_link_down,     // an established link was lost
  input  logic      host_reset,       // the only way back to SuperSpeed

  output active_bus_e active_bus,
  output logic      ss_data_enable,   // SuperSpeed carries data
  output logic      usb2_data_enable, // the USB 2 pair carries data
  output logic      usb2_pullup,      // PRESENCE -- not gated on the above
  output logic      training,

  output logic [31:0] fallbacks,
  output logic [31:0] training_attempts,
  output logic      ever_fell_back
);
  active_bus_e state;

  // THE MUTUAL EXCLUSION, structural. Both enables are decodes of one state
  // register, so there is no sequence of events that asserts both -- which
  // is a stronger guarantee than checking that they never are.
  //
  // AND BOTH ARE GATED ON VBUS, combinationally. The state register is
  // sequential: on the cycle VBUS disappears it still reads BUS_SS, and a
  // decode of it alone would drive a SuperSpeed transmitter into a host
  // that has just been unpowered. That is chapter 19.2's back-powering in
  // its SuperSpeed form, and the fix is the same one gate.
  assign active_bus       = state;
  assign ss_data_enable   = (state == BUS_SS)    && vbus_present;
  assign usb2_data_enable = (state == BUS_USB2)  && vbus_present;
  assign training         = (state == BUS_TRAIN) && vbus_present;

  // THE EXCEPTION. Presence detection is NOT part of the exclusion: the
  // pull-up follows VBUS and nothing else, so a USB 3 device remains
  // visible to a USB 2 host that will never speak SuperSpeed to it.
  // Chapter 19.2's guard still applies -- no VBUS, no pull-up, ever.
  assign usb2_pullup = vbus_present;

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      state             <= BUS_NONE;
      fallbacks         <= '0;
      training_attempts <= '0;
      ever_fell_back    <= 1'b0;
    end else if (!vbus_present) begin
      // Physical reality first, as everywhere in this track. No VBUS, no
      // bus of either kind.
      state <= BUS_NONE;
    end else if (host_reset) begin
      // THE ONLY WAY BACK. A reset returns the device to the undecided
      // state, where SuperSpeed will be attempted again. Without this the
      // fallback of the next branch would be permanent for the life of the
      // attachment.
      state <= BUS_NONE;
    end else begin
      case (state)
        BUS_NONE: begin
          if (ss_rx_detect) begin
            // A SuperSpeed partner is present: try SuperSpeed FIRST.
            state             <= BUS_TRAIN;
            training_attempts <= training_attempts + 1;
          end else begin
            // No SuperSpeed partner -- a USB 2 host, or a USB 2 cable.
            // Fall straight to USB 2 without attempting to train.
            state <= BUS_USB2;
          end
        end

        BUS_TRAIN: begin
          // Note the precedence: FAILURE outranks success. If both arrive
          // in one cycle the link is not trustworthy, and treating it as
          // trained would bring a bad link up rather than fall back.
          if (ss_training_fail) begin
            state          <= BUS_USB2;
            fallbacks      <= fallbacks + 1;
            ever_fell_back <= 1'b1;
          end else if (ss_training_ok) begin
            state <= BUS_SS;
          end
        end

        BUS_SS: begin
          if (ss_link_down) begin
            // A trained link that was lost gets ONE more attempt, not an
            // immediate fallback: a transient is not a reason to spend the
            // rest of the attachment at a twentieth of the bandwidth.
            state             <= BUS_TRAIN;
            training_attempts <= training_attempts + 1;
          end
        end

        BUS_USB2: begin
          // FALLBACK IS ONE-WAY. Nothing here moves to SuperSpeed --
          // ss_rx_detect asserting again does not, ss_training_ok does not.
          // Only the host_reset branch above escapes, and only by going
          // through BUS_NONE first.
          state <= BUS_USB2;
        end

        default: state <= BUS_NONE;
      endcase
    end
  end
endmodule

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

package usb3_dualbus_pkg is
  -- Which bus is carrying data. BUS_TRAIN is a state in its own right and
  -- not a flavour of "none": a link that is training has a SuperSpeed
  -- partner and has not given up on it, which is entirely different from a
  -- port with nothing attached.
  type active_bus_t is (
    BUS_NONE,    -- no VBUS: nothing is running
    BUS_SS,      -- SuperSpeed carries the data
    BUS_USB2,    -- the USB 2 pair carries the data
    BUS_TRAIN    -- deciding -- neither carries data yet
  );
end package;

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

-- usb3_dual_bus_arbiter_vhdl -- two complete buses in one cable, and the
-- decision between them.
--
-- A USB 3 cable does not carry a faster version of the USB 2 wires. It
-- carries the USB 2 wires UNCHANGED, plus two additional differential pairs:
--
--     D+ / D-        the USB 2 bus, exactly as Modules 1 to 19 described it
--     SSTX+ / SSTX-  SuperSpeed, device to host
--     SSRX+ / SSRX-  SuperSpeed, host to device
--
-- FULL DUPLEX. SuperSpeed has a pair in each direction, so both ends may
-- transmit at once. Chapter 18.1's repeater asymmetry -- broadcast down,
-- select one up -- was forced by a SINGLE shared path; with two, it is not
-- a constraint any more.
--
-- AND MUTUAL EXCLUSION. A device operates at SuperSpeed OR at USB 2, never
-- both at once for data. A device answering on both buses would answer every
-- transaction twice, and the host has no way to tell which reply is real.
--
-- THE PULL-UP IS THE EXCEPTION, AND IT IS NOT AN OVERSIGHT
--
-- The USB 2 attach detection runs whenever the port is powered, EVEN WHILE
-- SuperSpeed is active. It has to: a USB 3 device plugged into a USB-2-only
-- host must still be seen, and the only way the host can see it is the D+
-- pull-up of chapter 19.2. So:
--
--     DATA      exclusive -- exactly one bus at a time
--     PRESENCE  always -- the USB 2 pull-up is independent of the decision
--
-- FALLBACK IS ONE-WAY
--
-- SuperSpeed is attempted first. If training fails, the device falls back to
-- USB 2 -- and STAYS there until a reset. A device that oscillated between
-- buses would present and withdraw itself repeatedly, and the host would see
-- a device that will not enumerate rather than one that is slow.
entity usb3_dual_bus_arbiter_vhdl is
  port (
    clk               : in  std_logic;
    rst_n             : in  std_logic;

    vbus_present      : in  std_logic;
    ss_rx_detect      : in  std_logic;
    ss_training_ok    : in  std_logic;
    ss_training_fail  : in  std_logic;
    ss_link_down      : in  std_logic;
    host_reset        : in  std_logic;

    active_bus        : out active_bus_t;
    ss_data_enable    : out std_logic;
    usb2_data_enable  : out std_logic;
    usb2_pullup       : out std_logic;
    training          : out std_logic;

    fallbacks         : out unsigned(31 downto 0);
    training_attempts : out unsigned(31 downto 0);
    ever_fell_back    : out std_logic
  );
end entity;

architecture rtl of usb3_dual_bus_arbiter_vhdl is
  signal st_r   : active_bus_t := BUS_NONE;
  signal fb_r   : unsigned(31 downto 0) := (others => '0');
  signal ta_r   : unsigned(31 downto 0) := (others => '0');
  signal ever_r : std_logic := '0';
begin
  -- THE MUTUAL EXCLUSION, structural. Both enables are decodes of one state
  -- signal, so there is no sequence of events that asserts both -- which is
  -- a stronger guarantee than checking that they never are.
  --
  -- AND BOTH ARE GATED ON VBUS, combinationally. The state is sequential:
  -- on the cycle VBUS disappears it still reads BUS_SS, and a decode of it
  -- alone would drive a SuperSpeed transmitter into a host that has just
  -- been unpowered. That is chapter 19.2's back-powering in its SuperSpeed
  -- form, and the fix is the same one gate.
  active_bus       <= st_r;
  ss_data_enable   <= '1' when (st_r = BUS_SS    and vbus_present = '1') else '0';
  usb2_data_enable <= '1' when (st_r = BUS_USB2  and vbus_present = '1') else '0';
  training         <= '1' when (st_r = BUS_TRAIN and vbus_present = '1') else '0';

  -- THE EXCEPTION. Presence detection is NOT part of the exclusion: the
  -- pull-up follows VBUS and nothing else, so a USB 3 device remains
  -- visible to a USB 2 host that will never speak SuperSpeed to it.
  usb2_pullup <= vbus_present;

  fallbacks         <= fb_r;
  training_attempts <= ta_r;
  ever_fell_back    <= ever_r;

  process (clk, rst_n)
  begin
    if rst_n = '0' then
      st_r <= BUS_NONE; fb_r <= (others => '0');
      ta_r <= (others => '0'); ever_r <= '0';
    elsif rising_edge(clk) then
      if vbus_present = '0' then
        -- Physical reality first, as everywhere in this track.
        st_r <= BUS_NONE;
      elsif host_reset = '1' then
        -- THE ONLY WAY BACK. A reset returns the device to the undecided
        -- state, where SuperSpeed will be attempted again.
        st_r <= BUS_NONE;
      else
        case st_r is
          when BUS_NONE =>
            if ss_rx_detect = '1' then
              -- A SuperSpeed partner is present: try SuperSpeed FIRST.
              st_r <= BUS_TRAIN;
              ta_r <= ta_r + 1;
            else
              -- No SuperSpeed partner -- a USB 2 host, or a USB 2 cable.
              st_r <= BUS_USB2;
            end if;

          when BUS_TRAIN =>
            -- Note the precedence: FAILURE outranks success. If both arrive
            -- in one cycle the link is not trustworthy, and treating it as
            -- trained would bring a bad link up rather than fall back.
            if ss_training_fail = '1' then
              st_r <= BUS_USB2;
              fb_r <= fb_r + 1;
              ever_r <= '1';
            elsif ss_training_ok = '1' then
              st_r <= BUS_SS;
            end if;

          when BUS_SS =>
            if ss_link_down = '1' then
              -- A trained link that was lost gets ONE more attempt, not an
              -- immediate fallback: a transient is not a reason to spend
              -- the rest of the attachment at a twentieth of the bandwidth.
              st_r <= BUS_TRAIN;
              ta_r <= ta_r + 1;
            end if;

          when BUS_USB2 =>
            -- FALLBACK IS ONE-WAY. Nothing here moves to SuperSpeed --
            -- ss_rx_detect asserting again does not, ss_training_ok does
            -- not. Only the host_reset branch above escapes, and only by
            -- going through BUS_NONE first.
            st_r <= BUS_USB2;
        end case;
      end if;
    end if;
  end process;
end architecture;

      // 3. No VBUS, no bus of either kind.
      if (!vb) begin
        check(!ss_data_enable && !usb2_data_enable,
              "a bus was carrying data with no VBUS");
      end

    for (pos=0; pos<4; pos=pos+1)
     for (ic=0; ic<64; ic=ic+1) begin
       goto(pos);
       tick(ic[0], ic[1], ic[2], ic[3], ic[4], ic[5]);

    // Every interleaving of "the link trained" and "the link failed" across
    // a 6-tick window: 2^6 x 2^6 = 4096 scenarios. These are the two inputs
    // whose PRECEDENCE decides whether a bad link comes up, and the whole
    // point is that failure outranks success when both arrive together.

      // ---- THE HISTORY INVARIANT, which no model supplies ----
      // FALLBACK IS ONE-WAY. A device that has fallen back to USB 2 never
      // reaches SuperSpeed again without passing through BUS_NONE -- which
      // only a reset or a VBUS loss produces.
      if (active_bus === B_SS && m_prev !== B_SS) begin
        n_enter_ss = n_enter_ss + 1;
        check(m_prev === B_TRAIN,
              "SuperSpeed was entered from somewhere other than training");
      end
      if (m_prev === B_USB2)
        check(active_bus !== B_SS,
              "a device that had fallen back reached SuperSpeed without a reset");

  exhaustive transition sweep: 256 of 256 transitions verified
  exhaustive training-outcome sweep: 4096 of 4096 verified

  Verilog / SystemVerilog:
  REACH: ss-ticks=15010 usb2-ticks=33740 training-ticks=12424
         fallbacks=795 ss-entries=2765
  [Verilog] usb3_dual_bus_arbiter: 0 errors — PASS

  VHDL:
  REACH: ss-ticks=15390 usb2-ticks=33349 training-ticks=12386
         fallbacks=772 ss-entries=2746
  [VHDL] usb3_dual_bus_arbiter_vhdl: 0 errors — PASS

`timescale 1ns/1ps
module tb_db_v;
  localparam W = 6;
  reg clk=0, rst_n=0;
  reg vbus=0, ssrx=0, tok=0, tfail=0, ldown=0, hrst=0;
  wire [1:0] active_bus;
  wire ss_data_enable, usb2_data_enable, usb2_pullup, training;
  wire [31:0] fallbacks, training_attempts;
  wire ever_fell_back;
  always #5 clk=~clk;

  usb3_dual_bus_arbiter dut (
    .clk(clk), .rst_n(rst_n), .vbus_present(vbus), .ss_rx_detect(ssrx),
    .ss_training_ok(tok), .ss_training_fail(tfail), .ss_link_down(ldown),
    .host_reset(hrst), .active_bus(active_bus),
    .ss_data_enable(ss_data_enable), .usb2_data_enable(usb2_data_enable),
    .usb2_pullup(usb2_pullup), .training(training), .fallbacks(fallbacks),
    .training_attempts(training_attempts), .ever_fell_back(ever_fell_back));

  localparam [1:0] B_NONE=0, B_SS=1, B_USB2=2, B_TRAIN=3;

  integer errors=0, i, pos, ic, pat, t;
  integer n_trans=0, n_pat=0, n_ss=0, n_u2=0, n_train=0, n_fb=0;
  integer n_enter_ss=0;
  // ---- INDEPENDENT MODEL: its own state and counters ----
  integer m_state, m_fb, m_ta, m_prev;
  reg m_ever;

  task check(input cond, input [639:0] msg);
    begin if (!cond) begin errors=errors+1;
      if (errors <= 25)
        $display("  FAIL: %0s (vb=%b ssrx=%b ok=%b fail=%b down=%b rst=%b | bus=%0d sse=%b u2e=%b pu=%b, t=%0t)",
                 msg, vbus, ssrx, tok, tfail, ldown, hrst, active_bus,
                 ss_data_enable, usb2_data_enable, usb2_pullup, $time);
    end end
  endtask

  task tick(input vb, input sr, input ok, input fl, input dn, input hr);
    integer nst;
    begin
      vbus=vb; ssrx=sr; tok=ok; tfail=fl; ldown=dn; hrst=hr; #1;

      // ---- combinational contract ----
      check(active_bus       === m_state[1:0],       "active_bus matches the model");
      check(ss_data_enable   === ((m_state == B_SS)    && vb),
            "ss_data_enable decodes the state AND requires VBUS");
      check(usb2_data_enable === ((m_state == B_USB2)  && vb),
            "usb2_data_enable decodes the state AND requires VBUS");
      check(training         === ((m_state == B_TRAIN) && vb),
            "training decodes the state AND requires VBUS");

      // ---- SAFETY PROPERTIES, independent of the model ----
      // 1. THE one that matters: the two data paths are NEVER both live.
      //    A device answering on both buses answers every transaction
      //    twice, and the host cannot tell which reply is real.
      check(!(ss_data_enable && usb2_data_enable),
            "both buses carrying data at once: the device answers twice");
      // 2. THE EXCEPTION: presence detection is not part of the exclusion.
      //    The pull-up follows VBUS and nothing else, so a USB 3 device
      //    stays visible to a USB 2 host.
      check(usb2_pullup === vb,
            "the USB 2 pull-up was gated on something other than VBUS");
      // 3. No VBUS, no bus of either kind.
      if (!vb) begin
        check(!ss_data_enable && !usb2_data_enable,
              "a bus was carrying data with no VBUS");
      end
      // 4. Training carries no data on either bus.
      if (training)
        check(!ss_data_enable && !usb2_data_enable,
              "data flowed while the link was still training");

      // ---- advance the model ----
      nst = m_state;
      if (!vb)      nst = B_NONE;
      else if (hr)  nst = B_NONE;
      else case (m_state)
        B_NONE:  if (sr) begin nst = B_TRAIN; m_ta = m_ta + 1; end
                 else         nst = B_USB2;
        B_TRAIN: if (fl) begin nst = B_USB2; m_fb = m_fb + 1; m_ever = 1; end
                 else if (ok) nst = B_SS;
        B_SS:    if (dn) begin nst = B_TRAIN; m_ta = m_ta + 1; end
        B_USB2:  nst = B_USB2;
      endcase

      if (m_state == B_SS)    n_ss    = n_ss + 1;
      if (m_state == B_USB2)  n_u2    = n_u2 + 1;
      if (m_state == B_TRAIN) n_train = n_train + 1;

      m_prev = m_state;
      @(posedge clk); #1;
      m_state = nst;

      check(fallbacks         === m_fb[31:0], "fallbacks matches the model");
      check(training_attempts === m_ta[31:0], "training_attempts matches the model");
      check(ever_fell_back    === m_ever,     "ever_fell_back matches the model");

      // ---- THE HISTORY INVARIANT, which no model supplies ----
      // FALLBACK IS ONE-WAY. A device that has fallen back to USB 2 never
      // reaches SuperSpeed again without passing through BUS_NONE -- which
      // only a reset or a VBUS loss produces.
      if (active_bus === B_SS && m_prev !== B_SS) begin
        n_enter_ss = n_enter_ss + 1;
        check(m_prev === B_TRAIN,
              "SuperSpeed was entered from somewhere other than training");
      end
      if (m_prev === B_USB2)
        check(active_bus !== B_SS,
              "a device that had fallen back reached SuperSpeed without a reset");
    end
  endtask

  task hard_reset;
    begin
      rst_n=0; vbus=0; ssrx=0; tok=0; tfail=0; ldown=0; hrst=0;
      @(posedge clk); #1; @(posedge clk); #1; rst_n=1; #1;
      m_state=B_NONE; m_fb=0; m_ta=0; m_ever=0; m_prev=B_NONE;
    end
  endtask

  // Drive to one of the four states, legitimately.
  task goto(input integer p);
    begin
      hard_reset;
      if (p == B_NONE) begin end
      else if (p == B_USB2) begin
        tick(1,0,0,0,0,0);          // VBUS, no SS partner -> USB2
      end else begin
        tick(1,1,0,0,0,0);          // VBUS + SS partner -> TRAIN
        if (p == B_SS) tick(1,1,1,0,0,0);
      end
    end
  endtask

  initial begin
    hard_reset;
    check(active_bus === B_NONE, "the arbiter comes up with no bus");
    check(!usb2_pullup, "and no pull-up, because there is no VBUS");

    // ===== A. EXHAUSTIVE ONE-STEP TRANSITIONS =====
    // 4 states x all 64 combinations of the six control inputs = 256
    // transitions: the entire one-step domain.
    for (pos=0; pos<4; pos=pos+1)
     for (ic=0; ic<64; ic=ic+1) begin
       goto(pos);
       tick(ic[0], ic[1], ic[2], ic[3], ic[4], ic[5]);
       n_trans = n_trans + 1;
     end
    $display("  exhaustive transition sweep: %0d of %0d transitions verified",
             n_trans, 4*64);

    // ===== B. EXHAUSTIVE OVER TRAINING OUTCOMES, JOINTLY =====
    // Every interleaving of "the link trained" and "the link failed" across
    // a 6-tick window: 2^6 x 2^6 = 4096 scenarios. These are the two inputs
    // whose PRECEDENCE decides whether a bad link comes up, and the whole
    // point is that failure outranks success when both arrive together.
    for (pat=0; pat<4096; pat=pat+1) begin
      hard_reset;
      tick(1,1,0,0,0,0);            // VBUS + SS partner: enter training
      for (t=0; t<W; t=t+1)
        tick(1'b1, 1'b1, pat[t], pat[t+W], 1'b0, 1'b0);
      n_pat = n_pat + 1;
    end
    $display("  exhaustive training-outcome sweep: %0d of 4096 verified",
             n_pat);

    // ===== C. directed: the three rules =====
    // SuperSpeed is tried FIRST
    hard_reset;
    tick(1,1,0,0,0,0);
    check(training, "with a SuperSpeed partner present, SuperSpeed is tried");
    check(!usb2_data_enable, "and USB 2 carries nothing meanwhile");
    check(usb2_pullup, "but the pull-up is up: a USB 2 host must still see it");
    tick(1,1,1,0,0,0);
    check(ss_data_enable, "training succeeds and SuperSpeed carries the data");
    check(!usb2_data_enable, "and USB 2 does not");

    // no SuperSpeed partner: straight to USB 2, no training attempt
    hard_reset;
    tick(1,0,0,0,0,0);
    check(usb2_data_enable, "with no SuperSpeed partner it goes straight to USB 2");
    check(training_attempts === 32'd0, "without attempting to train at all");

    // failure outranks success
    hard_reset;
    tick(1,1,0,0,0,0);
    tick(1,1,1,1,0,0);              // ok AND fail in the same cycle
    check(usb2_data_enable,
          "failure outranks success: a doubtful link is not brought up");
    check(fallbacks === 32'd1, "and the fallback is counted");

    // fallback is ONE-WAY
    hard_reset;
    tick(1,1,0,0,0,0);
    tick(1,1,0,1,0,0);
    check(usb2_data_enable, "fallen back to USB 2");
    tick(1,1,1,0,0,0);
    check(usb2_data_enable, "a later training success does NOT move it back");
    tick(1,1,1,0,0,0);
    check(usb2_data_enable, "nor does another");
    tick(1,1,0,0,0,1);              // host reset
    check(active_bus === B_NONE, "only a reset escapes");
    tick(1,1,0,0,0,0);
    check(training, "and then SuperSpeed is tried again");

    // a lost link retrains rather than falling back immediately
    hard_reset;
    tick(1,1,0,0,0,0); tick(1,1,1,0,0,0);
    check(ss_data_enable, "SuperSpeed up");
    tick(1,1,0,0,1,0);
    check(training, "a lost link RETRAINS rather than falling back at once");
    check(training_attempts === 32'd2, "which is a second attempt");

    // the pull-up is independent of everything
    hard_reset;
    tick(1,1,0,0,0,0); tick(1,1,1,0,0,0);
    check(ss_data_enable && usb2_pullup,
          "the pull-up stays up while SuperSpeed carries the data");
    tick(0,0,0,0,0,0);
    check(!usb2_pullup, "and drops only with VBUS");

    // ===== D. randomised =====
    for (i=0;i<40000;i=i+1)
      tick(({$random}%16)!=0, ({$random}%3)!=0, ({$random}%4)==0,
           ({$random}%8)==0, ({$random}%16)==0, ({$random}%32)==0);

    check(n_ss>0 && n_u2>0 && n_train>0,
          "the run reached SuperSpeed, USB 2 and training");
    check(ever_fell_back, "and exercised the fallback path");

    $display("");
    $display("  REACH: transitions=%0d interleavings=%0d | ss-ticks=%0d usb2-ticks=%0d training-ticks=%0d fallbacks=%0d ss-entries=%0d",
             n_trans, n_pat, n_ss, n_u2, n_train, fallbacks, n_enter_ss);
    $display("  [Verilog] usb3_dual_bus_arbiter: %0d errors", errors);
    $display("  [Verilog] %0s", errors==0 ? "PASS" : "FAIL");
    $display("");
    $finish;
  end
endmodule

`timescale 1ns/1ps
module tb_db_sv;
  import usb3_dualbus_pkg::*;
  localparam W = 6;
  reg clk=0, rst_n=0;
  reg vbus=0, ssrx=0, tok=0, tfail=0, ldown=0, hrst=0;
  active_bus_e active_bus;
  wire ss_data_enable, usb2_data_enable, usb2_pullup, training;
  wire [31:0] fallbacks, training_attempts;
  wire ever_fell_back;
  always #5 clk=~clk;

  usb3_dual_bus_arbiter_sv dut (
    .clk(clk), .rst_n(rst_n), .vbus_present(vbus), .ss_rx_detect(ssrx),
    .ss_training_ok(tok), .ss_training_fail(tfail), .ss_link_down(ldown),
    .host_reset(hrst), .active_bus(active_bus),
    .ss_data_enable(ss_data_enable), .usb2_data_enable(usb2_data_enable),
    .usb2_pullup(usb2_pullup), .training(training), .fallbacks(fallbacks),
    .training_attempts(training_attempts), .ever_fell_back(ever_fell_back));



  localparam active_bus_e B_NONE=BUS_NONE, B_SS=BUS_SS,
                          B_USB2=BUS_USB2, B_TRAIN=BUS_TRAIN;
  integer errors=0, i, pos, ic, pat, t;
  integer n_trans=0, n_pat=0, n_ss=0, n_u2=0, n_train=0, n_fb=0;
  integer n_enter_ss=0;
  // ---- INDEPENDENT MODEL: its own state and counters ----
  integer m_state, m_fb, m_ta, m_prev;
  reg m_ever;

  task check(input cond, input [639:0] msg);
    begin if (!cond) begin errors=errors+1;
      if (errors <= 25)
        $display("  FAIL: %0s (vb=%b ssrx=%b ok=%b fail=%b down=%b rst=%b | bus=%0d sse=%b u2e=%b pu=%b, t=%0t)",
                 msg, vbus, ssrx, tok, tfail, ldown, hrst, active_bus,
                 ss_data_enable, usb2_data_enable, usb2_pullup, $time);
    end end
  endtask

  task tick(input vb, input sr, input ok, input fl, input dn, input hr);
    integer nst;
    begin
      vbus=vb; ssrx=sr; tok=ok; tfail=fl; ldown=dn; hrst=hr; #1;

      // ---- combinational contract ----
      check(active_bus === active_bus_e'(m_state[1:0]),
            "active_bus matches the model");
      check(ss_data_enable   === ((m_state == B_SS)    && vb),
            "ss_data_enable decodes the state AND requires VBUS");
      check(usb2_data_enable === ((m_state == B_USB2)  && vb),
            "usb2_data_enable decodes the state AND requires VBUS");
      check(training         === ((m_state == B_TRAIN) && vb),
            "training decodes the state AND requires VBUS");

      // ---- SAFETY PROPERTIES, independent of the model ----
      // 1. THE one that matters: the two data paths are NEVER both live.
      //    A device answering on both buses answers every transaction
      //    twice, and the host cannot tell which reply is real.
      check(!(ss_data_enable && usb2_data_enable),
            "both buses carrying data at once: the device answers twice");
      // 2. THE EXCEPTION: presence detection is not part of the exclusion.
      //    The pull-up follows VBUS and nothing else, so a USB 3 device
      //    stays visible to a USB 2 host.
      check(usb2_pullup === vb,
            "the USB 2 pull-up was gated on something other than VBUS");
      // 3. No VBUS, no bus of either kind.
      if (!vb) begin
        check(!ss_data_enable && !usb2_data_enable,
              "a bus was carrying data with no VBUS");
      end
      // 4. Training carries no data on either bus.
      if (training)
        check(!ss_data_enable && !usb2_data_enable,
              "data flowed while the link was still training");

      // ---- advance the model ----
      nst = m_state;
      if (!vb)      nst = B_NONE;
      else if (hr)  nst = B_NONE;
      else case (m_state)
        B_NONE:  if (sr) begin nst = B_TRAIN; m_ta = m_ta + 1; end
                 else         nst = B_USB2;
        B_TRAIN: if (fl) begin nst = B_USB2; m_fb = m_fb + 1; m_ever = 1; end
                 else if (ok) nst = B_SS;
        B_SS:    if (dn) begin nst = B_TRAIN; m_ta = m_ta + 1; end
        B_USB2:  nst = B_USB2;
      endcase

      if (m_state == B_SS)    n_ss    = n_ss + 1;
      if (m_state == B_USB2)  n_u2    = n_u2 + 1;
      if (m_state == B_TRAIN) n_train = n_train + 1;

      m_prev = m_state;
      @(posedge clk); #1;
      m_state = nst;

      check(fallbacks         === m_fb[31:0], "fallbacks matches the model");
      check(training_attempts === m_ta[31:0], "training_attempts matches the model");
      check(ever_fell_back    === m_ever,     "ever_fell_back matches the model");

      // ---- THE HISTORY INVARIANT, which no model supplies ----
      // FALLBACK IS ONE-WAY. A device that has fallen back to USB 2 never
      // reaches SuperSpeed again without passing through BUS_NONE -- which
      // only a reset or a VBUS loss produces.
      if (active_bus === B_SS && m_prev !== B_SS) begin
        n_enter_ss = n_enter_ss + 1;
        check(m_prev === B_TRAIN,
              "SuperSpeed was entered from somewhere other than training");
      end
      if (m_prev === B_USB2)
        check(active_bus !== B_SS,
              "a device that had fallen back reached SuperSpeed without a reset");
    end
  endtask

  task hard_reset;
    begin
      rst_n=0; vbus=0; ssrx=0; tok=0; tfail=0; ldown=0; hrst=0;
      @(posedge clk); #1; @(posedge clk); #1; rst_n=1; #1;
      m_state=B_NONE; m_fb=0; m_ta=0; m_ever=0; m_prev=B_NONE;
    end
  endtask

  // Drive to one of the four states, legitimately.
  task goto(input integer p);
    begin
      hard_reset;
      if (p == B_NONE) begin end
      else if (p == B_USB2) begin
        tick(1,0,0,0,0,0);          // VBUS, no SS partner -> USB2
      end else begin
        tick(1,1,0,0,0,0);          // VBUS + SS partner -> TRAIN
        if (p == B_SS) tick(1,1,1,0,0,0);
      end
    end
  endtask

  initial begin
    hard_reset;
    check(active_bus === B_NONE, "the arbiter comes up with no bus");
    check(!usb2_pullup, "and no pull-up, because there is no VBUS");

    // ===== A. EXHAUSTIVE ONE-STEP TRANSITIONS =====
    // 4 states x all 64 combinations of the six control inputs = 256
    // transitions: the entire one-step domain.
    for (pos=0; pos<4; pos=pos+1)
     for (ic=0; ic<64; ic=ic+1) begin
       goto(pos);
       tick(ic[0], ic[1], ic[2], ic[3], ic[4], ic[5]);
       n_trans = n_trans + 1;
     end
    $display("  exhaustive transition sweep: %0d of %0d transitions verified",
             n_trans, 4*64);

    // ===== B. EXHAUSTIVE OVER TRAINING OUTCOMES, JOINTLY =====
    // Every interleaving of "the link trained" and "the link failed" across
    // a 6-tick window: 2^6 x 2^6 = 4096 scenarios. These are the two inputs
    // whose PRECEDENCE decides whether a bad link comes up, and the whole
    // point is that failure outranks success when both arrive together.
    for (pat=0; pat<4096; pat=pat+1) begin
      hard_reset;
      tick(1,1,0,0,0,0);            // VBUS + SS partner: enter training
      for (t=0; t<W; t=t+1)
        tick(1'b1, 1'b1, pat[t], pat[t+W], 1'b0, 1'b0);
      n_pat = n_pat + 1;
    end
    $display("  exhaustive training-outcome sweep: %0d of 4096 verified",
             n_pat);

    // ===== C. directed: the three rules =====
    // SuperSpeed is tried FIRST
    hard_reset;
    tick(1,1,0,0,0,0);
    check(training, "with a SuperSpeed partner present, SuperSpeed is tried");
    check(!usb2_data_enable, "and USB 2 carries nothing meanwhile");
    check(usb2_pullup, "but the pull-up is up: a USB 2 host must still see it");
    tick(1,1,1,0,0,0);
    check(ss_data_enable, "training succeeds and SuperSpeed carries the data");
    check(!usb2_data_enable, "and USB 2 does not");

    // no SuperSpeed partner: straight to USB 2, no training attempt
    hard_reset;
    tick(1,0,0,0,0,0);
    check(usb2_data_enable, "with no SuperSpeed partner it goes straight to USB 2");
    check(training_attempts === 32'd0, "without attempting to train at all");

    // failure outranks success
    hard_reset;
    tick(1,1,0,0,0,0);
    tick(1,1,1,1,0,0);              // ok AND fail in the same cycle
    check(usb2_data_enable,
          "failure outranks success: a doubtful link is not brought up");
    check(fallbacks === 32'd1, "and the fallback is counted");

    // fallback is ONE-WAY
    hard_reset;
    tick(1,1,0,0,0,0);
    tick(1,1,0,1,0,0);
    check(usb2_data_enable, "fallen back to USB 2");
    tick(1,1,1,0,0,0);
    check(usb2_data_enable, "a later training success does NOT move it back");
    tick(1,1,1,0,0,0);
    check(usb2_data_enable, "nor does another");
    tick(1,1,0,0,0,1);              // host reset
    check(active_bus === B_NONE, "only a reset escapes");
    tick(1,1,0,0,0,0);
    check(training, "and then SuperSpeed is tried again");

    // a lost link retrains rather than falling back immediately
    hard_reset;
    tick(1,1,0,0,0,0); tick(1,1,1,0,0,0);
    check(ss_data_enable, "SuperSpeed up");
    tick(1,1,0,0,1,0);
    check(training, "a lost link RETRAINS rather than falling back at once");
    check(training_attempts === 32'd2, "which is a second attempt");

    // the pull-up is independent of everything
    hard_reset;
    tick(1,1,0,0,0,0); tick(1,1,1,0,0,0);
    check(ss_data_enable && usb2_pullup,
          "the pull-up stays up while SuperSpeed carries the data");
    tick(0,0,0,0,0,0);
    check(!usb2_pullup, "and drops only with VBUS");

    // ===== D. randomised =====
    for (i=0;i<40000;i=i+1)
      tick(({$random}%16)!=0, ({$random}%3)!=0, ({$random}%4)==0,
           ({$random}%8)==0, ({$random}%16)==0, ({$random}%32)==0);

    check(n_ss>0 && n_u2>0 && n_train>0,
          "the run reached SuperSpeed, USB 2 and training");
    check(ever_fell_back, "and exercised the fallback path");

    $display("");
    $display("  REACH: transitions=%0d interleavings=%0d | ss-ticks=%0d usb2-ticks=%0d training-ticks=%0d fallbacks=%0d ss-entries=%0d",
             n_trans, n_pat, n_ss, n_u2, n_train, fallbacks, n_enter_ss);
    $display("  [SystemVerilog] usb3_dual_bus_arbiter_sv: %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.usb3_dualbus_pkg.all;

entity tb_db_vhdl is end entity;

architecture sim of tb_db_vhdl is
  constant W : positive := 6;

  signal clk, rst_n : std_logic := '0';
  signal vbus, ssrx, tok, tfail, ldown, hrst : std_logic := '0';
  signal active_bus : active_bus_t;
  signal ss_data_enable, usb2_data_enable, usb2_pullup, training : std_logic;
  signal fallbacks, training_attempts : unsigned(31 downto 0);
  signal ever_fell_back : std_logic;
  signal done : boolean := false;
begin
  clk <= not clk after 5 ns when not done else '0';

  dut : entity work.usb3_dual_bus_arbiter_vhdl
    port map (clk, rst_n, vbus, ssrx, tok, tfail, ldown, hrst, active_bus,
              ss_data_enable, usb2_data_enable, usb2_pullup, training,
              fallbacks, training_attempts, ever_fell_back);

  stim : process
    variable errors : natural := 0;
    variable n_trans, n_pat, n_ss, n_u2, n_train, n_enter_ss : natural := 0;
    -- INDEPENDENT MODEL: its own state and counters.
    variable m_state, m_prev : active_bus_t := BUS_NONE;
    variable m_fb, m_ta : natural := 0;
    variable m_ever : boolean := false;
    variable seed1 : positive := 97; variable seed2 : positive := 41;
    variable r1, r2, r3, r4, r5, r6 : real;
    variable icv : std_logic_vector(5 downto 0);
    variable pv  : std_logic_vector(2*W-1 downto 0);

    function sl (b : boolean) return std_logic is
    begin
      if b then return '1'; else return '0'; end if;
    end function;

    procedure chk (c : boolean; m : string) is
    begin
      if not c then
        errors := errors + 1;
        if errors <= 25 then report "FAIL: " & m severity warning; end if;
      end if;
    end procedure;

    procedure tick (vb, sr, ok, fl, dn, hr : std_logic) is
      variable nst : active_bus_t;
    begin
      vbus <= vb; ssrx <= sr; tok <= ok; tfail <= fl;
      ldown <= dn; hrst <= hr;
      wait for 1 ns;

      -- ---- combinational contract ----
      chk(active_bus = m_state, "active_bus matches the model");
      chk((ss_data_enable = '1') = (m_state = BUS_SS and vb = '1'),
          "ss_data_enable decodes the state AND requires VBUS");
      chk((usb2_data_enable = '1') = (m_state = BUS_USB2 and vb = '1'),
          "usb2_data_enable decodes the state AND requires VBUS");
      chk((training = '1') = (m_state = BUS_TRAIN and vb = '1'),
          "training decodes the state AND requires VBUS");

      -- ---- SAFETY PROPERTIES, independent of the model ----
      -- 1. THE one that matters: the two data paths are NEVER both live.
      chk(not (ss_data_enable = '1' and usb2_data_enable = '1'),
          "both buses carrying data at once: the device answers twice");
      -- 2. THE EXCEPTION: presence detection is not part of the exclusion.
      chk(usb2_pullup = vb,
          "the USB 2 pull-up was gated on something other than VBUS");
      -- 3. No VBUS, no bus of either kind.
      if vb = '0' then
        chk(ss_data_enable = '0' and usb2_data_enable = '0',
            "a bus was carrying data with no VBUS");
      end if;
      -- 4. Training carries no data on either bus.
      if training = '1' then
        chk(ss_data_enable = '0' and usb2_data_enable = '0',
            "data flowed while the link was still training");
      end if;

      -- ---- advance the model ----
      nst := m_state;
      if vb = '0' then nst := BUS_NONE;
      elsif hr = '1' then nst := BUS_NONE;
      else
        case m_state is
          when BUS_NONE =>
            if sr = '1' then nst := BUS_TRAIN; m_ta := m_ta + 1;
            else nst := BUS_USB2; end if;
          when BUS_TRAIN =>
            if fl = '1' then
              nst := BUS_USB2; m_fb := m_fb + 1; m_ever := true;
            elsif ok = '1' then nst := BUS_SS; end if;
          when BUS_SS =>
            if dn = '1' then nst := BUS_TRAIN; m_ta := m_ta + 1; end if;
          when BUS_USB2 =>
            nst := BUS_USB2;
        end case;
      end if;

      if m_state = BUS_SS    then n_ss := n_ss + 1; end if;
      if m_state = BUS_USB2  then n_u2 := n_u2 + 1; end if;
      if m_state = BUS_TRAIN then n_train := n_train + 1; end if;

      m_prev := m_state;
      wait until rising_edge(clk); wait for 1 ns;
      m_state := nst;

      chk(fallbacks = to_unsigned(m_fb, 32), "fallbacks matches the model");
      chk(training_attempts = to_unsigned(m_ta, 32),
          "training_attempts matches the model");
      chk((ever_fell_back = '1') = m_ever,
          "ever_fell_back matches the model");

      -- ---- THE HISTORY INVARIANT, which no model supplies ----
      -- FALLBACK IS ONE-WAY.
      if active_bus = BUS_SS and m_prev /= BUS_SS then
        n_enter_ss := n_enter_ss + 1;
        chk(m_prev = BUS_TRAIN,
            "SuperSpeed was entered from somewhere other than training");
      end if;
      if m_prev = BUS_USB2 then
        chk(active_bus /= BUS_SS,
            "a device that had fallen back reached SuperSpeed without a reset");
      end if;
    end procedure;

    procedure hard_reset is
    begin
      rst_n <= '0'; vbus <= '0'; ssrx <= '0'; tok <= '0';
      tfail <= '0'; ldown <= '0'; hrst <= '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;
      m_state := BUS_NONE; m_prev := BUS_NONE;
      m_fb := 0; m_ta := 0; m_ever := false;
    end procedure;

    procedure goto (p : active_bus_t) is
    begin
      hard_reset;
      if p = BUS_NONE then null;
      elsif p = BUS_USB2 then tick('1','0','0','0','0','0');
      else
        tick('1','1','0','0','0','0');
        if p = BUS_SS then tick('1','1','1','0','0','0'); end if;
      end if;
    end procedure;

    type pos_arr is array (0 to 3) of active_bus_t;
    constant POSN : pos_arr := (BUS_NONE, BUS_SS, BUS_USB2, BUS_TRAIN);
  begin
    hard_reset;
    chk(active_bus = BUS_NONE, "the arbiter comes up with no bus");
    chk(usb2_pullup = '0', "and no pull-up, because there is no VBUS");

    -- ===== A. EXHAUSTIVE ONE-STEP TRANSITIONS =====
    -- 4 states x all 64 combinations of the six control inputs = 256.
    for pos in 0 to 3 loop
     for ic in 0 to 63 loop
       goto(POSN(pos));
       icv := std_logic_vector(to_unsigned(ic, 6));
       tick(icv(0), icv(1), icv(2), icv(3), icv(4), icv(5));
       n_trans := n_trans + 1;
     end loop;
    end loop;
    report "exhaustive transition sweep: " & integer'image(n_trans)
         & " of 256 transitions verified";

    -- ===== B. EXHAUSTIVE OVER TRAINING OUTCOMES, JOINTLY =====
    -- Every interleaving of "the link trained" and "the link failed" across
    -- a 6-tick window: 2^6 x 2^6 = 4096 scenarios.
    for pat in 0 to 4095 loop
      hard_reset;
      tick('1','1','0','0','0','0');
      pv := std_logic_vector(to_unsigned(pat, 2*W));
      for t in 0 to W-1 loop
        tick('1','1', pv(t), pv(t+W), '0','0');
      end loop;
      n_pat := n_pat + 1;
    end loop;
    report "exhaustive training-outcome sweep: " & integer'image(n_pat)
         & " of 4096 verified";

    -- ===== C. directed: the three rules =====
    hard_reset;
    tick('1','1','0','0','0','0');
    chk(training = '1',
        "with a SuperSpeed partner present, SuperSpeed is tried");
    chk(usb2_data_enable = '0', "and USB 2 carries nothing meanwhile");
    chk(usb2_pullup = '1',
        "but the pull-up is up: a USB 2 host must still see it");
    tick('1','1','1','0','0','0');
    chk(ss_data_enable = '1',
        "training succeeds and SuperSpeed carries the data");
    chk(usb2_data_enable = '0', "and USB 2 does not");

    hard_reset;
    tick('1','0','0','0','0','0');
    chk(usb2_data_enable = '1',
        "with no SuperSpeed partner it goes straight to USB 2");
    chk(training_attempts = to_unsigned(0, 32),
        "without attempting to train at all");

    hard_reset;
    tick('1','1','0','0','0','0');
    tick('1','1','1','1','0','0');
    chk(usb2_data_enable = '1',
        "failure outranks success: a doubtful link is not brought up");
    chk(fallbacks = to_unsigned(1, 32), "and the fallback is counted");

    hard_reset;
    tick('1','1','0','0','0','0');
    tick('1','1','0','1','0','0');
    chk(usb2_data_enable = '1', "fallen back to USB 2");
    tick('1','1','1','0','0','0');
    chk(usb2_data_enable = '1',
        "a later training success does NOT move it back");
    tick('1','1','1','0','0','0');
    chk(usb2_data_enable = '1', "nor does another");
    tick('1','1','0','0','0','1');
    chk(active_bus = BUS_NONE, "only a reset escapes");
    tick('1','1','0','0','0','0');
    chk(training = '1', "and then SuperSpeed is tried again");

    hard_reset;
    tick('1','1','0','0','0','0'); tick('1','1','1','0','0','0');
    chk(ss_data_enable = '1', "SuperSpeed up");
    tick('1','1','0','0','1','0');
    chk(training = '1',
        "a lost link RETRAINS rather than falling back at once");
    chk(training_attempts = to_unsigned(2, 32), "which is a second attempt");

    hard_reset;
    tick('1','1','0','0','0','0'); tick('1','1','1','0','0','0');
    chk(ss_data_enable = '1' and usb2_pullup = '1',
        "the pull-up stays up while SuperSpeed carries the data");
    tick('0','0','0','0','0','0');
    chk(usb2_pullup = '0', "and drops only with VBUS");

    -- ===== D. randomised =====
    for i in 1 to 40000 loop
      uniform(seed1, seed2, r1); uniform(seed1, seed2, r2);
      uniform(seed1, seed2, r3); uniform(seed1, seed2, r4);
      uniform(seed1, seed2, r5); uniform(seed1, seed2, r6);
      tick(sl(r1 >= 0.0625), sl(r2 >= 0.3333), sl(r3 < 0.25),
           sl(r4 < 0.125), sl(r5 < 0.0625), sl(r6 < 0.03125));
    end loop;

    chk(n_ss > 0 and n_u2 > 0 and n_train > 0,
        "the run reached SuperSpeed, USB 2 and training");
    chk(ever_fell_back = '1', "and exercised the fallback path");

    report "REACH: transitions=" & integer'image(n_trans)
         & " interleavings=" & integer'image(n_pat)
         & " | ss-ticks=" & integer'image(n_ss)
         & " usb2-ticks=" & integer'image(n_u2)
         & " training-ticks=" & integer'image(n_train)
         & " fallbacks=" & integer'image(to_integer(fallbacks))
         & " ss-entries=" & integer'image(n_enter_ss);
    report "[VHDL] usb3_dual_bus_arbiter_vhdl: " & integer'image(errors)
         & " errors";
    if errors = 0 then report "[VHDL] PASS";
    else report "[VHDL] FAIL" severity error; end if;
    done <= true;
    wait;
  end process;
end architecture;

nvc --std=2008 -a db_vhdl.vhd db_vhdl_tb.vhd
nvc --std=2008 -e tb_db_vhdl
nvc --std=2008 -r tb_db_vhdl

// Each host TYPE is a configuration, not a test. The USB-2-only host is the
// one that finds section 2's bug, and it is the one nobody has on the desk.
typedef enum { HOST_USB2_ONLY, HOST_USB3_GOOD, HOST_USB3_MARGINAL } host_kind_e;

class dualbus_env_cfg extends uvm_object;
  `uvm_object_utils(dualbus_env_cfg)
  rand host_kind_e host_kind;
  rand int unsigned train_fail_pct;

  constraint c_kind {
    // A marginal host fails training most of the time but not always --
    // which is what makes the one-way fallback of section 3 observable.
    host_kind == HOST_USB3_MARGINAL -> train_fail_pct inside {[40:90]};
    host_kind == HOST_USB3_GOOD     -> train_fail_pct inside {[0:5]};
    host_kind == HOST_USB2_ONLY     -> train_fail_pct == 0;
  }
endclass

// The scenario that matters most and is hardest to get on a bench: a host
// that cannot speak SuperSpeed at all. ss_rx_detect never asserts, and the
// ONLY thing that makes the device visible is the pull-up of section 2.
class usb2_only_host_seq extends uvm_sequence #(dualbus_item);
  `uvm_object_utils(usb2_only_host_seq)
  task body();
    dualbus_item it;
    `uvm_do_with(it, { vbus_present == 1; ss_rx_detect == 0; })
    repeat (32)
      `uvm_do_with(it, { vbus_present == 1; ss_rx_detect == 0;
                         ss_training_ok == 0; ss_training_fail == 0; })
  endtask
endclass

// Power removed mid-transfer -- section 11's window, generated on purpose.
class power_cut_seq extends uvm_sequence #(dualbus_item);
  `uvm_object_utils(power_cut_seq)
  task body();
    dualbus_item it;
    `uvm_do_with(it, { vbus_present == 1; ss_rx_detect == 1; })
    `uvm_do_with(it, { vbus_present == 1; ss_training_ok == 1; })
    // THE cycle. The state register still says SuperSpeed; nothing may be
    // driven onto a wire that has just lost its power.
    `uvm_do_with(it, { vbus_present == 0; })
  endtask
endclass

class dualbus_scoreboard extends uvm_scoreboard;
  `uvm_component_utils(dualbus_scoreboard)
  local active_bus_e m_prev = BUS_NONE;

  function void write(dualbus_txn t);
    // THE property. Both buses live is not a race that resolves -- both
    // replies are well formed and the host cannot tell them apart.
    if (t.ss_data_enable && t.usb2_data_enable)
      `uvm_fatal("DUALBUS/BOTH",
        "both buses carrying data: the device answers every transaction twice")

    // Section 11: nothing is driven without power.
    if (!t.vbus_present && (t.ss_data_enable || t.usb2_data_enable))
      `uvm_fatal("DUALBUS/UNPOWERED",
        "a data path was enabled with VBUS absent")

    // Section 2: the pull-up is NOT part of the exclusion. A device that
    // hides from a USB 2 host works perfectly on every USB 3 machine.
    if (t.usb2_pullup != t.vbus_present)
      `uvm_error("DUALBUS/PULLUP",
        "the pull-up was gated on something other than VBUS")

    // Section 3: fallback is one-way.
    if (m_prev == BUS_USB2 && t.active_bus == BUS_SS)
      `uvm_error("DUALBUS/ONEWAY",
        "a device that had fallen back reached SuperSpeed without a reset")

    m_prev = t.active_bus;
  endfunction
endclass

covergroup dualbus_cg with function sample(
    active_bus_e bus, bit vbus, bit ok, bit fail, host_kind_e host);
  cp_bus  : coverpoint bus;
  cp_host : coverpoint host;
  // THE bin section 2 lives in: a USB-2-only host, which no amount of
  // testing against USB 3 hosts will ever reach.
  x_host_bus : cross cp_host, cp_bus;
  // Both training outcomes in one cycle -- section 4's precedence.
  cp_collide : coverpoint {ok, fail} { bins both = {2'b11}; }
  // Power removed while a bus is live -- section 11's window.
  cp_cut : coverpoint {vbus, (bus == BUS_SS || bus == BUS_USB2)} {
    bins cut = {2'b01};
  }
endgroup

  // THE property: never both. Not a comparison -- a statement that one
  // combination is never produced, for any input.
  property p_never_both;
    @(posedge clk) disable iff (!rst_n)
      !(ss_data_enable && usb2_data_enable);
  endproperty
  a_never_both : assert property (p_never_both)
    else $fatal(1, "both buses carrying data: the device answers twice");

  // Nothing is driven without power. Section 11, mutation D7.
  property p_nothing_unpowered;
    @(posedge clk) disable iff (!rst_n)
      (!vbus_present) |-> (!ss_data_enable && !usb2_data_enable);
  endproperty
  a_nothing_unpowered : assert property (p_nothing_unpowered);

  // The pull-up is NOT part of the exclusion. Section 2, mutation D2.
  property p_pullup_follows_vbus;
    @(posedge clk) disable iff (!rst_n)
      usb2_pullup == vbus_present;
  endproperty
  a_pullup_follows_vbus : assert property (p_pullup_follows_vbus);

  // Fallback is one-way: SuperSpeed is only ever entered from training.
  property p_ss_from_training_only;
    @(posedge clk) disable iff (!rst_n)
      ($changed(active_bus) && active_bus == BUS_SS)
        |-> ($past(active_bus) == BUS_TRAIN);
  endproperty
  a_ss_from_training_only : assert property (p_ss_from_training_only)
    else $error("SuperSpeed entered from somewhere other than training");