Frame Validity — Runts, Giants and Malformed Frames

// SYNTHESIZABLE.
//
// Produces exactly ONE validity class per frame.
//
// The priority order is not arbitrary and is not a design preference: it
// follows the standard's rule that a frame with several error conditions
// is counted exclusively, by the single status reported upward. Getting
// the order wrong produces counters that are individually plausible and
// collectively wrong.
//
// Order, and why each is where it is:
//
//   1. TRUNCATED     -- carrier lost. There is no complete frame to
//                       classify, so nothing below can be evaluated.
//   2. ALIGNMENT     -- not a whole number of octets. Takes precedence
//                       over FCS by the standard's own definition.
//   3. FCS           -- whole octets, check failed.
//   4. UNDERSIZE     -- below the floor, check PASSED (Chapter 5.6 §8:
//                       a good check means the peer emitted it that way).
//   5. OVERSIZE      -- above the applicable STANDARD maximum.
//   6. VALID
//
// Note what is NOT in this list: anything about a local ceiling. That is
// a different predicate and Section 6 keeps it separate.
package validity_pkg;
 
  typedef enum logic [3:0] {
    V_VALID,
    V_TRUNCATED,     // carrier lost mid-frame
    V_ALIGNMENT,     // not an integral number of octets, check failed
    V_FCS,           // integral octets, check failed
    V_UNDERSIZE,     // below 64 octets, check PASSED
    V_FRAGMENT,      // below 64 octets, check FAILED
    V_OVERSIZE       // above the standard maximum, check passed
  } validity_e;
 
  // NORMATIVE. Chapter 5.6's floor and Chapter 5.7's three maxima.
  localparam int unsigned MIN_FRAME    = 64;
  localparam int unsigned MAX_BASIC    = 1518;
  localparam int unsigned MAX_QTAGGED  = 1522;
  localparam int unsigned MAX_ENVELOPE = 2000;
 
endpackage
 
module frame_validity_classifier
  import validity_pkg::*;
(
  input  logic clk,
  input  logic rst_n,
 
  input  logic        frame_done,
  input  logic [13:0] frame_octets,
  // Bits beyond the last complete octet, 0 to 7. Section 8 produces it.
  input  logic [2:0]  dribble_bits,
  input  logic        fcs_ok,
  input  logic        truncated,
  input  logic [1:0]  tags_present,
 
  output logic        class_valid,
  output validity_e   frame_class,
  // The maximum this frame was judged against, so a reader can see WHICH
  // normative ceiling applied rather than inferring it.
  output logic [13:0] applicable_max
);
 
  // Chapter 5.7 §3: the applicable maximum depends on the frame's own
  // structure, not on configuration. An envelope frame is judged against
  // 2000 whether or not this device would accept one.
  wire [13:0] normative_max = (tags_present == 2'd0) ? 14'(MAX_BASIC)
                            : (tags_present == 2'd1) ? 14'(MAX_QTAGGED)
                                                     : 14'(MAX_ENVELOPE);
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      class_valid    <= 1'b0;
      frame_class    <= V_VALID;
      applicable_max <= 14'(MAX_BASIC);
    end else begin
      class_valid <= frame_done;
 
      if (frame_done) begin
        applicable_max <= normative_max;
 
        // The priority chain of the header comment, in order. Each arm is
        // reached only when every arm above it did not apply, which is
        // what "counted exclusively" means in RTL.
        if (truncated) begin
          frame_class <= V_TRUNCATED;
        end else if (dribble_bits != 3'd0) begin
          // Not a whole number of octets. Takes precedence over the check
          // result even though the check also failed -- Section 3's
          // row c, and the ordering the standard requires.
          frame_class <= V_ALIGNMENT;
        end else if (frame_octets < 14'(MIN_FRAME)) begin
          // Chapter 5.6 §8's split, and the check sequence is the only
          // thing that separates a damaged frame from a peer that emitted
          // a short one deliberately.
          frame_class <= fcs_ok ? V_UNDERSIZE : V_FRAGMENT;
        end else if (!fcs_ok) begin
          frame_class <= V_FCS;
        end else if (frame_octets > normative_max) begin
          frame_class <= V_OVERSIZE;
        end else begin
          frame_class <= V_VALID;
        end
      end
    end
  end
 
endmodule

// SYNTHESIZABLE.
//
// Splits "this frame was rejected" into the two predicates of Section 2
// and refuses to let them be summed.
//
//   NORMATIVE  -- from the classifier. A property of the frame. Every
//        conforming device agrees, and a non-VALID class means somebody
//        emitted or damaged a frame.
//
//   LOCAL      -- this device's ceiling, and whatever else configuration
//        imposes. A property of THIS DEVICE. A frame rejected only here
//        is conformant, and the finding is usually a parameter.
//
// The two outputs are deliberately not combinable into a single "reject"
// signal by this module. A datapath that needs one must form it itself,
// visibly, at a place a reviewer will see.
module validity_predicate_split
  import validity_pkg::*;
(
  input  logic clk,
  input  logic rst_n,
  input  logic clear,
 
  input  logic      class_valid,
  input  validity_e frame_class,
  input  logic [13:0] frame_octets,
  input  logic [13:0] applicable_max,
 
  // Configuration. NOT normative, and named so that nothing downstream
  // can mistake it for a standard limit.
  input  logic [13:0] local_ceiling,
  input  logic [13:0] local_floor,
 
  output logic malformed,             // the frame is at fault
  output logic unacceptable_here,     // this device declined a valid frame
  output logic acceptable,
 
  output logic [31:0] c_malformed,
  output logic [31:0] c_unacceptable_here,
  output logic [31:0] c_acceptable,
 
  // The number that ends most oversize investigations: the smallest
  // frame this device declined that the STANDARD would have allowed.
  // Compare it against local_ceiling and the fix is immediate.
  output logic [13:0] smallest_locally_declined,
  output logic        locally_declined_seen
);
 
  // A frame is malformed if and only if the normative classifier says so.
  // Configuration does not appear in this expression at all, and that is
  // the module's entire point.
  wire is_malformed = class_valid && (frame_class != V_VALID);
 
  // A frame that the standard accepts and this device does not. Note the
  // guard: it can only be true when the frame is NOT malformed, so the
  // two are exclusive by construction rather than by convention.
  wire is_local_only = class_valid && (frame_class == V_VALID) &&
                       ((frame_octets > local_ceiling) ||
                        (frame_octets < local_floor));
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      malformed <= 1'b0; unacceptable_here <= 1'b0; acceptable <= 1'b0;
      c_malformed <= '0; c_unacceptable_here <= '0; c_acceptable <= '0;
      smallest_locally_declined <= '1;
      locally_declined_seen <= 1'b0;
    end else begin
      malformed         <= 1'b0;
      unacceptable_here <= 1'b0;
      acceptable        <= 1'b0;
 
      if (clear) begin
        c_malformed <= '0; c_unacceptable_here <= '0; c_acceptable <= '0;
        // The smallest locally declined size deliberately survives: it is
        // a bound on where the ceiling would have to move, and a routine
        // clear must not erase it.
      end else if (class_valid) begin
        if (is_malformed) begin
          malformed   <= 1'b1;
          c_malformed <= c_malformed + 1'b1;
        end else if (is_local_only) begin
          unacceptable_here   <= 1'b1;
          c_unacceptable_here <= c_unacceptable_here + 1'b1;
          if (!locally_declined_seen || (frame_octets < smallest_locally_declined)) begin
            smallest_locally_declined <= frame_octets;
            locally_declined_seen     <= 1'b1;
          end
        end else begin
          acceptable   <= 1'b1;
          c_acceptable <= c_acceptable + 1'b1;
        end
      end
    end
  end
 
  // The relationship a design must never violate: a local ceiling above
  // the standard maximum is legitimate (jumbo), a local ceiling BELOW the
  // standard minimum is not -- it would reject conforming frames of every
  // size and is always a configuration error.
  // synopsys translate_off
  a_local_floor_sane: assert final (local_floor <= 14'(MIN_FRAME))
    else $fatal(1, "local floor above the standard minimum rejects conforming frames");
  // synopsys translate_on
 
endmodule

// SYNTHESIZABLE.
//
// Counts bits after the last complete octet and reports how many.
//
// The count is what matters, not the values. Section 6: the PRESENCE of
// dribble bits is what selects alignment error over FCS error, so a
// receive path that discards them has discarded its own classification
// evidence.
//
// The module also reports the count rather than a flag, because the
// number is diagnostic: a consistent 4 bits points at a nibble-wide
// width adapter losing a transfer; a varying 1 to 7 points at the
// physical layer.
module alignment_error_detector
  import validity_pkg::*;
#(
  parameter int unsigned CNT_W = 32
) (
  input  logic clk,
  input  logic rst_n,
  input  logic clear,
 
  input  logic frame_start,
  // One bit per clock from the decoder, with an octet boundary marker.
  input  logic bit_valid,
  input  logic octet_complete,
  input  logic carrier,
 
  output logic       frame_done,
  output logic [2:0] dribble_bits,
  output logic       misaligned,
 
  output logic [CNT_W-1:0] c_misaligned,
  // Distribution of dribble counts. A histogram over seven buckets,
  // because WHICH count recurs names the cause.
  output logic [CNT_W-1:0] dribble_hist [7],
 
  // Sticky. At 1 Gb/s and above this must never fire (Section 6), so a
  // single occurrence is a finding about this device rather than a rate
  // to be trended.
  output logic misaligned_seen
);
 
  logic [2:0] partial_q;
  logic       in_frame_q;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      partial_q    <= '0;
      in_frame_q   <= 1'b0;
      frame_done   <= 1'b0;
      dribble_bits <= '0;
      misaligned   <= 1'b0;
      c_misaligned <= '0;
      for (int i = 0; i < 7; i++) dribble_hist[i] <= '0;
      misaligned_seen <= 1'b0;
    end else begin
      frame_done <= 1'b0;
      misaligned <= 1'b0;
 
      if (clear) begin
        c_misaligned <= '0;
        for (int i = 0; i < 7; i++) dribble_hist[i] <= '0;
        // misaligned_seen deliberately survives.
      end
 
      if (frame_start) begin
        partial_q  <= '0;
        in_frame_q <= 1'b1;
      end else if (in_frame_q) begin
        if (octet_complete) begin
          // A complete octet resets the partial count. Everything the
          // check sequence consumed is here.
          partial_q <= '0;
        end else if (bit_valid) begin
          partial_q <= partial_q + 1'b1;
        end
 
        if (!carrier) begin
          // The frame ended. Whatever is in partial_q is the dribble.
          in_frame_q   <= 1'b0;
          frame_done   <= 1'b1;
          dribble_bits <= partial_q;
          if (partial_q != 3'd0) begin
            misaligned      <= 1'b1;
            misaligned_seen <= 1'b1;
            c_misaligned    <= c_misaligned + 1'b1;
            dribble_hist[partial_q - 3'd1] <= dribble_hist[partial_q - 3'd1] + 1'b1;
          end
        end
      end
    end
  end
 
endmodule

// SYNTHESIZABLE.
//
// Handles the dribble bits themselves: they must not enter the check
// computation, must not be delivered to the client, and must not be
// silently dropped without being counted.
//
// Three wrong behaviours, all of which produce a plausible result:
//
//   1. feed them to the CRC engine -- the check now covers a fractional
//      octet, and Chapter 5.8's covered range is violated in a way no
//      peer can see because the frame was going to fail anyway
//   2. round them up into a padded final octet -- the frame becomes a
//      whole number of octets and is misclassified as an FCS error
//   3. discard them without counting -- the frame is misclassified in
//      the other direction, as an FCS error, because the evidence is gone
//
// All three convert an alignment error into an FCS error, which sends the
// investigation from the physical layer to the wrong place.
module dribble_bit_handler
  import validity_pkg::*;
(
  input  logic clk,
  input  logic rst_n,
 
  input  logic       bit_valid,
  input  logic       bit_in,
  input  logic       octet_complete,
  input  logic       carrier,
  input  logic       frame_start,
 
  // To the check engine. Gated so that a partial octet never enters.
  output logic       crc_bit_valid,
  output logic       crc_bit,
 
  // To the client. Likewise.
  output logic       cli_octet_valid,
  output logic [7:0] cli_octet,
 
  // To the classifier of Section 4.
  output logic [2:0] dribble_out,
  output logic       dribble_valid
);
 
  logic [7:0] sh_q;
  logic [2:0] cnt_q;
  logic       in_frame_q;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      sh_q <= '0; cnt_q <= '0; in_frame_q <= 1'b0;
      crc_bit_valid <= 1'b0; crc_bit <= 1'b0;
      cli_octet_valid <= 1'b0; cli_octet <= '0;
      dribble_out <= '0; dribble_valid <= 1'b0;
    end else begin
      crc_bit_valid   <= 1'b0;
      cli_octet_valid <= 1'b0;
      dribble_valid   <= 1'b0;
 
      if (frame_start) begin
        cnt_q      <= '0;
        in_frame_q <= 1'b1;
      end else if (in_frame_q) begin
        if (bit_valid) begin
          sh_q <= {sh_q[6:0], bit_in};
          // Bits enter the CRC one at a time as they arrive -- but only
          // as part of a complete octet, which the gate below enforces.
          if (cnt_q == 3'd7) begin
            cnt_q           <= '0;
            cli_octet_valid <= 1'b1;
            cli_octet       <= {sh_q[6:0], bit_in};
          end else begin
            cnt_q <= cnt_q + 1'b1;
          end
        end
 
        if (!carrier) begin
          in_frame_q    <= 1'b0;
          // Report the leftover count. The BITS themselves go nowhere:
          // not to the check (failure 1), not padded into an octet
          // (failure 2), and not dropped unrecorded (failure 3).
          dribble_out   <= cnt_q;
          dribble_valid <= 1'b1;
          cnt_q         <= '0;
        end
      end
    end
  end
 
  // The gate that keeps a partial octet out of the check. It is written
  // as a separate always_comb rather than folded above so that it is
  // visible: this is Chapter 5.8's covered range, enforced at the one
  // place a fractional octet could sneak into it.
  always_comb begin
    crc_bit_valid = bit_valid && in_frame_q && carrier;
    crc_bit       = bit_in;
  end
 
endmodule

// SYNTHESIZABLE MONITOR.
//
// Verifies the classifier's own invariants, which are unusual in being
// almost entirely about EXCLUSIVITY rather than about values.
//
// Section 3 established that the standard counts a frame by exactly one
// status. A classifier that satisfies that produces counters whose sum
// equals the frame count -- and one that does not produces counters that
// each look right and sum to more than the traffic.
//
// The sum check is the whole monitor, and it is the check nothing else
// performs: every individual counter can be verified against its own
// stimulus, and only the total reveals a frame counted twice.
module validity_conformance_monitor
  import validity_pkg::*;
#(
  parameter int unsigned CNT_W = 32
) (
  input  logic clk,
  input  logic rst_n,
  input  logic clear,
 
  input  logic      class_valid,
  input  validity_e frame_class,
  input  logic      malformed,
  input  logic      unacceptable_here,
  input  logic      acceptable,
 
  input  logic [13:0] frame_octets,
  input  logic [13:0] applicable_max,
  input  logic [2:0]  dribble_bits,
  input  logic        fcs_ok,
 
  output logic [CNT_W-1:0] c_frames,
  output logic [CNT_W-1:0] c_by_class [7],
 
  // Exclusivity violations, which are the only failures this can see.
  output logic             double_counted,
  output logic             unclassified,
  output logic [CNT_W-1:0] c_exclusivity_error,
 
  // Ordering violations: a class that contradicts its own evidence.
  output logic             ordering_error,
  output logic [CNT_W-1:0] c_ordering_error,
 
  output logic             any_violation      // sticky
);
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      c_frames <= '0;
      for (int i = 0; i < 7; i++) c_by_class[i] <= '0;
      double_counted <= 1'b0; unclassified <= 1'b0;
      c_exclusivity_error <= '0;
      ordering_error <= 1'b0; c_ordering_error <= '0;
      any_violation <= 1'b0;
    end else begin
      double_counted <= 1'b0;
      unclassified   <= 1'b0;
      ordering_error <= 1'b0;
 
      if (clear) begin
        c_frames <= '0;
        for (int i = 0; i < 7; i++) c_by_class[i] <= '0;
        c_exclusivity_error <= '0; c_ordering_error <= '0;
        // any_violation deliberately survives.
      end else if (class_valid) begin
        c_frames <= c_frames + 1'b1;
        c_by_class[frame_class] <= c_by_class[frame_class] + 1'b1;
 
        // Exactly one of the three predicate outputs. Section 5 made them
        // exclusive by construction; this checks the construction held.
        if (!$onehot({malformed, unacceptable_here, acceptable})) begin
          if (malformed + unacceptable_here + acceptable > 1) double_counted <= 1'b1;
          else                                                unclassified   <= 1'b1;
          c_exclusivity_error <= c_exclusivity_error + 1'b1;
          any_violation       <= 1'b1;
        end
 
        // The class must be consistent with the evidence that produced
        // it. Each of these is a case the priority chain of Section 4
        // could get wrong while still emitting exactly one class.
        if (((frame_class == V_ALIGNMENT) && (dribble_bits == 3'd0)) ||
            ((frame_class == V_FCS)       && (dribble_bits != 3'd0)) ||
            ((frame_class == V_FCS)       && fcs_ok)                 ||
            ((frame_class == V_UNDERSIZE) && !fcs_ok)                ||
            ((frame_class == V_FRAGMENT)  && fcs_ok)                 ||
            ((frame_class == V_OVERSIZE)  && (frame_octets <= applicable_max))) begin
          ordering_error   <= 1'b1;
          c_ordering_error <= c_ordering_error + 1'b1;
          any_violation    <= 1'b1;
        end
      end
    end
  end
 
endmodule

// ---------------------------------------------------------------------
// P1 -- THE NORMATIVE RULE. Exactly one class per frame. Section 3
// showed this is required by the standard's counting convention, not
// merely convenient.
// ---------------------------------------------------------------------
property p_exactly_one_class;
  @(posedge clk) disable iff (!rst_n)
    class_valid |-> (frame_class inside {V_VALID, V_TRUNCATED, V_ALIGNMENT,
                                         V_FCS, V_UNDERSIZE, V_FRAGMENT, V_OVERSIZE});
endproperty
a_exactly_one_class: assert property (p_exactly_one_class);
 
// ---------------------------------------------------------------------
// P2 -- Alignment takes precedence over FCS. A misaligned frame is
// counted as an alignment error even though its check also failed.
// ---------------------------------------------------------------------
property p_alignment_precedes_fcs;
  @(posedge clk) disable iff (!rst_n)
    (class_valid && ($past(dribble_bits) != 3'd0) && !$past(truncated))
      |-> (frame_class == V_ALIGNMENT);
endproperty
a_alignment_precedes_fcs: assert property (p_alignment_precedes_fcs)
  else $error("a misaligned frame was counted as an FCS error");
 
// ---------------------------------------------------------------------
// P3 -- An FCS error is a whole number of octets, by definition.
// ---------------------------------------------------------------------
property p_fcs_error_is_whole_octets;
  @(posedge clk) disable iff (!rst_n)
    (class_valid && (frame_class == V_FCS)) |-> ($past(dribble_bits) == 3'd0);
endproperty
a_fcs_error_is_whole_octets: assert property (p_fcs_error_is_whole_octets);
 
// ---------------------------------------------------------------------
// P4 -- Truncation outranks everything. There is no complete frame to
// classify, so nothing below it can be evaluated.
// ---------------------------------------------------------------------
property p_truncation_outranks;
  @(posedge clk) disable iff (!rst_n)
    (class_valid && $past(truncated)) |-> (frame_class == V_TRUNCATED);
endproperty
a_truncation_outranks: assert property (p_truncation_outranks);
 
// ---------------------------------------------------------------------
// P5 -- Chapter 5.6 §8's split, restated where it is classified: below
// the floor, the check sequence alone separates the two classes.
// ---------------------------------------------------------------------
property p_short_frame_split_by_fcs;
  @(posedge clk) disable iff (!rst_n)
    (class_valid && ($past(frame_octets) < 14'(MIN_FRAME)) &&
     ($past(dribble_bits) == 3'd0) && !$past(truncated))
      |-> (frame_class == ($past(fcs_ok) ? V_UNDERSIZE : V_FRAGMENT));
endproperty
a_short_frame_split_by_fcs: assert property (p_short_frame_split_by_fcs);
 
// ---------------------------------------------------------------------
// P6 -- The applicable maximum is a property of the FRAME's structure,
// never of this device's configuration.
// ---------------------------------------------------------------------
property p_applicable_max_is_normative;
  @(posedge clk) disable iff (!rst_n)
    class_valid |-> (applicable_max inside {14'(MAX_BASIC), 14'(MAX_QTAGGED),
                                            14'(MAX_ENVELOPE)});
endproperty
a_applicable_max_is_normative: assert property (p_applicable_max_is_normative);
 
// ---------------------------------------------------------------------
// P7 -- THE SEPARATION. A frame the standard accepts is never counted as
// malformed, whatever this device is configured for.
// ---------------------------------------------------------------------
property p_conformant_never_malformed;
  @(posedge clk) disable iff (!rst_n)
    (class_valid && (frame_class == V_VALID)) |-> !malformed;
endproperty
a_conformant_never_malformed: assert property (p_conformant_never_malformed)
  else $error("a conformant frame was counted as malformed");
 
// ---------------------------------------------------------------------
// P8 -- And the converse: a locally declined frame is one the standard
// accepted. The two predicates are exclusive by construction (Section 5).
// ---------------------------------------------------------------------
property p_local_decline_implies_conformant;
  @(posedge clk) disable iff (!rst_n)
    unacceptable_here |-> (frame_class == V_VALID);
endproperty
a_local_decline_implies_conformant: assert property (p_local_decline_implies_conformant);
 
// ---------------------------------------------------------------------
// P9 -- Exactly one of the three predicate outputs, every frame.
// ---------------------------------------------------------------------
property p_predicates_onehot;
  @(posedge clk) disable iff (!rst_n)
    class_valid |-> $onehot({malformed, unacceptable_here, acceptable});
endproperty
a_predicates_onehot: assert property (p_predicates_onehot);
 
// ---------------------------------------------------------------------
// P10 -- CONSERVATION. The per-class counters sum to the frame count.
// The only check that sees a frame counted twice.
// ---------------------------------------------------------------------
property p_class_counters_conserve;
  @(posedge clk) disable iff (!rst_n)
    class_valid |=> (class_sum == c_frames);
endproperty
a_class_counters_conserve: assert property (p_class_counters_conserve);
 
// ---------------------------------------------------------------------
// P11 -- The local floor never rises above the standard minimum. A
// configuration that does rejects conforming frames of every size.
// ---------------------------------------------------------------------
property p_local_floor_sane;
  @(posedge clk) disable iff (!rst_n)
    (local_floor <= 14'(MIN_FRAME));
endproperty
a_local_floor_sane: assert property (p_local_floor_sane);
 
// ---------------------------------------------------------------------
// P12 -- Dribble bits never enter the check computation. Chapter 5.8's
// covered range, at the one place a fractional octet could reach it.
// ---------------------------------------------------------------------
property p_dribble_never_in_crc;
  @(posedge clk) disable iff (!rst_n)
    (!carrier) |-> !crc_bit_valid;
endproperty
a_dribble_never_in_crc: assert property (p_dribble_never_in_crc);
 
// ---------------------------------------------------------------------
// P13 -- A partial octet is never delivered to the client.
// ---------------------------------------------------------------------
property p_no_partial_octet_delivered;
  @(posedge clk) disable iff (!rst_n)
    cli_octet_valid |-> ($past(cnt_q) == 3'd7);
endproperty
a_no_partial_octet_delivered: assert property (p_no_partial_octet_delivered);
 
// ---------------------------------------------------------------------
// P14 -- The dribble count is bounded. Eight leftover bits would be a
// complete octet and a counter that can reach eight has an off-by-one.
// ---------------------------------------------------------------------
property p_dribble_bounded;
  @(posedge clk) disable iff (!rst_n)
    dribble_valid |-> (dribble_out <= 3'd7);
endproperty
a_dribble_bounded: assert property (p_dribble_bounded);
 
// ---------------------------------------------------------------------
// P15 -- Misalignment is sticky. At 1 Gb/s and above it must never
// occur, so a single event is a finding rather than a rate.
// ---------------------------------------------------------------------
property p_misaligned_seen_sticky;
  @(posedge clk) disable iff (!rst_n)
    misaligned_seen |=> misaligned_seen;
endproperty
a_misaligned_seen_sticky: assert property (p_misaligned_seen_sticky);
 
// ---------------------------------------------------------------------
// P16 -- The smallest locally declined size survives a counter clear:
// it bounds where the ceiling would have to move.
// ---------------------------------------------------------------------
property p_smallest_declined_survives;
  @(posedge clk) disable iff (!rst_n)
    clear |=> $stable(smallest_locally_declined);
endproperty
a_smallest_declined_survives: assert property (p_smallest_declined_survives);
 
// ---------------------------------------------------------------------
// P17 -- COVERAGE. Each class reached, including the two that ordinary
// traffic never produces.
// ---------------------------------------------------------------------
c_class_alignment: cover property (@(posedge clk) disable iff (!rst_n) (frame_class == V_ALIGNMENT));
c_class_undersize: cover property (@(posedge clk) disable iff (!rst_n) (frame_class == V_UNDERSIZE));
c_class_fragment:  cover property (@(posedge clk) disable iff (!rst_n) (frame_class == V_FRAGMENT));
c_class_oversize:  cover property (@(posedge clk) disable iff (!rst_n) (frame_class == V_OVERSIZE));
 
// ---------------------------------------------------------------------
// P18 -- COVERAGE. A frame that is conformant and locally declined --
// the middle predicate, which no malformed frame can reach.
// ---------------------------------------------------------------------
c_locally_declined_only: cover property (
  @(posedge clk) disable iff (!rst_n) unacceptable_here
);