Power Budgeting

   remaining = hdev->bus_mA - hub->descriptor->bHubContrCurrent;
   for (port1 = 1; port1 <= hdev->maxchild; ++port1) {
           if (udev->actconfig)
                   delta = usb_get_max_power(udev, udev->actconfig);
           else if (port1 != udev->bus->otg_port || hdev->parent)
                   delta = unit_load;
           else
                   delta = 8;
           if (delta > hub->mA_per_port)
                   dev_warn(... "%dmA is over %umA budget!\n", ...);
           remaining -= delta;
   }
   if (remaining < 0) {
           dev_warn(... "%dmA over power budget!\n", -remaining);
           remaining = 0;
   }

// usb_tree_power_walk -- the host's whole-tree accounting, where chapter
// 18.5's per-hub rule and chapter 19.1's per-device rule finally meet.
//
// Module 18 asked what a HUB can supply. Chapters 19.1 and 19.2 asked what a
// DEVICE may take. Neither question is the one a host actually has to answer,
// which is: given this tree, with these devices in these states, is the next
// thing anyone plugs in going to work?
//
// The host answers it by WALKING. Linux does it in a loop:
//
//     remaining = hdev->bus_mA - hub->descriptor->bHubContrCurrent;
//     for (port1 = 1; port1 <= hdev->maxchild; ++port1) {
//             ...
//             if (udev->actconfig)
//                     delta = usb_get_max_power(udev, udev->actconfig);
//             else if (port1 != udev->bus->otg_port || hdev->parent)
//                     delta = unit_load;
//             else
//                     delta = 8;
//             if (delta > hub->mA_per_port)
//                     dev_warn(... "%dmA is over %umA budget!\n", ...);
//             remaining -= delta;
//     }
//     if (remaining < 0) {
//             dev_warn(... "%dmA over power budget!\n", -remaining);
//             remaining = 0;
//     }
//
// THE TERM THAT SURPRISES PEOPLE
//
// Look at the `else` branch. A device that is present but NOT CONFIGURED is
// charged a full UNIT LOAD -- not zero, and not what its descriptor asks for.
//
// That is chapter 19.1's floor seen from the host's side. The device is
// ENTITLED to one unit load from the moment it attaches, whether it is
// drawing it or not, so the host must reserve it. A budget that charged
// unconfigured devices nothing would be reserving power it has already
// promised away, and the first device to actually use its entitlement would
// take the tree over.
//
// TWO DIFFERENT WARNINGS
//
// The loop produces two, and they are not the same condition:
//
//   PER PORT   delta > mA_per_port -- this ONE device wants more than a port
//              on this hub is offered (18.5). The hub may have plenty left.
//   WHOLE HUB  remaining < 0 -- the devices TOGETHER exceed what the hub can
//              source, though each one individually fits.
//
// A design reporting one flag for both cannot tell a user whether to move a
// device or remove one, which are the two different fixes.
//
// And `remaining` SATURATES at zero after the warning rather than going
// negative -- an unsigned budget that wrapped would report an enormous
// amount of headroom at the exact moment it had none.
module usb_tree_power_walk #(
  parameter integer NPORTS        = 4,
  parameter integer UNIT_LOAD_HS  = 100,  // one unit load, USB 2.0, mA
  parameter integer UNIT_LOAD_SS  = 150,  // one unit load, SuperSpeed, mA
  parameter integer OTG_UNCONF_MA = 8     // an unconfigured OTG port gets 8
) (
  input  wire                  clk,
  input  wire                  rst_n,

  input  wire [15:0]           bus_mA,        // what this hub may draw
  input  wire [15:0]           contr_current, // bHubContrCurrent (18.5)
  input  wire [15:0]           mA_per_port,   // what it offers a port (18.5)
  input  wire                  superspeed,

  input  wire [NPORTS-1:0]     present,
  input  wire [NPORTS-1:0]     configured,
  input  wire [NPORTS*8-1:0]   max_power_flat, // bMaxPower per port, in UNITS
  input  wire                  otg_port0,      // port 0 is a root OTG port

  output wire [15:0]           unit_load_mA,
  output reg  [NPORTS-1:0]     port_over_budget,
  output reg  [15:0]           total_charged,
  output wire [15:0]           remaining_mA,
  output wire                  tree_over_budget,
  output wire [1:0]            budget_verdict,  // the two conditions, named
  output reg  [31:0]           over_events,
  output reg                   ever_over
);
  // The unit load follows the speed, as in 19.1. A SuperSpeed tree reserves
  // more per unconfigured device because a SuperSpeed device is entitled to
  // more from the moment it attaches.
  assign unit_load_mA = superspeed ? UNIT_LOAD_SS[15:0] : UNIT_LOAD_HS[15:0];

  // What the hub has to give out at all, after its own controller. Saturating
  // (18.5): a malformed descriptor claiming more than the upstream supplies
  // must yield zero, not a wrapped enormous number.
  wire [15:0] available = (bus_mA > contr_current)
                        ? (bus_mA - contr_current) : 16'd0;

  integer i;
  reg [15:0] delta;
  reg [31:0] charged;      // 32 bits: the SUM must not wrap even if the
                           // individual deltas are all at their maximum

  always @* begin
    charged          = 32'd0;
    port_over_budget = {NPORTS{1'b0}};
    for (i = 0; i < NPORTS; i = i + 1) begin
      if (!present[i])
        // Nothing attached costs nothing. This is the only case that does.
        delta = 16'd0;
      else if (configured[i])
        // Configured: what it declared, scaled. 19.1's arithmetic.
        delta = superspeed ? ({8'd0, max_power_flat[i*8 +: 8]} << 3)
                           : ({8'd0, max_power_flat[i*8 +: 8]} << 1);
      else if (otg_port0 && i == 0)
        // The OTG exception: an unconfigured device on a root hub's OTG
        // port is charged 8 mA rather than a unit load.
        delta = OTG_UNCONF_MA[15:0];
      else
        // THE TERM. Present but unconfigured still costs a full unit load,
        // because 19.1 entitles it to one from the moment it attached.
        delta = unit_load_mA;

      // PER-PORT warning: this one device wants more than a port here is
      // offered. Independent of whether the hub has room overall.
      if (delta > mA_per_port) port_over_budget[i] = 1'b1;

      charged = charged + {16'd0, delta};
    end
    total_charged = (charged > 32'hFFFF) ? 16'hFFFF : charged[15:0];
  end

  // WHOLE-HUB condition: the devices together exceed what the hub can source.
  assign tree_over_budget = (total_charged > available);

  // Saturating, and for the same reason the subtraction above is: a budget
  // that wrapped would report enormous headroom at the moment it had none.
  assign remaining_mA = tree_over_budget ? 16'd0 : (available - total_charged);

  // The two conditions as one named verdict. They are INDEPENDENT -- either,
  // neither, or both -- and a reader seeing BUDGET_PORT_OVER knows to move a
  // device, where BUDGET_TREE_OVER means remove one. Verilog-2005 has no
  // enumerated type, so the encoding is localparams; chapters 19.2 and 19.3
  // both measured what happens when one language exposes less than the rest.
  localparam [1:0] BUDGET_OK        = 2'd0,
                   BUDGET_PORT_OVER = 2'd1,   // one device wants too much
                   BUDGET_TREE_OVER = 2'd2,   // the devices TOGETHER do
                   BUDGET_BOTH      = 2'd3;
  assign budget_verdict =
      ( tree_over_budget &&  (port_over_budget != {NPORTS{1'b0}})) ? BUDGET_BOTH
    : ( tree_over_budget)                                          ? BUDGET_TREE_OVER
    : ((port_over_budget != {NPORTS{1'b0}}))                       ? BUDGET_PORT_OVER
    :                                                                BUDGET_OK;

  always @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      over_events <= 32'd0;
      ever_over   <= 1'b0;
    end else if (tree_over_budget || (port_over_budget != {NPORTS{1'b0}})) begin
      over_events <= over_events + 32'd1;
      ever_over   <= 1'b1;
    end
  end
endmodule

package usb_budget_pkg;
  // The two over-budget conditions, named. They are INDEPENDENT -- either,
  // neither, or both -- and the distinction is the difference between two
  // pieces of advice: BUDGET_PORT_OVER means move a device to a hub that
  // offers more per port; BUDGET_TREE_OVER means remove one.
  typedef enum logic [1:0] {
    BUDGET_OK,
    BUDGET_PORT_OVER,   // one device wants more than a port here offers
    BUDGET_TREE_OVER,   // the devices TOGETHER exceed the hub
    BUDGET_BOTH
  } budget_verdict_e;
endpackage

// usb_tree_power_walk_sv -- the host's whole-tree accounting, where chapter
// 18.5's per-hub rule and chapter 19.1's per-device rule finally meet.
//
// Module 18 asked what a HUB can supply. Chapters 19.1 and 19.2 asked what a
// DEVICE may take. Neither question is the one a host actually has to answer,
// which is: given this tree, with these devices in these states, is the next
// thing anyone plugs in going to work?
//
// The host answers it by WALKING. Linux does it in a loop:
//
//     remaining = hdev->bus_mA - hub->descriptor->bHubContrCurrent;
//     for (port1 = 1; port1 <= hdev->maxchild; ++port1) {
//             ...
//             if (udev->actconfig)
//                     delta = usb_get_max_power(udev, udev->actconfig);
//             else if (port1 != udev->bus->otg_port || hdev->parent)
//                     delta = unit_load;
//             else
//                     delta = 8;
//             if (delta > hub->mA_per_port)
//                     dev_warn(... "%dmA is over %umA budget!\n", ...);
//             remaining -= delta;
//     }
//     if (remaining < 0) {
//             dev_warn(... "%dmA over power budget!\n", -remaining);
//             remaining = 0;
//     }
//
// THE TERM THAT SURPRISES PEOPLE
//
// Look at the `else` branch. A device that is present but NOT CONFIGURED is
// charged a full UNIT LOAD -- not zero, and not what its descriptor asks for.
//
// That is chapter 19.1's floor seen from the host's side. The device is
// ENTITLED to one unit load from the moment it attaches, whether it is
// drawing it or not, so the host must reserve it. A budget that charged
// unconfigured devices nothing would be reserving power it has already
// promised away, and the first device to actually use its entitlement would
// take the tree over.
//
// TWO DIFFERENT WARNINGS
//
// The loop produces two, and they are not the same condition:
//
//   PER PORT   delta > mA_per_port -- this ONE device wants more than a port
//              on this hub is offered (18.5). The hub may have plenty left.
//   WHOLE HUB  remaining < 0 -- the devices TOGETHER exceed what the hub can
//              source, though each one individually fits.
//
// A design reporting one flag for both cannot tell a user whether to move a
// device or remove one, which are the two different fixes.
//
// And `remaining` SATURATES at zero after the warning rather than going
// negative -- an unsigned budget that wrapped would report an enormous
// amount of headroom at the exact moment it had none.
module usb_tree_power_walk_sv
  import usb_budget_pkg::*;
#(
  parameter int unsigned NPORTS        = 4,
  parameter int unsigned UNIT_LOAD_HS  = 100,  // one unit load, USB 2.0, mA
  parameter int unsigned UNIT_LOAD_SS  = 150,  // one unit load, SuperSpeed
  parameter int unsigned OTG_UNCONF_MA = 8     // an unconfigured OTG port
) (
  input  logic                 clk,
  input  logic                 rst_n,

  input  logic [15:0]          bus_mA,        // what this hub may draw
  input  logic [15:0]          contr_current, // bHubContrCurrent (18.5)
  input  logic [15:0]          mA_per_port,   // what it offers a port (18.5)
  input  logic                 superspeed,

  input  logic [NPORTS-1:0]    present,
  input  logic [NPORTS-1:0]    configured,
  input  logic [NPORTS*8-1:0]  max_power_flat, // bMaxPower per port, in UNITS
  input  logic                 otg_port0,      // port 0 is a root OTG port

  output logic [15:0]          unit_load_mA,
  output logic [NPORTS-1:0]    port_over_budget,
  output logic [15:0]          total_charged,
  output logic [15:0]          remaining_mA,
  output logic                 tree_over_budget,
  output budget_verdict_e      budget_verdict,
  output logic [31:0]          over_events,
  output logic                 ever_over
);
  // The unit load follows the speed, as in 19.1. A SuperSpeed tree reserves
  // more per unconfigured device because a SuperSpeed device is entitled to
  // more from the moment it attaches.
  assign unit_load_mA = superspeed ? 16'(UNIT_LOAD_SS) : 16'(UNIT_LOAD_HS);

  // What the hub has to give out at all, after its own controller. Saturating
  // (18.5): a malformed descriptor claiming more than the upstream supplies
  // must yield zero, not a wrapped enormous number.
  wire [15:0] available = (bus_mA > contr_current)
                        ? (bus_mA - contr_current) : 16'd0;

  initial begin
    if (UNIT_LOAD_HS < 1 || UNIT_LOAD_SS < 1)
      $fatal(1, "a unit load of zero reserves nothing for an attached device");
  end

  logic [15:0] delta;
  logic [31:0] charged;      // 32 bits: the SUM must not wrap even if the
                           // individual deltas are all at their maximum

  always_comb begin
    charged          = 32'd0;
    port_over_budget = '0;
    for (int i = 0; i < int'(NPORTS); i++) begin
      if (!present[i])
        // Nothing attached costs nothing. This is the only case that does.
        delta = 16'd0;
      else if (configured[i])
        // Configured: what it declared, scaled. 19.1's arithmetic.
        delta = superspeed ? ({8'd0, max_power_flat[i*8 +: 8]} << 3)
                           : ({8'd0, max_power_flat[i*8 +: 8]} << 1);
      else if (otg_port0 && i == 0)
        // The OTG exception: an unconfigured device on a root hub's OTG
        // port is charged 8 mA rather than a unit load.
        delta = 16'(OTG_UNCONF_MA);
      else
        // THE TERM. Present but unconfigured still costs a full unit load,
        // because 19.1 entitles it to one from the moment it attached.
        delta = unit_load_mA;

      // PER-PORT warning: this one device wants more than a port here is
      // offered. Independent of whether the hub has room overall.
      if (delta > mA_per_port) port_over_budget[i] = 1'b1;

      charged = charged + {16'd0, delta};
    end
  end
  // Continuous, so the 32-bit accumulator is narrowed in one place and the
  // process contains no part-select.
  assign total_charged = (charged > 32'hFFFF) ? 16'hFFFF : charged[15:0];

  // WHOLE-HUB condition: the devices together exceed what the hub can source.
  assign tree_over_budget = (total_charged > available);

  // Saturating, and for the same reason the subtraction above is: a budget
  // that wrapped would report enormous headroom at the moment it had none.
  assign remaining_mA = tree_over_budget ? 16'd0 : (available - total_charged);

  // The two conditions as one named verdict. They are INDEPENDENT -- either,
  // neither, or both -- and a reader seeing BUDGET_PORT_OVER knows to move a
  // device, where BUDGET_TREE_OVER means remove one.
  always_comb begin
    if      (tree_over_budget && port_over_budget != '0) budget_verdict = BUDGET_BOTH;
    else if (tree_over_budget)                           budget_verdict = BUDGET_TREE_OVER;
    else if (port_over_budget != '0)                     budget_verdict = BUDGET_PORT_OVER;
    else                                                 budget_verdict = BUDGET_OK;
  end

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      over_events <= '0;
      ever_over   <= 1'b0;
    end else if (tree_over_budget || port_over_budget != '0) begin
      over_events <= over_events + 1;
      ever_over   <= 1'b1;
    end
  end
endmodule

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

package usb_budget_pkg is
  -- The two over-budget conditions, named. They are INDEPENDENT -- either,
  -- neither, or both -- and the distinction is the difference between two
  -- pieces of advice: BUDGET_PORT_OVER means move a device to a hub that
  -- offers more per port; BUDGET_TREE_OVER means remove one.
  type budget_verdict_t is (
    BUDGET_OK,
    BUDGET_PORT_OVER,   -- one device wants more than a port here offers
    BUDGET_TREE_OVER,   -- the devices TOGETHER exceed the hub
    BUDGET_BOTH
  );

  -- An UNCONSTRAINED array of per-port bMaxPower values, in UNITS. The
  -- Verilog and SystemVerilog flatten this into one wide vector and slice
  -- it back out; here the port is what it actually is (chapter 18.5).
  type mp_array_t is array (natural range <>) of unsigned(7 downto 0);
end package;

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

-- usb_tree_power_walk_vhdl -- the host's whole-tree accounting, where chapter
-- 18.5's per-hub rule and chapter 19.1's per-device rule finally meet.
--
-- Module 18 asked what a HUB can supply. Chapters 19.1 and 19.2 asked what a
-- DEVICE may take. Neither is the question a host actually has to answer,
-- which is: given this tree, with these devices in these states, is the next
-- thing anyone plugs in going to work?
--
-- The host answers it by WALKING. Linux does it in a loop:
--
--     remaining = hdev->bus_mA - hub->descriptor->bHubContrCurrent;
--     for (port1 = 1; port1 <= hdev->maxchild; ++port1) {
--             if (udev->actconfig)
--                     delta = usb_get_max_power(udev, udev->actconfig);
--             else if (port1 != udev->bus->otg_port || hdev->parent)
--                     delta = unit_load;
--             else
--                     delta = 8;
--             if (delta > hub->mA_per_port)
--                     dev_warn(... "%dmA is over %umA budget!\n", ...);
--             remaining -= delta;
--     }
--     if (remaining < 0) {
--             dev_warn(... "%dmA over power budget!\n", -remaining);
--             remaining = 0;
--     }
--
-- THE TERM THAT SURPRISES PEOPLE
--
-- Look at the `else` branch. A device that is present but NOT CONFIGURED is
-- charged a full UNIT LOAD -- not zero, and not what its descriptor asks for.
--
-- That is chapter 19.1's floor seen from the host's side. The device is
-- ENTITLED to one unit load from the moment it attaches, whether it is
-- drawing it or not, so the host must reserve it.
--
-- TWO DIFFERENT WARNINGS
--
--   PER PORT   delta > mA_per_port -- this ONE device wants more than a port
--              on this hub is offered (18.5). The hub may have plenty left.
--   WHOLE HUB  remaining < 0 -- the devices TOGETHER exceed what the hub can
--              source, though each one individually fits.
entity usb_tree_power_walk_vhdl is
  generic (
    NPORTS        : positive := 4;
    UNIT_LOAD_HS  : positive := 100;  -- one unit load, USB 2.0, mA
    UNIT_LOAD_SS  : positive := 150;  -- one unit load, SuperSpeed, mA
    OTG_UNCONF_MA : positive := 8     -- an unconfigured OTG port gets 8
  );
  port (
    clk              : in  std_logic;
    rst_n            : in  std_logic;

    bus_mA           : in  unsigned(15 downto 0);
    contr_current    : in  unsigned(15 downto 0);
    mA_per_port      : in  unsigned(15 downto 0);
    superspeed       : in  std_logic;

    present          : in  std_logic_vector(NPORTS-1 downto 0);
    configured       : in  std_logic_vector(NPORTS-1 downto 0);
    max_power        : in  mp_array_t(0 to NPORTS-1);
    otg_port0        : in  std_logic;

    unit_load_mA     : out unsigned(15 downto 0);
    port_over_budget : out std_logic_vector(NPORTS-1 downto 0);
    total_charged    : out unsigned(15 downto 0);
    remaining_mA     : out unsigned(15 downto 0);
    tree_over_budget : out std_logic;
    budget_verdict   : out budget_verdict_t;
    over_events      : out unsigned(31 downto 0);
    ever_over        : out std_logic
  );
end entity;

architecture rtl of usb_tree_power_walk_vhdl is
  constant ZERO : std_logic_vector(NPORTS-1 downto 0) := (others => '0');

  signal ul_i     : unsigned(15 downto 0);
  signal avail_i  : unsigned(15 downto 0);
  signal chg_i    : unsigned(15 downto 0);
  signal pob_i    : std_logic_vector(NPORTS-1 downto 0);
  signal tob_i    : std_logic;
  signal evt_r    : unsigned(31 downto 0) := (others => '0');
  signal ever_r   : std_logic := '0';
begin
  -- The unit load follows the speed, as in 19.1. A SuperSpeed tree reserves
  -- more per unconfigured device because a SuperSpeed device is entitled to
  -- more from the moment it attaches.
  ul_i <= to_unsigned(UNIT_LOAD_SS, 16) when superspeed = '1'
          else to_unsigned(UNIT_LOAD_HS, 16);

  -- What the hub has to give out at all, after its own controller.
  -- Saturating (18.5): a malformed descriptor claiming more than the
  -- upstream supplies must yield zero, not a wrapped enormous number.
  avail_i <= (bus_mA - contr_current) when bus_mA > contr_current
             else to_unsigned(0, 16);

  process (present, configured, max_power, otg_port0, ul_i, mA_per_port,
           superspeed)
    variable delta   : unsigned(15 downto 0);
    variable charged : unsigned(31 downto 0);
    variable pob     : std_logic_vector(NPORTS-1 downto 0);
  begin
    charged := (others => '0');
    pob     := (others => '0');
    for i in 0 to NPORTS-1 loop
      if present(i) = '0' then
        -- Nothing attached costs nothing. This is the only case that does.
        delta := to_unsigned(0, 16);
      elsif configured(i) = '1' then
        -- Configured: what it declared, scaled. 19.1's arithmetic.
        if superspeed = '1' then
          delta := shift_left(resize(max_power(i), 16), 3);
        else
          delta := shift_left(resize(max_power(i), 16), 1);
        end if;
      elsif otg_port0 = '1' and i = 0 then
        -- The OTG exception: an unconfigured device on a root hub's OTG
        -- port is charged 8 mA rather than a unit load.
        delta := to_unsigned(OTG_UNCONF_MA, 16);
      else
        -- THE TERM. Present but unconfigured still costs a full unit load,
        -- because 19.1 entitles it to one from the moment it attached.
        delta := ul_i;
      end if;

      -- PER-PORT warning: this one device wants more than a port here is
      -- offered. Independent of whether the hub has room overall.
      if delta > mA_per_port then pob(i) := '1'; end if;

      charged := charged + resize(delta, 32);
    end loop;
    pob_i <= pob;
    if charged > 65535 then chg_i <= to_unsigned(65535, 16);
    else chg_i <= charged(15 downto 0); end if;
  end process;

  -- WHOLE-HUB condition: the devices together exceed what the hub can source.
  tob_i <= '1' when chg_i > avail_i else '0';

  unit_load_mA     <= ul_i;
  port_over_budget <= pob_i;
  total_charged    <= chg_i;
  tree_over_budget <= tob_i;
  over_events      <= evt_r;
  ever_over        <= ever_r;

  -- Saturating, and for the same reason the subtraction above is: a budget
  -- that wrapped would report enormous headroom at the moment it had none.
  remaining_mA <= to_unsigned(0, 16) when tob_i = '1'
                  else (avail_i - chg_i);

  -- The two conditions as one named verdict. They are INDEPENDENT -- either,
  -- neither, or both -- and a reader seeing BUDGET_PORT_OVER knows to move a
  -- device, where BUDGET_TREE_OVER means remove one.
  budget_verdict <= BUDGET_BOTH      when (tob_i = '1' and pob_i /= ZERO) else
                    BUDGET_TREE_OVER when tob_i = '1'                     else
                    BUDGET_PORT_OVER when pob_i /= ZERO                   else
                    BUDGET_OK;

  process (clk, rst_n)
  begin
    if rst_n = '0' then
      evt_r <= (others => '0'); ever_r <= '0';
    elsif rising_edge(clk) then
      if tob_i = '1' or pob_i /= ZERO then
        evt_r  <= evt_r + 1;
        ever_r <= '1';
      end if;
    end if;
  end process;
end architecture;

    // The OTG dimension is swept rather than held at zero: an earlier
    // version fixed it, and mutation T5 -- the OTG exception applied to
    // every port instead of port 0 -- was then reachable only from the
    // randomised phase. A dimension held constant is a dimension untested.
    for (s=0; s<2; s=s+1)
     for (cfgi=0; cfgi<256; cfgi=cfgi+1)
      for (b=0; b<8; b=b+1)
       for (o=0; o<2; o=o+1) begin

      // ---- SAFETY PROPERTIES, independent of the model ----
      // 1. THE one that matters: remaining is never more than available.
      //    A budget reporting headroom it does not have is worse than one
      //    reporting none.
      check(remaining_mA <= e_avail[15:0],
            "the budget reported more headroom than the hub can source");
      // 2. remaining and over_budget never both say the tree is fine.
      check(!tree_over_budget || remaining_mA === 16'd0,
            "an over-budget tree still reported headroom");
      // 3. A port with nothing attached is never flagged.
      check((port_over_budget & ~present) === {N{1'b0}},
            "an empty port was flagged as over budget");

  exhaustive tree sweep: 8192 of 8192 trees verified

  Verilog / SystemVerilog:
  REACH: trees=8192 tree-over=17812 port-over=17445
         budget-exactly-spent=606 with-unconfigured=5600
  [Verilog] usb_tree_power_walk: 0 errors — PASS

  VHDL:
  REACH: trees=8192 tree-over=17802 port-over=17417
         budget-exactly-spent=628 with-unconfigured=5600
  [VHDL] usb_tree_power_walk_vhdl: 0 errors — PASS

class tree_item extends uvm_sequence_item;
  `uvm_object_utils(tree_item)
  rand bit [3:0]  present;
  rand bit [3:0]  configured;
  rand bit [7:0]  max_power [4];
  rand bit [15:0] bus_mA, contr_current, mA_per_port;
  rand bit        superspeed, otg_port0;

  // A device cannot be configured without being present. Without this the
  // solver spends most of its time on trees that cannot exist.
  constraint c_sane { (configured & ~present) == 0; }

  // Requests come from the alphabet real descriptors contain, not uniformly
  // over 8 bits.
  constraint c_realistic {
    foreach (max_power[i]) max_power[i] inside {0, 25, 50, 100, 250};
    mA_per_port inside {100, 150, 500, 900};
  }

  // THE constraint: make the total land exactly ON the budget. Section 9
  // reached that 606 times out of 8192 by luck; this reaches it on demand,
  // and it is the only place an inclusive bound can be distinguished from
  // an exclusive one.
  constraint c_on_boundary {
    solve present, configured, max_power before bus_mA, contr_current;
    (bus_mA - contr_current) == charged_total();
  }

  function int unsigned charged_total();
    int unsigned t = 0;
    foreach (present[i])
      if (present[i])
        t += configured[i] ? max_power[i] * (superspeed ? 8 : 2)
                           : (superspeed ? 150 : 100);
    return t;
  endfunction
endclass

class budget_scoreboard extends uvm_scoreboard;
  `uvm_component_utils(budget_scoreboard)

  function void write(budget_txn t);
    int unsigned avail = (t.bus_mA > t.contr_current)
                       ? t.bus_mA - t.contr_current : 0;
    int unsigned charged = 0;
    int unsigned unit_load = t.superspeed ? 150 : 100;

    foreach (t.present[i])
      if (!t.present[i])          charged += 0;
      else if (t.configured[i])   charged += t.max_power[i]
                                             * (t.superspeed ? 8 : 2);
      else if (t.otg_port0 && i == 0) charged += 8;
      else                        charged += unit_load;   // SECTION 2

    // THE property: never report headroom the hub does not have. Its
    // violation causes the host to admit the NEXT device too, which is how
    // one accounting error becomes a brown-out.
    if (t.remaining_mA > avail)
      `uvm_error("BUDGET/PHANTOM", $sformatf(
        "reported %0d mA of headroom from a %0d mA budget",
        t.remaining_mA, avail))

    // The two verdicts stay independent.
    if (t.tree_over_budget != (charged > avail))
      `uvm_error("BUDGET/TREE", "whole-hub verdict disagrees with the sum")
  endfunction
endclass

covergroup budget_cg with function sample(
    int unsigned charged, int unsigned avail, bit port_over, bit tree_over,
    int unsigned n_unconfigured);
  // The relationship between what is charged and what is available. The
  // `exactly` bin is the one that distinguishes an inclusive bound.
  cp_fit : coverpoint (charged == avail ? 0 : charged < avail ? 1 : 2) {
    bins exactly = {0};
    bins fits    = {1};
    bins over    = {2};
  }
  // Section 3's independence, as a cross. All FOUR cells must be reached:
  // a run that never hits port-over-without-tree-over has not shown the
  // two conditions are separate, it has only assumed it.
  x_independence : cross
    coverpoint port_over { bins no = {0}; bins yes = {1}; },
    coverpoint tree_over { bins no = {0}; bins yes = {1}; };
  // Section 2's term: trees containing unconfigured devices.
  cp_unconf : coverpoint n_unconfigured { bins none = {0}; bins some = {[1:4]}; }
endgroup

  // THE property: never report headroom the hub does not have.
  property p_no_phantom_headroom;
    @(posedge clk) disable iff (!rst_n)
      remaining_mA <= ((bus_mA > contr_current)
                       ? (bus_mA - contr_current) : 16'd0);
  endproperty
  a_no_phantom_headroom : assert property (p_no_phantom_headroom)
    else $error("the budget reported headroom the hub cannot source");

  // An over-budget tree reports no headroom at all. Mutation T3.
  property p_over_means_zero;
    @(posedge clk) disable iff (!rst_n)
      tree_over_budget |-> (remaining_mA == '0);
  endproperty
  a_over_means_zero : assert property (p_over_means_zero);

  // An empty port is never charged and never flagged.
  property p_absent_costs_nothing;
    @(posedge clk) disable iff (!rst_n)
      (port_over_budget & ~present) == '0;
  endproperty
  a_absent_costs_nothing : assert property (p_absent_costs_nothing);

  // The two verdicts are independent: neither implies the other. Stated as
  // the absence of an implication, which is what mutation T2 introduces.
  property p_verdicts_independent;
    @(posedge clk) disable iff (!rst_n)
      (budget_verdict == BUDGET_PORT_OVER) |-> !tree_over_budget;
  endproperty
  a_verdicts_independent : assert property (p_verdicts_independent);