USB Assertions

    every request is eventually answered

   MIN_LAT is not paranoia. It is the half of the window
   that catches a response to the WRONG request.

       age <  MIN_LAT    it cannot be ours
       age >= MAX_LAT    it is too late
       otherwise         PASS

   A run that ends with obligations outstanding and reports
   zero failures has not verified the property.

   It has run out of time while the property was still being
   tested, and called that success.

  usb_assert_engine  #(N_OBL = 4, MIN_LAT = 2, MAX_LAT = 12)

  inputs                    outputs
  ------                    -------
  trigger    an obligation  outstanding / oldest_age
             begins         pass_pulse / fail_pulse
  response   one is         fail_code   LATE / EARLY /
             discharged                 SPURIOUS / OVERFLOW /
  eot        drain & report             DANGLING

  n_triggers n_pass n_late n_early
  n_spurious n_overflow n_dangling

  ONE EVENT PER CYCLE. A reporting channel has one slot, and
  an engine that can emit three failures in a cycle cannot
  say which one it was. A drain therefore takes as many
  cycles as there are obligations.

// usb_assert_engine -- what an assertion actually is when you build one, and
// the four things every real liveness check needs that "eventually" does not
// give you.
//
// THE PROPERTY EVERYBODY WANTS TO WRITE
//
//     every request is eventually answered
//
// It is unimplementable, unsynthesisable, and uncheckable in a finite
// simulation. "Eventually" has no failing case: at any moment during a run
// the answer to "has it been answered yet?" is either yes or NOT YET, and not
// yet is not a failure. A simulation that ends with the request outstanding
// has not disproved the property -- it has simply stopped early.
//
// So every liveness check that exists in practice is a BOUNDED one:
//
//     every request is answered within MAX_LAT cycles
//
// and choosing MAX_LAT is the whole job. This block is that check, built as
// hardware, and the four things it needs are the four things a hand-written
// timer usually lacks.
//
// 1. A WINDOW HAS TWO EDGES
//
// MAX_LAT alone accepts a response that arrives IMPOSSIBLY EARLY -- one cycle
// after the request, when the pipeline that produces it is four stages deep.
// Such a response did not come from this request. It came from the previous
// one, or from a signal that is stuck asserted, and either way the check has
// passed while the design is broken.
//
//     MIN_LAT is not paranoia. It is the half of the window that
//     catches a response to the WRONG request.
//
// 2. OBLIGATIONS OVERLAP, SO ONE TIMER IS NOT ENOUGH
//
// A second request can arrive before the first is answered. With a single
// timer there is no way to tell which response belongs to which request, and
// the usual implementation -- clear the timer on any response -- lets ONE
// response satisfy BOTH obligations. The bus then drops a response for every
// overlapping pair, for ever, and the check never fires.
//
// An engine needs a QUEUE of outstanding obligations, retired in order.
//
// 3. RUNNING OUT OF TRACKING CAPACITY IS A FAILURE, NOT A LIMIT
//
// The queue is finite. When it is full and another request arrives, there are
// two choices: report it, or drop it. Dropping it is how a checker silently
// stops checking exactly when the design is at its busiest -- which is when
// it is most likely to be wrong. So overflow is a reported failure.
//
// 4. AN UNFINISHED OBLIGATION IS NOT A PASS
//
// This is the one that is missed most often. At the end of the run, whatever
// is still outstanding has NOT been answered. It is not "inconclusive" and it
// is not "still in flight" -- the simulation is over and nothing more is
// coming.
//
//     A run that ends with obligations outstanding and reports
//     zero failures has not verified the property. It has run
//     out of time while the property was still being tested,
//     and called that success.
//
// So `eot` drains the queue and every survivor is a DANGLING failure.
//
// ONE EVENT PER CYCLE
//
// The engine retires at most one obligation per cycle, because a reporting
// channel has one slot and an engine that can emit three failures in a cycle
// cannot say which one it was. A drain therefore takes as many cycles as
// there are obligations, and the testbench holds `eot` long enough for it.
module usb_assert_engine #(
  parameter integer N_OBL   = 4,   // obligations trackable at once
  parameter integer MIN_LAT = 2,   // a response sooner than this is not ours
  parameter integer MAX_LAT = 12   // a response later than this is a failure
) (
  input  wire       clk,
  input  wire       rst_n,

  input  wire       trigger,    // the antecedent fired: an obligation begins
  input  wire       response,   // the consequent fired: one is discharged
  input  wire       eot,        // end of test: drain and report

  output wire [2:0] outstanding,
  output wire [4:0] oldest_age,
  output wire       pass_pulse,
  output wire       fail_pulse,
  output wire [2:0] fail_code,

  output reg [31:0] n_triggers,
  output reg [31:0] n_pass,
  output reg [31:0] n_late,
  output reg [31:0] n_early,
  output reg [31:0] n_spurious,
  output reg [31:0] n_overflow,
  output reg [31:0] n_dangling
);

  localparam [2:0] F_NONE     = 3'd0,
                   F_LATE     = 3'd1,  // no response within MAX_LAT
                   F_EARLY    = 3'd2,  // a response before MIN_LAT
                   F_SPURIOUS = 3'd3,  // a response with nothing outstanding
                   F_OVERFLOW = 3'd4,  // more obligations than trackable
                   F_DANGLING = 3'd5;  // still outstanding at end of test

  // ---- The queue of outstanding obligations. Just their ages: an
  // ---- obligation has no other content, because the only question ever
  // ---- asked of it is "how long has it been waiting".
  reg [4:0] age_r [0:N_OBL-1];
  reg [2:0] cnt_r;
  reg [2:0] fc_r;
  reg       pass_r, fail_r;

  assign outstanding = cnt_r;
  assign oldest_age  = (cnt_r == 3'd0) ? 5'd0 : age_r[0];
  assign pass_pulse  = pass_r;
  assign fail_pulse  = fail_r;
  assign fail_code   = fc_r;

  integer i;
  reg [4:0] age_n [0:N_OBL-1];
  reg [2:0] cnt_n, fc_n;
  reg       pass_n, fail_n;
  reg       retired;            // an obligation left the queue this cycle

  // Shift the queue down by one: the OLDEST leaves. FIFO order is not a
  // style choice -- responses arrive in the order their requests were made,
  // so retiring the newest would charge the wrong obligation's age against
  // the window and let a genuinely late response pass as a prompt one.
  task retire_oldest;
    integer k;
    begin
      for (k = 0; k < N_OBL - 1; k = k + 1) age_n[k] = age_n[k+1];
      age_n[N_OBL-1] = 5'd0;
      cnt_n = cnt_n - 3'd1;
    end
  endtask

  always @* begin
    for (i = 0; i < N_OBL; i = i + 1) age_n[i] = age_r[i];
    cnt_n   = cnt_r;
    fc_n    = F_NONE;
    pass_n  = 1'b0;
    fail_n  = 1'b0;
    retired = 1'b0;

    // ---- 1. END OF TEST drains first, and every survivor is a failure. ----
    if (eot) begin
      if (cnt_r != 3'd0) begin
        retire_oldest;
        retired = 1'b1;
        fail_n  = 1'b1;
        fc_n    = F_DANGLING;
      end
    end else begin
      // ---- 2. A response discharges the OLDEST outstanding obligation. ----
      if (response) begin
        if (cnt_r == 3'd0) begin
          // Nothing was outstanding. A response to nothing is not harmless:
          // it means the consequent can fire on its own, so a later real
          // obligation could be discharged by a signal that has nothing to
          // do with it.
          fail_n = 1'b1;
          fc_n   = F_SPURIOUS;
        end else begin
          if (age_r[0] < MIN_LAT[4:0]) begin
            // Too soon to be ours. See note 1 in the header.
            fail_n = 1'b1;
            fc_n   = F_EARLY;
          end else if (age_r[0] >= MAX_LAT[4:0]) begin
            // ---- The UPPER edge, stated HERE and not left to the timeout.
            //
            // It is tempting to leave this out: the timeout below retires
            // anything that reaches MAX_LAT, so surely a response can never
            // see an obligation that old. It can -- on the exact cycle the
            // age reaches MAX_LAT, because the response is evaluated first.
            //
            // With the test omitted, that one tie cycle is a PASS, and which
            // way it goes is decided by the order of two `if` statements
            // rather than by the specification. A bound whose boundary case
            // depends on evaluation order is not a bound anybody can quote.
            //
            // The window is MIN_LAT <= age < MAX_LAT, written in one place.
            fail_n = 1'b1;
            fc_n   = F_LATE;
          end else begin
            pass_n = 1'b1;
          end
          retire_oldest;
          retired = 1'b1;
        end
      end

      // ---- 3. The timeout, checked on the oldest, and only if nothing was
      // ---- retired this cycle -- one event per cycle.
      if (!retired && (cnt_r != 3'd0) && (age_r[0] >= MAX_LAT[4:0])) begin
        retire_oldest;
        retired = 1'b1;
        fail_n  = 1'b1;
        fc_n    = F_LATE;
      end

      // ---- 4. Everything still outstanding gets one cycle older. ----
      //
      // Done BEFORE the new obligation is pushed, not after, so that the
      // new one starts at age 0 and is not charged for the cycle it was
      // created in. Ageing after the push needs an exclusion for the
      // just-pushed entry, and that exclusion is exactly the kind of
      // condition that is written once, is wrong by one, and is never
      // noticed because MIN_LAT hides it.
      for (i = 0; i < N_OBL; i = i + 1)
        if ((i[2:0] < cnt_n) && (age_n[i] < MAX_LAT[4:0]))
          age_n[i] = age_n[i] + 5'd1;

      // ---- 5. A new obligation. Overflow is REPORTED, never dropped. ----
      if (trigger) begin
        if (cnt_n >= N_OBL[2:0]) begin
          // The queue is full. Saying so is the point: silently dropping the
          // obligation makes the engine stop checking precisely when the
          // design is busiest.
          fail_n = 1'b1;
          fc_n   = F_OVERFLOW;
        end else begin
          age_n[cnt_n] = 5'd0;
          cnt_n = cnt_n + 3'd1;
        end
      end
    end
  end

  always @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      for (i = 0; i < N_OBL; i = i + 1) age_r[i] <= 5'd0;
      cnt_r      <= 3'd0;
      fc_r       <= F_NONE;
      pass_r     <= 1'b0;
      fail_r     <= 1'b0;
      n_triggers <= 32'd0;
      n_pass     <= 32'd0;
      n_late     <= 32'd0;
      n_early    <= 32'd0;
      n_spurious <= 32'd0;
      n_overflow <= 32'd0;
      n_dangling <= 32'd0;
    end else begin
      for (i = 0; i < N_OBL; i = i + 1) age_r[i] <= age_n[i];
      cnt_r  <= cnt_n;
      fc_r   <= fc_n;
      pass_r <= pass_n;
      fail_r <= fail_n;

      if (trigger && !eot) n_triggers <= n_triggers + 32'd1;
      if (pass_n)          n_pass     <= n_pass + 32'd1;

      // The per-cause counters are driven by the SAME pulse as the failure,
      // so they sum to the failure total by construction (chapter 23.4).
      if (fail_n) begin
        case (fc_n)
          F_LATE:     n_late     <= n_late     + 32'd1;
          F_EARLY:    n_early    <= n_early    + 32'd1;
          F_SPURIOUS: n_spurious <= n_spurious + 32'd1;
          F_OVERFLOW: n_overflow <= n_overflow + 32'd1;
          F_DANGLING: n_dangling <= n_dangling + 32'd1;
          default: ;
        endcase
      end
    end
  end
endmodule

// usb_assert_engine -- what an assertion actually is when you build one, and
// the four things every real liveness check needs that "eventually" does not
// give you.
//
// THE PROPERTY EVERYBODY WANTS TO WRITE
//
//     every request is eventually answered
//
// It is unimplementable, unsynthesisable, and uncheckable in a finite
// simulation. "Eventually" has no failing case: at any moment during a run
// the answer to "has it been answered yet?" is either yes or NOT YET, and not
// yet is not a failure. A simulation that ends with the request outstanding
// has not disproved the property -- it has simply stopped early.
//
// So every liveness check that exists in practice is a BOUNDED one:
//
//     every request is answered within MAX_LAT cycles
//
// and choosing MAX_LAT is the whole job. This block is that check, built as
// hardware, and the four things it needs are the four things a hand-written
// timer usually lacks.
//
// 1. A WINDOW HAS TWO EDGES
//
// MAX_LAT alone accepts a response that arrives IMPOSSIBLY EARLY -- one cycle
// after the request, when the pipeline that produces it is four stages deep.
// Such a response did not come from this request. It came from the previous
// one, or from a signal that is stuck asserted, and either way the check has
// passed while the design is broken.
//
//     MIN_LAT is not paranoia. It is the half of the window that
//     catches a response to the WRONG request.
//
// 2. OBLIGATIONS OVERLAP, SO ONE TIMER IS NOT ENOUGH
//
// A second request can arrive before the first is answered. With a single
// timer there is no way to tell which response belongs to which request, and
// the usual implementation -- clear the timer on any response -- lets ONE
// response satisfy BOTH obligations. The bus then drops a response for every
// overlapping pair, for ever, and the check never fires.
//
// An engine needs a QUEUE of outstanding obligations, retired in order.
//
// 3. RUNNING OUT OF TRACKING CAPACITY IS A FAILURE, NOT A LIMIT
//
// The queue is finite. When it is full and another request arrives, there are
// two choices: report it, or drop it. Dropping it is how a checker silently
// stops checking exactly when the design is at its busiest -- which is when
// it is most likely to be wrong. So overflow is a reported failure.
//
// 4. AN UNFINISHED OBLIGATION IS NOT A PASS
//
// This is the one that is missed most often. At the end of the run, whatever
// is still outstanding has NOT been answered. It is not "inconclusive" and it
// is not "still in flight" -- the simulation is over and nothing more is
// coming.
//
//     A run that ends with obligations outstanding and reports
//     zero failures has not verified the property. It has run
//     out of time while the property was still being tested,
//     and called that success.
//
// So `eot` drains the queue and every survivor is a DANGLING failure.
//
// ONE EVENT PER CYCLE
//
// The engine retires at most one obligation per cycle, because a reporting
// channel has one slot and an engine that can emit three failures in a cycle
// cannot say which one it was. A drain therefore takes as many cycles as
// there are obligations, and the testbench holds `eot` long enough for it.
package usb_ae_pkg;
  // The five ways an obligation can fail, named. F_DANGLING is the one that
  // is usually missing, and it is the one that decides whether a run that
  // ended early counts as a pass.
  typedef enum logic [2:0] {
    F_NONE     = 3'd0,
    F_LATE     = 3'd1,   // no response within MAX_LAT
    F_EARLY    = 3'd2,   // a response before MIN_LAT
    F_SPURIOUS = 3'd3,   // a response with nothing outstanding
    F_OVERFLOW = 3'd4,   // more obligations than the engine can track
    F_DANGLING = 3'd5    // still outstanding at end of test
  } fail_e;
endpackage

module usb_assert_engine
  import usb_ae_pkg::*;
 #(
  parameter int N_OBL   = 4,   // obligations trackable at once
  parameter int MIN_LAT = 2,   // a response sooner than this is not ours
  parameter int MAX_LAT = 12   // a response later than this is a failure
) (
  input  logic       clk,
  input  logic       rst_n,

  input  logic       trigger,    // the antecedent fired: an obligation begins
  input  logic       response,   // the consequent fired: one is discharged
  input  logic       eot,        // end of test: drain and report

  output logic [2:0] outstanding,
  output logic [4:0] oldest_age,
  output logic       pass_pulse,
  output logic       fail_pulse,
  output fail_e      fail_code,

  output logic [31:0] n_triggers,
  output logic [31:0] n_pass,
  output logic [31:0] n_late,
  output logic [31:0] n_early,
  output logic [31:0] n_spurious,
  output logic [31:0] n_overflow,
  output logic [31:0] n_dangling
);

  // ---- The queue of outstanding obligations. Just their ages: an
  // ---- obligation has no other content, because the only question ever
  // ---- asked of it is "how long has it been waiting".
  logic [4:0] age_r [N_OBL];
  logic [2:0] cnt_r;
  fail_e      fc_r;
  logic       pass_r, fail_r;

  assign outstanding = cnt_r;
  assign oldest_age  = (cnt_r == 3'd0) ? 5'd0 : age_r[0];
  assign pass_pulse  = pass_r;
  assign fail_pulse  = fail_r;
  assign fail_code   = fc_r;

  int         i;
  logic [4:0] age_n [N_OBL];
  logic [2:0] cnt_n;
  fail_e      fc_n;
  logic       pass_n, fail_n;
  logic       retired;          // an obligation left the queue this cycle

  // Shift the queue down by one: the OLDEST leaves. FIFO order is not a
  // style choice -- responses arrive in the order their requests were made,
  // so retiring the newest would charge the wrong obligation's age against
  // the window and let a genuinely late response pass as a prompt one.
  //
  // Written out at each of the three retirement points rather than shared,
  // because a subprogram that mutates module-level state from inside an
  // always_comb is exactly the construct simulators disagree about.
  `define RETIRE_OLDEST                                       \
      for (int k = 0; k < N_OBL - 1; k++) age_n[k] = age_n[k+1]; \
      age_n[N_OBL-1] = 5'd0;                                  \
      cnt_n = cnt_n - 3'd1;

  always_comb begin
    for (i = 0; i < N_OBL; i++) age_n[i] = age_r[i];
    cnt_n   = cnt_r;
    fc_n    = F_NONE;
    pass_n  = 1'b0;
    fail_n  = 1'b0;
    retired = 1'b0;

    // ---- 1. END OF TEST drains first, and every survivor is a failure. ----
    if (eot) begin
      if (cnt_r != 3'd0) begin
        `RETIRE_OLDEST
        retired = 1'b1;
        fail_n  = 1'b1;
        fc_n    = F_DANGLING;
      end
    end else begin
      // ---- 2. A response discharges the OLDEST outstanding obligation. ----
      if (response) begin
        if (cnt_r == 3'd0) begin
          // Nothing was outstanding. A response to nothing is not harmless:
          // it means the consequent can fire on its own, so a later real
          // obligation could be discharged by a signal that has nothing to
          // do with it.
          fail_n = 1'b1;
          fc_n   = F_SPURIOUS;
        end else begin
          if (age_r[0] < 5'(MIN_LAT)) begin
            // Too soon to be ours. See note 1 in the header.
            fail_n = 1'b1;
            fc_n   = F_EARLY;
          end else if (age_r[0] >= 5'(MAX_LAT)) begin
            // ---- The UPPER edge, stated HERE and not left to the timeout.
            //
            // It is tempting to leave this out: the timeout below retires
            // anything that reaches MAX_LAT, so surely a response can never
            // see an obligation that old. It can -- on the exact cycle the
            // age reaches MAX_LAT, because the response is evaluated first.
            //
            // With the test omitted, that one tie cycle is a PASS, and which
            // way it goes is decided by the order of two `if` statements
            // rather than by the specification. A bound whose boundary case
            // depends on evaluation order is not a bound anybody can quote.
            //
            // The window is MIN_LAT <= age < MAX_LAT, written in one place.
            fail_n = 1'b1;
            fc_n   = F_LATE;
          end else begin
            pass_n = 1'b1;
          end
          `RETIRE_OLDEST
          retired = 1'b1;
        end
      end

      // ---- 3. The timeout, checked on the oldest, and only if nothing was
      // ---- retired this cycle -- one event per cycle.
      if (!retired && (cnt_r != 3'd0) && (age_r[0] >= 5'(MAX_LAT))) begin
        `RETIRE_OLDEST
        retired = 1'b1;
        fail_n  = 1'b1;
        fc_n    = F_LATE;
      end

      // ---- 4. Everything still outstanding gets one cycle older. ----
      //
      // Done BEFORE the new obligation is pushed, not after, so that the
      // new one starts at age 0 and is not charged for the cycle it was
      // created in. Ageing after the push needs an exclusion for the
      // just-pushed entry, and that exclusion is exactly the kind of
      // condition that is written once, is wrong by one, and is never
      // noticed because MIN_LAT hides it.
      for (i = 0; i < N_OBL; i++)
        if ((3'(i) < cnt_n) && (age_n[i] < 5'(MAX_LAT)))
          age_n[i] = age_n[i] + 5'd1;

      // ---- 5. A new obligation. Overflow is REPORTED, never dropped. ----
      if (trigger) begin
        if (cnt_n >= 3'(N_OBL)) begin
          // The queue is full. Saying so is the point: silently dropping the
          // obligation makes the engine stop checking precisely when the
          // design is busiest.
          fail_n = 1'b1;
          fc_n   = F_OVERFLOW;
        end else begin
          age_n[cnt_n] = 5'd0;
          cnt_n = cnt_n + 3'd1;
        end
      end
    end
  end

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      for (i = 0; i < N_OBL; i++) age_r[i] <= 5'd0;
      cnt_r      <= 3'd0;
      fc_r       <= F_NONE;
      pass_r     <= 1'b0;
      fail_r     <= 1'b0;
      n_triggers <= 32'd0;
      n_pass     <= 32'd0;
      n_late     <= 32'd0;
      n_early    <= 32'd0;
      n_spurious <= 32'd0;
      n_overflow <= 32'd0;
      n_dangling <= 32'd0;
    end else begin
      for (i = 0; i < N_OBL; i++) age_r[i] <= age_n[i];
      cnt_r  <= cnt_n;
      fc_r   <= fc_n;
      pass_r <= pass_n;
      fail_r <= fail_n;

      if (trigger && !eot) n_triggers <= n_triggers + 32'd1;
      if (pass_n)          n_pass     <= n_pass + 32'd1;

      // The per-cause counters are driven by the SAME pulse as the failure,
      // so they sum to the failure total by construction (chapter 23.4).
      if (fail_n) begin
        case (fc_n)
          F_LATE:     n_late     <= n_late     + 32'd1;
          F_EARLY:    n_early    <= n_early    + 32'd1;
          F_SPURIOUS: n_spurious <= n_spurious + 32'd1;
          F_OVERFLOW: n_overflow <= n_overflow + 32'd1;
          F_DANGLING: n_dangling <= n_dangling + 32'd1;
          default: ;
        endcase
      end
    end
  end
endmodule

-- usb_assert_engine -- what an assertion actually is when you build one, and
-- the four things every real liveness check needs that "eventually" does not
-- give you.
--
-- THE PROPERTY EVERYBODY WANTS TO WRITE
--
--     every request is eventually answered
--
-- It is unimplementable, unsynthesisable, and uncheckable in a finite
-- simulation. "Eventually" has no failing case: at any moment during a run
-- the answer to "has it been answered yet?" is either yes or NOT YET, and not
-- yet is not a failure. A simulation that ends with the request outstanding
-- has not disproved the property -- it has simply stopped early.
--
-- So every liveness check that exists in practice is a BOUNDED one:
--
--     every request is answered within MAX_LAT cycles
--
-- and choosing MAX_LAT is the whole job. This block is that check, built as
-- hardware, and the four things it needs are the four things a hand-written
-- timer usually lacks.
--
-- 1. A WINDOW HAS TWO EDGES
--
-- MAX_LAT alone accepts a response that arrives IMPOSSIBLY EARLY -- one cycle
-- after the request, when the pipeline that produces it is four stages deep.
-- Such a response did not come from this request. It came from the previous
-- one, or from a signal that is stuck asserted, and either way the check has
-- passed while the design is broken.
--
--     MIN_LAT is not paranoia. It is the half of the window that
--     catches a response to the WRONG request.
--
-- 2. OBLIGATIONS OVERLAP, SO ONE TIMER IS NOT ENOUGH
--
-- A second request can arrive before the first is answered. With a single
-- timer there is no way to tell which response belongs to which request, and
-- the usual implementation -- clear the timer on any response -- lets ONE
-- response satisfy BOTH obligations. The bus then drops a response for every
-- overlapping pair, for ever, and the check never fires.
--
-- An engine needs a QUEUE of outstanding obligations, retired in order.
--
-- 3. RUNNING OUT OF TRACKING CAPACITY IS A FAILURE, NOT A LIMIT
--
-- The queue is finite. When it is full and another request arrives, there are
-- two choices: report it, or drop it. Dropping it is how a checker silently
-- stops checking exactly when the design is at its busiest -- which is when
-- it is most likely to be wrong. So overflow is a reported failure.
--
-- 4. AN UNFINISHED OBLIGATION IS NOT A PASS
--
-- This is the one that is missed most often. At the end of the run, whatever
-- is still outstanding has NOT been answered. It is not "inconclusive" and it
-- is not "still in flight" -- the simulation is over and nothing more is
-- coming.
--
--     A run that ends with obligations outstanding and reports
--     zero failures has not verified the property. It has run
--     out of time while the property was still being tested,
--     and called that success.
--
-- So `eot` drains the queue and every survivor is a DANGLING failure.
--
-- ONE EVENT PER CYCLE
--
-- The engine retires at most one obligation per cycle, because a reporting
-- channel has one slot and an engine that can emit three failures in a cycle
-- cannot say which one it was. A drain therefore takes as many cycles as
-- there are obligations, and the testbench holds `eot` long enough for it.
library ieee;
use ieee.std_logic_1164.all;

package usb_ae_pkg is
  -- The five ways an obligation can fail, named. F_DANGLING is the one that
  -- is usually missing, and it is the one that decides whether a run that
  -- ended early counts as a pass.
  type fail_t is (F_NONE, F_LATE, F_EARLY, F_SPURIOUS, F_OVERFLOW, F_DANGLING);
  function fc_code (f : fail_t) return std_logic_vector;
end package usb_ae_pkg;

package body usb_ae_pkg is
  -- Written out rather than derived from position, so the encoding is pinned
  -- to the same numbers the Verilog and SystemVerilog use.
  function fc_code (f : fail_t) return std_logic_vector is
  begin
    case f is
      when F_NONE     => return "000";
      when F_LATE     => return "001";
      when F_EARLY    => return "010";
      when F_SPURIOUS => return "011";
      when F_OVERFLOW => return "100";
      when F_DANGLING => return "101";
    end case;
  end function;
end package body usb_ae_pkg;

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

entity usb_assert_engine is
  generic (
    N_OBL   : integer := 4;   -- obligations trackable at once
    MIN_LAT : integer := 2;   -- a response sooner than this is not ours
    MAX_LAT : integer := 12   -- a response later than this is a failure
  );
  port (
    clk         : in  std_logic;
    rst_n       : in  std_logic;

    trigger     : in  std_logic;   -- the antecedent fired
    response    : in  std_logic;   -- the consequent fired
    eot         : in  std_logic;   -- end of test: drain and report

    outstanding : out std_logic_vector(2 downto 0);
    oldest_age  : out std_logic_vector(4 downto 0);
    pass_pulse  : out std_logic;
    fail_pulse  : out std_logic;
    fail_code   : out std_logic_vector(2 downto 0);

    n_triggers  : out std_logic_vector(31 downto 0);
    n_pass      : out std_logic_vector(31 downto 0);
    n_late      : out std_logic_vector(31 downto 0);
    n_early     : out std_logic_vector(31 downto 0);
    n_spurious  : out std_logic_vector(31 downto 0);
    n_overflow  : out std_logic_vector(31 downto 0);
    n_dangling  : out std_logic_vector(31 downto 0)
  );
end entity usb_assert_engine;

architecture rtl of usb_assert_engine is

  type age_arr is array (0 to N_OBL-1) of unsigned(4 downto 0);

  signal age_r  : age_arr := (others => (others => '0'));
  signal cnt_r  : unsigned(2 downto 0) := (others => '0');
  signal fc_r   : fail_t := F_NONE;
  signal pass_r, fail_r : std_logic := '0';

  -- Accumulators are held as unsigned rather than as range-constrained
  -- integers: a constrained integer aborts simulation on overflow, which
  -- turns a mutation into a crash instead of a measured kill.
  signal c_trg, c_p, c_late : unsigned(31 downto 0) := (others => '0');
  signal c_early, c_spur, c_ovf, c_dng : unsigned(31 downto 0) := (others => '0');

begin

  outstanding <= std_logic_vector(cnt_r);
  oldest_age  <= (others => '0') when cnt_r = 0
                 else std_logic_vector(age_r(0));
  pass_pulse  <= pass_r;
  fail_pulse  <= fail_r;
  fail_code   <= fc_code(fc_r);

  n_triggers <= std_logic_vector(c_trg);
  n_pass     <= std_logic_vector(c_p);
  n_late     <= std_logic_vector(c_late);
  n_early    <= std_logic_vector(c_early);
  n_spurious <= std_logic_vector(c_spur);
  n_overflow <= std_logic_vector(c_ovf);
  n_dangling <= std_logic_vector(c_dng);

  process (clk, rst_n)
    variable na  : age_arr;
    variable nc  : unsigned(2 downto 0);
    variable nfc : fail_t;
    variable np, nf, ret : std_logic;

    -- Shift the queue down by one: the OLDEST leaves. FIFO order is not a
    -- style choice -- responses arrive in the order their requests were
    -- made, so retiring the newest would charge the wrong obligation's age
    -- against the window and let a genuinely late response pass as a
    -- prompt one.
    procedure retire_oldest is
    begin
      for k in 0 to N_OBL - 2 loop
        na(k) := na(k+1);
      end loop;
      na(N_OBL-1) := (others => '0');
      nc := nc - 1;
    end procedure;
  begin
    if rst_n = '0' then
      age_r   <= (others => (others => '0'));
      cnt_r   <= (others => '0');
      fc_r    <= F_NONE;
      pass_r  <= '0';
      fail_r  <= '0';
      c_trg   <= (others => '0');
      c_p     <= (others => '0');
      c_late  <= (others => '0');
      c_early <= (others => '0');
      c_spur  <= (others => '0');
      c_ovf   <= (others => '0');
      c_dng   <= (others => '0');
    elsif rising_edge(clk) then
      na  := age_r;
      nc  := cnt_r;
      nfc := F_NONE;
      np  := '0'; nf := '0'; ret := '0';

      -- ---- 1. END OF TEST drains first, and every survivor is a failure. --
      if eot = '1' then
        if cnt_r /= 0 then
          retire_oldest;
          ret := '1'; nf := '1'; nfc := F_DANGLING;
        end if;
      else
        -- ---- 2. A response discharges the OLDEST outstanding obligation. --
        if response = '1' then
          if cnt_r = 0 then
            -- Nothing was outstanding. A response to nothing is not
            -- harmless: it means the consequent can fire on its own, so a
            -- later real obligation could be discharged by a signal that
            -- has nothing to do with it.
            nf := '1'; nfc := F_SPURIOUS;
          else
            if age_r(0) < to_unsigned(MIN_LAT, 5) then
              -- Too soon to be ours. See note 1 in the header.
              nf := '1'; nfc := F_EARLY;
            elsif age_r(0) >= to_unsigned(MAX_LAT, 5) then
              -- ---- The UPPER edge, stated HERE and not left to the
              -- ---- timeout.
              --
              -- It is tempting to leave this out: the timeout below retires
              -- anything that reaches MAX_LAT, so surely a response can
              -- never see an obligation that old. It can -- on the exact
              -- cycle the age reaches MAX_LAT, because the response is
              -- evaluated first.
              --
              -- With the test omitted, that one tie cycle is a PASS, and
              -- which way it goes is decided by the order of two branches
              -- rather than by the specification. A bound whose boundary
              -- case depends on evaluation order is not a bound anybody
              -- can quote.
              --
              -- The window is MIN_LAT <= age < MAX_LAT, written in one
              -- place.
              nf := '1'; nfc := F_LATE;
            else
              np := '1';
            end if;
            retire_oldest;
            ret := '1';
          end if;
        end if;

        -- ---- 3. The timeout, checked on the oldest, and only if nothing
        -- ---- was retired this cycle -- one event per cycle.
        if ret = '0' and cnt_r /= 0
           and age_r(0) >= to_unsigned(MAX_LAT, 5) then
          retire_oldest;
          ret := '1'; nf := '1'; nfc := F_LATE;
        end if;

        -- ---- 4. Everything still outstanding gets one cycle older. ----
        --
        -- Done BEFORE the new obligation is pushed, not after, so that the
        -- new one starts at age 0 and is not charged for the cycle it was
        -- created in. Ageing after the push needs an exclusion for the
        -- just-pushed entry, and that exclusion is exactly the kind of
        -- condition that is written once, is wrong by one, and is never
        -- noticed because MIN_LAT hides it.
        for i in 0 to N_OBL - 1 loop
          if to_unsigned(i, 3) < nc and na(i) < to_unsigned(MAX_LAT, 5) then
            na(i) := na(i) + 1;
          end if;
        end loop;

        -- ---- 5. A new obligation. Overflow is REPORTED, never dropped. ---
        if trigger = '1' then
          if nc >= to_unsigned(N_OBL, 3) then
            -- The queue is full. Saying so is the point: silently dropping
            -- the obligation makes the engine stop checking precisely when
            -- the design is busiest.
            nf := '1'; nfc := F_OVERFLOW;
          else
            na(to_integer(nc)) := (others => '0');
            nc := nc + 1;
          end if;
        end if;
      end if;

      age_r  <= na;
      cnt_r  <= nc;
      fc_r   <= nfc;
      pass_r <= np;
      fail_r <= nf;

      if trigger = '1' and eot = '0' then c_trg <= c_trg + 1; end if;
      if np = '1' then c_p <= c_p + 1; end if;

      -- The per-cause counters are driven by the SAME pulse as the failure,
      -- so they sum to the failure total by construction (chapter 23.4).
      if nf = '1' then
        case nfc is
          when F_LATE     => c_late  <= c_late  + 1;
          when F_EARLY    => c_early <= c_early + 1;
          when F_SPURIOUS => c_spur  <= c_spur  + 1;
          when F_OVERFLOW => c_ovf   <= c_ovf   + 1;
          when F_DANGLING => c_dng   <= c_dng   + 1;
          when others     => null;
        end case;
      end if;
    end if;
  end process;

end architecture rtl;

   1.  every queue occupancy 0..N_OBL  x  all 8 combinations of
       {trigger, response, eot}                    =  40 pairs

   2.  every age of the oldest obligation 0..MAX_LAT
       x  {a response arrived, none did}            =  26 pairs

   Both required complete, and every occupancy reached by
   real triggers.

      if (lat < MIN_LAT) begin
        check(n_early == before_f + 1,
              "a response that arrived sooner than MIN_LAT was accepted -- it cannot have been a response to this request");
        check(n_pass == before_p,
              "an impossibly early response was counted as a pass");
      end else if (lat < MAX_LAT) begin
        check(n_pass == before_p + 1,
              "a response inside the window was not accepted");
        check(n_early == before_f && n_late == before_l,
              "a response inside the window was reported as a failure");
      end else begin
        check(n_late == before_l + 1,
              "a response later than MAX_LAT was accepted -- the bound is not a bound");
        check(n_pass == before_p,
              "a response later than MAX_LAT was counted as a pass");
      end

      step(1'b1, 1'b0, 1'b0);          // obligation 1
      idle(MIN_LAT + 2);
      step(1'b1, 1'b0, 1'b0);          // obligation 2, much younger
      step(1'b0, 1'b1, 1'b0);          // one response
      idle(1);
      check(n_pass == before_p + 1,
            "a response was not charged against the OLDEST outstanding obligation -- the engine is not FIFO");
      check(n_early == before_f,
            "a response was charged against a younger obligation and reported as early");

      check(n_dangling == before_f + oc,
            "obligations outstanding at end of test were not reported -- a run that stops while the property is still being tested has not verified it");
      check(n_pass == before_p,
            "an obligation that was never answered was counted as a pass");

// Testbench for usb_assert_engine (Verilog-2005).
//
// WHAT IS EXHAUSTIVE HERE
//
//   1. Every occupancy of the obligation queue, 0 to N_OBL, crossed with
//      all eight combinations of {trigger, response, eot} = 40 pairs, each
//      reached by real triggers and real responses.
//
//   2. Every age of the oldest obligation, 0 to MAX_LAT, crossed with
//      "a response arrived" and "none did" = 26 pairs.
//
// AND THE THINGS THAT ARE NOT SWEEPS
//
//   BOTH EDGES OF THE WINDOW. A response at MAX_LAT-1 must PASS and one at
//   MAX_LAT must FAIL. Checking only the second accepts an engine with no
//   window at all; checking only the first accepts one that never fires.
//
//   FIFO ORDER. Two obligations of different ages, one response: it must be
//   charged against the OLDER. A LIFO engine charges the younger, which is
//   below MIN_LAT, so the discriminator is that a correct engine PASSES here
//   and a LIFO one reports an EARLY failure on perfectly good traffic.
//
//   THE DRAIN. Triggers, then end-of-test, and every survivor must be
//   reported. An engine that simply stops has not passed -- it has run out
//   of time while the property was still being tested.
`timescale 1ns/1ps
module tb_ae_v;

  localparam integer N_OBL   = 4;
  localparam integer MIN_LAT = 2;
  localparam integer MAX_LAT = 12;

  localparam [2:0] F_NONE=3'd0, F_LATE=3'd1, F_EARLY=3'd2,
                   F_SPURIOUS=3'd3, F_OVERFLOW=3'd4, F_DANGLING=3'd5;

  reg clk = 1'b0, rst_n = 1'b0;
  reg trigger = 1'b0, response = 1'b0, eot = 1'b0;

  wire [2:0] outstanding, fail_code;
  wire [4:0] oldest_age;
  wire pass_pulse, fail_pulse;
  wire [31:0] n_triggers, n_pass, n_late, n_early, n_spurious,
              n_overflow, n_dangling;

  usb_assert_engine #(.N_OBL(N_OBL), .MIN_LAT(MIN_LAT), .MAX_LAT(MAX_LAT)) dut (
    .clk(clk), .rst_n(rst_n),
    .trigger(trigger), .response(response), .eot(eot),
    .outstanding(outstanding), .oldest_age(oldest_age),
    .pass_pulse(pass_pulse), .fail_pulse(fail_pulse), .fail_code(fail_code),
    .n_triggers(n_triggers), .n_pass(n_pass), .n_late(n_late),
    .n_early(n_early), .n_spurious(n_spurious), .n_overflow(n_overflow),
    .n_dangling(n_dangling)
  );

  always #5 clk = ~clk;

  integer errors = 0, checks = 0;
  task check(input cond, input [1023:0] msg);
    begin
      checks = checks + 1;
      if (!cond) begin
        errors = errors + 1;
        if (errors <= 25)
          $display("FAIL @%0t: %0s | out=%0d age=%0d pass=%b fail=%b code=%0d",
                   $time, msg, outstanding, oldest_age, pass_pulse,
                   fail_pulse, fail_code);
      end
    end
  endtask

  // ------------------------------------------------------------------
  // The shadow engine. Its own queue, its own ages.
  // ------------------------------------------------------------------
  reg [4:0] m_age [0:N_OBL-1];
  reg [2:0] m_cnt, m_fc;
  reg       m_pass, m_fail;
  integer   m_trg, m_p, m_late, m_early, m_spur, m_ovf, m_dng;

  integer seen_oc [0:39];       // (N_OBL+1) x 8 input combinations
  integer seen_ag [0:25];       // (MAX_LAT+1) x {response, none}
  integer n_oc, n_ag, n_steps;

  task model_reset;
    integer i;
    begin
      for (i = 0; i < N_OBL; i = i + 1) m_age[i] = 5'd0;
      m_cnt = 3'd0; m_fc = F_NONE; m_pass = 1'b0; m_fail = 1'b0;
      m_trg = 0; m_p = 0; m_late = 0; m_early = 0;
      m_spur = 0; m_ovf = 0; m_dng = 0;
      for (i = 0; i < 40; i = i + 1) seen_oc[i] = 0;
      for (i = 0; i < 26; i = i + 1) seen_ag[i] = 0;
      n_oc = 0; n_ag = 0; n_steps = 0;
    end
  endtask

  integer q, ia, ic;
  task step(input tg, input rs, input et);
    reg [4:0] na [0:N_OBL-1];
    reg [2:0] nc, nfc;
    reg np, nf, ret;
    begin
      trigger = tg; response = rs; eot = et;
      #1;

      check(outstanding === m_cnt, "outstanding disagrees with the shadow engine");
      check(oldest_age  === ((m_cnt == 3'd0) ? 5'd0 : m_age[0]),
            "oldest_age disagrees -- the queue is not being aged the way the model says");
      check(pass_pulse  === m_pass, "the pass pulse disagrees");
      check(fail_pulse  === m_fail, "the fail pulse disagrees");
      check(fail_code   === m_fc,   "fail_code disagrees");
      check(!(pass_pulse && fail_pulse),
            "an obligation was reported as both a pass and a failure");
      check(outstanding <= N_OBL[2:0],
            "more obligations are outstanding than the engine can track");
      check(oldest_age <= MAX_LAT[4:0],
            "an obligation aged past MAX_LAT without being reported -- the bound is not a bound");
      check(!((m_cnt == 3'd0) && (oldest_age != 5'd0)),
            "an age is being reported with nothing outstanding");

      // ---- ages are MONOTONIC down the queue: the oldest is at the front.
      // ---- If this is ever false the engine is not FIFO and every window
      // ---- decision after it is charged against the wrong obligation.
      for (q = 0; q + 1 < N_OBL; q = q + 1)
        if (q + 1 < m_cnt)
          check(m_age[q] >= m_age[q+1],
                "the obligation queue is out of order -- it is not FIFO, and the window is being applied to the wrong request");

      ic = m_cnt * 8 + (tg ? 4 : 0) + (rs ? 2 : 0) + (et ? 1 : 0);
      if (seen_oc[ic] == 0) begin seen_oc[ic] = 1; n_oc = n_oc + 1; end
      ia = ((m_cnt == 3'd0) ? 0 : m_age[0]) * 2 + (rs ? 1 : 0);
      if (seen_ag[ia] == 0) begin seen_ag[ia] = 1; n_ag = n_ag + 1; end
      n_steps = n_steps + 1;

      // ---- advance the shadow engine ----
      for (q = 0; q < N_OBL; q = q + 1) na[q] = m_age[q];
      nc = m_cnt; nfc = F_NONE; np = 1'b0; nf = 1'b0; ret = 1'b0;

      if (et) begin
        if (m_cnt != 3'd0) begin
          for (q = 0; q < N_OBL - 1; q = q + 1) na[q] = na[q+1];
          na[N_OBL-1] = 5'd0;
          nc = nc - 3'd1;
          ret = 1'b1; nf = 1'b1; nfc = F_DANGLING;
        end
      end else begin
        if (rs) begin
          if (m_cnt == 3'd0) begin
            nf = 1'b1; nfc = F_SPURIOUS;
          end else begin
            if (m_age[0] < MIN_LAT[4:0]) begin nf = 1'b1; nfc = F_EARLY; end
            else if (m_age[0] >= MAX_LAT[4:0]) begin nf = 1'b1; nfc = F_LATE; end
            else np = 1'b1;
            for (q = 0; q < N_OBL - 1; q = q + 1) na[q] = na[q+1];
            na[N_OBL-1] = 5'd0;
            nc = nc - 3'd1;
            ret = 1'b1;
          end
        end
        if (!ret && (m_cnt != 3'd0) && (m_age[0] >= MAX_LAT[4:0])) begin
          for (q = 0; q < N_OBL - 1; q = q + 1) na[q] = na[q+1];
          na[N_OBL-1] = 5'd0;
          nc = nc - 3'd1;
          ret = 1'b1; nf = 1'b1; nfc = F_LATE;
        end
        for (q = 0; q < N_OBL; q = q + 1)
          if ((q[2:0] < nc) && (na[q] < MAX_LAT[4:0])) na[q] = na[q] + 5'd1;
        if (tg) begin
          if (nc >= N_OBL[2:0]) begin nf = 1'b1; nfc = F_OVERFLOW; end
          else begin na[nc] = 5'd0; nc = nc + 3'd1; end
        end
      end

      for (q = 0; q < N_OBL; q = q + 1) m_age[q] = na[q];
      m_cnt = nc; m_fc = nfc; m_pass = np; m_fail = nf;
      if (tg && !et) m_trg = m_trg + 1;
      if (np) m_p = m_p + 1;
      if (nf) begin
        case (nfc)
          F_LATE:     m_late  = m_late + 1;
          F_EARLY:    m_early = m_early + 1;
          F_SPURIOUS: m_spur  = m_spur + 1;
          F_OVERFLOW: m_ovf   = m_ovf + 1;
          F_DANGLING: m_dng   = m_dng + 1;
          default: ;
        endcase
      end

      @(posedge clk); #1;
      trigger = 1'b0; response = 1'b0; eot = 1'b0;
    end
  endtask

  task idle(input integer n);
    integer i;
    begin for (i = 0; i < n; i = i + 1) step(1'b0, 1'b0, 1'b0); end
  endtask

  // Drain the queue the way the engine provides for -- by asserting eot
  // until it is empty -- never by forcing it.
  task drain;
    integer g;
    begin
      for (g = 0; g < N_OBL + 2; g = g + 1) step(1'b0, 1'b0, 1'b1);
      check(outstanding === 3'd0, "the drain did not empty the obligation queue");
      idle(2);
    end
  endtask

  integer before_p, before_f, before_l, k, lat, oc, cb, a;

  initial begin
    model_reset;
    repeat (3) @(posedge clk);
    rst_n = 1'b1;
    @(posedge clk); #1;

    // ---- Phase A: the state after reset ----
    check(outstanding === 3'd0, "reset left obligations outstanding");
    check(oldest_age  === 5'd0, "reset left an age set");
    check(pass_pulse  === 1'b0, "reset asserted a pass");
    check(fail_pulse  === 1'b0, "reset asserted a failure");

    // ---- Phase B: BOTH EDGES OF THE WINDOW, at every latency. ----
    for (lat = 0; lat <= MAX_LAT + 2; lat = lat + 1) begin
      before_p = n_pass;
      before_f = n_early;
      before_l = n_late;
      step(1'b1, 1'b0, 1'b0);         // trigger
      idle(lat);                       // wait `lat` cycles
      step(1'b0, 1'b1, 1'b0);         // respond
      idle(1);
      if (lat < MIN_LAT) begin
        check(n_early == before_f + 1,
              "a response that arrived sooner than MIN_LAT was accepted -- it cannot have been a response to this request");
        check(n_pass == before_p,
              "an impossibly early response was counted as a pass");
      end else if (lat < MAX_LAT) begin
        check(n_pass == before_p + 1,
              "a response inside the window was not accepted");
        check(n_early == before_f && n_late == before_l,
              "a response inside the window was reported as a failure");
      end else begin
        check(n_late == before_l + 1,
              "a response later than MAX_LAT was accepted -- the bound is not a bound");
        check(n_pass == before_p,
              "a response later than MAX_LAT was counted as a pass");
      end
      drain;
    end

    // ---- Phase C: FIFO ORDER. Two obligations, different ages, one
    // ---- response. It must be charged against the OLDER one -- which is
    // ---- mature, so a correct engine PASSES. A LIFO engine charges the
    // ---- younger one, which is below MIN_LAT, and reports EARLY on
    // ---- perfectly good traffic.
    for (k = 0; k < 40; k = k + 1) begin
      before_p = n_pass;
      before_f = n_early;
      step(1'b1, 1'b0, 1'b0);          // obligation 1
      idle(MIN_LAT + 2);
      step(1'b1, 1'b0, 1'b0);          // obligation 2, much younger
      step(1'b0, 1'b1, 1'b0);          // one response
      idle(1);
      check(n_pass == before_p + 1,
            "a response was not charged against the OLDEST outstanding obligation -- the engine is not FIFO");
      check(n_early == before_f,
            "a response was charged against a younger obligation and reported as early");
      drain;
    end

    // ---- Phase D: OVERLAP. Fill the queue and discharge it in order. ----
    for (oc = 1; oc <= N_OBL; oc = oc + 1) begin
      before_p = n_pass;
      for (k = 0; k < oc; k = k + 1) step(1'b1, 1'b0, 1'b0);
      check(outstanding === oc[2:0],
            "the queue did not accept the obligations offered to it");
      idle(MIN_LAT + 1);
      for (k = 0; k < oc; k = k + 1) step(1'b0, 1'b1, 1'b0);
      idle(1);
      check(n_pass == before_p + oc,
            "one response discharged more than one obligation -- a single timer cannot tell overlapping obligations apart");
      check(outstanding === 3'd0, "obligations were left outstanding");
      drain;
    end

    // ---- Phase E: OVERFLOW is reported, never dropped. ----
    before_f = n_overflow;
    for (k = 0; k < N_OBL; k = k + 1) step(1'b1, 1'b0, 1'b0);
    check(outstanding === N_OBL[2:0], "the queue is not full when it should be");
    step(1'b1, 1'b0, 1'b0);
    idle(1);
    check(n_overflow == before_f + 1,
          "a trigger was silently dropped when the queue was full -- the engine stopped checking exactly when the design was busiest");
    check(outstanding === N_OBL[2:0],
          "the overflowing trigger displaced an obligation already being tracked");
    drain;

    // ---- Phase F: a response with nothing outstanding. ----
    before_f = n_spurious;
    step(1'b0, 1'b1, 1'b0);
    idle(1);
    check(n_spurious == before_f + 1,
          "a response arrived with nothing outstanding and was ignored -- the consequent can fire on its own, so a later real obligation could be discharged by something unrelated");

    // ---- Phase G: THE DRAIN. An unfinished obligation is not a pass. ----
    for (oc = 1; oc <= N_OBL; oc = oc + 1) begin
      before_f = n_dangling;
      before_p = n_pass;
      for (k = 0; k < oc; k = k + 1) step(1'b1, 1'b0, 1'b0);
      idle(2);
      for (k = 0; k < N_OBL + 2; k = k + 1) step(1'b0, 1'b0, 1'b1);
      check(n_dangling == before_f + oc,
            "obligations outstanding at end of test were not reported -- a run that stops while the property is still being tested has not verified it");
      check(n_pass == before_p,
            "an obligation that was never answered was counted as a pass");
      check(outstanding === 3'd0, "the drain left obligations outstanding");
      idle(2);
    end

    // ---- Phase H: EXHAUSTIVE. Every occupancy x every input combination. ----
    for (oc = 0; oc <= N_OBL; oc = oc + 1) begin
      for (cb = 0; cb < 8; cb = cb + 1) begin
        drain;
        for (k = 0; k < oc; k = k + 1) step(1'b1, 1'b0, 1'b0);
        check(outstanding === oc[2:0],
              "the sweep could not reach the occupancy it meant to reach");
        step(cb[2], cb[1], cb[0]);
        step(cb[2], cb[1], cb[0]);
      end
    end

    // ---- Phase I: every age of the oldest obligation, with and without a
    // ---- response, so the window is swept rather than sampled.
    for (a = 0; a <= MAX_LAT; a = a + 1) begin
      for (k = 0; k < 2; k = k + 1) begin
        drain;
        step(1'b1, 1'b0, 1'b0);
        idle(a);
        step(1'b0, k[0], 1'b0);
        idle(1);
      end
    end

    // ---- Phase J: random ----
    for (k = 0; k < 40000; k = k + 1)
      step(($unsigned($random) % 100) < 26,
           ($unsigned($random) % 100) < 24,
           ($unsigned($random) % 1000) < 6);

    // ---- Phase K: and clean traffic afterwards, so the engine is shown to
    // ---- still work rather than merely to have stopped.
    drain;
    before_p = n_pass;
    before_f = n_pass + n_late + n_early + n_spurious + n_overflow + n_dangling;
    for (k = 0; k < 300; k = k + 1) begin
      step(1'b1, 1'b0, 1'b0);
      idle(MIN_LAT + 1);
      step(1'b0, 1'b1, 1'b0);
      idle(1);
    end
    check(n_pass == before_p + 300,
          "the engine stopped accepting clean traffic after the random phase");

    // ---- Final agreement ----
    check(n_triggers === m_trg[31:0],  "n_triggers disagrees with the model");
    check(n_pass     === m_p[31:0],    "n_pass disagrees with the model");
    check(n_late     === m_late[31:0], "n_late disagrees");
    check(n_early    === m_early[31:0],"n_early disagrees");
    check(n_spurious === m_spur[31:0], "n_spurious disagrees");
    check(n_overflow === m_ovf[31:0],  "n_overflow disagrees");
    check(n_dangling === m_dng[31:0],  "n_dangling disagrees");

    check(n_oc == 40, "not every queue occupancy was crossed with every input combination");
    check(n_ag == 26, "not every age of the oldest obligation was seen with and without a response");
    check(n_pass     > 32'd0, "no obligation was ever discharged cleanly");
    check(n_late     > 32'd0, "the MAX_LAT bound was never exercised");
    check(n_early    > 32'd0, "the MIN_LAT bound was never exercised");
    check(n_spurious > 32'd0, "a response with nothing outstanding was never seen");
    check(n_overflow > 32'd0, "the tracking capacity was never exceeded");
    check(n_dangling > 32'd0, "the end-of-test drain was never exercised");

    $display("REACH occupancy-x-input=%0d/40 age-x-response=%0d/26 steps=%0d",
             n_oc, n_ag, n_steps);
    $display("COUNTERS triggers=%0d pass=%0d late=%0d early=%0d spurious=%0d overflow=%0d dangling=%0d",
             n_triggers, n_pass, n_late, n_early, n_spurious, n_overflow, n_dangling);
    $display("%0s: %0d errors in %0d checks", (errors==0)?"PASS":"FAIL", errors, checks);
    $finish;
  end
endmodule

// Testbench for usb_assert_engine (SystemVerilog).
//
// WHAT IS EXHAUSTIVE HERE
//
//   1. Every occupancy of the obligation queue, 0 to N_OBL, crossed with
//      all eight combinations of {trigger, response, eot} = 40 pairs, each
//      reached by real triggers and real responses.
//
//   2. Every age of the oldest obligation, 0 to MAX_LAT, crossed with
//      "a response arrived" and "none did" = 26 pairs.
//
// AND THE THINGS THAT ARE NOT SWEEPS
//
//   BOTH EDGES OF THE WINDOW. A response at MAX_LAT-1 must PASS and one at
//   MAX_LAT must FAIL. Checking only the second accepts an engine with no
//   window at all; checking only the first accepts one that never fires.
//
//   FIFO ORDER. Two obligations of different ages, one response: it must be
//   charged against the OLDER. A LIFO engine charges the younger, which is
//   below MIN_LAT, so the discriminator is that a correct engine PASSES here
//   and a LIFO one reports an EARLY failure on perfectly good traffic.
//
//   THE DRAIN. Triggers, then end-of-test, and every survivor must be
//   reported. An engine that simply stops has not passed -- it has run out
//   of time while the property was still being tested.
`timescale 1ns/1ps
module tb_ae_sv;
  import usb_ae_pkg::*;

  localparam int N_OBL   = 4;
  localparam int MIN_LAT = 2;
  localparam int MAX_LAT = 12;

  logic clk = 1'b0, rst_n = 1'b0;
  logic trigger = 1'b0, response = 1'b0, eot = 1'b0;

  logic [2:0] outstanding;
  fail_e      fail_code;
  logic [4:0] oldest_age;
  logic pass_pulse, fail_pulse;
  logic [31:0] n_triggers, n_pass, n_late, n_early, n_spurious,
               n_overflow, n_dangling;

  usb_assert_engine #(.N_OBL(N_OBL), .MIN_LAT(MIN_LAT), .MAX_LAT(MAX_LAT))
    dut (.*);

  always #5 clk = ~clk;

  int errors = 0, checks = 0;
  task automatic check(input logic cond, input string msg);
    checks++;
    if (!cond) begin
      errors++;
      if (errors <= 25)
        $display("FAIL @%0t: %0s | out=%0d age=%0d pass=%b fail=%b code=%0d",
                 $time, msg, outstanding, oldest_age, pass_pulse,
                 fail_pulse, fail_code);
    end
  endtask

  // ------------------------------------------------------------------
  // The shadow engine. Its own queue, its own ages.
  // ------------------------------------------------------------------
  logic [4:0] m_age [N_OBL];
  logic [2:0] m_cnt;
  fail_e      m_fc;
  logic       m_pass, m_fail;
  int         m_trg, m_p, m_late, m_early, m_spur, m_ovf, m_dng;

  int seen_oc [40];             // (N_OBL+1) x 8 input combinations
  int seen_ag [26];             // (MAX_LAT+1) x {response, none}
  int n_oc, n_ag, n_steps;

  task automatic model_reset();
    foreach (m_age[i]) m_age[i] = '0;
    m_cnt = '0; m_fc = F_NONE; m_pass = 1'b0; m_fail = 1'b0;
    m_trg = 0; m_p = 0; m_late = 0; m_early = 0;
    m_spur = 0; m_ovf = 0; m_dng = 0;
    foreach (seen_oc[i]) seen_oc[i] = 0;
    foreach (seen_ag[i]) seen_ag[i] = 0;
    n_oc = 0; n_ag = 0; n_steps = 0;
  endtask

  int q, ia, ic;
  task automatic step(input logic tg, input logic rs, input logic et);
    logic [4:0] na [N_OBL];
    logic [2:0] nc;
    fail_e      nfc;
    logic np, nf, ret;
    begin
      trigger = tg; response = rs; eot = et;
      #1;

      check(outstanding === m_cnt, "outstanding disagrees with the shadow engine");
      check(oldest_age  === ((m_cnt == 3'd0) ? 5'd0 : m_age[0]),
            "oldest_age disagrees -- the queue is not being aged the way the model says");
      check(pass_pulse  === m_pass, "the pass pulse disagrees");
      check(fail_pulse  === m_fail, "the fail pulse disagrees");
      check(fail_code   === m_fc,   "fail_code disagrees");
      check(!(pass_pulse && fail_pulse),
            "an obligation was reported as both a pass and a failure");
      check(outstanding <= 3'(N_OBL),
            "more obligations are outstanding than the engine can track");
      check(oldest_age <= 5'(MAX_LAT),
            "an obligation aged past MAX_LAT without being reported -- the bound is not a bound");
      check(!((m_cnt == 3'd0) && (oldest_age != 5'd0)),
            "an age is being reported with nothing outstanding");

      // ---- ages are MONOTONIC down the queue: the oldest is at the front.
      // ---- If this is ever false the engine is not FIFO and every window
      // ---- decision after it is charged against the wrong obligation.
      for (q = 0; q + 1 < N_OBL; q++)
        if (q + 1 < m_cnt)
          check(m_age[q] >= m_age[q+1],
                "the obligation queue is out of order -- it is not FIFO, and the window is being applied to the wrong request");

      ic = int'(m_cnt) * 8 + (tg ? 4 : 0) + (rs ? 2 : 0) + (et ? 1 : 0);
      if (seen_oc[ic] == 0) begin seen_oc[ic] = 1; n_oc = n_oc + 1; end
      ia = int'((m_cnt == 3'd0) ? 5'd0 : m_age[0]) * 2 + (rs ? 1 : 0);
      if (seen_ag[ia] == 0) begin seen_ag[ia] = 1; n_ag = n_ag + 1; end
      n_steps = n_steps + 1;

      // ---- advance the shadow engine ----
      for (q = 0; q < N_OBL; q++) na[q] = m_age[q];
      nc = m_cnt; nfc = F_NONE; np = 1'b0; nf = 1'b0; ret = 1'b0;

      if (et) begin
        if (m_cnt != 3'd0) begin
          for (q = 0; q < N_OBL - 1; q++) na[q] = na[q+1];
          na[N_OBL-1] = 5'd0;
          nc = nc - 3'd1;
          ret = 1'b1; nf = 1'b1; nfc = F_DANGLING;
        end
      end else begin
        if (rs) begin
          if (m_cnt == 3'd0) begin
            nf = 1'b1; nfc = F_SPURIOUS;
          end else begin
            if (m_age[0] < 5'(MIN_LAT)) begin nf = 1'b1; nfc = F_EARLY; end
            else if (m_age[0] >= 5'(MAX_LAT)) begin nf = 1'b1; nfc = F_LATE; end
            else np = 1'b1;
            for (q = 0; q < N_OBL - 1; q++) na[q] = na[q+1];
            na[N_OBL-1] = 5'd0;
            nc = nc - 3'd1;
            ret = 1'b1;
          end
        end
        if (!ret && (m_cnt != 3'd0) && (m_age[0] >= 5'(MAX_LAT))) begin
          for (q = 0; q < N_OBL - 1; q++) na[q] = na[q+1];
          na[N_OBL-1] = 5'd0;
          nc = nc - 3'd1;
          ret = 1'b1; nf = 1'b1; nfc = F_LATE;
        end
        for (q = 0; q < N_OBL; q++)
          if ((3'(q) < nc) && (na[q] < 5'(MAX_LAT))) na[q] = na[q] + 5'd1;
        if (tg) begin
          if (nc >= 3'(N_OBL)) begin nf = 1'b1; nfc = F_OVERFLOW; end
          else begin na[nc] = 5'd0; nc = nc + 3'd1; end
        end
      end

      for (q = 0; q < N_OBL; q++) m_age[q] = na[q];
      m_cnt = nc; m_fc = nfc; m_pass = np; m_fail = nf;
      if (tg && !et) m_trg = m_trg + 1;
      if (np) m_p = m_p + 1;
      if (nf) begin
        case (nfc)
          F_LATE:     m_late  = m_late + 1;
          F_EARLY:    m_early = m_early + 1;
          F_SPURIOUS: m_spur  = m_spur + 1;
          F_OVERFLOW: m_ovf   = m_ovf + 1;
          F_DANGLING: m_dng   = m_dng + 1;
          default: ;
        endcase
      end

      @(posedge clk); #1;
      trigger = 1'b0; response = 1'b0; eot = 1'b0;
    end
  endtask

  task automatic idle(input int n);
    repeat (n) step(1'b0, 1'b0, 1'b0);
  endtask

  // Drain the queue the way the engine provides for -- by asserting eot
  // until it is empty -- never by forcing it.
  task automatic drain();
    repeat (N_OBL + 2) step(1'b0, 1'b0, 1'b1);
    check(outstanding === 3'd0, "the drain did not empty the obligation queue");
    idle(2);
  endtask

  int before_p, before_f, before_l, k, lat, oc, cb, a;

  initial begin
    model_reset();
    repeat (3) @(posedge clk);
    rst_n = 1'b1;
    @(posedge clk); #1;

    // ---- Phase A: the state after reset ----
    check(outstanding === 3'd0, "reset left obligations outstanding");
    check(oldest_age  === 5'd0, "reset left an age set");
    check(pass_pulse  === 1'b0, "reset asserted a pass");
    check(fail_pulse  === 1'b0, "reset asserted a failure");

    // ---- Phase B: BOTH EDGES OF THE WINDOW, at every latency. ----
    for (lat = 0; lat <= MAX_LAT + 2; lat++) begin
      before_p = n_pass;
      before_f = n_early;
      before_l = n_late;
      step(1'b1, 1'b0, 1'b0);         // trigger
      idle(lat);                       // wait `lat` cycles
      step(1'b0, 1'b1, 1'b0);         // respond
      idle(1);
      if (lat < MIN_LAT) begin
        check(n_early == before_f + 1,
              "a response that arrived sooner than MIN_LAT was accepted -- it cannot have been a response to this request");
        check(n_pass == before_p,
              "an impossibly early response was counted as a pass");
      end else if (lat < MAX_LAT) begin
        check(n_pass == before_p + 1,
              "a response inside the window was not accepted");
        check(n_early == before_f && n_late == before_l,
              "a response inside the window was reported as a failure");
      end else begin
        check(n_late == before_l + 1,
              "a response later than MAX_LAT was accepted -- the bound is not a bound");
        check(n_pass == before_p,
              "a response later than MAX_LAT was counted as a pass");
      end
      drain();
    end

    // ---- Phase C: FIFO ORDER. Two obligations, different ages, one
    // ---- response. It must be charged against the OLDER one -- which is
    // ---- mature, so a correct engine PASSES. A LIFO engine charges the
    // ---- younger one, which is below MIN_LAT, and reports EARLY on
    // ---- perfectly good traffic.
    for (k = 0; k < 40; k++) begin
      before_p = n_pass;
      before_f = n_early;
      step(1'b1, 1'b0, 1'b0);          // obligation 1
      idle(MIN_LAT + 2);
      step(1'b1, 1'b0, 1'b0);          // obligation 2, much younger
      step(1'b0, 1'b1, 1'b0);          // one response
      idle(1);
      check(n_pass == before_p + 1,
            "a response was not charged against the OLDEST outstanding obligation -- the engine is not FIFO");
      check(n_early == before_f,
            "a response was charged against a younger obligation and reported as early");
      drain();
    end

    // ---- Phase D: OVERLAP. Fill the queue and discharge it in order. ----
    for (oc = 1; oc <= N_OBL; oc++) begin
      before_p = n_pass;
      for (k = 0; k < oc; k++) step(1'b1, 1'b0, 1'b0);
      check(outstanding === 3'(oc),
            "the queue did not accept the obligations offered to it");
      idle(MIN_LAT + 1);
      for (k = 0; k < oc; k++) step(1'b0, 1'b1, 1'b0);
      idle(1);
      check(n_pass == before_p + oc,
            "one response discharged more than one obligation -- a single timer cannot tell overlapping obligations apart");
      check(outstanding === 3'd0, "obligations were left outstanding");
      drain();
    end

    // ---- Phase E: OVERFLOW is reported, never dropped. ----
    before_f = n_overflow;
    for (k = 0; k < N_OBL; k++) step(1'b1, 1'b0, 1'b0);
    check(outstanding === 3'(N_OBL), "the queue is not full when it should be");
    step(1'b1, 1'b0, 1'b0);
    idle(1);
    check(n_overflow == before_f + 1,
          "a trigger was silently dropped when the queue was full -- the engine stopped checking exactly when the design was busiest");
    check(outstanding === 3'(N_OBL),
          "the overflowing trigger displaced an obligation already being tracked");
    drain();

    // ---- Phase F: a response with nothing outstanding. ----
    before_f = n_spurious;
    step(1'b0, 1'b1, 1'b0);
    idle(1);
    check(n_spurious == before_f + 1,
          "a response arrived with nothing outstanding and was ignored -- the consequent can fire on its own, so a later real obligation could be discharged by something unrelated");

    // ---- Phase G: THE DRAIN. An unfinished obligation is not a pass. ----
    for (oc = 1; oc <= N_OBL; oc++) begin
      before_f = n_dangling;
      before_p = n_pass;
      for (k = 0; k < oc; k++) step(1'b1, 1'b0, 1'b0);
      idle(2);
      for (k = 0; k < N_OBL + 2; k++) step(1'b0, 1'b0, 1'b1);
      check(n_dangling == before_f + oc,
            "obligations outstanding at end of test were not reported -- a run that stops while the property is still being tested has not verified it");
      check(n_pass == before_p,
            "an obligation that was never answered was counted as a pass");
      check(outstanding === 3'd0, "the drain left obligations outstanding");
      idle(2);
    end

    // ---- Phase H: EXHAUSTIVE. Every occupancy x every input combination. ----
    for (oc = 0; oc <= N_OBL; oc++) begin
      for (cb = 0; cb < 8; cb++) begin
        drain();
        for (k = 0; k < oc; k++) step(1'b1, 1'b0, 1'b0);
        check(outstanding === 3'(oc),
              "the sweep could not reach the occupancy it meant to reach");
        step(1'(cb[2]), 1'(cb[1]), 1'(cb[0]));
        step(1'(cb[2]), 1'(cb[1]), 1'(cb[0]));
      end
    end

    // ---- Phase I: every age of the oldest obligation, with and without a
    // ---- response, so the window is swept rather than sampled.
    for (a = 0; a <= MAX_LAT; a++) begin
      for (k = 0; k < 2; k++) begin
        drain();
        step(1'b1, 1'b0, 1'b0);
        idle(a);
        step(1'b0, 1'(k[0]), 1'b0);
        idle(1);
      end
    end

    // ---- Phase J: random ----
    for (k = 0; k < 40000; k++)
      step($urandom_range(0,99) < 26,
           $urandom_range(0,99) < 24,
           $urandom_range(0,999) < 6);

    // ---- Phase K: and clean traffic afterwards, so the engine is shown to
    // ---- still work rather than merely to have stopped.
    drain();
    before_p = n_pass;
    before_f = n_pass + n_late + n_early + n_spurious + n_overflow + n_dangling;
    for (k = 0; k < 300; k++) begin
      step(1'b1, 1'b0, 1'b0);
      idle(MIN_LAT + 1);
      step(1'b0, 1'b1, 1'b0);
      idle(1);
    end
    check(n_pass == before_p + 300,
          "the engine stopped accepting clean traffic after the random phase");

    // ---- Final agreement ----
    check(n_triggers === 32'(m_trg),  "n_triggers disagrees with the model");
    check(n_pass     === 32'(m_p),    "n_pass disagrees with the model");
    check(n_late     === 32'(m_late), "n_late disagrees");
    check(n_early    === 32'(m_early),"n_early disagrees");
    check(n_spurious === 32'(m_spur), "n_spurious disagrees");
    check(n_overflow === 32'(m_ovf),  "n_overflow disagrees");
    check(n_dangling === 32'(m_dng),  "n_dangling disagrees");

    check(n_oc == 40, "not every queue occupancy was crossed with every input combination");
    check(n_ag == 26, "not every age of the oldest obligation was seen with and without a response");
    check(n_pass     > 32'd0, "no obligation was ever discharged cleanly");
    check(n_late     > 32'd0, "the MAX_LAT bound was never exercised");
    check(n_early    > 32'd0, "the MIN_LAT bound was never exercised");
    check(n_spurious > 32'd0, "a response with nothing outstanding was never seen");
    check(n_overflow > 32'd0, "the tracking capacity was never exceeded");
    check(n_dangling > 32'd0, "the end-of-test drain was never exercised");

    $display("REACH occupancy-x-input=%0d/40 age-x-response=%0d/26 steps=%0d",
             n_oc, n_ag, n_steps);
    $display("COUNTERS triggers=%0d pass=%0d late=%0d early=%0d spurious=%0d overflow=%0d dangling=%0d",
             n_triggers, n_pass, n_late, n_early, n_spurious, n_overflow, n_dangling);
    $display("%0s: %0d errors in %0d checks", (errors==0)?"PASS":"FAIL", errors, checks);
    $finish;
  end
endmodule