The Receive Path

// SYNTHESIZABLE.
//
// The receive datapath's control. The state graph looks like the mirror
// of Chapter 7.1's and is not: each state here is an INTERPRETATION of
// arriving octets rather than the emission of a decided region.
//
// Every output this module produces before R_DONE is provisional. The
// module says so explicitly, with a `provisional` qualifier that travels
// with the data -- because a downstream stage that cannot tell a settled
// result from a provisional one will act on both identically.
package mac_rx_pkg;
 
  typedef enum logic [3:0] {
    R_IDLE,        // waiting for carrier
    R_PREAMBLE,    // synchronising -- Chapter 5.2
    R_DA,          // destination address: the filter's input
    R_SA,          // source address
    R_LENTYPE,     // the two ambiguous octets -- Chapter 5.5
    R_PAYLOAD,     // client data and, indistinguishably, pad
    R_DONE,        // frame ended; the check has a verdict
    R_ABORTED      // ended early: no verdict is possible
  } rx_state_e;
 
  // Why a frame was discarded. Every discard carries one of these, which
  // is what makes Section 10's attribution possible.
  typedef enum logic [3:0] {
    D_NONE,
    D_NO_DELIMITER,   // never synchronised
    D_FILTER,         // not for this station -- Chapter 5.4
    D_UNDERSIZE,      // below the floor -- Chapter 5.6
    D_OVERSIZE,       // above the ceiling -- Chapter 5.7
    D_LENTYPE_BAND,   // the undefined band -- Chapter 5.5
    D_SHORT_DECLARED, // declared more than arrived
    D_FCS,            // the check disagreed -- Chapter 6.3
    D_FCS_STOMPED,    // deliberately marked upstream -- Chapter 5.8
    D_TRUNCATED,      // carrier lost mid-frame
    D_CLIENT_FULL     // nowhere to put it
  } discard_e;
 
endpackage
 
module mac_rx_controller
  import mac_rx_pkg::*;
  import frame_size_pkg::*;
  import ltype_pkg::*;
  import frame_size_pkg::*;
(
  input  logic clk,
  input  logic rst_n,
 
  input  logic       rx_valid,
  input  logic [7:0] rx_data,
  input  logic       carrier,
  input  logic       sfd_seen,
 
  // From the stages, as each reaches a provisional conclusion.
  input  logic       filter_accept,
  input  logic       filter_valid,
  input  logic       lentype_valid,
  input  lt_class_e  lentype_class,
  input  logic [10:0] declared_length,
  input  logic       fcs_ok,
  input  logic       fcs_stomped,
  input  logic       fcs_valid,
 
  // To the client. `provisional` is high for every octet handed over
  // before the check has a verdict -- so a client can tell the two apart
  // without knowing this module's policy.
  output logic       cli_valid,
  output logic [7:0] cli_data,
  output logic       cli_last,
  output logic       cli_provisional,
 
  output rx_state_e  state,
  output logic       frame_settled,
  output logic       discard_valid,
  output discard_e   discard_reason,
  output logic [13:0] frame_octets
);
 
  rx_state_e   state_q;
  logic [13:0] len_q;
  logic [3:0]  fld_q;
  logic        accepted_q;
 
  assign state        = state_q;
  assign frame_octets = len_q;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      state_q        <= R_IDLE;
      len_q          <= '0;
      fld_q          <= '0;
      accepted_q     <= 1'b0;
      cli_valid      <= 1'b0;
      cli_data       <= '0;
      cli_last       <= 1'b0;
      cli_provisional<= 1'b0;
      frame_settled  <= 1'b0;
      discard_valid  <= 1'b0;
      discard_reason <= D_NONE;
    end else begin
      cli_valid      <= 1'b0;
      cli_last       <= 1'b0;
      frame_settled  <= 1'b0;
      discard_valid  <= 1'b0;
 
      // Carrier loss is checked FIRST and outside the case, because it
      // can happen in any state and the response is the same: there is
      // no verdict to be had, so the frame is aborted rather than judged
      // (Chapter 6.3 §8, and Chapter 5.8 §4's rule that a truncation
      // must not be reported as a check-sequence mismatch).
      if (!carrier && (state_q != R_IDLE) && (state_q != R_DONE)) begin
        state_q        <= R_ABORTED;
        discard_valid  <= 1'b1;
        discard_reason <= D_TRUNCATED;
      end else begin
        case (state_q)
          R_IDLE: if (carrier) begin
            state_q <= R_PREAMBLE;
            len_q   <= '0;
          end
 
          R_PREAMBLE: if (sfd_seen) begin
            state_q <= R_DA;
            fld_q   <= '0;
            len_q   <= '0;
          end
 
          R_DA: if (rx_valid) begin
            len_q <= len_q + 1'b1;
            if (fld_q == 4'd5) begin state_q <= R_SA; fld_q <= '0; end
            else                     fld_q   <= fld_q + 1'b1;
          end
 
          R_SA: if (rx_valid) begin
            len_q <= len_q + 1'b1;
            if (fld_q == 4'd5) begin state_q <= R_LENTYPE; fld_q <= '0; end
            else                     fld_q   <= fld_q + 1'b1;
          end
 
          R_LENTYPE: if (rx_valid) begin
            len_q <= len_q + 1'b1;
            if (fld_q == 4'd1) begin
              state_q    <= R_PAYLOAD;
              fld_q      <= '0;
              // The filter's verdict is available by now -- one octet in,
              // per Chapter 5.3 -- and it is PROVISIONAL like everything
              // else. A corrupt address can produce an accept.
              accepted_q <= filter_valid ? filter_accept : 1'b0;
            end else begin
              fld_q <= fld_q + 1'b1;
            end
          end
 
          R_PAYLOAD: if (rx_valid) begin
            len_q <= len_q + 1'b1;
            if (accepted_q) begin
              cli_valid       <= 1'b1;
              cli_data        <= rx_data;
              // Provisional until fcs_valid. The qualifier travels with
              // the data rather than being a mode the client must know.
              cli_provisional <= 1'b1;
            end
            if (fcs_valid) begin
              state_q       <= R_DONE;
              frame_settled <= 1'b1;
              cli_last      <= accepted_q;
              if (!fcs_ok) begin
                discard_valid  <= 1'b1;
                // Stomped and mismatched are DIFFERENT discards, because
                // a stomp says an upstream device already found the
                // error and this link is proven good (Chapter 5.8 §9).
                discard_reason <= fcs_stomped ? D_FCS_STOMPED : D_FCS;
              end
            end
          end
 
          R_DONE, R_ABORTED: state_q <= R_IDLE;
          default:           state_q <= R_IDLE;
        endcase
      end
    end
  end
 
endmodule

// SYNTHESIZABLE.
//
// Governs when octets are released to the client and marks each release
// as provisional or committed.
//
// The three events that matter, and they are distinct:
//
//   RELEASE  -- an octet is handed to the client. May be provisional.
//   COMMIT   -- the check passed; every octet already released is now
//               final and nothing will be withdrawn.
//   ABORT    -- the check failed (or the frame ended early); every octet
//               released for this frame must be discarded by the client.
//
// A design that merges COMMIT and ABORT into a single "frame done, here
// is a status bit" has made the client responsible for noticing, which
// is the same failure as not having an abort at all.
module provisional_delivery_manager
  import mac_rx_pkg::*;
#(
  // CUT_THROUGH: release on filter accept. Otherwise release only after
  // the check has a verdict.
  parameter bit CUT_THROUGH = 1'b1,
  parameter int unsigned CNT_W = 32
) (
  input  logic clk,
  input  logic rst_n,
 
  input  logic       frame_start,
  input  logic       filter_accept_valid,
  input  logic       filter_accept,
  input  logic       rx_valid,
  input  logic [7:0] rx_data,
  input  logic       frame_end,
  input  logic       fcs_valid,
  input  logic       fcs_ok,
 
  // Buffered frame data, for the store-and-forward path.
  input  logic       buf_valid,
  input  logic [7:0] buf_data,
  input  logic       buf_last,
 
  output logic       rel_valid,
  output logic [7:0] rel_data,
  output logic       rel_last,
  output logic       rel_provisional,
 
  // The two terminal events. Exactly one fires per accepted frame.
  output logic       commit,
  output logic       abort,
 
  output logic [CNT_W-1:0] c_committed,
  output logic [CNT_W-1:0] c_aborted,
  // Octets the client had to throw away. The cost of cut-through,
  // measured rather than assumed.
  output logic [CNT_W-1:0] c_wasted_octets,
  output logic [13:0]      worst_wasted
);
 
  logic        releasing_q;
  logic [13:0] released_q;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      releasing_q     <= 1'b0;
      released_q      <= '0;
      rel_valid       <= 1'b0;
      rel_data        <= '0;
      rel_last        <= 1'b0;
      rel_provisional <= 1'b0;
      commit          <= 1'b0;
      abort           <= 1'b0;
      c_committed     <= '0;
      c_aborted       <= '0;
      c_wasted_octets <= '0;
      worst_wasted    <= '0;
    end else begin
      rel_valid <= 1'b0;
      rel_last  <= 1'b0;
      commit    <= 1'b0;
      abort     <= 1'b0;
 
      if (frame_start) begin
        releasing_q <= 1'b0;
        released_q  <= '0;
      end
 
      if (CUT_THROUGH) begin
        // Release begins as soon as the filter accepts, and every octet
        // carries the provisional qualifier until the verdict.
        if (filter_accept_valid && filter_accept) releasing_q <= 1'b1;
 
        if (releasing_q && rx_valid) begin
          rel_valid       <= 1'b1;
          rel_data        <= rx_data;
          rel_provisional <= 1'b1;
          released_q      <= released_q + 1'b1;
        end
 
        if (fcs_valid && releasing_q) begin
          if (fcs_ok) begin
            commit      <= 1'b1;
            rel_last    <= 1'b1;
            c_committed <= c_committed + 1'b1;
          end else begin
            // The abort is an EVENT, not a status bit the client must
            // poll. Everything released for this frame is now worthless.
            abort     <= 1'b1;
            c_aborted <= c_aborted + 1'b1;
            c_wasted_octets <= c_wasted_octets + CNT_W'(released_q);
            if (released_q > worst_wasted) worst_wasted <= released_q;
          end
          releasing_q <= 1'b0;
        end
      end else begin
        // Store-and-forward: nothing is released until the verdict, so
        // `rel_provisional` is never asserted and `abort` never fires on
        // released data. The frame is simply not released.
        if (fcs_valid && fcs_ok) releasing_q <= 1'b1;
 
        if (releasing_q && buf_valid) begin
          rel_valid       <= 1'b1;
          rel_data        <= buf_data;
          rel_provisional <= 1'b0;
          rel_last        <= buf_last;
          if (buf_last) begin
            commit      <= 1'b1;
            c_committed <= c_committed + 1'b1;
            releasing_q <= 1'b0;
          end
        end
 
        if (fcs_valid && !fcs_ok) begin
          // Discarded before release. Not an abort -- nothing was given
          // to the client -- and counting it as one would overstate the
          // cost of a policy that has none.
          c_aborted <= c_aborted + 1'b1;
        end
      end
    end
  end
 
endmodule

// SYNTHESIZABLE.
//
// Delivers the abort to the client with a bounded latency, and proves
// the bound.
//
// The requirement that is easy to miss: an abort must reach the client
// BEFORE the client could have committed the octets on its own. A client
// holds provisional data until commit -- but it also has finite buffer,
// and a receiver that takes too long to abort forces the client to
// either overflow or commit early.
//
// So the abort's latency is not a performance figure. It is part of the
// contract, and this module reports violations of it rather than
// assuming they cannot happen.
module rx_late_abort
  import mac_rx_pkg::*;
#(
  // Cycles from the last octet within which the abort must be delivered.
  // Derived from the client's holding capacity, not chosen freely.
  parameter int unsigned ABORT_DEADLINE = 8,
  parameter int unsigned CNT_W = 32
) (
  input  logic clk,
  input  logic rst_n,
  input  logic clear,
 
  input  logic     last_octet,        // last octet released to the client
  input  logic     fcs_valid,
  input  logic     fcs_ok,
  input  logic     fcs_stomped,
  input  logic     truncated,
 
  output logic     abort_out,
  output discard_e abort_reason,
  output logic     commit_out,
 
  // The contract check. High if an abort was delivered later than the
  // deadline -- which means the client may already have committed.
  output logic             deadline_missed,
  output logic [CNT_W-1:0] c_deadline_missed,
  output logic [7:0]       worst_abort_latency
);
 
  logic [7:0] since_q;
  logic       pending_q;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      since_q             <= '0;
      pending_q           <= 1'b0;
      abort_out           <= 1'b0;
      abort_reason        <= D_NONE;
      commit_out          <= 1'b0;
      deadline_missed     <= 1'b0;
      c_deadline_missed   <= '0;
      worst_abort_latency <= '0;
    end else begin
      abort_out       <= 1'b0;
      commit_out      <= 1'b0;
      deadline_missed <= 1'b0;
 
      if (clear) begin
        c_deadline_missed <= '0;
        // worst_abort_latency deliberately survives: it bounds what the
        // client's buffer must have survived, and a clear must not erase
        // the only record of the worst case.
      end
 
      if (last_octet) begin
        pending_q <= 1'b1;
        since_q   <= '0;
      end else if (pending_q) begin
        since_q <= (since_q == 8'hFF) ? since_q : (since_q + 1'b1);
      end
 
      // A truncation resolves the frame with no verdict available, and it
      // is a DIFFERENT reason from a failed check (Chapter 5.8 §4).
      if (truncated && pending_q) begin
        abort_out    <= 1'b1;
        abort_reason <= D_TRUNCATED;
        pending_q    <= 1'b0;
        if (since_q > worst_abort_latency) worst_abort_latency <= since_q;
        if (since_q > 8'(ABORT_DEADLINE)) begin
          deadline_missed   <= 1'b1;
          c_deadline_missed <= c_deadline_missed + 1'b1;
        end
      end else if (fcs_valid && pending_q) begin
        pending_q <= 1'b0;
        if (since_q > worst_abort_latency) worst_abort_latency <= since_q;
 
        if (fcs_ok) begin
          commit_out <= 1'b1;
        end else begin
          abort_out    <= 1'b1;
          // Stomped is kept distinct all the way to the client, because
          // it says the fault is upstream and this link is proven good.
          abort_reason <= fcs_stomped ? D_FCS_STOMPED : D_FCS;
          if (since_q > 8'(ABORT_DEADLINE)) begin
            deadline_missed   <= 1'b1;
            c_deadline_missed <= c_deadline_missed + 1'b1;
          end
        end
      end
    end
  end
 
endmodule

// SYNTHESIZABLE INSTRUMENTATION.
//
// Attributes every frame that did not reach the client to the stage that
// stopped it, and keeps the one non-fault separate from the five faults.
//
// The split that matters most is the first one:
//
//   NOT A FAULT  -- filter discards. Traffic for other stations. On a
//        flooded segment this is most arrivals, and folding it into a
//        drop count makes the drop count track traffic volume.
//
//   THIS DEVICE  -- client-full. The receive path worked; there was
//        nowhere to put the frame.
//
//   THIS LINK    -- check-sequence mismatch, truncation.
//
//   UPSTREAM     -- a stomped frame: an earlier device already found the
//        error, so this link is proven good (Chapter 5.8 §9).
//
//   A PEER       -- undersize with a good check, undefined length/type
//        band, a declared length exceeding what arrived.
module rx_discard_accounting
  import mac_rx_pkg::*;
#(
  parameter int unsigned CNT_W = 32
) (
  input  logic clk,
  input  logic rst_n,
  input  logic clear,
 
  input  logic     frame_done,
  input  logic     delivered,
  input  logic     discard_valid,
  input  discard_e discard_reason,
  input  logic [13:0] frame_octets,
 
  output logic [CNT_W-1:0] c_delivered,
 
  // Not a fault. Deliberately first, and deliberately not summed with
  // anything below it.
  output logic [CNT_W-1:0] c_filtered,
 
  // This device.
  output logic [CNT_W-1:0] c_client_full,
 
  // This link.
  output logic [CNT_W-1:0] c_fcs,
  output logic [CNT_W-1:0] c_truncated,
  output logic [CNT_W-1:0] c_no_delimiter,
 
  // Upstream.
  output logic [CNT_W-1:0] c_stomped,
 
  // A peer.
  output logic [CNT_W-1:0] c_undersize,
  output logic [CNT_W-1:0] c_oversize,
  output logic [CNT_W-1:0] c_lentype_band,
  output logic [CNT_W-1:0] c_short_declared,
 
  // The aggregate a management interface usually wants -- computed HERE,
  // from the fault categories only, so it cannot accidentally include
  // filter discards.
  output logic [CNT_W-1:0] c_faults_total,
 
  // First cause, kept across a clear.
  output logic             first_fault_seen,
  output discard_e         first_fault_reason,
  output logic [13:0]      first_fault_octets
);
 
  function automatic logic [CNT_W-1:0] bump(input logic [CNT_W-1:0] v);
    bump = (&v) ? v : (v + 1'b1);
  endfunction
 
  wire is_fault = discard_valid && (discard_reason != D_FILTER);
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      c_delivered <= '0; c_filtered <= '0; c_client_full <= '0;
      c_fcs <= '0; c_truncated <= '0; c_no_delimiter <= '0;
      c_stomped <= '0; c_undersize <= '0; c_oversize <= '0;
      c_lentype_band <= '0; c_short_declared <= '0; c_faults_total <= '0;
      first_fault_seen <= 1'b0; first_fault_reason <= D_NONE;
      first_fault_octets <= '0;
    end else begin
      if (clear) begin
        c_delivered <= '0; c_filtered <= '0; c_client_full <= '0;
        c_fcs <= '0; c_truncated <= '0; c_no_delimiter <= '0;
        c_stomped <= '0; c_undersize <= '0; c_oversize <= '0;
        c_lentype_band <= '0; c_short_declared <= '0; c_faults_total <= '0;
        // The first fault's identity deliberately survives.
      end else if (frame_done) begin
        if (delivered) c_delivered <= bump(c_delivered);
 
        if (discard_valid) begin
          case (discard_reason)
            D_FILTER:         c_filtered       <= bump(c_filtered);
            D_CLIENT_FULL:    c_client_full    <= bump(c_client_full);
            D_FCS:            c_fcs            <= bump(c_fcs);
            D_FCS_STOMPED:    c_stomped        <= bump(c_stomped);
            D_TRUNCATED:      c_truncated      <= bump(c_truncated);
            D_NO_DELIMITER:   c_no_delimiter   <= bump(c_no_delimiter);
            D_UNDERSIZE:      c_undersize      <= bump(c_undersize);
            D_OVERSIZE:       c_oversize       <= bump(c_oversize);
            D_LENTYPE_BAND:   c_lentype_band   <= bump(c_lentype_band);
            D_SHORT_DECLARED: c_short_declared <= bump(c_short_declared);
            default: ;
          endcase
 
          if (is_fault) begin
            c_faults_total <= bump(c_faults_total);
            if (!first_fault_seen) begin
              first_fault_seen   <= 1'b1;
              first_fault_reason <= discard_reason;
              first_fault_octets <= frame_octets;
            end
          end
        end
      end
    end
  end
 
endmodule

// SYNTHESIZABLE MONITOR.
//
// Verifies the receive path's own invariants: that every frame is
// accounted for exactly once, that provisional data is always resolved,
// and that no octet reaches the client without a subsequent verdict.
//
// The property it exists for is conservation. A receive path processes
// N frames; each is delivered or discarded, exactly once, with exactly
// one reason. A frame that is neither -- lost in the pipeline, or
// counted twice -- is invisible to every other check in this chapter,
// because every other check looks at frames it can see.
module rx_conformance_monitor
  import mac_rx_pkg::*;
#(
  parameter int unsigned CNT_W = 32,
  // Cycles after the last released octet by which a verdict must exist.
  parameter int unsigned VERDICT_DEADLINE = 16
) (
  input  logic clk,
  input  logic rst_n,
  input  logic clear,
 
  input  logic     frame_start,
  input  logic     frame_done,
  input  logic     delivered,
  input  logic     discard_valid,
  input  discard_e discard_reason,
 
  input  logic     rel_valid,
  input  logic     rel_provisional,
  input  logic     commit,
  input  logic     abort,
 
  output logic [CNT_W-1:0] c_started,
  output logic [CNT_W-1:0] c_accounted,
 
  // The conservation violation: a frame started and never resolved, or
  // resolved twice.
  output logic             conservation_error,
  output logic [CNT_W-1:0] c_conservation_error,
 
  // Provisional octets were released and no verdict followed within the
  // deadline. The contract of Section 6, checked rather than assumed.
  output logic             unresolved_provisional,
  output logic [CNT_W-1:0] c_unresolved,
 
  output logic             any_violation      // sticky
);
 
  logic [7:0] since_q;
  logic       prov_open_q;
  logic       frame_open_q;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      c_started <= '0; c_accounted <= '0;
      conservation_error <= 1'b0; c_conservation_error <= '0;
      unresolved_provisional <= 1'b0; c_unresolved <= '0;
      since_q <= '0; prov_open_q <= 1'b0; frame_open_q <= 1'b0;
      any_violation <= 1'b0;
    end else begin
      conservation_error     <= 1'b0;
      unresolved_provisional <= 1'b0;
 
      if (clear) begin
        c_started <= '0; c_accounted <= '0;
        c_conservation_error <= '0; c_unresolved <= '0;
        // any_violation deliberately survives.
      end
 
      if (frame_start) begin
        // A frame starting while one is still open is a conservation
        // violation on its own: the previous frame was never resolved.
        if (frame_open_q) begin
          conservation_error   <= 1'b1;
          c_conservation_error <= c_conservation_error + 1'b1;
          any_violation        <= 1'b1;
        end
        frame_open_q <= 1'b1;
        c_started    <= c_started + 1'b1;
      end
 
      if (frame_done) begin
        // Exactly one of delivered / discarded, and never both.
        if (delivered == discard_valid) begin
          conservation_error   <= 1'b1;
          c_conservation_error <= c_conservation_error + 1'b1;
          any_violation        <= 1'b1;
        end else begin
          c_accounted <= c_accounted + 1'b1;
        end
        frame_open_q <= 1'b0;
      end
 
      // Provisional release must be resolved by commit or abort.
      if (rel_valid && rel_provisional) begin
        prov_open_q <= 1'b1;
        since_q     <= '0;
      end else if (prov_open_q) begin
        if (commit || abort) begin
          prov_open_q <= 1'b0;
        end else begin
          since_q <= (since_q == 8'hFF) ? since_q : (since_q + 1'b1);
          if (since_q == 8'(VERDICT_DEADLINE)) begin
            unresolved_provisional <= 1'b1;
            c_unresolved           <= c_unresolved + 1'b1;
            any_violation          <= 1'b1;
          end
        end
      end
    end
  end
 
endmodule

// ---------------------------------------------------------------------
// P1 -- THE CENTRAL PROPERTY. Every provisionally released frame is
// resolved: exactly one of commit or abort follows, within a bound.
// ---------------------------------------------------------------------
property p_provisional_is_resolved;
  @(posedge clk) disable iff (!rst_n)
    (rel_valid && rel_provisional)
      |-> ##[1:VERDICT_DEADLINE] (commit || abort);
endproperty
a_provisional_is_resolved: assert property (p_provisional_is_resolved)
  else $error("provisional octets released and never resolved");
 
// ---------------------------------------------------------------------
// P2 -- Commit and abort are mutually exclusive on one frame.
// ---------------------------------------------------------------------
property p_commit_xor_abort;
  @(posedge clk) disable iff (!rst_n)
    (commit || abort) |-> !(commit && abort);
endproperty
a_commit_xor_abort: assert property (p_commit_xor_abort);
 
// ---------------------------------------------------------------------
// P3 -- A committed frame passed its check. Note the direction: this is
// about what commit MEANS, and it is the property the rejected one below
// tries to state at the wrong moment.
// ---------------------------------------------------------------------
property p_commit_implies_fcs_ok;
  @(posedge clk) disable iff (!rst_n)
    commit |-> $past(fcs_ok);
endproperty
a_commit_implies_fcs_ok: assert property (p_commit_implies_fcs_ok);
 
// ---------------------------------------------------------------------
// P4 -- A frame that failed its check is never committed.
// ---------------------------------------------------------------------
property p_bad_frame_never_committed;
  @(posedge clk) disable iff (!rst_n)
    (fcs_valid && !fcs_ok) |-> !commit;
endproperty
a_bad_frame_never_committed: assert property (p_bad_frame_never_committed);
 
// ---------------------------------------------------------------------
// P5 -- Every octet released before a verdict exists is MARKED
// provisional. The qualifier is what makes the contract local.
// ---------------------------------------------------------------------
property p_unverified_release_is_marked;
  @(posedge clk) disable iff (!rst_n)
    (rel_valid && !verdict_available) |-> rel_provisional;
endproperty
a_unverified_release_is_marked: assert property (p_unverified_release_is_marked);
 
// ---------------------------------------------------------------------
// P6 -- Under store-and-forward, nothing is ever provisional.
// ---------------------------------------------------------------------
property p_store_forward_never_provisional;
  @(posedge clk) disable iff (!rst_n)
    (!CUT_THROUGH && rel_valid) |-> !rel_provisional;
endproperty
a_store_forward_never_provisional: assert property (p_store_forward_never_provisional);
 
// ---------------------------------------------------------------------
// P7 -- The abort arrives within its deadline, because a late abort is
// an abort the client may already have been unable to honour.
// ---------------------------------------------------------------------
property p_abort_within_deadline;
  @(posedge clk) disable iff (!rst_n)
    abort |-> (since_q <= 8'(ABORT_DEADLINE));
endproperty
a_abort_within_deadline: assert property (p_abort_within_deadline);
 
// ---------------------------------------------------------------------
// P8 -- CONSERVATION. Every frame that starts is resolved exactly once.
// The property no other check in this chapter can see.
// ---------------------------------------------------------------------
property p_every_frame_accounted;
  @(posedge clk) disable iff (!rst_n)
    frame_start |-> ##[1:$] (frame_done && (delivered ^ discard_valid));
endproperty
a_every_frame_accounted: assert property (p_every_frame_accounted);
 
// ---------------------------------------------------------------------
// P9 -- A frame cannot start while another is open.
// ---------------------------------------------------------------------
property p_no_overlapping_frames;
  @(posedge clk) disable iff (!rst_n)
    frame_start |-> !frame_open_q;
endproperty
a_no_overlapping_frames: assert property (p_no_overlapping_frames);
 
// ---------------------------------------------------------------------
// P10 -- Exactly one discard reason per discarded frame.
// ---------------------------------------------------------------------
property p_one_reason_per_discard;
  @(posedge clk) disable iff (!rst_n)
    discard_valid |-> (discard_reason != D_NONE);
endproperty
a_one_reason_per_discard: assert property (p_one_reason_per_discard);
 
// ---------------------------------------------------------------------
// P11 -- A truncation is NEVER reported as a check-sequence mismatch.
// Chapter 5.8 §4's rule, enforced at the point where the two could be
// confused.
// ---------------------------------------------------------------------
property p_truncation_not_fcs;
  @(posedge clk) disable iff (!rst_n)
    (discard_valid && (discard_reason == D_TRUNCATED)) |-> !fcs_valid;
endproperty
a_truncation_not_fcs: assert property (p_truncation_not_fcs);
 
// ---------------------------------------------------------------------
// P12 -- A stomped frame is attributed UPSTREAM, never to this link.
// The single most valuable split in Section 9.
// ---------------------------------------------------------------------
property p_stomp_not_this_link;
  @(posedge clk) disable iff (!rst_n)
    (discard_valid && (discard_reason == D_FCS_STOMPED))
      |=> ($stable(c_fcs) && (c_stomped == $past(c_stomped) + 1));
endproperty
a_stomp_not_this_link: assert property (p_stomp_not_this_link);
 
// ---------------------------------------------------------------------
// P13 -- Filter discards are NOT faults. The aggregate must not move.
// ---------------------------------------------------------------------
property p_filter_is_not_a_fault;
  @(posedge clk) disable iff (!rst_n)
    (discard_valid && (discard_reason == D_FILTER)) |=> $stable(c_faults_total);
endproperty
a_filter_is_not_a_fault: assert property (p_filter_is_not_a_fault);
 
// ---------------------------------------------------------------------
// P14 -- Carrier loss aborts from any state. Written over the state set
// rather than per state, because a per-state version omits one.
// ---------------------------------------------------------------------
property p_carrier_loss_aborts_anywhere;
  @(posedge clk) disable iff (!rst_n)
    (!carrier && (state inside {R_PREAMBLE, R_DA, R_SA, R_LENTYPE, R_PAYLOAD}))
      |=> (state == R_ABORTED);
endproperty
a_carrier_loss_aborts_anywhere: assert property (p_carrier_loss_aborts_anywhere);
 
// ---------------------------------------------------------------------
// P15 -- Nothing is released for a frame the filter rejected.
// ---------------------------------------------------------------------
property p_no_release_when_filtered;
  @(posedge clk) disable iff (!rst_n)
    (filter_accept_valid && !filter_accept) |=> !rel_valid until frame_start;
endproperty
a_no_release_when_filtered: assert property (p_no_release_when_filtered);
 
// ---------------------------------------------------------------------
// P16 -- First-cause attribution survives a counter clear.
// ---------------------------------------------------------------------
property p_first_fault_survives_clear;
  @(posedge clk) disable iff (!rst_n)
    clear |=> ($stable(first_fault_reason) && $stable(first_fault_octets));
endproperty
a_first_fault_survives_clear: assert property (p_first_fault_survives_clear);
 
// ---------------------------------------------------------------------
// P17 -- COVERAGE. An abort that follows real provisional delivery. A
// run without one has not exercised the cut-through path at all.
// ---------------------------------------------------------------------
c_abort_after_release: cover property (
  @(posedge clk) disable iff (!rst_n)
    ((rel_valid && rel_provisional) ##[1:$] abort)
);
 
// ---------------------------------------------------------------------
// P18 -- COVERAGE. Each discard reason reached at least once.
// ---------------------------------------------------------------------
c_discard_fcs:       cover property (@(posedge clk) disable iff (!rst_n) (discard_reason == D_FCS));
c_discard_stomped:   cover property (@(posedge clk) disable iff (!rst_n) (discard_reason == D_FCS_STOMPED));
c_discard_truncated: cover property (@(posedge clk) disable iff (!rst_n) (discard_reason == D_TRUNCATED));
c_discard_client:    cover property (@(posedge clk) disable iff (!rst_n) (discard_reason == D_CLIENT_FULL));