The Transmit Path

// SYNTHESIZABLE.
//
// The transmit datapath's control, with the stage order of Section 2
// expressed as a state graph.
//
// Two things are computed at frame start and never recomputed:
//
//   the LENGTH to emit  -- the CLIENT's octet count
//   the PAD target      -- the client-data region's size
//
// They come from one decision (Chapter 5.6 §5) so they cannot disagree.
// A design that recomputes either later has two representations of one
// boundary and no mechanism keeping them equal.
package mac_tx_pkg;
  import frame_size_pkg::*;
 
  typedef enum logic [3:0] {
    S_IDLE,
    S_PREAMBLE,   // outside the covered range
    S_SFD,        // outside the covered range
    S_HEADER,     // covered range begins here
    S_DATA,       // covered
    S_PAD,        // covered -- BEFORE the check, per Section 2
    S_FCS,        // the frame's last field
    S_GAP,        // outside the frame -- AFTER the check
    S_ABORT       // underrun: finish the frame and mark it (Section 9)
  } tx_state_e;
 
endpackage
 
module mac_tx_controller
  import mac_tx_pkg::*;
  import frame_size_pkg::*;
  import crc32_pkg::*;
(
  input  logic clk,
  input  logic rst_n,
 
  // From the client.
  input  logic        req_valid,
  input  logic [10:0] req_octets,        // client data only
  input  logic        req_is_length_form,
  input  logic        cli_valid,
  input  logic [7:0]  cli_data,
  input  logic        cli_last,
 
  // From the gap enforcer of Chapter 5.9. The transmit path may not
  // start a frame until this permits it, and it is an INPUT rather than
  // something this module counts, so the gap's floor stays structural.
  input  logic        gap_permits_start,
 
  // To the interface.
  output logic        tx_valid,
  output logic [7:0]  tx_data,
  output logic        tx_last,
 
  // To the CRC engine. Note crc_enable is high for exactly the covered
  // range -- Chapter 5.8's boundary, expressed as one signal.
  output logic        crc_start,
  output logic        crc_enable,
  output logic [7:0]  crc_data,
  input  logic [31:0] crc_fcs,
 
  output tx_state_e   state,
  output logic        frame_aborted,
  output logic [10:0] emitted_length
);
 
  tx_state_e   state_q;
  logic [3:0]  cnt_q;          // preamble octets, FCS octets
  logic [10:0] sent_q;         // octets of the client-data region sent
  logic [10:0] target_q;       // that region's size
  logic [10:0] length_q;       // the value the length field will carry
  logic [31:0] fcs_q;
 
  assign state          = state_q;
  assign emitted_length = length_q;
 
  // ONE decision, taken at frame start. The pad count and the length are
  // both read off it, so they cannot drift (Chapter 5.6 §5).
  wire [10:0] region_target = (req_octets < 11'(MIN_CLIENT))
                                ? 11'(MIN_CLIENT) : req_octets;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      state_q       <= S_IDLE;
      cnt_q         <= '0;
      sent_q        <= '0;
      target_q      <= '0;
      length_q      <= '0;
      fcs_q         <= '0;
      tx_valid      <= 1'b0;
      tx_data       <= '0;
      tx_last       <= 1'b0;
      crc_start     <= 1'b0;
      crc_enable    <= 1'b0;
      crc_data      <= '0;
      frame_aborted <= 1'b0;
    end else begin
      tx_valid   <= 1'b0;
      tx_last    <= 1'b0;
      crc_start  <= 1'b0;
      crc_enable <= 1'b0;
 
      case (state_q)
        S_IDLE: if (req_valid && gap_permits_start) begin
          state_q       <= S_PREAMBLE;
          cnt_q         <= '0;
          sent_q        <= '0;
          target_q      <= region_target;
          // The CLIENT's count, never the target. Section 3's fourth row.
          length_q      <= req_octets;
          frame_aborted <= 1'b0;
        end
 
        // Seven preamble octets. crc_enable stays LOW: outside the
        // covered range (Chapter 5.8 §2).
        S_PREAMBLE: begin
          tx_valid <= 1'b1;
          tx_data  <= 8'h55;
          if (cnt_q == 4'd6) begin state_q <= S_SFD; cnt_q <= '0; end
          else                     cnt_q   <= cnt_q + 1'b1;
        end
 
        S_SFD: begin
          tx_valid  <= 1'b1;
          tx_data   <= 8'hD5;
          // The engine is started HERE, so the first covered octet is the
          // first address octet and not the delimiter.
          crc_start <= 1'b1;
          state_q   <= S_HEADER;
          cnt_q     <= '0;
        end
 
        // Addresses and length/type. Covered.
        S_HEADER: if (cli_valid) begin
          tx_valid   <= 1'b1;
          tx_data    <= cli_data;
          crc_enable <= 1'b1;
          crc_data   <= cli_data;
          if (cnt_q == 4'd13) begin state_q <= S_DATA; cnt_q <= '0; end
          else                      cnt_q   <= cnt_q + 1'b1;
        end
 
        S_DATA: begin
          if (cli_valid) begin
            tx_valid   <= 1'b1;
            tx_data    <= cli_data;
            crc_enable <= 1'b1;
            crc_data   <= cli_data;
            sent_q     <= sent_q + 1'b1;
            if (cli_last) begin
              // Pad if short, otherwise straight to the check. The two
              // exits are the only ones, and neither can reach S_GAP.
              state_q <= ((sent_q + 1'b1) < target_q) ? S_PAD : S_FCS;
              cnt_q   <= '0;
            end
          end else if (tx_needs_octet_now) begin
            // UNDERRUN. The frame cannot be un-started, so it is finished
            // and marked. Section 9 owns what "marked" means.
            state_q <= S_ABORT;
          end
        end
 
        // Pad is COVERED, so crc_enable is high here too. This is the
        // constraint of Section 2 expressed in one line.
        S_PAD: begin
          tx_valid   <= 1'b1;
          tx_data    <= 8'h00;
          crc_enable <= 1'b1;
          crc_data   <= 8'h00;
          sent_q     <= sent_q + 1'b1;
          if ((sent_q + 1'b1) >= target_q) begin
            state_q <= S_FCS;
            cnt_q   <= '0;
            fcs_q   <= crc_fcs;
          end
        end
 
        // The check sequence. crc_enable is LOW: the field does not cover
        // itself (Chapter 5.8 §3).
        S_FCS: begin
          tx_valid <= 1'b1;
          tx_data  <= fcs_q[8*cnt_q +: 8];
          if (cnt_q == 4'd3) begin
            tx_last <= 1'b1;
            state_q <= S_GAP;
            cnt_q   <= '0;
          end else begin
            cnt_q <= cnt_q + 1'b1;
          end
        end
 
        // The gap is entered unconditionally after the check and left
        // only when the enforcer permits -- so the floor is not this
        // module's to get wrong (Chapter 5.9 §9).
        S_GAP: if (gap_permits_start) state_q <= S_IDLE;
 
        S_ABORT: begin
          frame_aborted <= 1'b1;
          state_q       <= S_GAP;
        end
 
        default: state_q <= S_IDLE;
      endcase
    end
  end
 
endmodule

// SYNTHESIZABLE.
//
// The assembler between a bursty client and an interface that cannot be
// stalled.
//
// The two directions are not symmetric and conflating them is the bug:
//
//   client -> assembler : may stall. The client is a memory system and
//        stalls whenever it feels like it. The assembler absorbs this.
//
//   assembler -> wire   : may NOT stall. Once the preamble is out, the
//        interface consumes an octet per cycle until the frame ends.
//        There is no back-pressure signal in that direction because
//        there is no such thing as pausing a frame mid-transmission.
//
// So the assembler's job is to guarantee that, from the moment it starts
// a frame, it can supply an octet every cycle until the end -- and its
// only tool is refusing to start until it can.
module tx_assembler
#(
  parameter int unsigned DEPTH = 64,
  // Octets that must be buffered before a frame may start. The whole
  // underrun defence lives in this number.
  parameter int unsigned START_THRESHOLD = 32
) (
  input  logic clk,
  input  logic rst_n,
 
  // Client side: may stall freely.
  input  logic        cli_valid,
  input  logic [7:0]  cli_data,
  input  logic        cli_last,
  output logic        cli_ready,
 
  // Wire side: consumes on demand, cannot be stalled.
  input  logic        wire_take,
  output logic        wire_valid,
  output logic [7:0]  wire_data,
  output logic        wire_last,
 
  // To the controller: it is safe to begin a frame.
  output logic        safe_to_start,
  // The frame is in flight and the buffer has run dry.
  output logic        underrun
);
 
  logic [7:0]  mem_q [DEPTH];
  logic [7:0]  wr_q, rd_q;
  logic [8:0]  occ_q;
  logic        in_frame_q;
  logic        last_seen_q;
 
  assign cli_ready = (occ_q != 9'(DEPTH));
 
  // A frame may start when either the whole frame is buffered -- the
  // client's last octet has arrived -- or enough is buffered to cover
  // the client's worst-case stall. The first condition is what a
  // store-and-forward transmitter uses and it removes underrun entirely.
  assign safe_to_start = last_seen_q || (occ_q >= 9'(START_THRESHOLD));
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      wr_q <= '0; rd_q <= '0; occ_q <= '0;
      in_frame_q <= 1'b0; last_seen_q <= 1'b0;
      wire_valid <= 1'b0; wire_data <= '0; wire_last <= 1'b0;
      underrun <= 1'b0;
    end else begin
      wire_valid <= 1'b0;
      wire_last  <= 1'b0;
      underrun   <= 1'b0;
 
      if (cli_valid && cli_ready) begin
        mem_q[wr_q] <= cli_data;
        wr_q        <= wr_q + 1'b1;
        occ_q       <= occ_q + 1'b1;
        if (cli_last) last_seen_q <= 1'b1;
      end
 
      if (wire_take) begin
        if (occ_q != '0) begin
          wire_valid <= 1'b1;
          wire_data  <= mem_q[rd_q];
          rd_q       <= rd_q + 1'b1;
          occ_q      <= occ_q - 1'b1;
          if (last_seen_q && (occ_q == 9'd1)) begin
            wire_last   <= 1'b1;
            last_seen_q <= 1'b0;
            in_frame_q  <= 1'b0;
          end else begin
            in_frame_q <= 1'b1;
          end
        end else if (in_frame_q) begin
          // The wire wants an octet, the buffer is empty, and a frame is
          // in flight. There is no stall available in this direction, so
          // the frame is already unfixable -- report it and let the
          // controller mark it (Section 9).
          underrun <= 1'b1;
        end
      end
    end
  end
 
endmodule

// SYNTHESIZABLE.
//
// Finishes a starved frame to the correct length and marks it, and
// records enough locally that the fault is attributable HERE rather than
// only at the far end.
//
// The three outputs are three different audiences:
//
//   force_bad_fcs   -> the receiver, which must reject the frame
//   c_underrun      -> whoever operates this device, who must fix it
//   first_at_octet  -> whoever debugs it, because WHERE it starved names
//                      the subsystem that starved
module tx_underrun_handler
  import frame_size_pkg::*;
#(
  parameter int unsigned CNT_W = 32
) (
  input  logic clk,
  input  logic rst_n,
  input  logic clear,
 
  input  logic        frame_start,
  input  logic        underrun,
  input  logic [13:0] octets_sent,
  input  logic [13:0] octets_expected,
 
  // To the datapath: keep transmitting to the correct length, with
  // filler, so the frame is the right SIZE -- and then invert the check
  // sequence so it is rejected. Length correct, check deliberately wrong.
  output logic        fill_active,
  output logic [7:0]  fill_data,
  output logic        force_bad_fcs,
 
  output logic [CNT_W-1:0] c_underrun,
  output logic             underrun_seen,     // sticky
  output logic [13:0]      first_at_octet,
  output logic [13:0]      first_frame_length,
  // Deepest into a frame that a starvation has ever occurred. Survives
  // clear: it bounds how much buffering would have been enough.
  output logic [13:0]      worst_at_octet
);
 
  logic active_q;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      active_q           <= 1'b0;
      fill_active        <= 1'b0;
      fill_data          <= '0;
      force_bad_fcs      <= 1'b0;
      c_underrun         <= '0;
      underrun_seen      <= 1'b0;
      first_at_octet     <= '0;
      first_frame_length <= '0;
      worst_at_octet     <= '0;
    end else begin
      if (clear) begin
        c_underrun <= '0;
        // The context deliberately survives. A count says how often; the
        // octet position says which subsystem, and only one of those can
        // be reconstructed later.
      end
 
      if (frame_start) begin
        active_q      <= 1'b0;
        fill_active   <= 1'b0;
        force_bad_fcs <= 1'b0;
      end else if (underrun && !active_q) begin
        active_q      <= 1'b1;
        // Fill to the CORRECT length. A frame that is the right size and
        // fails its check is unambiguous; a short frame is a fragment and
        // points at the link (Section 7).
        fill_active   <= 1'b1;
        fill_data     <= 8'h00;
        // And mark it. The inversion is Chapter 5.8 §9's convention, so a
        // receiver that tests for it learns this frame was known-bad
        // rather than corrupted in transit.
        force_bad_fcs <= 1'b1;
 
        if (!(&c_underrun)) c_underrun <= c_underrun + 1'b1;
        underrun_seen <= 1'b1;
 
        if (octets_sent > worst_at_octet) worst_at_octet <= octets_sent;
 
        if (c_underrun == '0) begin
          first_at_octet     <= octets_sent;
          first_frame_length <= octets_expected;
        end
      end
    end
  end
 
endmodule

// SYNTHESIZABLE TEST FEATURE.
//
// Emits deliberately malformed frames so that a receive path's error
// handling can be exercised against real traffic.
//
// Every error class Chapters 5 and 6 defined is reachable from here, and
// each is generated by ONE mechanism rather than by a special path, so
// the normal datapath is exercised even while producing bad frames.
//
// The guard is the design content. A test feature that can be enabled in
// production is a way to emit corrupt traffic onto a live network, and
// "it defaults to off" is not a guard -- a register defaults to whatever
// software last wrote.
module tx_error_insertion
  import frame_size_pkg::*;
#(
  // Tied off at integration. A production build ties this low and the
  // whole feature synthesises away; a test build ties it high. It is NOT
  // a software-writable bit, which is the point.
  parameter bit ERROR_INSERTION_PRESENT = 1'b0
) (
  input  logic clk,
  input  logic rst_n,
 
  input  logic       enable,           // ignored unless PRESENT
  input  logic [2:0] error_class,
 
  input  logic       frame_start,
  input  logic [13:0] octet_index,
  input  logic [13:0] frame_length,
 
  output logic       corrupt_octet,    // flip a bit in this octet
  output logic       force_bad_fcs,
  output logic       force_short,      // end the frame early: a fragment
  output logic       force_long,       // overrun the ceiling: a giant
  output logic       force_short_gap,  // Chapter 5.9's floor, violated
  output logic       insertion_active
);
 
  localparam logic [2:0] E_NONE      = 3'd0;
  localparam logic [2:0] E_BIT_FLIP  = 3'd1;  // one payload bit
  localparam logic [2:0] E_BAD_FCS   = 3'd2;  // Chapter 5.8's mismatch
  localparam logic [2:0] E_STOMP     = 3'd3;  // the exact inverse
  localparam logic [2:0] E_FRAGMENT  = 3'd4;  // below the floor
  localparam logic [2:0] E_GIANT     = 3'd5;  // above the ceiling
  localparam logic [2:0] E_SHORT_GAP = 3'd6;  // below the gap floor
 
  wire armed = ERROR_INSERTION_PRESENT && enable;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      corrupt_octet    <= 1'b0;
      force_bad_fcs    <= 1'b0;
      force_short      <= 1'b0;
      force_long       <= 1'b0;
      force_short_gap  <= 1'b0;
      insertion_active <= 1'b0;
    end else begin
      corrupt_octet   <= 1'b0;
      force_short     <= 1'b0;
      force_short_gap <= 1'b0;
 
      if (frame_start) begin
        force_bad_fcs    <= 1'b0;
        force_long       <= 1'b0;
        insertion_active <= armed && (error_class != E_NONE);
      end else if (armed) begin
        case (error_class)
          // A bit flipped mid-payload. Inside the covered range, so the
          // check catches it -- which is what makes it a useful stimulus
          // rather than an interesting one.
          E_BIT_FLIP: if (octet_index == (frame_length >> 1)) corrupt_octet <= 1'b1;
          E_BAD_FCS:  force_bad_fcs <= 1'b1;
          E_STOMP:    force_bad_fcs <= 1'b1;   // datapath inverts instead
          E_FRAGMENT: if (octet_index == 14'd40) force_short <= 1'b1;
          E_GIANT:    force_long <= 1'b1;
          E_SHORT_GAP: force_short_gap <= 1'b1;
          default: ;
        endcase
      end
    end
  end
 
  // The guard, restated where a reviewer will see it. A feature that can
  // emit malformed frames onto a live network must be ABSENT from the
  // netlist, not merely disabled in it -- so the check is on the
  // parameter, and a production build proves it by elaboration.
`ifndef TEST_BUILD
  // synopsys translate_off
  a_insertion_absent_in_production: assert final (ERROR_INSERTION_PRESENT == 1'b0)
    else $fatal(1, "error insertion is present in a non-test build");
  // synopsys translate_on
`endif
 
endmodule

// SYNTHESIZABLE MONITOR.
//
// Watches the octet stream at the INTERFACE and checks that every frame
// leaving this device is well formed.
//
// Placement is the design decision. A monitor on the controller's state
// confirms the state machine sequenced correctly -- which it did, because
// it was written to. A monitor at the interface confirms what actually
// LEFT, so it also catches everything between: a serialiser dropping an
// octet, a clock-domain crossing losing a transfer, a physical-layer
// wrapper inserting or removing idle.
module tx_conformance_monitor
  import frame_size_pkg::*;
  import ifg_pkg::*;
#(
  parameter int unsigned CNT_W = 32,
  parameter int unsigned MAX_FRAME = 1518
) (
  input  logic clk,
  input  logic rst_n,
  input  logic clear,
 
  input  logic       tx_valid,
  input  logic [7:0] tx_data,
  input  logic       tx_last,
  input  logic       in_preamble,
 
  output logic [CNT_W-1:0] c_frames,
  output logic [CNT_W-1:0] c_short_preamble,
  output logic [CNT_W-1:0] c_undersize,     // below the floor
  output logic [CNT_W-1:0] c_oversize,      // above the ceiling
  output logic [CNT_W-1:0] c_short_gap,     // below Chapter 5.9's floor
 
  output logic             any_violation,   // sticky
  output logic [13:0]      first_bad_length
);
 
  logic [13:0] len_q;
  logic [7:0]  pre_q;
  logic [7:0]  gap_q;
  logic        in_frame_q;
 
  function automatic logic [CNT_W-1:0] bump(input logic [CNT_W-1:0] v);
    bump = (&v) ? v : (v + 1'b1);
  endfunction
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      len_q <= '0; pre_q <= '0; gap_q <= '0; in_frame_q <= 1'b0;
      c_frames <= '0; c_short_preamble <= '0; c_undersize <= '0;
      c_oversize <= '0; c_short_gap <= '0;
      any_violation <= 1'b0; first_bad_length <= '0;
    end else begin
      if (clear) begin
        c_frames <= '0; c_short_preamble <= '0; c_undersize <= '0;
        c_oversize <= '0; c_short_gap <= '0;
        // any_violation and first_bad_length deliberately survive: a
        // malformed frame leaving this device is never routine.
      end
 
      if (tx_valid) begin
        gap_q <= '0;
        if (in_preamble) begin
          pre_q      <= pre_q + 1'b1;
          in_frame_q <= 1'b0;
        end else begin
          len_q      <= in_frame_q ? (len_q + 1'b1) : 14'd1;
          in_frame_q <= 1'b1;
 
          if (!in_frame_q) begin
            // First octet after the delimiter: the preamble just ended,
            // so its length can be judged now.
            if (pre_q != 8'd8) begin
              c_short_preamble <= bump(c_short_preamble);
              any_violation    <= 1'b1;
            end
            pre_q <= '0;
          end
        end
 
        if (tx_last) begin
          automatic logic [13:0] final_len = in_frame_q ? (len_q + 1'b1) : 14'd1;
          c_frames <= bump(c_frames);
          in_frame_q <= 1'b0;
 
          // The two size bounds, checked on what actually left rather
          // than on what the controller intended.
          if (final_len < 14'(MIN_FRAME_OCTETS)) begin
            c_undersize <= bump(c_undersize);
            any_violation <= 1'b1;
            if (first_bad_length == '0) first_bad_length <= final_len;
          end
          if (final_len > 14'(MAX_FRAME)) begin
            c_oversize <= bump(c_oversize);
            any_violation <= 1'b1;
            if (first_bad_length == '0) first_bad_length <= final_len;
          end
        end
      end else begin
        // Idle. Counting it here means the gap is measured on the wire,
        // which is the only place it is real.
        gap_q <= (gap_q == 8'hFF) ? gap_q : (gap_q + 1'b1);
        if (tx_valid_next_cycle && (gap_q < 8'(MIN_SINGLE_GAP))) begin
          c_short_gap   <= bump(c_short_gap);
          any_violation <= 1'b1;
        end
      end
    end
  end
 
endmodule

// ---------------------------------------------------------------------
// P1 -- THE COVERED RANGE, as a property of crc_enable across the state
// graph. This one property is Chapter 5.8's Figure 1 (Section 4).
// ---------------------------------------------------------------------
property p_crc_enable_matches_covered_range;
  @(posedge clk) disable iff (!rst_n)
    crc_enable |-> (state inside {S_HEADER, S_DATA, S_PAD});
endproperty
a_crc_enable_matches_covered_range: assert property (p_crc_enable_matches_covered_range);
 
// ---------------------------------------------------------------------
// P2 -- The preamble and delimiter are never covered.
// ---------------------------------------------------------------------
property p_preamble_never_covered;
  @(posedge clk) disable iff (!rst_n)
    (state inside {S_PREAMBLE, S_SFD}) |-> !crc_enable;
endproperty
a_preamble_never_covered: assert property (p_preamble_never_covered);
 
// ---------------------------------------------------------------------
// P3 -- The check sequence never covers itself.
// ---------------------------------------------------------------------
property p_fcs_never_covered;
  @(posedge clk) disable iff (!rst_n)
    (state == S_FCS) |-> !crc_enable;
endproperty
a_fcs_never_covered: assert property (p_fcs_never_covered);
 
// ---------------------------------------------------------------------
// P4 -- THE FIRST ORDERING CONSTRAINT. Padding, when it happens, happens
// before the check sequence -- there is no path from S_FCS to S_PAD.
// ---------------------------------------------------------------------
property p_pad_precedes_fcs;
  @(posedge clk) disable iff (!rst_n)
    (state == S_FCS) |=> (state != S_PAD);
endproperty
a_pad_precedes_fcs: assert property (p_pad_precedes_fcs);
 
// ---------------------------------------------------------------------
// P5 -- THE SECOND ORDERING CONSTRAINT. The gap is only ever entered
// from the check sequence or an abort, never from data or pad.
// ---------------------------------------------------------------------
property p_gap_only_after_fcs;
  @(posedge clk) disable iff (!rst_n)
    (state == S_GAP) |-> ($past(state) inside {S_FCS, S_ABORT, S_GAP});
endproperty
a_gap_only_after_fcs: assert property (p_gap_only_after_fcs);
 
// ---------------------------------------------------------------------
// P6 -- THE QUANTITY, not an ordering. The length field carries the
// CLIENT's octet count. Section 3's fourth row, and the one failure that
// produces a well-formed frame.
// ---------------------------------------------------------------------
property p_length_is_client_count;
  @(posedge clk) disable iff (!rst_n)
    (state == S_HEADER) |-> (emitted_length == $past(req_octets, header_offset));
endproperty
a_length_is_client_count: assert property (p_length_is_client_count)
  else $error("length field carries the padded size, not the client's");
 
// ---------------------------------------------------------------------
// P7 -- The client-data region always reaches the floor.
// ---------------------------------------------------------------------
property p_region_reaches_floor;
  @(posedge clk) disable iff (!rst_n)
    (state == S_FCS) |-> (sent_q >= 11'(MIN_CLIENT));
endproperty
a_region_reaches_floor: assert property (p_region_reaches_floor);
 
// ---------------------------------------------------------------------
// P8 -- A frame is only started when the gap enforcer permits it. The
// floor stays structural because this module asks rather than counts.
// ---------------------------------------------------------------------
property p_start_requires_gap_permission;
  @(posedge clk) disable iff (!rst_n)
    ($past(state) == S_IDLE && state == S_PREAMBLE) |-> $past(gap_permits_start);
endproperty
a_start_requires_gap_permission: assert property (p_start_requires_gap_permission);
 
// ---------------------------------------------------------------------
// P9 -- A frame is only started when the assembler says it can be
// finished. The entire underrun defence (Section 5).
// ---------------------------------------------------------------------
property p_start_requires_safe_to_start;
  @(posedge clk) disable iff (!rst_n)
    ($past(state) == S_IDLE && state == S_PREAMBLE) |-> $past(safe_to_start);
endproperty
a_start_requires_safe_to_start: assert property (p_start_requires_safe_to_start);
 
// ---------------------------------------------------------------------
// P10 -- THE RESPONSE TO STARVATION. An underrun always produces a
// marked frame. Note the shape: it constrains what the design DOES when
// the event happens, and does not forbid the event (Section 11).
// ---------------------------------------------------------------------
property p_underrun_marks_the_frame;
  @(posedge clk) disable iff (!rst_n)
    underrun |-> ##[1:$] (force_bad_fcs until_with tx_last);
endproperty
a_underrun_marks_the_frame: assert property (p_underrun_marks_the_frame)
  else $error("a starved frame was transmitted without being marked");
 
// ---------------------------------------------------------------------
// P11 -- A starved frame is filled to the correct LENGTH as well as
// marked. Marking without filling produces a fragment, which points at
// the link (Section 7).
// ---------------------------------------------------------------------
property p_underrun_frame_is_full_length;
  @(posedge clk) disable iff (!rst_n)
    (frame_aborted && tx_last) |-> (frame_octets >= 14'(MIN_FRAME_OCTETS));
endproperty
a_underrun_frame_is_full_length: assert property (p_underrun_frame_is_full_length);
 
// ---------------------------------------------------------------------
// P12 -- A starved frame is NEVER emitted with a valid check sequence.
// The prohibition on Section 7's second row -- fill and finish normally.
// ---------------------------------------------------------------------
property p_underrun_never_valid;
  @(posedge clk) disable iff (!rst_n)
    (frame_aborted && tx_last) |-> force_bad_fcs;
endproperty
a_underrun_never_valid: assert property (p_underrun_never_valid);
 
// ---------------------------------------------------------------------
// P13 -- An underrun is counted locally. The receiver's rejection tells
// the far end; only this counter tells whoever can fix it.
// ---------------------------------------------------------------------
property p_underrun_counted_locally;
  @(posedge clk) disable iff (!rst_n)
    $rose(underrun) |=> (c_underrun == $past(c_underrun) + 1);
endproperty
a_underrun_counted_locally: assert property (p_underrun_counted_locally);
 
// ---------------------------------------------------------------------
// P14 -- First-cause context survives a counter clear.
// ---------------------------------------------------------------------
property p_underrun_context_survives_clear;
  @(posedge clk) disable iff (!rst_n)
    clear |=> ($stable(first_at_octet) && $stable(worst_at_octet) &&
               $stable(underrun_seen));
endproperty
a_underrun_context_survives_clear: assert property (p_underrun_context_survives_clear);
 
// ---------------------------------------------------------------------
// P15 -- Error insertion is absent, not merely disabled, unless the
// build is a test build.
// ---------------------------------------------------------------------
property p_no_insertion_when_absent;
  @(posedge clk) disable iff (!rst_n)
    (!ERROR_INSERTION_PRESENT) |-> !insertion_active;
endproperty
a_no_insertion_when_absent: assert property (p_no_insertion_when_absent);
 
// ---------------------------------------------------------------------
// P16 -- Every frame leaving the interface is within the size bounds,
// checked on the WIRE rather than on the controller's intent.
// ---------------------------------------------------------------------
property p_wire_frames_in_bounds;
  @(posedge clk) disable iff (!rst_n)
    (tx_valid && tx_last && !frame_aborted)
      |-> ((frame_octets >= 14'(MIN_FRAME_OCTETS)) && (frame_octets <= 14'(MAX_FRAME)));
endproperty
a_wire_frames_in_bounds: assert property (p_wire_frames_in_bounds);
 
// ---------------------------------------------------------------------
// P17 -- The preamble is exactly eight octets including the delimiter.
// ---------------------------------------------------------------------
property p_preamble_length;
  @(posedge clk) disable iff (!rst_n)
    $rose(in_frame_q) |-> ($past(pre_q) == 8'd8);
endproperty
a_preamble_length: assert property (p_preamble_length);
 
// ---------------------------------------------------------------------
// P18 -- COVERAGE. A padded frame, an unpadded frame, and an underrun.
// A run without the third has not exercised Section 8 at all.
// ---------------------------------------------------------------------
c_padded_frame:   cover property (@(posedge clk) disable iff (!rst_n) (state == S_PAD));
c_unpadded_frame: cover property (@(posedge clk) disable iff (!rst_n) (state == S_DATA ##1 state == S_FCS));
c_underrun_seen:  cover property (@(posedge clk) disable iff (!rst_n) underrun);