Interframe Gap and Idle

// SYNTHESIZABLE.
//
// Enforces the interframe gap on a wide interface, where the gap is
// quantised to the interface width and cannot always be the nominal
// value.
//
// The mechanism is a DEFICIT: octets of gap this transmitter owes.
//
//   gap shorter than nominal -> deficit increases by the shortfall
//   gap longer than nominal  -> deficit decreases by the excess
//
// Bounded at both ends. The upper bound is what makes the guarantee an
// average rather than a hope: with a deficit that can never exceed
// MAX_DEFICIT, the shortfall over ANY interval is at most MAX_DEFICIT
// octets, so the mean gap over a run of frames converges to the nominal
// from above.
package ifg_pkg;
 
  // NORMATIVE. 96 bit times.
  localparam int unsigned IFG_OCTETS = 12;
 
  // Deficit bound. With a four-octet interface the worst rounding is
  // three octets, so three is the smallest bound that never forces a
  // round-up -- and a larger bound would permit gaps shorter than any
  // alignment requires.
  localparam int unsigned MAX_DEFICIT = 3;
 
  // Shortest single gap this permits: nominal minus the bound.
  localparam int unsigned MIN_SINGLE_GAP = IFG_OCTETS - MAX_DEFICIT;  // 9
 
endpackage
 
module ifg_enforcer
  import ifg_pkg::*;
#(
  // Octets per transfer. A frame may only start on a boundary of this.
  parameter int unsigned LANES = 4,
  parameter int unsigned DEF_W = $clog2(MAX_DEFICIT + 1)
) (
  input  logic clk,
  input  logic rst_n,
 
  input  logic       frame_end,        // last octet of a frame went out
  input  logic [2:0] end_lane,         // lane the frame ended on
  input  logic       want_start,       // a frame is queued and ready
 
  output logic       start_permitted,
  output logic [7:0] gap_emitted,      // octets of gap in the last interval
  output logic       gap_valid,
 
  output logic [DEF_W-1:0] deficit,
  // High when this gap was shortened. Not an error -- a permitted use of
  // the deficit, counted so the rate is visible.
  output logic             gap_shortened
);
 
  logic [7:0] count_q;
  logic       in_gap_q;
 
  // The gap this alignment would produce if the frame started at the next
  // permitted boundary at or after the nominal gap.
  wire [7:0] nominal_end   = 8'(IFG_OCTETS);
  wire [7:0] aligned_up    = ((count_q + 8'(LANES) - 8'd1) / 8'(LANES)) * 8'(LANES);
  wire [7:0] aligned_down  = (count_q / 8'(LANES)) * 8'(LANES);
 
  // Shortening is permitted only when the deficit can absorb it. This one
  // condition is the entire safety argument.
  wire can_shorten = (count_q >= 8'(MIN_SINGLE_GAP)) &&
                     ((8'(IFG_OCTETS) - count_q) <= 8'(MAX_DEFICIT)) &&
                     ((deficit + DEF_W'(8'(IFG_OCTETS) - count_q)) <= DEF_W'(MAX_DEFICIT));
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      count_q         <= '0;
      in_gap_q        <= 1'b0;
      start_permitted <= 1'b0;
      gap_emitted     <= '0;
      gap_valid       <= 1'b0;
      deficit         <= '0;
      gap_shortened   <= 1'b0;
    end else begin
      start_permitted <= 1'b0;
      gap_valid       <= 1'b0;
      gap_shortened   <= 1'b0;
 
      if (frame_end) begin
        in_gap_q <= 1'b1;
        count_q  <= '0;
      end else if (in_gap_q) begin
        count_q <= count_q + 8'(LANES);
 
        if (want_start) begin
          // Two candidate start points exist because of the alignment.
          // Taking the earlier one BORROWS from the deficit; taking the
          // later one REPAYS it.
          if ((count_q >= nominal_end) || can_shorten) begin
            start_permitted <= 1'b1;
            in_gap_q        <= 1'b0;
            gap_emitted     <= count_q;
            gap_valid       <= 1'b1;
 
            if (count_q < 8'(IFG_OCTETS)) begin
              deficit       <= deficit + DEF_W'(8'(IFG_OCTETS) - count_q);
              gap_shortened <= 1'b1;
            end else if (deficit != '0) begin
              // Repay, saturating at zero. Credit does NOT accumulate: a
              // long idle period must not buy the right to a run of short
              // gaps later, which is what an unsaturated counter would do.
              if (DEF_W'(count_q - 8'(IFG_OCTETS)) >= deficit) deficit <= '0;
              else deficit <= deficit - DEF_W'(count_q - 8'(IFG_OCTETS));
            end
          end
        end
      end
    end
  end
 
endmodule

// SYNTHESIZABLE INSTRUMENTATION.
//
// Measures the gap DISTRIBUTION and its running mean, because the
// requirement is a mean and a minimum-only check cannot express it.
//
// The bucket edges are placed to make the three conclusions of Figure 2
// separable in one read:
//
//   below MIN_SINGLE_GAP -> non-conforming, whatever the mean
//   MIN_SINGLE_GAP..11   -> shortened, legitimate if the mean holds
//   exactly 12           -> nominal
//   13 and above         -> repayment, or simply a quiet link
module gap_histogram
  import ifg_pkg::*;
#(
  parameter int unsigned CNT_W   = 40,
  parameter int unsigned NBUCKET = 6,
  parameter int unsigned WINDOW  = 65_536,
  parameter int unsigned WIN_W   = $clog2(WINDOW + 1)
) (
  input  logic clk,
  input  logic rst_n,
  input  logic clear,
 
  input  logic       gap_valid,
  input  logic [7:0] gap_octets,
 
  output logic [CNT_W-1:0] bucket [NBUCKET],
  output logic [CNT_W-1:0] gaps_total,
 
  // The number the requirement is actually about. Reported per window,
  // in tenths of an octet, because the mean of a conforming transmitter
  // sits just above twelve and an integer mean cannot show the margin.
  output logic [CNT_W-1:0] mean_tenths,
  output logic             mean_valid,
 
  // Smallest gap ever observed. Survives `clear`: one gap below the
  // permitted minimum is a finding, and a count of them is not.
  output logic [7:0]       smallest_gap,
  output logic             smallest_valid
);
 
  logic [WIN_W-1:0] win_q;
  logic [CNT_W-1:0] sum_q, n_q;
 
  function automatic int unsigned bucket_of(input logic [7:0] g);
    if      (g <  8'(MIN_SINGLE_GAP)) bucket_of = 0;   // non-conforming
    else if (g <  8'd11)              bucket_of = 1;   // 9..10 shortened
    else if (g == 8'd11)              bucket_of = 2;   // one short
    else if (g == 8'(IFG_OCTETS))     bucket_of = 3;   // nominal
    else if (g <= 8'd16)              bucket_of = 4;   // repayment range
    else                              bucket_of = 5;   // idle link
  endfunction
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      for (int i = 0; i < NBUCKET; i++) bucket[i] <= '0;
      gaps_total     <= '0;
      win_q          <= '0;
      sum_q          <= '0;
      n_q            <= '0;
      mean_tenths    <= '0;
      mean_valid     <= 1'b0;
      smallest_gap   <= '1;
      smallest_valid <= 1'b0;
    end else begin
      mean_valid <= 1'b0;
 
      if (clear) begin
        for (int i = 0; i < NBUCKET; i++) bucket[i] <= '0;
        gaps_total <= '0;
        // smallest_gap deliberately survives.
      end else if (gap_valid) begin
        automatic int unsigned b = bucket_of(gap_octets);
        if (!(&bucket[b]))     bucket[b]  <= bucket[b] + 1'b1;
        if (!(&gaps_total))    gaps_total <= gaps_total + 1'b1;
        sum_q <= sum_q + CNT_W'(gap_octets);
        n_q   <= n_q + 1'b1;
        if (!smallest_valid || (gap_octets < smallest_gap)) begin
          smallest_gap   <= gap_octets;
          smallest_valid <= 1'b1;
        end
      end
 
      if (win_q == WIN_W'(WINDOW - 1)) begin
        // Tenths, and the division happens once per window rather than
        // once per gap -- the same placement argument as Chapter 5.6 §12.
        mean_tenths <= (n_q == '0) ? '0 : ((sum_q * 10) / n_q);
        mean_valid  <= 1'b1;
        sum_q <= '0; n_q <= '0; win_q <= '0;
      end else begin
        win_q <= win_q + 1'b1;
      end
    end
  end
 
endmodule

// SYNTHESIZABLE DIAGNOSTIC.
//
// An undersized gap is rare, consequential, and almost impossible to
// reconstruct after the fact -- so the moment it happens is the only
// moment the context exists.
//
// Captures, on the FIRST occurrence only:
//   - the gap's size
//   - the deficit at the time, which says whether the mechanism was
//     involved or bypassed
//   - the length of the frame that preceded it, because alignment
//     rounding depends on it
//   - whether a frame was queued and waiting, which distinguishes a
//     scheduler bug from a back-pressure event
module undersized_gap_first_cause
  import ifg_pkg::*;
#(
  parameter int unsigned DEF_W = 2,
  parameter int unsigned CNT_W = 32
) (
  input  logic clk,
  input  logic rst_n,
  input  logic clear,
 
  input  logic             gap_valid,
  input  logic [7:0]       gap_octets,
  input  logic [DEF_W-1:0] deficit,
  input  logic [13:0]      prev_frame_octets,
  input  logic             was_queued,
 
  output logic             undersized_seen,
  output logic [7:0]       first_gap,
  output logic [DEF_W-1:0] first_deficit,
  output logic [13:0]      first_prev_frame,
  output logic             first_was_queued,
  output logic [CNT_W-1:0] c_undersized
);
 
  wire undersized = gap_valid && (gap_octets < 8'(MIN_SINGLE_GAP));
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      undersized_seen  <= 1'b0;
      first_gap        <= '0;
      first_deficit    <= '0;
      first_prev_frame <= '0;
      first_was_queued <= 1'b0;
      c_undersized     <= '0;
    end else begin
      if (clear) begin
        c_undersized <= '0;
        // The captured context deliberately survives. It is the only
        // record of an event that cannot be reproduced on demand.
      end
 
      if (undersized) begin
        if (!(&c_undersized)) c_undersized <= c_undersized + 1'b1;
        if (!undersized_seen) begin
          undersized_seen  <= 1'b1;
          first_gap        <= gap_octets;
          first_deficit    <= deficit;
          first_prev_frame <= prev_frame_octets;
          first_was_queued <= was_queued;
        end
      end
    end
  end
 
endmodule

// SYNTHESIZABLE.
//
// Verifies that the symbols occupying the gap are the ones that should be
// there, and counts what is not.
//
// Why this is worth doing at all: on a lightly loaded link, idle is the
// overwhelming majority of what crosses the channel. A bit error rate
// that has not yet produced a single frame error will already have
// produced many idle errors -- so this counter moves FIRST, and moves
// long before anything a user notices.
//
// It is a leading indicator built from a region nothing else examines.
module idle_pattern_monitor
  import ifg_pkg::*;
#(
  // The expected idle codeword for this line code. Chapter 3.5 owns what
  // this actually is; parameterised so the monitor does not encode one
  // code's choice.
  parameter logic [7:0] IDLE_SYMBOL = 8'h07,
  parameter int unsigned CNT_W = 40
) (
  input  logic clk,
  input  logic rst_n,
  input  logic clear,
 
  input  logic       in_gap,
  input  logic       sym_valid,
  input  logic [7:0] sym_data,
  input  logic       sym_is_control,   // control character, not data
 
  output logic [CNT_W-1:0] c_idle_symbols,
  output logic [CNT_W-1:0] c_idle_wrong_value,
  output logic [CNT_W-1:0] c_idle_not_control,
 
  // Errors per million idle symbols in the window that just closed. A
  // RATE, because the raw count grows with link idleness and says nothing
  // on its own.
  output logic [CNT_W-1:0] error_ppm,
  output logic             rate_valid,
  output logic [CNT_W-1:0] worst_ppm
);
 
  logic [CNT_W-1:0] win_sym_q, win_err_q;
  logic [15:0]      win_q;
 
  // The classification. Three outcomes, and the second and third are
  // different faults rather than degrees of one.
  wire idle_ok        = in_gap && sym_valid &&  sym_is_control && (sym_data == IDLE_SYMBOL);
  wire idle_wrong_val = in_gap && sym_valid &&  sym_is_control && (sym_data != IDLE_SYMBOL);
  wire idle_not_ctrl  = in_gap && sym_valid && !sym_is_control;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      c_idle_symbols     <= '0;
      c_idle_wrong_value <= '0;
      c_idle_not_control <= '0;
      win_sym_q          <= '0;
      win_err_q          <= '0;
      win_q              <= '0;
      error_ppm          <= '0;
      rate_valid         <= 1'b0;
      worst_ppm          <= '0;
    end else begin
      rate_valid <= 1'b0;
 
      if (clear) begin
        c_idle_symbols     <= '0;
        c_idle_wrong_value <= '0;
        c_idle_not_control <= '0;
        // worst_ppm deliberately survives: the worst the channel has ever
        // been is a property of the channel, not of a measurement window.
      end else if (in_gap && sym_valid) begin
        c_idle_symbols <= c_idle_symbols + 1'b1;
        win_sym_q      <= win_sym_q + 1'b1;
        if (idle_wrong_val) c_idle_wrong_value <= c_idle_wrong_value + 1'b1;
        if (idle_not_ctrl)  c_idle_not_control <= c_idle_not_control + 1'b1;
        if (idle_wrong_val || idle_not_ctrl) win_err_q <= win_err_q + 1'b1;
      end
 
      if (&win_q) begin
        // A RATE, not a count. The raw count grows with how idle the link
        // is and therefore says nothing on its own.
        error_ppm  <= (win_sym_q == '0) ? '0 : ((win_err_q * 1_000_000) / win_sym_q);
        rate_valid <= 1'b1;
        if (((win_sym_q == '0) ? '0 : ((win_err_q * 1_000_000) / win_sym_q)) > worst_ppm)
          worst_ppm <= (win_sym_q == '0) ? '0 : ((win_err_q * 1_000_000) / win_sym_q);
        win_sym_q <= '0;
        win_err_q <= '0;
        win_q     <= '0;
      end else begin
        win_q <= win_q + 1'b1;
      end
 
      if (idle_ok) begin end   // named for readability; no action needed
    end
  end
 
endmodule

// SYNTHESIZABLE.
//
// The gap is guaranteed STRUCTURALLY: there is no state from which this
// module can assert `tx_start` too early, so the guarantee does not
// depend on a checker being correct or enabled.
//
// Contrast with Section 5, which enforces the gap by computing whether a
// start is permitted. Both are correct; this one cannot be made incorrect
// by a later edit to the permission logic, because there is no permission
// logic -- the timing is a property of the state graph.
module ifg_safe_scheduler
  import ifg_pkg::*;
#(
  parameter int unsigned LANES = 4,
  parameter int unsigned DEF_W = 2
) (
  input  logic clk,
  input  logic rst_n,
 
  input  logic             tx_done,
  input  logic             frame_ready,
  input  logic [DEF_W-1:0] deficit_in,
 
  output logic             tx_start,
  output logic [7:0]       gap_octets,
  output logic             gap_valid,
  output logic [DEF_W-1:0] deficit_out
);
 
  typedef enum logic [1:0] { G_XMIT, G_HOLD, G_ARM, G_GO } g_e;
  g_e         state_q;
  logic [7:0] cnt_q;
 
  // The minimum this state machine will EVER wait. Not a comparison
  // performed at run time -- a bound the state graph cannot cross,
  // because G_HOLD has no exit before the count is reached.
  localparam int unsigned FLOOR = MIN_SINGLE_GAP;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      state_q     <= G_XMIT;
      cnt_q       <= '0;
      tx_start    <= 1'b0;
      gap_octets  <= '0;
      gap_valid   <= 1'b0;
      deficit_out <= '0;
    end else begin
      tx_start  <= 1'b0;
      gap_valid <= 1'b0;
 
      case (state_q)
        G_XMIT: if (tx_done) begin
          state_q <= G_HOLD;
          cnt_q   <= '0;
        end
 
        // The ONLY exit from this state is reaching the floor. No input
        // can shorten it: frame_ready is not read here, and there is no
        // condition on the transition. That is the guarantee.
        G_HOLD: begin
          cnt_q <= cnt_q + 8'(LANES);
          if ((cnt_q + 8'(LANES)) >= 8'(FLOOR)) state_q <= G_ARM;
        end
 
        // Between the floor and the nominal, a start is permitted only if
        // the deficit can absorb the shortfall. This is where the policy
        // lives, and it can only ever make the gap LONGER than G_HOLD
        // already guaranteed.
        G_ARM: begin
          cnt_q <= cnt_q + 8'(LANES);
          if (frame_ready) begin
            if ((cnt_q >= 8'(IFG_OCTETS)) ||
                ((deficit_in + DEF_W'(8'(IFG_OCTETS) - cnt_q)) <= DEF_W'(MAX_DEFICIT)))
              state_q <= G_GO;
          end
        end
 
        G_GO: begin
          tx_start   <= 1'b1;
          gap_octets <= cnt_q;
          gap_valid  <= 1'b1;
          deficit_out <= (cnt_q < 8'(IFG_OCTETS))
                           ? (deficit_in + DEF_W'(8'(IFG_OCTETS) - cnt_q))
                           : ((DEF_W'(cnt_q - 8'(IFG_OCTETS)) >= deficit_in)
                                ? '0 : (deficit_in - DEF_W'(cnt_q - 8'(IFG_OCTETS))));
          state_q    <= G_XMIT;
        end
 
        default: state_q <= G_XMIT;
      endcase
    end
  end
 
endmodule

// ---------------------------------------------------------------------
// P1 -- THE FLOOR. No single gap is ever shorter than the permitted
// minimum, whatever the deficit says. This is the structural guarantee
// of Section 9, asserted so a refactor cannot remove it.
// ---------------------------------------------------------------------
property p_never_below_floor;
  @(posedge clk) disable iff (!rst_n)
    gap_valid |-> (gap_octets >= 8'(MIN_SINGLE_GAP));
endproperty
a_never_below_floor: assert property (p_never_below_floor)
  else $error("gap below the permitted single-gap minimum");
 
// ---------------------------------------------------------------------
// P2 -- The deficit is bounded above. An unbounded deficit still repays
// eventually, which is a weaker guarantee than the one required.
// ---------------------------------------------------------------------
property p_deficit_bounded;
  @(posedge clk) disable iff (!rst_n)
    (deficit <= DEF_W'(MAX_DEFICIT));
endproperty
a_deficit_bounded: assert property (p_deficit_bounded);
 
// ---------------------------------------------------------------------
// P3 -- The deficit saturates at zero. Accumulating CREDIT during an idle
// period would buy a burst of short gaps afterwards -- exactly the burst
// a receiver cannot absorb.
// ---------------------------------------------------------------------
property p_no_credit_accumulation;
  @(posedge clk) disable iff (!rst_n)
    (deficit >= 0) and (gap_valid && gap_octets > 8'(IFG_OCTETS)) |=> (deficit >= '0);
endproperty
a_no_credit_accumulation: assert property (p_no_credit_accumulation);
 
// ---------------------------------------------------------------------
// P4 -- A shortened gap always increases the deficit by exactly the
// shortfall. Shortening without recording it is how the average is lost.
// ---------------------------------------------------------------------
property p_shortfall_is_recorded;
  @(posedge clk) disable iff (!rst_n)
    (gap_valid && gap_octets < 8'(IFG_OCTETS))
      |=> (deficit == $past(deficit) + DEF_W'(8'(IFG_OCTETS) - $past(gap_octets)));
endproperty
a_shortfall_is_recorded: assert property (p_shortfall_is_recorded);
 
// ---------------------------------------------------------------------
// P5 -- A gap may only be shortened when the deficit can absorb it. The
// single safety condition of Section 5.
// ---------------------------------------------------------------------
property p_shorten_only_within_bound;
  @(posedge clk) disable iff (!rst_n)
    (gap_valid && gap_octets < 8'(IFG_OCTETS))
      |-> (($past(deficit) + DEF_W'(8'(IFG_OCTETS) - gap_octets)) <= DEF_W'(MAX_DEFICIT));
endproperty
a_shorten_only_within_bound: assert property (p_shorten_only_within_bound);
 
// ---------------------------------------------------------------------
// P6 -- THE AVERAGE, which is the actual requirement. Over any window,
// the mean gap is at least the nominal. Note the WINDOW in the property:
// a requirement about a mean cannot be written without one.
// ---------------------------------------------------------------------
property p_mean_gap_at_least_nominal;
  @(posedge clk) disable iff (!rst_n)
    mean_valid |-> (mean_tenths >= CNT_W'(IFG_OCTETS * 10));
endproperty
a_mean_gap_at_least_nominal: assert property (p_mean_gap_at_least_nominal);
 
// ---------------------------------------------------------------------
// P7 -- Every frame start is on a lane boundary. The reason the gap
// cannot be a constant in the first place.
// ---------------------------------------------------------------------
property p_start_is_lane_aligned;
  @(posedge clk) disable iff (!rst_n)
    tx_start |-> ((start_octet_index % LANES) == 0);
endproperty
a_start_is_lane_aligned: assert property (p_start_is_lane_aligned);
 
// ---------------------------------------------------------------------
// P8 -- The floor state has no early exit. Written over the state graph
// rather than over the gap value, because this is what makes the
// guarantee structural rather than computed (Section 9).
// ---------------------------------------------------------------------
property p_hold_has_no_early_exit;
  @(posedge clk) disable iff (!rst_n)
    ((state == G_HOLD) && (cnt_q + LANES < FLOOR)) |=> (state == G_HOLD);
endproperty
a_hold_has_no_early_exit: assert property (p_hold_has_no_early_exit);
 
// ---------------------------------------------------------------------
// P9 -- frame_ready cannot shorten the floor. The scheduler must not read
// it in the holding state at all.
// ---------------------------------------------------------------------
property p_ready_does_not_shorten;
  @(posedge clk) disable iff (!rst_n)
    ((state == G_HOLD) && frame_ready) |-> !tx_start;
endproperty
a_ready_does_not_shorten: assert property (p_ready_does_not_shorten);
 
// ---------------------------------------------------------------------
// P10 -- Exactly one histogram bucket per measured gap.
// ---------------------------------------------------------------------
property p_one_bucket_per_gap;
  @(posedge clk) disable iff (!rst_n)
    gap_valid |=> (bucket_sum == $past(bucket_sum) + 1);
endproperty
a_one_bucket_per_gap: assert property (p_one_bucket_per_gap);
 
// ---------------------------------------------------------------------
// P11 -- The non-conforming bucket stays empty on a conforming design.
// A cover on this bucket would be a coverage goal for a BUG.
// ---------------------------------------------------------------------
property p_nonconforming_bucket_empty;
  @(posedge clk) disable iff (!rst_n)
    (bucket[0] == '0);
endproperty
a_nonconforming_bucket_empty: assert property (p_nonconforming_bucket_empty);
 
// ---------------------------------------------------------------------
// P12 -- The mean is reported in tenths. An integer mean cannot separate
// a transmitter that is exactly conforming from one fractionally under.
// ---------------------------------------------------------------------
property p_mean_has_resolution;
  @(posedge clk) disable iff (!rst_n)
    mean_valid |-> (mean_tenths != CNT_W'(0));
endproperty
a_mean_has_resolution: assert property (p_mean_has_resolution);
 
// ---------------------------------------------------------------------
// P13 -- First-cause context is captured once and survives a clear.
// ---------------------------------------------------------------------
property p_first_cause_stable;
  @(posedge clk) disable iff (!rst_n)
    undersized_seen |=> ($stable(first_gap) && $stable(first_deficit) &&
                         $stable(first_prev_frame));
endproperty
a_first_cause_stable: assert property (p_first_cause_stable);
 
// ---------------------------------------------------------------------
// P14 -- Idle symbols are only counted inside a gap. Counting them during
// a frame destroys the denominator the error rate depends on.
// ---------------------------------------------------------------------
property p_idle_counted_only_in_gap;
  @(posedge clk) disable iff (!rst_n)
    (!in_gap) |=> $stable(c_idle_symbols);
endproperty
a_idle_counted_only_in_gap: assert property (p_idle_counted_only_in_gap);
 
// ---------------------------------------------------------------------
// P15 -- The two idle failure classes are disjoint. A symbol is either
// not a control character, or a control character with a wrong value.
// ---------------------------------------------------------------------
property p_idle_failures_disjoint;
  @(posedge clk) disable iff (!rst_n)
    !(idle_wrong_val && idle_not_ctrl);
endproperty
a_idle_failures_disjoint: assert property (p_idle_failures_disjoint);
 
// ---------------------------------------------------------------------
// P16 -- COVERAGE. The deficit reaches its bound. A run that never got
// there never exercised the mechanism this chapter is about.
// ---------------------------------------------------------------------
c_deficit_at_bound: cover property (
  @(posedge clk) disable iff (!rst_n) (deficit == DEF_W'(MAX_DEFICIT))
);
 
// ---------------------------------------------------------------------
// P17 -- COVERAGE. A gap at exactly the permitted floor, which is one
// octet from a violation and is legal.
// ---------------------------------------------------------------------
c_gap_at_floor: cover property (
  @(posedge clk) disable iff (!rst_n)
    (gap_valid && gap_octets == 8'(MIN_SINGLE_GAP))
);
 
// ---------------------------------------------------------------------
// P18 -- COVERAGE. A shortened gap immediately followed by a repayment,
// which is the mechanism completing a cycle rather than merely borrowing.
// ---------------------------------------------------------------------
c_borrow_then_repay: cover property (
  @(posedge clk) disable iff (!rst_n)
    (gap_valid && gap_octets < 8'(IFG_OCTETS))
      ##[1:$] (gap_valid && gap_octets > 8'(IFG_OCTETS))
);