Self Power

   /* from config descriptor bmAttributes */
   #define USB_CONFIG_ATT_ONE        (1 << 7)   /* must be set */
   #define USB_CONFIG_ATT_SELFPOWER  (1 << 6)   /* self powered */
   #define USB_CONFIG_ATT_WAKEUP     (1 << 5)   /* can wakeup */
   #define USB_CONFIG_ATT_BATTERY    (1 << 4)   /* battery powered */

// usb_selfpower_control -- a device that supplies itself, and what it still
// owes the bus.
//
// Chapter 19.1 built a device that takes its power from VBUS. Many devices
// do not: a printer, a powered hub, a desktop drive. They declare themselves
// SELF-POWERED with a bit in the configuration descriptor's bmAttributes,
// and the host's budget arithmetic (19.6) then skips them.
//
// The interesting question is what such a device still owes the bus, and the
// answer is: IT MUST KEEP WATCHING VBUS.
//
// THE FAILURE THIS MODULE EXISTS TO PREVENT
//
// A device signals its presence by pulling D+ (or D-) up to its own 3.3 V
// through a resistor. A BUS-powered device physically cannot do this with
// VBUS absent -- it has no power. A SELF-powered device can, and if it does,
// current flows out of the device, through the pull-up, down the data line,
// and into a host that has DELIBERATELY removed power.
//
// The consequences are all bad and none of them are obvious:
//
//   * the host sees a device attached to a port it has powered off, so its
//     model of the bus is wrong;
//   * the host cannot complete a power-cycle of that port, because the port
//     never actually goes quiet;
//   * current flows into a rail that is supposed to be dead, which can hold
//     up a supply rail the host was trying to bring down, and on a laptop
//     can keep a controller partly alive across a sleep transition.
//
// This is "back-powering", and the fix is one gate: the pull-up is driven
// ONLY when VBUS is present, whatever the device's own logic wants.
//
// The second rule worth stating: SELF-POWERED IS NOT A CONSTANT. A device
// with both supplies is self-powered while its own supply is up and bus-
// powered when it is not, and GetStatus reports the state it is in NOW --
// not the claim its descriptor makes. Linux reads that bit from the device
// rather than from the descriptor for exactly this reason.
module usb_selfpower_control #(
  parameter integer UNIT_LOAD_MA = 100  // what the bus grants before config
) (
  input  wire        clk,
  input  wire        rst_n,

  input  wire        vbus_present,
  input  wire        local_power_good,   // the device's OWN supply is up
  input  wire        cfg_self_powered,   // bmAttributes bit 6, the CLAIM
  input  wire        cfg_remote_wakeup,  // bmAttributes bit 5
  input  wire [7:0]  b_max_power,        // units of 2 mA drawn FROM THE BUS
  input  wire        pullup_request,     // the device's logic wants to attach

  output wire        pullup_enable,      // what actually drives the resistor
  output wire        status_self_powered,// GetStatus bit 0 -- the state NOW
  output wire        status_remote_wakeup,
  output wire [7:0]  bm_attributes,      // the descriptor byte, assembled
  output wire [15:0] bus_draw_mA,        // what it takes from VBUS
  output wire        operational,        // the device can actually function
  output wire [1:0]  power_source,       // where the current comes from NOW

  output wire        guard_blocked,      // the guard is blocking RIGHT NOW
  output reg  [31:0] blocked_count,      // how often it has had to
  output reg         ever_blocked
);
  // THE GUARD. One AND gate, and the entire point of the module: the device
  // may want to attach, but with no VBUS there is nothing to attach TO, and
  // driving the pull-up would push current into the host.
  assign pullup_enable = pullup_request && vbus_present;

  // Live, not dead: this asserts whenever the device's own logic asked for
  // the pull-up and the guard refused. A design where this can never fire
  // would be a design where the guard does nothing, and the testbench needs
  // to prove the guard was actually exercised rather than assume it.
  assign guard_blocked = pullup_request && !vbus_present;

  // GetStatus reports the state the device is in NOW. A dual-powered device
  // that has lost its own supply and is running from the bus reports zero
  // here even though its descriptor claims self-powered -- and the host
  // needs that, because it changes whether the device counts against the
  // port's budget.
  assign status_self_powered  = cfg_self_powered && local_power_good;
  assign status_remote_wakeup = cfg_remote_wakeup;

  // bmAttributes, assembled. Bit 7 is reserved and MUST be set -- Linux
  // names it USB_CONFIG_ATT_ONE. It carries no information; it is a legacy
  // constant, and a descriptor with it clear is malformed.
  assign bm_attributes = {1'b1,                 // bit 7: must be one
                          cfg_self_powered,     // bit 6
                          cfg_remote_wakeup,    // bit 5
                          5'b00000};

  // What the device takes FROM THE BUS -- which is not what it consumes.
  // A self-powered device running on its own supply draws only what
  // bMaxPower declares, and a well-behaved one declares nearly nothing.
  // Running on bus power instead, it is a bus-powered device and is held
  // to chapter 19.1's one-unit-load floor until it is configured.
  assign bus_draw_mA = !vbus_present        ? 16'd0
                     : status_self_powered  ? ({8'd0, b_max_power} << 1)
                                            : UNIT_LOAD_MA[15:0];

  // The same facts as a named source. Verilog-2005 has no enumerated type,
  // so the encoding is stated as localparams -- which is the nearest thing
  // available and still better than leaving a reader to reconstruct the
  // source from two separate bits.
  localparam [1:0] SRC_NONE = 2'd0,   // no VBUS and no local supply
                   SRC_BUS  = 2'd1,   // drawing from VBUS (19.1's floor)
                   SRC_SELF = 2'd2;   // running on its own supply
  assign power_source = status_self_powered ? SRC_SELF
                      : vbus_present        ? SRC_BUS
                                            : SRC_NONE;

  // A device is operational when it has power from SOMEWHERE and a bus to
  // talk on. Note both terms: its own supply is not enough, because with no
  // VBUS there is no host to talk to.
  assign operational = vbus_present && (local_power_good || !cfg_self_powered);

  always @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      blocked_count <= 32'd0;
      ever_blocked  <= 1'b0;
    end else if (guard_blocked) begin
      blocked_count <= blocked_count + 32'd1;
      ever_blocked  <= 1'b1;
    end
  end
endmodule

package usb_selfpower_pkg;
  // Where the device's current is ACTUALLY coming from this instant, which
  // is not the same as what its descriptor claims. A dual-powered device
  // moves between SRC_SELF and SRC_BUS without its descriptor changing, and
  // GetStatus reports this, not the claim.
  typedef enum logic [1:0] {
    SRC_NONE,   // no VBUS and no local supply: the device is off
    SRC_BUS,    // drawing from VBUS -- subject to 19.1's unit-load floor
    SRC_SELF    // running on its own supply
  } power_source_e;
endpackage

// usb_selfpower_control_sv -- a device that supplies itself, and what it still
// owes the bus.
//
// Chapter 19.1 built a device that takes its power from VBUS. Many devices
// do not: a printer, a powered hub, a desktop drive. They declare themselves
// SELF-POWERED with a bit in the configuration descriptor's bmAttributes,
// and the host's budget arithmetic (19.6) then skips them.
//
// The interesting question is what such a device still owes the bus, and the
// answer is: IT MUST KEEP WATCHING VBUS.
//
// THE FAILURE THIS MODULE EXISTS TO PREVENT
//
// A device signals its presence by pulling D+ (or D-) up to its own 3.3 V
// through a resistor. A BUS-powered device physically cannot do this with
// VBUS absent -- it has no power. A SELF-powered device can, and if it does,
// current flows out of the device, through the pull-up, down the data line,
// and into a host that has DELIBERATELY removed power.
//
// The consequences are all bad and none of them are obvious:
//
//   * the host sees a device attached to a port it has powered off, so its
//     model of the bus is wrong;
//   * the host cannot complete a power-cycle of that port, because the port
//     never actually goes quiet;
//   * current flows into a rail that is supposed to be dead, which can hold
//     up a supply rail the host was trying to bring down, and on a laptop
//     can keep a controller partly alive across a sleep transition.
//
// This is "back-powering", and the fix is one gate: the pull-up is driven
// ONLY when VBUS is present, whatever the device's own logic wants.
//
// The second rule worth stating: SELF-POWERED IS NOT A CONSTANT. A device
// with both supplies is self-powered while its own supply is up and bus-
// powered when it is not, and GetStatus reports the state it is in NOW --
// not the claim its descriptor makes. Linux reads that bit from the device
// rather than from the descriptor for exactly this reason.
module usb_selfpower_control_sv
  import usb_selfpower_pkg::*;
#(
  parameter int unsigned UNIT_LOAD_MA = 100  // what the bus grants before config
) (
  input  logic       clk,
  input  logic       rst_n,

  input  logic       vbus_present,
  input  logic       local_power_good,   // the device's OWN supply is up
  input  logic       cfg_self_powered,   // bmAttributes bit 6, the CLAIM
  input  logic       cfg_remote_wakeup,  // bmAttributes bit 5
  input  logic [7:0] b_max_power,        // units of 2 mA drawn FROM THE BUS
  input  logic       pullup_request,     // the device's logic wants to attach

  output logic        pullup_enable,      // what actually drives the resistor
  output logic        status_self_powered,// GetStatus bit 0 -- the state NOW
  output logic        status_remote_wakeup,
  output logic [7:0]  bm_attributes,      // the descriptor byte, assembled
  output logic [15:0] bus_draw_mA,        // what it takes from VBUS
  output logic        operational,        // the device can actually function
  output power_source_e power_source,     // where the current comes from NOW

  output logic        guard_blocked,      // the guard is blocking RIGHT NOW
  output logic [31:0] blocked_count,      // how often it has had to
  output logic        ever_blocked
);
  // THE GUARD. One AND gate, and the entire point of the module: the device
  // may want to attach, but with no VBUS there is nothing to attach TO, and
  // driving the pull-up would push current into the host.
  assign pullup_enable = pullup_request && vbus_present;

  // Live, not dead: this asserts whenever the device's own logic asked for
  // the pull-up and the guard refused. A design where this can never fire
  // would be a design where the guard does nothing, and the testbench needs
  // to prove the guard was actually exercised rather than assume it.
  assign guard_blocked = pullup_request && !vbus_present;

  // GetStatus reports the state the device is in NOW. A dual-powered device
  // that has lost its own supply and is running from the bus reports zero
  // here even though its descriptor claims self-powered -- and the host
  // needs that, because it changes whether the device counts against the
  // port's budget.
  assign status_self_powered  = cfg_self_powered && local_power_good;
  assign status_remote_wakeup = cfg_remote_wakeup;

  // bmAttributes, assembled. Bit 7 is reserved and MUST be set -- Linux
  // names it USB_CONFIG_ATT_ONE. It carries no information; it is a legacy
  // constant, and a descriptor with it clear is malformed.
  assign bm_attributes = {1'b1,                 // bit 7: must be one
                          cfg_self_powered,     // bit 6
                          cfg_remote_wakeup,    // bit 5
                          5'b00000};

  // What the device takes FROM THE BUS -- which is not what it consumes.
  // A self-powered device running on its own supply draws only what
  // bMaxPower declares, and a well-behaved one declares nearly nothing.
  // Running on bus power instead, it is a bus-powered device and is held
  // to chapter 19.1's one-unit-load floor until it is configured.
  assign bus_draw_mA = !vbus_present        ? 16'd0
                     : status_self_powered  ? (16'(b_max_power) << 1)
                                            : 16'(UNIT_LOAD_MA);

  // The same facts as a named source. A reader of a waveform can see
  // SRC_SELF become SRC_BUS at the instant a local supply fails; two
  // separate bits require them to reconstruct it.
  always_comb begin
    if      (status_self_powered) power_source = SRC_SELF;
    else if (vbus_present)        power_source = SRC_BUS;
    else                          power_source = SRC_NONE;
  end

  // A device is operational when it has power from SOMEWHERE and a bus to
  // talk on. Note both terms: its own supply is not enough, because with no
  // VBUS there is no host to talk to.
  assign operational = vbus_present && (local_power_good || !cfg_self_powered);

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      blocked_count <= '0;
      ever_blocked  <= 1'b0;
    end else if (guard_blocked) begin
      blocked_count <= blocked_count + 1;
      ever_blocked  <= 1'b1;
    end
  end
endmodule

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

package usb_selfpower_pkg is
  -- Where the device's current is ACTUALLY coming from this instant, which
  -- is not the same as what its descriptor claims. A dual-powered device
  -- moves between SRC_SELF and SRC_BUS without its descriptor changing, and
  -- GetStatus reports this, not the claim.
  type power_source_t is (
    SRC_NONE,   -- no VBUS and no local supply: the device is off
    SRC_BUS,    -- drawing from VBUS -- subject to 19.1's unit-load floor
    SRC_SELF    -- running on its own supply
  );
end package;

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

-- usb_selfpower_control_vhdl -- a device that supplies itself, and what it
-- still owes the bus.
--
-- Chapter 19.1 built a device that takes its power from VBUS. Many devices
-- do not: a printer, a powered hub, a desktop drive. They declare themselves
-- SELF-POWERED with a bit in the configuration descriptor's bmAttributes,
-- and the host's budget arithmetic (19.6) then skips them.
--
-- The interesting question is what such a device still owes the bus, and the
-- answer is: IT MUST KEEP WATCHING VBUS.
--
-- THE FAILURE THIS MODULE EXISTS TO PREVENT
--
-- A device signals its presence by pulling D+ (or D-) up to its own 3.3 V
-- through a resistor. A BUS-powered device physically cannot do this with
-- VBUS absent -- it has no power. A SELF-powered device can, and if it does,
-- current flows out of the device, through the pull-up, down the data line,
-- and into a host that has DELIBERATELY removed power.
--
-- The consequences are all bad and none of them are obvious:
--
--   * the host sees a device attached to a port it has powered off, so its
--     model of the bus is wrong;
--   * the host cannot complete a power-cycle of that port, because the port
--     never actually goes quiet;
--   * current flows into a rail that is supposed to be dead, which can hold
--     up a supply rail the host was trying to bring down, and on a laptop
--     can keep a controller partly alive across a sleep transition.
--
-- This is "back-powering", and the fix is one gate: the pull-up is driven
-- ONLY when VBUS is present, whatever the device's own logic wants.
--
-- The second rule worth stating: SELF-POWERED IS NOT A CONSTANT. A device
-- with both supplies is self-powered while its own supply is up and bus-
-- powered when it is not, and GetStatus reports the state it is in NOW --
-- not the claim its descriptor makes.
entity usb_selfpower_control_vhdl is
  generic (
    UNIT_LOAD_MA : positive := 100  -- what the bus grants before config
  );
  port (
    clk                  : in  std_logic;
    rst_n                : in  std_logic;

    vbus_present         : in  std_logic;
    local_power_good     : in  std_logic;  -- the device's OWN supply is up
    cfg_self_powered     : in  std_logic;  -- bmAttributes bit 6, the CLAIM
    cfg_remote_wakeup    : in  std_logic;  -- bmAttributes bit 5
    b_max_power          : in  unsigned(7 downto 0);
    pullup_request       : in  std_logic;  -- the device's logic wants to attach

    pullup_enable        : out std_logic;  -- what actually drives the resistor
    status_self_powered  : out std_logic;  -- GetStatus bit 0 -- the state NOW
    status_remote_wakeup : out std_logic;
    bm_attributes        : out std_logic_vector(7 downto 0);
    bus_draw_mA          : out unsigned(15 downto 0);
    operational          : out std_logic;
    power_source         : out power_source_t;

    guard_blocked        : out std_logic;  -- the guard is blocking RIGHT NOW
    blocked_count        : out unsigned(31 downto 0);
    ever_blocked         : out std_logic
  );
end entity;

architecture rtl of usb_selfpower_control_vhdl is
  signal pu_i, blk_i, ssp_i : std_logic;
  signal cnt_r : unsigned(31 downto 0) := (others => '0');
  signal ever_r : std_logic := '0';
begin
  -- THE GUARD. One AND gate, and the entire point of the module: the device
  -- may want to attach, but with no VBUS there is nothing to attach TO, and
  -- driving the pull-up would push current into the host.
  pu_i <= pullup_request and vbus_present;

  -- Live, not dead: this asserts whenever the device's own logic asked for
  -- the pull-up and the guard refused. A design where this can never fire
  -- would be a design where the guard does nothing, and the testbench needs
  -- to prove the guard was actually exercised rather than assume it.
  blk_i <= pullup_request and (not vbus_present);

  -- GetStatus reports the state the device is in NOW. A dual-powered device
  -- that has lost its own supply and is running from the bus reports zero
  -- here even though its descriptor claims self-powered.
  ssp_i <= cfg_self_powered and local_power_good;

  pullup_enable        <= pu_i;
  guard_blocked        <= blk_i;
  status_self_powered  <= ssp_i;
  status_remote_wakeup <= cfg_remote_wakeup;
  blocked_count        <= cnt_r;
  ever_blocked         <= ever_r;

  -- bmAttributes, assembled. Bit 7 is reserved and MUST be set -- Linux
  -- names it USB_CONFIG_ATT_ONE. It carries no information; it is a legacy
  -- constant, and a descriptor with it clear is malformed.
  bm_attributes <= '1' & cfg_self_powered & cfg_remote_wakeup & "00000";

  -- What the device takes FROM THE BUS -- which is not what it consumes.
  -- A self-powered device running on its own supply draws only what
  -- bMaxPower declares. Running on bus power instead, it is a bus-powered
  -- device and is held to chapter 19.1's one-unit-load floor.
  bus_draw_mA <= to_unsigned(0, 16) when vbus_present = '0' else
                 shift_left(resize(b_max_power, 16), 1) when ssp_i = '1' else
                 to_unsigned(UNIT_LOAD_MA, 16);

  -- A device is operational when it has power from SOMEWHERE and a bus to
  -- talk on. Note both terms: its own supply is not enough, because with no
  -- VBUS there is no host to talk to.
  operational <= '1' when (vbus_present = '1'
                           and (local_power_good = '1'
                                or cfg_self_powered = '0'))
                 else '0';

  -- The same facts as a named source. A reader of a waveform can see
  -- SRC_SELF become SRC_BUS at the instant a local supply fails; two
  -- separate bits require them to reconstruct it.
  power_source <= SRC_SELF when ssp_i = '1' else
                  SRC_BUS  when vbus_present = '1' else
                  SRC_NONE;

  process (clk, rst_n)
  begin
    if rst_n = '0' then
      cnt_r <= (others => '0'); ever_r <= '0';
    elsif rising_edge(clk) then
      if blk_i = '1' then
        cnt_r <= cnt_r + 1;
        ever_r <= '1';
      end if;
    end if;
  end process;
end architecture;

    for (st=0; st<32; st=st+1)
     for (p=0; p<256; p=p+1) begin
       vbus=st[0]; lpg=st[1]; cfg_sp=st[2]; cfg_rw=st[3]; pur=st[4];
       bmp=p[7:0];
       step;
       n_exh = n_exh + 1;
     end

      // ---- SAFETY PROPERTIES, independent of the model ----
      // 1. THE one that matters. No VBUS, no pull-up -- ever, for any
      //    combination of the device's own state. This is back-powering.
      if (!vbus)
        check(!pullup_enable,
              "the device drove its pull-up with VBUS absent: BACK-POWERING");
      // 2. With no VBUS a device takes nothing from the bus.
      if (!vbus)
        check(bus_draw_mA === 16'd0, "current drawn from an unpowered bus");
      // 3. bmAttributes bit 7 is always set -- USB_CONFIG_ATT_ONE.
      check(bm_attributes[7], "bmAttributes bit 7 must be one");
      // 4. A device reporting self-powered really does have its own supply.
      check(!status_self_powered || lpg,
            "reported self-powered without a local supply");
      // 5. An operational device always has VBUS.
      check(!operational || vbus, "operational with no bus to talk on");

    // a self-powered device, its own supply up, VBUS REMOVED, and its logic
    // still asking to attach: the back-powering scenario exactly.
    vbus=0; lpg=1; cfg_sp=1; cfg_rw=0; pur=1; bmp=8'd0; step;
    check(!pullup_enable,
          "with VBUS gone the pull-up stays down even though the device can drive it");
    check(guard_blocked, "and the guard reports that it is blocking");
    check(bus_draw_mA === 16'd0, "and nothing flows into the host");

    // VBUS returns: the same device attaches immediately
    vbus=1; step;
    check(pullup_enable, "VBUS returns and the device attaches");

    // the dual-powered case: its own supply fails while attached
    lpg=0; step;
    check(pullup_enable, "it stays attached -- VBUS is still there");
    check(!status_self_powered,
          "but now reports BUS-powered: the status bit is dynamic");
    check(bus_draw_mA === 16'd100,
          "and it falls back to the one-unit-load floor of 19.1");

  exhaustive self-power sweep: 8192 of 8192 points verified

  Verilog / SystemVerilog:
  REACH: exhaustive=8192 guard-blocks=5818 operational=15565 dual-on-bus=3526
  [Verilog] usb_selfpower_control: 0 errors — PASS

  VHDL:
  REACH: exhaustive=8192 guard-blocks=5836 operational=15646 dual-on-bus=3459
  [VHDL] usb_selfpower_control_vhdl: 0 errors — PASS

      // 6. The named source and the individual bits never disagree.
      check(power_source === (e_sp ? 2'd2 : vbus ? 2'd1 : 2'd0),
            "power_source names what the bits already say");

  // The same facts as a named source. Verilog-2005 has no enumerated type,
  // so the encoding is stated as localparams -- which is the nearest thing
  // available and still better than leaving a reader to reconstruct the
  // source from two separate bits.
  localparam [1:0] SRC_NONE = 2'd0,   // no VBUS and no local supply
                   SRC_BUS  = 2'd1,   // drawing from VBUS (19.1's floor)
                   SRC_SELF = 2'd2;   // running on its own supply

// The adversarial agent. Its job is to make the device attach at the worst
// possible moment -- which is precisely what a real device's internal logic
// does by accident when a user yanks a cable.
class backpower_attack_seq extends uvm_sequence #(selfpower_item);
  `uvm_object_utils(backpower_attack_seq)

  task body();
    selfpower_item it;
    // Raise the pull-up request FIRST, with the local supply up, and only
    // then remove VBUS. A device whose guard is level-sensitive passes;
    // one that latched the request at attach time does not.
    `uvm_do_with(it, { vbus_present == 1; local_power_good == 1;
                       pullup_request == 1; })
    `uvm_do_with(it, { vbus_present == 0; local_power_good == 1;
                       pullup_request == 1; })   // the moment of truth
    // and hold it there, because a guard that only blocks on the EDGE of
    // VBUS loss would pass the cycle above and fail the ones after.
    repeat (8)
      `uvm_do_with(it, { vbus_present == 0; local_power_good == 1;
                         pullup_request == 1; })
  endtask
endclass

class selfpower_scoreboard extends uvm_scoreboard;
  `uvm_component_utils(selfpower_scoreboard)

  function void write(selfpower_txn t);
    // THE property. Not a comparison against an expected value -- an
    // assertion that one combination is never produced, for any input.
    // Its violation damages the host, not the data.
    if (!t.vbus_present && t.pullup_enable)
      `uvm_fatal("SELFPWR/BACKPOWER",
        "pull-up driven with VBUS absent: current is flowing into the host")

    // The status bit is dynamic. A device claiming self-power without a
    // local supply is lying to the host's budget arithmetic (19.6).
    if (t.status_self_powered && !t.local_power_good)
      `uvm_error("SELFPWR/STATUS",
        "reported self-powered with no local supply")
  endfunction
endclass

covergroup selfpower_cg with function sample(
    bit vbus, bit lpg, bit cfg_sp, bit pur);
  // The bin that matters: the device WANTED to attach and VBUS was gone.
  // A run where this reads zero has not tested the guard at all, however
  // many points it swept.
  cp_attack : coverpoint {pur, vbus} { bins wants_but_cannot = {2'b10}; }
  // The dual-powered transition of section 3.
  cp_dual : coverpoint {cfg_sp, lpg, vbus} {
    bins self_powered   = {3'b111};
    bins fell_to_bus    = {3'b101};   // claims self, supply down, VBUS up
  }
  x_attack : cross cp_attack, cp_dual;
endgroup

  // THE property: no VBUS, no pull-up. Unconditional, and it needs no
  // antecedent beyond the absence of VBUS itself.
  property p_no_backpower;
    @(posedge clk) disable iff (!rst_n)
      (!vbus_present) |-> (!pullup_enable);
  endproperty
  a_no_backpower : assert property (p_no_backpower)
    else $fatal(1, "pull-up driven with VBUS absent: BACK-POWERING");

  // The status bit is the state, not the claim. Mutation S2.
  property p_status_is_state;
    @(posedge clk) disable iff (!rst_n)
      status_self_powered == (cfg_self_powered && local_power_good);
  endproperty
  a_status_is_state : assert property (p_status_is_state);

  // Nothing is drawn from a bus that is not powered. Mutation S4.
  property p_no_draw_unpowered;
    @(posedge clk) disable iff (!rst_n)
      (!vbus_present) |-> (bus_draw_mA == '0);
  endproperty
  a_no_draw_unpowered : assert property (p_no_draw_unpowered);

  // bmAttributes bit 7 is a constant. USB_CONFIG_ATT_ONE. Mutation S3.
  property p_attr_bit7;
    @(posedge clk) disable iff (!rst_n) bm_attributes[7];
  endproperty
  a_attr_bit7 : assert property (p_attr_bit7);