Resume

   1. DRIVE K    the host holds the opposite of the idle state.
                 This is the wakeup itself.
   2. EOP        SE0 for two bit times — a low-speed end-of-packet.
                 This says the resume signalling has ENDED.
   3. IDLE (J)   the bus returns to idle and normal traffic resumes.

   (b) Some (many) devices actually need more than 20 ms of resume
   signalling, and while we can argue that's against the USB
   Specification, we don't have control over which devices a certification
   laboratory will be using for certification. If CertLab uses a device
   which was tested against Windows and that happens to have relaxed
   resume signalling rules, we might fall into situations where we fail
   interoperability and electrical tests.

   #define USB_RESUME_TIMEOUT  40 /* ms */

  parameter integer RESUME_TICKS   = 40,  // what this host drives (ms)
  parameter integer SPEC_MIN_TICKS = 20,  // the specification's floor (ms)

      // 2. The EOP is only ever reached after a full-length K. A resume
      //    whose K was short must never reach the end-of-packet, because
      //    the device would treat a too-short wakeup as a complete one.
      if (drive_se0)
        check(k_ticks >= RT,
              "the EOP was reached without holding K for the full duration");

// usb_resume_sequencer -- waking a suspended device, and the twenty
// milliseconds that turned into forty.
//
// Chapter 19.3 put a device to sleep by measuring silence. This wakes it,
// and the waking is not a packet -- there is nothing to address a packet to,
// because a suspended device is not listening for tokens. It is an
// ELECTRICAL signal held on the data lines long enough that a device running
// on microamps cannot miss it.
//
// The sequence has three phases and they are not interchangeable:
//
//   1. DRIVE K   the host holds the opposite of the idle state on the bus.
//                This is the wakeup itself, and it must be held for a long
//                time by bus standards -- see the note below.
//   2. EOP       a low-speed end-of-packet: SE0 for two bit times, which
//                tells the device the resume signalling has ENDED and normal
//                traffic is about to start. Without it the device cannot
//                tell a finished resume from a resume still in progress.
//   3. IDLE (J)  the bus returns to its idle state and traffic resumes.
//
// TWENTY MILLISECONDS, OR FORTY
//
// The specification requires the host to drive resume for AT LEAST 20 ms and
// gives no upper bound. Linux drives it for 40, and the comment explaining
// why is worth reading in full because it is unusually candid:
//
//     (b) Some (many) devices actually need more than 20 ms of resume
//     signalling, and while we can argue that's against the USB
//     Specification, we don't have control over which devices a
//     certification laboratory will be using for certification. If CertLab
//     uses a device which was tested against Windows and that happens to
//     have relaxed resume signalling rules, we might fall into situations
//     where we fail interoperability and electrical tests.
//
//     #define USB_RESUME_TIMEOUT  40 /* ms */
//
// So RESUME_TICKS is what this host actually drives and SPEC_MIN_TICKS is
// the floor the specification sets. They are separate parameters ON PURPOSE:
// a design that hard-codes one number cannot express the difference between
// "what we do" and "what we must not go below", and this block's whole
// reason for existing is that those are different numbers.
//
// A resume cut short below SPEC_MIN_TICKS is a protocol violation, and it is
// reported rather than silently tolerated -- because the device it fails to
// wake will simply stay asleep, and nothing else in the system will say why.
module usb_resume_sequencer #(
  parameter integer RESUME_TICKS   = 40,  // what this host drives (ms)
  parameter integer SPEC_MIN_TICKS = 20,  // the specification's floor (ms)
  parameter integer EOP_TICKS      = 2    // SE0 for two bit times
) (
  input  wire        clk,
  input  wire        rst_n,

  input  wire        start_resume,   // the host decides to wake the bus
  input  wire        abort,          // something cut the sequence short

  output reg  [1:0]  phase,
  output wire        drive_k,        // the wakeup signal itself
  output wire        drive_se0,      // the end-of-packet
  output wire        drive_j,        // idle -- normal traffic may follow
  output reg  [15:0] k_ticks,        // how long K has been held

  output reg         resume_complete,// one-tick pulse: the bus is awake
  output reg         spec_violation, // sticky: a resume below the floor
  output reg  [31:0] resumes_done,
  output reg  [31:0] violations
);
  localparam [1:0] R_IDLE = 2'd0, R_K = 2'd1, R_EOP = 2'd2, R_DONE = 2'd3;

  // The three drive states are mutually exclusive by construction: they are
  // decodes of one phase register, not three independent enables. Three
  // enables would admit the one state that must never occur -- two of them
  // asserted at once, which on a real bus is a short.
  assign drive_k   = (phase == R_K);
  assign drive_se0 = (phase == R_EOP);
  assign drive_j   = (phase == R_IDLE) || (phase == R_DONE);

  reg [15:0] eop_ticks;

  always @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      phase           <= R_IDLE;
      k_ticks         <= 16'd0;
      eop_ticks       <= 16'd0;
      resume_complete <= 1'b0;
      spec_violation  <= 1'b0;
      resumes_done    <= 32'd0;
      violations      <= 32'd0;
    end else begin
      resume_complete <= 1'b0;

      case (phase)
        R_IDLE: begin
          if (start_resume && !abort) begin
            phase     <= R_K;
            k_ticks   <= 16'd0;
            eop_ticks <= 16'd0;
          end
        end

        R_K: begin
          if (abort) begin
            // Cut short. If K was held for less than the specification's
            // floor, this is a violation and it is RECORDED -- the device
            // that fails to wake will not report anything, so if this
            // block does not, nothing does.
            if (k_ticks < SPEC_MIN_TICKS[15:0]) begin
              spec_violation <= 1'b1;
              violations     <= violations + 32'd1;
            end
            phase <= R_IDLE;
          end else if (k_ticks + 16'd1 >= RESUME_TICKS[15:0]) begin
            k_ticks <= k_ticks + 16'd1;
            phase   <= R_EOP;
          end else begin
            // A start arriving mid-sequence is IGNORED. A resume already in
            // progress must not be restarted: restarting resets k_ticks, and
            // a host that retriggered every millisecond would drive K
            // forever without ever reaching the EOP that ends it.
            k_ticks <= k_ticks + 16'd1;
          end
        end

        R_EOP: begin
          if (abort) begin
            // Aborting during the EOP is not a spec violation on the K
            // duration -- K was already held long enough -- but the resume
            // did not complete, so no completion is announced.
            phase <= R_IDLE;
          end else if (eop_ticks + 16'd1 >= EOP_TICKS[15:0]) begin
            phase <= R_DONE;
          end else begin
            eop_ticks <= eop_ticks + 16'd1;
          end
        end

        R_DONE: begin
          resume_complete <= 1'b1;
          resumes_done    <= resumes_done + 32'd1;
          phase           <= R_IDLE;
        end

        default: phase <= R_IDLE;
      endcase
    end
  end
endmodule

package usb_resume_pkg;
  // The three phases of a resume, plus the one-tick completion. They are
  // not interchangeable and they are not independent enables: exactly one
  // is driven at a time, because two at once is a short on a real bus.
  typedef enum logic [1:0] {
    R_IDLE,   // driving J -- normal traffic may flow
    R_K,      // driving K -- this IS the wakeup
    R_EOP,    // driving SE0 -- the resume has ended
    R_DONE    // one tick: announce completion, return to idle
  } resume_phase_e;
endpackage

// usb_resume_sequencer_sv -- waking a suspended device, and the twenty
// milliseconds that turned into forty.
//
// Chapter 19.3 put a device to sleep by measuring silence. This wakes it,
// and the waking is not a packet -- there is nothing to address a packet to,
// because a suspended device is not listening for tokens. It is an
// ELECTRICAL signal held on the data lines long enough that a device running
// on microamps cannot miss it.
//
// The sequence has three phases and they are not interchangeable:
//
//   1. DRIVE K   the host holds the opposite of the idle state on the bus.
//                This is the wakeup itself, and it must be held for a long
//                time by bus standards -- see the note below.
//   2. EOP       a low-speed end-of-packet: SE0 for two bit times, which
//                tells the device the resume signalling has ENDED and normal
//                traffic is about to start. Without it the device cannot
//                tell a finished resume from a resume still in progress.
//   3. IDLE (J)  the bus returns to its idle state and traffic resumes.
//
// TWENTY MILLISECONDS, OR FORTY
//
// The specification requires the host to drive resume for AT LEAST 20 ms and
// gives no upper bound. Linux drives it for 40, and the comment explaining
// why is worth reading in full because it is unusually candid:
//
//     (b) Some (many) devices actually need more than 20 ms of resume
//     signalling, and while we can argue that's against the USB
//     Specification, we don't have control over which devices a
//     certification laboratory will be using for certification. If CertLab
//     uses a device which was tested against Windows and that happens to
//     have relaxed resume signalling rules, we might fall into situations
//     where we fail interoperability and electrical tests.
//
//     #define USB_RESUME_TIMEOUT  40 /* ms */
//
// So RESUME_TICKS is what this host actually drives and SPEC_MIN_TICKS is
// the floor the specification sets. They are separate parameters ON PURPOSE:
// a design that hard-codes one number cannot express the difference between
// "what we do" and "what we must not go below", and this block's whole
// reason for existing is that those are different numbers.
//
// A resume cut short below SPEC_MIN_TICKS is a protocol violation, and it is
// reported rather than silently tolerated -- because the device it fails to
// wake will simply stay asleep, and nothing else in the system will say why.
module usb_resume_sequencer_sv
  import usb_resume_pkg::*;
#(
  parameter int unsigned RESUME_TICKS   = 40,  // what this host drives (ms)
  parameter int unsigned SPEC_MIN_TICKS = 20,  // the spec's floor (ms)
  parameter int unsigned EOP_TICKS      = 2    // SE0 for two bit times
) (
  input  logic        clk,
  input  logic        rst_n,

  input  logic        start_resume,   // the host decides to wake the bus
  input  logic        abort,          // something cut the sequence short

  output resume_phase_e phase,
  output logic        drive_k,        // the wakeup signal itself
  output logic        drive_se0,      // the end-of-packet
  output logic        drive_j,        // idle -- normal traffic may follow
  output logic [15:0] k_ticks,        // how long K has been held

  output logic        resume_complete,// one-tick pulse: the bus is awake
  output logic        spec_violation, // sticky: a resume below the floor
  output logic [31:0] resumes_done,
  output logic [31:0] violations
);
  initial begin
    if (SPEC_MIN_TICKS > RESUME_TICKS)
      $fatal(1, "RESUME_TICKS=%0d is below the specification floor of %0d",
             RESUME_TICKS, SPEC_MIN_TICKS);
    if (EOP_TICKS < 1)
      $fatal(1, "an end-of-packet with no duration does not end anything");
  end

  // The three drive states are mutually exclusive by construction: they are
  // decodes of one phase register, not three independent enables. Three
  // enables would admit the one state that must never occur -- two of them
  // asserted at once, which on a real bus is a short.
  assign drive_k   = (phase == R_K);
  assign drive_se0 = (phase == R_EOP);
  assign drive_j   = (phase == R_IDLE) || (phase == R_DONE);

  logic [15:0] eop_ticks;

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      phase           <= R_IDLE;
      k_ticks         <= 16'd0;
      eop_ticks       <= 16'd0;
      resume_complete <= 1'b0;
      spec_violation  <= 1'b0;
      resumes_done    <= 32'd0;
      violations      <= 32'd0;
    end else begin
      resume_complete <= 1'b0;

      case (phase)
        R_IDLE: begin
          if (start_resume && !abort) begin
            phase     <= R_K;
            k_ticks   <= 16'd0;
            eop_ticks <= 16'd0;
          end
        end

        R_K: begin
          if (abort) begin
            // Cut short. If K was held for less than the specification's
            // floor, this is a violation and it is RECORDED -- the device
            // that fails to wake will not report anything, so if this
            // block does not, nothing does.
            if (k_ticks < 16'(SPEC_MIN_TICKS)) begin
              spec_violation <= 1'b1;
              violations     <= violations + 32'd1;
            end
            phase <= R_IDLE;
          end else if (k_ticks + 16'd1 >= 16'(RESUME_TICKS)) begin
            k_ticks <= k_ticks + 16'd1;
            phase   <= R_EOP;
          end else begin
            // A start arriving mid-sequence is IGNORED. A resume already in
            // progress must not be restarted: restarting resets k_ticks, and
            // a host that retriggered every millisecond would drive K
            // forever without ever reaching the EOP that ends it.
            k_ticks <= k_ticks + 16'd1;
          end
        end

        R_EOP: begin
          if (abort) begin
            // Aborting during the EOP is not a spec violation on the K
            // duration -- K was already held long enough -- but the resume
            // did not complete, so no completion is announced.
            phase <= R_IDLE;
          end else if (eop_ticks + 16'd1 >= 16'(EOP_TICKS)) begin
            phase <= R_DONE;
          end else begin
            eop_ticks <= eop_ticks + 16'd1;
          end
        end

        R_DONE: begin
          resume_complete <= 1'b1;
          resumes_done    <= resumes_done + 32'd1;
          phase           <= R_IDLE;
        end

        default: phase <= R_IDLE;
      endcase
    end
  end
endmodule

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

package usb_resume_pkg is
  -- The three phases of a resume, plus the one-tick completion. They are
  -- not interchangeable and they are not independent enables: exactly one
  -- is driven at a time, because two at once is a short on a real bus.
  type resume_phase_t is (
    R_IDLE,   -- driving J -- normal traffic may flow
    R_K,      -- driving K -- this IS the wakeup
    R_EOP,    -- driving SE0 -- the resume has ended
    R_DONE    -- one tick: announce completion, return to idle
  );
end package;

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

-- usb_resume_sequencer_vhdl -- waking a suspended device, and the twenty
-- milliseconds that turned into forty.
--
-- Chapter 19.3 put a device to sleep by measuring silence. This wakes it,
-- and the waking is not a packet -- there is nothing to address a packet to,
-- because a suspended device is not listening for tokens. It is an
-- ELECTRICAL signal held on the data lines long enough that a device running
-- on microamps cannot miss it.
--
-- The sequence has three phases and they are not interchangeable:
--
--   1. DRIVE K   the host holds the opposite of the idle state on the bus.
--   2. EOP       a low-speed end-of-packet: SE0 for two bit times, which
--                tells the device the resume signalling has ENDED.
--   3. IDLE (J)  the bus returns to its idle state and traffic resumes.
--
-- TWENTY MILLISECONDS, OR FORTY
--
-- The specification requires the host to drive resume for AT LEAST 20 ms and
-- gives no upper bound. Linux drives it for 40, and the comment explaining
-- why is worth reading in full because it is unusually candid:
--
--     (b) Some (many) devices actually need more than 20 ms of resume
--     signalling, and while we can argue that's against the USB
--     Specification, we don't have control over which devices a
--     certification laboratory will be using for certification.
--
--     #define USB_RESUME_TIMEOUT  40 /* ms */
--
-- So RESUME_TICKS is what this host actually drives and SPEC_MIN_TICKS is
-- the floor the specification sets. They are separate generics ON PURPOSE:
-- a design that hard-codes one number cannot express the difference between
-- "what we do" and "what we must not go below".
entity usb_resume_sequencer_vhdl is
  generic (
    RESUME_TICKS   : positive := 40;  -- what this host drives (ms)
    SPEC_MIN_TICKS : positive := 20;  -- the specification's floor (ms)
    EOP_TICKS      : positive := 2    -- SE0 for two bit times
  );
  port (
    clk             : in  std_logic;
    rst_n           : in  std_logic;

    start_resume    : in  std_logic;
    abort_in        : in  std_logic;

    phase           : out resume_phase_t;
    drive_k         : out std_logic;
    drive_se0       : out std_logic;
    drive_j         : out std_logic;
    k_ticks         : out unsigned(15 downto 0);

    resume_complete : out std_logic;
    spec_violation  : out std_logic;
    resumes_done    : out unsigned(31 downto 0);
    violations      : out unsigned(31 downto 0)
  );
end entity;

architecture rtl of usb_resume_sequencer_vhdl is
  signal ph_r    : resume_phase_t := R_IDLE;
  signal k_r     : unsigned(15 downto 0) := (others => '0');
  signal eop_r   : unsigned(15 downto 0) := (others => '0');
  signal done_r  : std_logic := '0';
  signal sviol_r : std_logic := '0';
  signal rcnt_r  : unsigned(31 downto 0) := (others => '0');
  signal vcnt_r  : unsigned(31 downto 0) := (others => '0');
begin
  assert SPEC_MIN_TICKS <= RESUME_TICKS
    report "RESUME_TICKS is below the specification floor" severity failure;

  -- The three drive states are mutually exclusive by construction: they are
  -- decodes of one phase signal, not three independent enables. Three
  -- enables would admit the one state that must never occur -- two of them
  -- asserted at once, which on a real bus is a short.
  drive_k   <= '1' when ph_r = R_K   else '0';
  drive_se0 <= '1' when ph_r = R_EOP else '0';
  drive_j   <= '1' when (ph_r = R_IDLE or ph_r = R_DONE) else '0';

  phase           <= ph_r;
  k_ticks         <= k_r;
  resume_complete <= done_r;
  spec_violation  <= sviol_r;
  resumes_done    <= rcnt_r;
  violations      <= vcnt_r;

  process (clk, rst_n)
  begin
    if rst_n = '0' then
      ph_r <= R_IDLE; k_r <= (others => '0'); eop_r <= (others => '0');
      done_r <= '0'; sviol_r <= '0';
      rcnt_r <= (others => '0'); vcnt_r <= (others => '0');
    elsif rising_edge(clk) then
      done_r <= '0';

      case ph_r is
        when R_IDLE =>
          if start_resume = '1' and abort_in = '0' then
            ph_r <= R_K; k_r <= (others => '0'); eop_r <= (others => '0');
          end if;

        when R_K =>
          if abort_in = '1' then
            -- Cut short. If K was held for less than the specification's
            -- floor, this is a violation and it is RECORDED -- the device
            -- that fails to wake will not report anything, so if this
            -- block does not, nothing does.
            if k_r < to_unsigned(SPEC_MIN_TICKS, 16) then
              sviol_r <= '1';
              vcnt_r  <= vcnt_r + 1;
            end if;
            ph_r <= R_IDLE;
          elsif k_r + 1 >= to_unsigned(RESUME_TICKS, 16) then
            k_r  <= k_r + 1;
            ph_r <= R_EOP;
          else
            -- A start arriving mid-sequence is IGNORED. A resume already in
            -- progress must not be restarted: restarting resets k_ticks, and
            -- a host that retriggered every millisecond would drive K
            -- forever without ever reaching the EOP that ends it.
            k_r <= k_r + 1;
          end if;

        when R_EOP =>
          if abort_in = '1' then
            -- Aborting during the EOP is not a spec violation on the K
            -- duration -- K was already held long enough -- but the resume
            -- did not complete, so no completion is announced.
            ph_r <= R_IDLE;
          elsif eop_r + 1 >= to_unsigned(EOP_TICKS, 16) then
            ph_r <= R_DONE;
          else
            eop_r <= eop_r + 1;
          end if;

        when R_DONE =>
          done_r <= '1';
          rcnt_r <= rcnt_r + 1;
          ph_r   <= R_IDLE;
      end case;
    end if;
  end process;
end architecture;

    // Every combination of start and abort events over an 8-tick window:
    // 2^8 start patterns x 2^8 abort patterns = 65536 scenarios, 524288
    // ticks. This covers every possible interleaving of "wake the bus" and
    // "something interrupted it", including every retrigger mid-sequence
    // and every abort at every point in the sequence.
    for (sp=0; sp<(1<<W); sp=sp+1)
     for (ap=0; ap<(1<<W); ap=ap+1) begin
       hard_reset;
       for (t=0; t<W; t=t+1) tick(sp[t], ap[t]);
       n_scen = n_scen + 1;
     end

      // ---- SAFETY PROPERTIES, independent of the model ----
      // 1. THE electrical one: never two drive states at once. On a real
      //    bus that is a short, not a protocol error.
      check((drive_k + drive_se0 + drive_j) == 1,
            "two drive states asserted at once: that is a bus short");
      // 2. The EOP is only ever reached after a full-length K. A resume
      //    whose K was short must never reach the end-of-packet, because
      //    the device would treat a too-short wakeup as a complete one.
      if (drive_se0)
        check(k_ticks >= RT,
              "the EOP was reached without holding K for the full duration");
      // 3. And therefore never below the specification's floor either.
      if (drive_se0)
        check(k_ticks >= SMIN,
              "the EOP was reached with K held below the spec minimum");

  exhaustive start/abort pattern sweep: 65536 of 65536 scenarios verified

  Verilog / SystemVerilog:
  REACH: scenarios=65536 completions=749 violations=205
         aborts-in-K=71248 retriggers-in-K=71456
  [Verilog] usb_resume_sequencer: 0 errors — PASS

  VHDL:
  REACH: scenarios=65536 completions=775 violations=173
         aborts-in-K=71219 retriggers-in-K=71508
  [VHDL] usb_resume_sequencer_vhdl: 0 errors — PASS

    for (t=0; t<EOPT-1; t=t+1) tick(1'b0, 1'b0);
    check(drive_j, "and the EOP is followed by idle");      // FAILED

    // EOPT ticks are spent IN the EOP phase -- the first enters it and the
    // last leaves it. An earlier version of this loop ran EOPT-1 and then
    // asserted the bus was idle, which failed against a correct design:
    // the sequencer was still driving SE0, exactly as it should have been.
    for (t=0; t<EOPT; t=t+1) tick(1'b0, 1'b0);

class resume_event_item extends uvm_sequence_item;
  `uvm_object_utils(resume_event_item)
  rand bit start_resume;
  rand bit abort;

  // Aborts are rare in the field and central to this block, so the
  // generator over-weights them relative to reality. Realistic rates would
  // reach section 12's R4 and R5 a handful of times per run.
  constraint c_rates {
    start_resume dist { 1 := 1, 0 := 5 };
    abort        dist { 1 := 1, 0 := 9 };
  }
endclass

// Aborting at EVERY point in the sequence, deliberately, one point per
// iteration -- the directed complement to the random interleaving above.
class abort_walk_seq extends uvm_sequence #(resume_event_item);
  `uvm_object_utils(abort_walk_seq)
  rand int unsigned abort_at;
  constraint c_at { abort_at inside {[0:RESUME_TICKS+EOP_TICKS+1]}; }

  task body();
    resume_event_item it;
    `uvm_do_with(it, { start_resume == 1; abort == 0; })
    for (int i = 0; i < abort_at; i++)
      `uvm_do_with(it, { start_resume == 0; abort == 0; })
    // THE point: whether this abort is a spec violation depends entirely on
    // how far K had got, and that is the one thing the design must get
    // right about aborts.
    `uvm_do_with(it, { start_resume == 0; abort == 1; })
  endtask
endclass

class resume_scoreboard extends uvm_scoreboard;
  `uvm_component_utils(resume_scoreboard)

  function void write(resume_txn t);
    // THE electrical property. Counted, not compared -- its violation is a
    // short, and there is no "expected value" that makes two drivers OK.
    int unsigned drivers = t.drive_k + t.drive_se0 + t.drive_j;
    if (drivers != 1)
      `uvm_fatal("RESUME/SHORT", $sformatf(
        "%0d drive signals asserted at once", drivers))

    // A device seeing the EOP treats the resume as complete. It must
    // therefore never follow a K that was too short.
    if (t.drive_se0 && t.k_ticks < RESUME_TICKS)
      `uvm_error("RESUME/SHORT_K", $sformatf(
        "EOP after only %0d ticks of K (need %0d)", t.k_ticks, RESUME_TICKS))

    // And the promise, which is stricter than the standard.
    if (t.drive_se0 && t.k_ticks < SPEC_MIN_TICKS)
      `uvm_error("RESUME/SUBSPEC", "K held below the specification floor")
  endfunction
endclass

covergroup resume_cg with function sample(
    int unsigned phase, int unsigned k_at_abort, bit retrigger);
  // Where in the sequence the abort landed. The bins either side of the
  // specification floor are the ones that decide whether it was a
  // violation, and they are what section 12's R4 lives in.
  cp_abort_point : coverpoint k_at_abort {
    bins below_floor = {[0:SPEC_MIN_TICKS-1]};
    bins at_floor    = {SPEC_MIN_TICKS};
    bins above_floor = {[SPEC_MIN_TICKS+1:RESUME_TICKS]};
  }
  // A start arriving mid-sequence. Section 4's livelock lives here.
  cp_retrigger : coverpoint retrigger { bins mid_sequence = {1}; }
  cp_phase : coverpoint phase;
  x_abort_phase : cross cp_abort_point, cp_phase, cp_retrigger;
endgroup

  // THE electrical property: exactly one driver, always.
  property p_one_driver;
    @(posedge clk) disable iff (!rst_n)
      $countones({drive_k, drive_se0, drive_j}) == 1;
  endproperty
  a_one_driver : assert property (p_one_driver)
    else $fatal(1, "two drive states asserted at once: bus short");

  // The EOP never follows a short K. Mutations R1 and R2 together.
  property p_eop_after_full_k;
    @(posedge clk) disable iff (!rst_n)
      drive_se0 |-> (k_ticks >= RESUME_TICKS);
  endproperty
  a_eop_after_full_k : assert property (p_eop_after_full_k);

  // A resume in progress is never restarted. Mutation R3.
  property p_no_restart;
    @(posedge clk) disable iff (!rst_n)
      (drive_k && start_resume && !abort) |=> (k_ticks == $past(k_ticks) + 1);
  endproperty
  a_no_restart : assert property (p_no_restart)
    else $error("a start mid-K restarted the sequence");

  // The completion is a pulse. Mutation R7.
  property p_completion_is_a_pulse;
    @(posedge clk) disable iff (!rst_n)
      resume_complete |=> !resume_complete;
  endproperty
  a_completion_is_a_pulse : assert property (p_completion_is_a_pulse);