Suspend

   "nothing is happening right now"     — SOFs still arriving
   "the bus is gone"                    — no SOFs at all

   bus:    quiet quiet  BUSY  quiet quiet  BUSY  quiet quiet
   accumulating counter:  1     2     2      3     4     4     5     6
   correct counter:       1     2     0      1     2     0     1     2

     idle_count <= bus_activity ? 0 : idle_count + 1;           // correct
     idle_count <= bus_activity ? idle_count : idle_count + 1;  // MUT U1

// usb_suspend_detect -- when a device must stop drawing power, and why the
// word "continuous" in the rule is doing all the work.
//
// USB HAS NO IDLE. The host transmits a start-of-frame every millisecond
// whether or not there is anything to say, and that is not an accident of
// the design -- it exists so that a device can tell the difference between
//
//     "nothing is happening right now"      (SOFs still arriving)
//     "the bus is gone"                     (no SOFs at all)
//
// which are otherwise indistinguishable from the far end of a cable.
//
// So a device measures silence, and the threshold is 3 ms -- three missed
// frames. At that point it must begin suspending; within 10 ms of the idle
// starting it must have cut its draw to a trickle.
//
// THE WORD THAT MATTERS IS "CONTINUOUS"
//
// The rule is 3 ms of CONTINUOUS idle, and the obvious implementation --
// count ticks where the bus was quiet -- is wrong in a way that no ordinary
// test catches. A bus that is quiet, busy, quiet, busy, quiet has had
// plenty of quiet ticks and has never been idle for 3 ms. A counter that
// accumulates instead of restarting will suspend a device on a BUSY bus,
// which then stops responding to a host that is actively talking to it.
//
// One line separates the two implementations:
//
//     idle_count <= bus_activity ? 0 : idle_count + 1;      // correct
//     idle_count <= bus_activity ? idle_count : idle_count + 1;  // MUT U1
//
// and the difference is invisible unless the stimulus contains activity
// patterns with gaps in them -- which is why this chapter's sweep enumerates
// every possible pattern in a window rather than sampling realistic ones.
//
// SUSPEND CURRENT
//
// A suspended device is held to a few hundred microamps, not milliamps. The
// exact figure depends on whether it has been armed for remote wakeup
// (19.5): an armed device must keep enough of itself alive to notice a
// reason to wake, and is allowed more.
module usb_suspend_detect #(
  parameter integer SUSPEND_TICKS   = 3000,  // 3 ms, at one tick per us
  parameter integer SUSPEND_UA_BASE = 500,   // suspended, not armed
  parameter integer SUSPEND_UA_RW   = 2500,  // suspended, armed for wakeup
  parameter integer RUN_UA          = 500000 // operating: 500 mA in uA
) (
  input  wire        clk,
  input  wire        rst_n,

  input  wire        vbus_present,
  input  wire        bus_activity,           // ANY activity this tick
  input  wire        remote_wakeup_enabled,  // armed by the host (19.5)

  output reg  [31:0] idle_ticks,             // CONSECUTIVE idle ticks
  output wire        suspended,
  output wire [31:0] draw_limit_uA,          // what it may draw RIGHT NOW
  output wire [1:0]  suspend_state,          // the case, named
  output reg         suspend_entry,          // one-tick pulse on entry
  output reg         resume_detected,        // one-tick pulse on exit

  output reg  [31:0] suspends_entered,
  output reg  [31:0] max_idle_ticks          // the longest silence seen
);
  // Suspended is a THRESHOLD on the consecutive count, not a separate state
  // bit. Deriving it means it cannot disagree with the counter, and it means
  // any activity un-suspends the device in the same tick the activity
  // arrives -- which is what resume requires (19.4).
  assign suspended = vbus_present && (idle_ticks >= SUSPEND_TICKS[31:0]);

  // The same fact with the intermediate case named. Verilog-2005 has no
  // enumerated type, so the encoding is localparams -- the nearest thing
  // available, and still better than leaving a reader to infer the case
  // from a counter and two flags.
  localparam [1:0] SUSP_NOBUS     = 2'd0,   // no VBUS: absent, not suspended
                   SUSP_RUNNING   = 2'd1,   // the bus is active
                   SUSP_COUNTING  = 2'd2,   // quiet, not yet long enough
                   SUSP_SUSPENDED = 2'd3;   // the threshold was crossed
  assign suspend_state = !vbus_present ? SUSP_NOBUS
                       : bus_activity  ? SUSP_RUNNING
                       : (idle_ticks >= SUSPEND_TICKS[31:0]) ? SUSP_SUSPENDED
                                                             : SUSP_COUNTING;

  // A suspended device is held to microamps. An armed device is allowed
  // more, because it must keep enough alive to notice a reason to wake.
  assign draw_limit_uA = !vbus_present ? 32'd0
                       : !suspended    ? RUN_UA[31:0]
                       : remote_wakeup_enabled ? SUSPEND_UA_RW[31:0]
                                               : SUSPEND_UA_BASE[31:0];

  always @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      idle_ticks       <= 32'd0;
      suspend_entry    <= 1'b0;
      resume_detected  <= 1'b0;
      suspends_entered <= 32'd0;
      max_idle_ticks   <= 32'd0;
    end else begin
      suspend_entry   <= 1'b0;
      resume_detected <= 1'b0;

      if (!vbus_present) begin
        // No bus at all. This is not suspend -- suspend is a state a device
        // enters ON a powered bus that has gone quiet. With VBUS gone there
        // is nothing to be suspended from.
        idle_ticks <= 32'd0;
      end else if (bus_activity) begin
        // THE LINE. Activity RESTARTS the measurement; it does not pause it.
        // 3 ms of continuous idle means continuous.
        if (suspended) resume_detected <= 1'b1;
        idle_ticks <= 32'd0;
      end else begin
        idle_ticks <= idle_ticks + 32'd1;
        if (idle_ticks + 32'd1 > max_idle_ticks)
          max_idle_ticks <= idle_ticks + 32'd1;
        // The entry pulse fires on the tick the threshold is first crossed,
        // and only then -- a level would re-announce the entry every tick
        // the device stayed suspended, which chapter 18.2 paid 22009 errors
        // to learn about change bits.
        if (idle_ticks + 32'd1 == SUSPEND_TICKS[31:0]) begin
          suspend_entry    <= 1'b1;
          suspends_entered <= suspends_entered + 32'd1;
        end
      end
    end
  end
endmodule

package usb_suspend_pkg;
  // Where a device sits on the road to suspend. Three of these look alike
  // from outside -- the device is quiet in all of them -- and they mean
  // entirely different things about what it may draw and what will wake it.
  typedef enum logic [1:0] {
    SUSP_NOBUS,      // no VBUS: not suspended, just absent
    SUSP_RUNNING,    // the bus is active
    SUSP_COUNTING,   // quiet, but not yet for long enough
    SUSP_SUSPENDED   // the threshold was crossed
  } suspend_state_e;
endpackage

// usb_suspend_detect_sv -- when a device must stop drawing power, and why the
// word "continuous" in the rule is doing all the work.
//
// USB HAS NO IDLE. The host transmits a start-of-frame every millisecond
// whether or not there is anything to say, and that is not an accident of
// the design -- it exists so that a device can tell the difference between
//
//     "nothing is happening right now"      (SOFs still arriving)
//     "the bus is gone"                     (no SOFs at all)
//
// which are otherwise indistinguishable from the far end of a cable.
//
// So a device measures silence, and the threshold is 3 ms -- three missed
// frames. At that point it must begin suspending; within 10 ms of the idle
// starting it must have cut its draw to a trickle.
//
// THE WORD THAT MATTERS IS "CONTINUOUS"
//
// The rule is 3 ms of CONTINUOUS idle, and the obvious implementation --
// count ticks where the bus was quiet -- is wrong in a way that no ordinary
// test catches. A bus that is quiet, busy, quiet, busy, quiet has had
// plenty of quiet ticks and has never been idle for 3 ms. A counter that
// accumulates instead of restarting will suspend a device on a BUSY bus,
// which then stops responding to a host that is actively talking to it.
//
// One line separates the two implementations:
//
//     idle_count <= bus_activity ? 0 : idle_count + 1;      // correct
//     idle_count <= bus_activity ? idle_count : idle_count + 1;  // MUT U1
//
// and the difference is invisible unless the stimulus contains activity
// patterns with gaps in them -- which is why this chapter's sweep enumerates
// every possible pattern in a window rather than sampling realistic ones.
//
// SUSPEND CURRENT
//
// A suspended device is held to a few hundred microamps, not milliamps. The
// exact figure depends on whether it has been armed for remote wakeup
// (19.5): an armed device must keep enough of itself alive to notice a
// reason to wake, and is allowed more.
module usb_suspend_detect_sv
  import usb_suspend_pkg::*;
#(
  parameter int unsigned SUSPEND_TICKS   = 3000,  // 3 ms, one tick per us
  parameter int unsigned SUSPEND_UA_BASE = 500,   // suspended, not armed
  parameter int unsigned SUSPEND_UA_RW   = 2500,  // suspended, armed
  parameter int unsigned RUN_UA          = 500000 // operating: 500 mA in uA
) (
  input  logic        clk,
  input  logic        rst_n,

  input  logic        vbus_present,
  input  logic        bus_activity,           // ANY activity this tick
  input  logic        remote_wakeup_enabled,  // armed by the host (19.5)

  output logic [31:0] idle_ticks,             // CONSECUTIVE idle ticks
  output logic        suspended,
  output logic [31:0] draw_limit_uA,          // what it may draw RIGHT NOW
  output suspend_state_e suspend_state,
  output logic        suspend_entry,          // one-tick pulse on entry
  output logic        resume_detected,        // one-tick pulse on exit

  output logic [31:0] suspends_entered,
  output logic [31:0] max_idle_ticks          // the longest silence seen
);
  // Suspended is a THRESHOLD on the consecutive count, not a separate state
  // bit. Deriving it means it cannot disagree with the counter, and it means
  // any activity un-suspends the device in the same tick the activity
  // arrives -- which is what resume requires (19.4).
  assign suspended = vbus_present && (idle_ticks >= 32'(SUSPEND_TICKS));

  // The same fact with the intermediate case named. A reader seeing
  // SUSP_COUNTING knows the device is quiet AND that a clock is running on
  // it, which two separate signals leave them to infer.
  always_comb begin
    if      (!vbus_present)                  suspend_state = SUSP_NOBUS;
    else if (bus_activity)                   suspend_state = SUSP_RUNNING;
    else if (idle_ticks >= 32'(SUSPEND_TICKS)) suspend_state = SUSP_SUSPENDED;
    else                                     suspend_state = SUSP_COUNTING;
  end

  // A suspended device is held to microamps. An armed device is allowed
  // more, because it must keep enough alive to notice a reason to wake.
  assign draw_limit_uA = !vbus_present ? 32'd0
                       : !suspended    ? 32'(RUN_UA)
                       : remote_wakeup_enabled ? 32'(SUSPEND_UA_RW)
                                               : 32'(SUSPEND_UA_BASE);

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      idle_ticks       <= 32'd0;
      suspend_entry    <= 1'b0;
      resume_detected  <= 1'b0;
      suspends_entered <= 32'd0;
      max_idle_ticks   <= 32'd0;
    end else begin
      suspend_entry   <= 1'b0;
      resume_detected <= 1'b0;

      if (!vbus_present) begin
        // No bus at all. This is not suspend -- suspend is a state a device
        // enters ON a powered bus that has gone quiet. With VBUS gone there
        // is nothing to be suspended from.
        idle_ticks <= 32'd0;
      end else if (bus_activity) begin
        // THE LINE. Activity RESTARTS the measurement; it does not pause it.
        // 3 ms of continuous idle means continuous.
        if (suspended) resume_detected <= 1'b1;
        idle_ticks <= 32'd0;
      end else begin
        idle_ticks <= idle_ticks + 32'd1;
        if (idle_ticks + 32'd1 > max_idle_ticks)
          max_idle_ticks <= idle_ticks + 32'd1;
        // The entry pulse fires on the tick the threshold is first crossed,
        // and only then -- a level would re-announce the entry every tick
        // the device stayed suspended, which chapter 18.2 paid 22009 errors
        // to learn about change bits.
        if (idle_ticks + 32'd1 == 32'(SUSPEND_TICKS)) begin
          suspend_entry    <= 1'b1;
          suspends_entered <= suspends_entered + 32'd1;
        end
      end
    end
  end
endmodule

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

package usb_suspend_pkg is
  -- Where a device sits on the road to suspend. Three of these look alike
  -- from outside -- the device is quiet in all of them -- and they mean
  -- entirely different things about what it may draw and what will wake it.
  type suspend_state_t is (
    SUSP_NOBUS,      -- no VBUS: not suspended, just absent
    SUSP_RUNNING,    -- the bus is active
    SUSP_COUNTING,   -- quiet, but not yet for long enough
    SUSP_SUSPENDED   -- the threshold was crossed
  );
end package;

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

-- usb_suspend_detect_vhdl -- when a device must stop drawing power, and why
-- the word "continuous" in the rule is doing all the work.
--
-- USB HAS NO IDLE. The host transmits a start-of-frame every millisecond
-- whether or not there is anything to say, and that is not an accident of
-- the design -- it exists so that a device can tell the difference between
--
--     "nothing is happening right now"      (SOFs still arriving)
--     "the bus is gone"                     (no SOFs at all)
--
-- which are otherwise indistinguishable from the far end of a cable.
--
-- So a device measures silence, and the threshold is 3 ms -- three missed
-- frames. At that point it must begin suspending; within 10 ms of the idle
-- starting it must have cut its draw to a trickle.
--
-- THE WORD THAT MATTERS IS "CONTINUOUS"
--
-- The rule is 3 ms of CONTINUOUS idle, and the obvious implementation --
-- count ticks where the bus was quiet -- is wrong in a way that no ordinary
-- test catches. A bus that is quiet, busy, quiet, busy, quiet has had
-- plenty of quiet ticks and has never been idle for 3 ms. A counter that
-- accumulates instead of restarting will suspend a device on a BUSY bus,
-- which then stops responding to a host that is actively talking to it.
--
-- SUSPEND CURRENT
--
-- A suspended device is held to a few hundred microamps, not milliamps. The
-- exact figure depends on whether it has been armed for remote wakeup
-- (19.5): an armed device must keep enough of itself alive to notice a
-- reason to wake, and is allowed more.
entity usb_suspend_detect_vhdl is
  generic (
    SUSPEND_TICKS   : positive := 3000;   -- 3 ms, at one tick per us
    SUSPEND_UA_BASE : positive := 500;    -- suspended, not armed
    SUSPEND_UA_RW   : positive := 2500;   -- suspended, armed for wakeup
    RUN_UA          : positive := 500000  -- operating: 500 mA in uA
  );
  port (
    clk                   : in  std_logic;
    rst_n                 : in  std_logic;

    vbus_present          : in  std_logic;
    bus_activity          : in  std_logic;  -- ANY activity this tick
    remote_wakeup_enabled : in  std_logic;  -- armed by the host (19.5)

    idle_ticks            : out unsigned(31 downto 0);
    suspended             : out std_logic;
    draw_limit_uA         : out unsigned(31 downto 0);
    suspend_state         : out suspend_state_t;
    suspend_entry         : out std_logic;
    resume_detected       : out std_logic;

    suspends_entered      : out unsigned(31 downto 0);
    max_idle_ticks        : out unsigned(31 downto 0)
  );
end entity;

architecture rtl of usb_suspend_detect_vhdl is
  signal idle_r    : unsigned(31 downto 0) := (others => '0');
  signal entry_r   : std_logic := '0';
  signal resume_r  : std_logic := '0';
  signal count_r   : unsigned(31 downto 0) := (others => '0');
  signal maxidle_r : unsigned(31 downto 0) := (others => '0');
  signal susp_i    : std_logic;
begin
  -- Suspended is a THRESHOLD on the consecutive count, not a separate state
  -- bit. Deriving it means it cannot disagree with the counter, and it means
  -- any activity un-suspends the device in the same tick the activity
  -- arrives -- which is what resume requires (19.4).
  susp_i <= '1' when (vbus_present = '1'
                      and idle_r >= to_unsigned(SUSPEND_TICKS, 32))
            else '0';

  idle_ticks       <= idle_r;
  suspended        <= susp_i;
  suspend_entry    <= entry_r;
  resume_detected  <= resume_r;
  suspends_entered <= count_r;
  max_idle_ticks   <= maxidle_r;

  -- A suspended device is held to microamps. An armed device is allowed
  -- more, because it must keep enough alive to notice a reason to wake.
  draw_limit_uA <= to_unsigned(0, 32) when vbus_present = '0' else
                   to_unsigned(RUN_UA, 32) when susp_i = '0' else
                   to_unsigned(SUSPEND_UA_RW, 32)
                     when remote_wakeup_enabled = '1' else
                   to_unsigned(SUSPEND_UA_BASE, 32);

  -- The same fact with the intermediate case named. A reader seeing
  -- SUSP_COUNTING knows the device is quiet AND that a clock is running on
  -- it, which two separate signals leave them to infer.
  suspend_state <= SUSP_NOBUS     when vbus_present = '0' else
                   SUSP_RUNNING   when bus_activity = '1' else
                   SUSP_SUSPENDED when idle_r >= to_unsigned(SUSPEND_TICKS, 32)
                   else SUSP_COUNTING;

  process (clk, rst_n)
  begin
    if rst_n = '0' then
      idle_r <= (others => '0'); entry_r <= '0'; resume_r <= '0';
      count_r <= (others => '0'); maxidle_r <= (others => '0');
    elsif rising_edge(clk) then
      entry_r  <= '0';
      resume_r <= '0';

      if vbus_present = '0' then
        -- No bus at all. This is not suspend -- suspend is a state a device
        -- enters ON a powered bus that has gone quiet. With VBUS gone there
        -- is nothing to be suspended from.
        idle_r <= (others => '0');
      elsif bus_activity = '1' then
        -- THE LINE. Activity RESTARTS the measurement; it does not pause it.
        -- 3 ms of continuous idle means continuous.
        if susp_i = '1' then resume_r <= '1'; end if;
        idle_r <= (others => '0');
      else
        idle_r <= idle_r + 1;
        if idle_r + 1 > maxidle_r then maxidle_r <= idle_r + 1; end if;
        -- The entry pulse fires on the tick the threshold is first crossed,
        -- and only then -- a level would re-announce the entry every tick
        -- the device stayed suspended, which chapter 18.2 paid 22009 errors
        -- to learn about change bits.
        if idle_r + 1 = to_unsigned(SUSPEND_TICKS, 32) then
          entry_r <= '1';
          count_r <= count_r + 1;
        end if;
      end if;
    end if;
  end process;
end architecture;

    // Every one of the 4096 possible activity patterns in a 12-tick window,
    // crossed with remote-wakeup armed or not = 8192 scenarios, 98304
    // individual ticks. This is exhaustive over the TEMPORAL domain: every
    // arrangement of activity and silence, including every gapped one.
    for (cfgi=0; cfgi<2; cfgi=cfgi+1)
     for (pat=0; pat<(1<<W); pat=pat+1) begin
       hard_reset;
       if (gapped(pat[W-1:0])) n_gapped = n_gapped + 1;
       for (t=0; t<W; t=t+1)
         tick(pat[t], 1'b1, cfgi[0]);
       n_pat = n_pat + 1;
     end

      // ---- SAFETY PROPERTIES, independent of the model ----
      // 1. A suspended device is ALWAYS at microamps, never running current.
      if (suspended)
        check(draw_limit_uA <= UA_RW,
              "a suspended device is still drawing operating current");
      // 2. With no VBUS nothing is suspended and nothing is drawn.
      if (!vb) begin
        check(!suspended, "suspended with no VBUS");
        check(draw_limit_uA === 32'd0, "drawing from an unpowered bus");
      end
      // 3. THE property: a device is never suspended when the bus was
      //    active on this very tick. Activity restarts the measurement.
      if (a && vb)
        check(idle_ticks !== 32'd0 || !suspended,
              "suspended on a tick the bus was active");

    // ST-1 idle ticks, then ONE activity tick, then ST-1 idle again.
    // Cumulatively that is 2*(ST-1) idle ticks -- more than the threshold --
    // and the device must NOT suspend, because it was never idle for ST
    // ticks in a row.
    for (t=0; t<ST-1; t=t+1) tick(1'b0, 1'b1, 1'b0);
    tick(1'b1, 1'b1, 1'b0);                 // one SOF
    check(!suspended, "the SOF restarts the measurement");
    check(idle_ticks === 32'd0, "and the count is back to zero");
    for (t=0; t<ST-1; t=t+1) tick(1'b0, 1'b1, 1'b0);
    check(!suspended,
          "still not suspended: 2x(ST-1) idle ticks were never CONSECUTIVE");
    check(suspends_entered === 32'd0, "and no suspend was ever entered");

  exhaustive activity-pattern sweep: 8192 of 8192 patterns verified
  of which contained a gap (activity-idle-activity): 8034

  Verilog / SystemVerilog:
  REACH: patterns=8192 gapped=8034 suspended-ticks=17319 entries=5664
         resumes=4367 max-idle=30
  [Verilog] usb_suspend_detect: 0 errors — PASS

  VHDL:
  REACH: patterns=8192 gapped=8034 suspended-ticks=17514 entries=5747
         resumes=4435 max-idle=32
  [VHDL] usb_suspend_detect_vhdl: 0 errors — PASS

  assign suspended   = vbus_present && (idle_ticks >= SUSPEND_TICKS[31:0]);
  ...
  wire was_suspended = vbus_present && (idle_ticks >= SUSPEND_TICKS[31:0]);

        if (suspended) resume_detected <= 1'b1;

// Realistic traffic is the WRONG stimulus for this block. A generator that
// models a believable bus produces long runs of activity and long runs of
// silence; the patterns that matter are ragged, and section 10 measured how
// rare they are otherwise.
class ragged_traffic_seq extends uvm_sequence #(bus_tick_item);
  `uvm_object_utils(ragged_traffic_seq)
  rand int unsigned len;
  rand bit          pattern [];

  constraint c_len { len inside {[8:24]}; pattern.size() == len; }

  // Force gaps. Without this the solver produces mostly-quiet or
  // mostly-busy runs, which is precisely the distribution that hides
  // mutation U1.
  constraint c_ragged {
    // at least two activity ticks with at least one quiet tick between them
    pattern.sum() with (int'(item)) inside {[2:len-2]};
  }

  task body();
    bus_tick_item it;
    foreach (pattern[i])
      `uvm_do_with(it, { bus_activity == pattern[i]; vbus_present == 1; })
  endtask
endclass

class suspend_scoreboard extends uvm_scoreboard;
  `uvm_component_utils(suspend_scoreboard)
  local int unsigned m_consecutive;   // its OWN count (chapter 17.3)

  function void write(suspend_txn t);
    // THE property, stated as the rule rather than as an expected value:
    // a device is suspended if and only if it has been quiet for the
    // threshold CONSECUTIVELY.
    if (t.bus_activity) m_consecutive = 0;
    else                m_consecutive++;

    if (t.suspended != (m_consecutive >= SUSPEND_TICKS))
      `uvm_error("SUSP/STATE", $sformatf(
        "suspended=%0b after %0d consecutive idle ticks (threshold %0d)",
        t.suspended, m_consecutive, SUSPEND_TICKS))

    // A suspended device is at microamps. Its violation is measurable on a
    // bench with a current probe, which is more than can be said for most
    // protocol errors.
    if (t.suspended && t.draw_limit_uA > SUSPEND_UA_RW)
      `uvm_error("SUSP/CURRENT", $sformatf(
        "suspended device allowed %0d uA", t.draw_limit_uA))
  endfunction
endclass

covergroup suspend_cg with function sample(
    int unsigned run_len, bit gapped, bit armed, bit suspended);
  // How long the silence ran before it was interrupted. The bins below the
  // threshold are the ones that must NOT suspend.
  cp_run : coverpoint run_len {
    bins short [] = {[0:SUSPEND_TICKS-1]};
    bins at_threshold = {SUSPEND_TICKS};
    bins beyond = {[SUSPEND_TICKS+1:$]};
  }
  // THE bin. A run that never contains a gap has not tested section 2 at
  // all, however many ticks it covers.
  cp_gap : coverpoint gapped { bins ragged = {1}; }
  cp_armed : coverpoint armed;
  x_gap_run : cross cp_gap, cp_run, cp_armed;
endgroup

  // THE property: suspended if and only if the silence has been CONTINUOUS.
  // Stated with $past rather than a counter, so it does not re-implement
  // the design it is checking.
  property p_activity_restarts;
    @(posedge clk) disable iff (!rst_n)
      (vbus_present && bus_activity) |=> (idle_ticks == 0);
  endproperty
  a_activity_restarts : assert property (p_activity_restarts)
    else $error("activity did not restart the idle measurement");

  // A suspended device is at microamps, always.
  property p_suspended_current;
    @(posedge clk) disable iff (!rst_n)
      suspended |-> (draw_limit_uA <= SUSPEND_UA_RW);
  endproperty
  a_suspended_current : assert property (p_suspended_current);

  // The entry pulse is a pulse: it never asserts twice in a row.
  property p_entry_is_a_pulse;
    @(posedge clk) disable iff (!rst_n)
      suspend_entry |=> !suspend_entry;
  endproperty
  a_entry_is_a_pulse : assert property (p_entry_is_a_pulse);

  // No VBUS, no suspend -- suspend is a state on a POWERED bus.
  property p_no_suspend_without_vbus;
    @(posedge clk) disable iff (!rst_n)
      (!vbus_present) |-> (!suspended);
  endproperty
  a_no_suspend_without_vbus : assert property (p_no_suspend_without_vbus);