10 Mbps — The Original Shared-Medium MAC

// SYNTHESIZABLE.
//
// Manchester encoder. The whole transformation is one XOR.
//
// A data bit occupies one bit time and is emitted as two half-bit
// levels: the first is the bit's complement and the second is the bit,
// so the mid-bit transition carries the value.
//
// IEEE 802.3 convention: a HIGH-to-LOW mid-bit transition is a ZERO and
// a LOW-to-HIGH transition is a ONE. Getting this backwards produces a
// perfectly working encoder that every conforming receiver decodes
// inverted -- and Section 4's decoder can recover from exactly that,
// which is why the error survives bring-up.
package mac10_pkg;
 
  // 10 Mb/s: 100 ns bit period, 50 ns half-bit.
  localparam int unsigned BIT_PERIOD_NS  = 100;
  localparam int unsigned HALF_BIT_NS    = 50;
  // Chapter 1.2's slot time, in bit times.
  localparam int unsigned SLOT_BIT_TIMES = 512;
  // Jam emitted on collision, in bits.
  localparam int unsigned JAM_BITS       = 32;
  // Attempts before a frame is abandoned.
  localparam int unsigned MAX_ATTEMPTS   = 16;
  // Backoff exponent stops growing here -- "truncated" binary
  // exponential backoff.
  localparam int unsigned BACKOFF_LIMIT  = 10;
 
endpackage
 
module manchester_encoder
  import mac10_pkg::*;
(
  input  logic clk_2x,       // 20 MHz: one edge per half-bit
  input  logic rst_n,
 
  input  logic bit_valid,
  input  logic bit_in,
  output logic bit_taken,
 
  output logic tx_level,
  output logic tx_active
);
 
  logic phase_q;             // 0 = first half-bit, 1 = second
  logic bit_q;
  logic active_q;
 
  assign bit_taken = bit_valid && !phase_q;
  assign tx_active = active_q;
 
  always_ff @(posedge clk_2x or negedge rst_n) begin
    if (!rst_n) begin
      phase_q  <= 1'b0;
      bit_q    <= 1'b0;
      active_q <= 1'b0;
      tx_level <= 1'b0;
    end else begin
      if (!phase_q) begin
        if (bit_valid) begin
          bit_q    <= bit_in;
          active_q <= 1'b1;
          // First half-bit: the COMPLEMENT. So a one starts low and
          // rises at mid-bit; a zero starts high and falls.
          tx_level <= ~bit_in;
          phase_q  <= 1'b1;
        end else begin
          active_q <= 1'b0;
          tx_level <= 1'b0;
        end
      end else begin
        // Second half-bit: the bit itself. The transition between the
        // two halves IS the encoded value.
        tx_level <= bit_q;
        phase_q  <= 1'b0;
      end
    end
  end
 
endmodule

// SYNTHESIZABLE.
//
// Manchester decoder with polarity recovery.
//
// Two jobs, and the second is the one that gets forgotten:
//
//   1. sample the mid-bit transition and recover the data
//   2. determine which POLARITY the line is in
//
// Twisted pair can be wired with a pair reversed, and a reversed pair
// inverts every transition -- turning every one into a zero and every
// zero into a one. The frame is otherwise perfect: the transitions are
// all present, the timing is all correct, and every bit is wrong.
//
// The preamble is what resolves it. Alternating ones and zeros are
// symmetric under inversion, so the preamble alone cannot -- but the
// START FRAME DELIMITER is not symmetric, and that is what pins the
// polarity down (Chapter 5.2's asymmetry, used for a second purpose).
module manchester_decoder
  import mac10_pkg::*;
(
  input  logic clk_4x,       // 40 MHz: oversample the half-bits
  input  logic rst_n,
 
  input  logic rx_level,
  input  logic carrier,
 
  output logic       bit_valid,
  output logic       bit_out,
  output logic       polarity_inverted,
  output logic       polarity_known,
  // A bit period with no mid-bit transition. Not a data value: a coding
  // violation, which is how the end of a frame is recognised.
  output logic       code_violation,
  output logic [15:0] c_violations
);
 
  logic [1:0] samp_q;
  logic [2:0] cnt_q;
  logic       last_q;
  logic       raw_bit;
 
  // The mid-bit transition's direction is the bit, before polarity is
  // applied. Section 3's convention: low-to-high is a one.
  assign raw_bit = (~last_q) & rx_level;
 
  always_ff @(posedge clk_4x or negedge rst_n) begin
    if (!rst_n) begin
      samp_q <= '0; cnt_q <= '0; last_q <= 1'b0;
      bit_valid <= 1'b0; bit_out <= 1'b0;
      polarity_inverted <= 1'b0; polarity_known <= 1'b0;
      code_violation <= 1'b0; c_violations <= '0;
    end else begin
      bit_valid      <= 1'b0;
      code_violation <= 1'b0;
 
      if (!carrier) begin
        cnt_q <= '0;
        // Polarity is NOT forgotten between frames. It is a property of
        // the cabling, which does not change while the link is up, and
        // relearning it every frame wastes the preamble on a question
        // that was already answered.
      end else begin
        samp_q <= {samp_q[0], rx_level};
 
        if (cnt_q == 3'd3) begin
          cnt_q <= '0;
          if (samp_q[1] == samp_q[0]) begin
            // No transition where one is guaranteed. Either the frame
            // has ended or the signal is corrupt.
            code_violation <= 1'b1;
            if (!(&c_violations)) c_violations <= c_violations + 1'b1;
          end else begin
            bit_valid <= 1'b1;
            bit_out   <= polarity_inverted ? ~raw_bit : raw_bit;
          end
          last_q <= rx_level;
        end else begin
          cnt_q <= cnt_q + 1'b1;
        end
      end
    end
  end
 
endmodule

// SYNTHESIZABLE.
//
// Carrier sense, collision detect, jam and backoff.
//
// The part worth reading is the collision CLASSIFICATION. A collision
// inside the slot time is ordinary contention: the protocol working
// exactly as designed, and the correct response is to jam, back off and
// retry. A collision AFTER the slot time cannot happen on a conforming
// network, so it means the network is not conforming -- too long, too
// many repeaters, or a duplex mismatch (Chapter 9.2's classic fault).
//
// Retrying a late collision is the default behaviour and it is wrong.
// The frame will collide again for the same physical reason, and the
// retry hides a configuration fault behind an error counter.
module carrier_collision_frontend
  import mac10_pkg::*;
#(
  parameter int unsigned CNT_W = 16
) (
  input  logic clk,          // 10 MHz bit clock
  input  logic rst_n,
  input  logic clear,
 
  // From the transceiver.
  input  logic carrier_sense,
  input  logic collision_in,
 
  input  logic tx_request,
  input  logic tx_last_bit,
 
  output logic tx_enable,
  output logic jam_active,
  output logic frame_abandoned,
 
  output logic             late_collision,
  output logic [CNT_W-1:0] c_collisions,
  output logic [CNT_W-1:0] c_late_collisions,
  output logic [CNT_W-1:0] c_abandoned,
  // Attempts on the frame that needed the most. A saturated network
  // shows in this long before frames start being abandoned.
  output logic [4:0]       worst_attempts,
  output logic             late_collision_seen   // sticky
);
 
  typedef enum logic [2:0] {
    C_IDLE, C_DEFER, C_XMIT, C_JAM, C_BACKOFF
  } c_state_e;
 
  c_state_e    state_q;
  logic [9:0]  bits_q;        // bit times into the current transmission
  logic [4:0]  attempts_q;
  logic [15:0] backoff_q;
  logic [4:0]  jam_q;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      state_q <= C_IDLE; bits_q <= '0; attempts_q <= '0;
      backoff_q <= '0; jam_q <= '0;
      tx_enable <= 1'b0; jam_active <= 1'b0; frame_abandoned <= 1'b0;
      late_collision <= 1'b0; c_collisions <= '0; c_late_collisions <= '0;
      c_abandoned <= '0; worst_attempts <= '0; late_collision_seen <= 1'b0;
    end else begin
      late_collision  <= 1'b0;
      frame_abandoned <= 1'b0;
 
      if (clear) begin
        c_collisions <= '0; c_late_collisions <= '0; c_abandoned <= '0;
        // worst_attempts and late_collision_seen deliberately survive.
      end
 
      case (state_q)
        C_IDLE: if (tx_request) begin
          // Carrier sense: defer while the medium is busy. This is the
          // "CS" of CSMA/CD and it is a whole state because deferring is
          // the common case on a busy segment.
          state_q    <= carrier_sense ? C_DEFER : C_XMIT;
          bits_q     <= '0;
          attempts_q <= '0;
          tx_enable  <= !carrier_sense;
        end
 
        C_DEFER: if (!carrier_sense) begin
          // The interframe gap is enforced elsewhere (Chapter 5.9); this
          // state only waits for the medium to go quiet.
          state_q   <= C_XMIT;
          tx_enable <= 1'b1;
          bits_q    <= '0;
        end
 
        C_XMIT: begin
          bits_q <= bits_q + 1'b1;
 
          if (collision_in) begin
            tx_enable  <= 1'b0;
            jam_active <= 1'b1;
            jam_q      <= '0;
            state_q    <= C_JAM;
            if (!(&c_collisions)) c_collisions <= c_collisions + 1'b1;
 
            // THE CLASSIFICATION. Past the slot time, a collision cannot
            // happen on a conforming network.
            if (bits_q >= 10'(SLOT_BIT_TIMES)) begin
              late_collision      <= 1'b1;
              late_collision_seen <= 1'b1;
              if (!(&c_late_collisions)) c_late_collisions <= c_late_collisions + 1'b1;
            end
          end else if (tx_last_bit) begin
            tx_enable <= 1'b0;
            state_q   <= C_IDLE;
            if (attempts_q > worst_attempts) worst_attempts <= attempts_q;
          end
        end
 
        C_JAM: begin
          // A fixed 32 bits, so that every station on the segment sees
          // the collision for long enough to detect it.
          if (jam_q == 5'(JAM_BITS - 1)) begin
            jam_active <= 1'b0;
            attempts_q <= attempts_q + 1'b1;
 
            if (late_collision_seen && (bits_q >= 10'(SLOT_BIT_TIMES))) begin
              // A late collision is not retried. Retrying reproduces the
              // physical fault and hides it.
              state_q         <= C_IDLE;
              frame_abandoned <= 1'b1;
              if (!(&c_abandoned)) c_abandoned <= c_abandoned + 1'b1;
            end else if (attempts_q == 5'(MAX_ATTEMPTS - 1)) begin
              state_q         <= C_IDLE;
              frame_abandoned <= 1'b1;
              if (!(&c_abandoned)) c_abandoned <= c_abandoned + 1'b1;
              if (attempts_q > worst_attempts) worst_attempts <= attempts_q;
            end else begin
              state_q <= C_BACKOFF;
              // Truncated binary exponential: the range doubles with each
              // attempt and stops doubling at BACKOFF_LIMIT.
              backoff_q <= random_slots(attempts_q);
            end
          end else begin
            jam_q <= jam_q + 1'b1;
          end
        end
 
        C_BACKOFF: if (backoff_q == '0) begin
          state_q <= carrier_sense ? C_DEFER : C_XMIT;
          bits_q  <= '0;
        end else begin
          backoff_q <= backoff_q - 1'b1;
        end
 
        default: state_q <= C_IDLE;
      endcase
    end
  end
 
  // Uniform over 0 .. 2^k - 1 slot times, k capped at BACKOFF_LIMIT.
  // The cap is what makes it "truncated": without it the range doubles
  // sixteen times and the last attempts wait for minutes.
  function automatic logic [15:0] random_slots(input logic [4:0] attempt);
    automatic int unsigned k =
        (attempt > 5'(BACKOFF_LIMIT)) ? BACKOFF_LIMIT : int'(attempt);
    random_slots = 16'($urandom_range((1 << k) - 1, 0)) * 16'(SLOT_BIT_TIMES);
  endfunction
 
endmodule

// SYNTHESIZABLE.
//
// Observes the SQE test and turns its presence or absence into a
// statement about the transceiver.
//
// Three states, and they are genuinely different findings:
//
//   heartbeat present after every frame -> the collision detector is
//        connected and working. The normal case for a station attached
//        directly to a medium.
//   heartbeat absent, consistently     -> either the transceiver has
//        SQE disabled (correct when attached to a repeater) or its
//        collision circuitry has failed. THESE ARE INDISTINGUISHABLE
//        from the signal alone, which is why the expected mode is a
//        configuration input rather than something inferred.
//   heartbeat intermittent             -> a fault. A working test is
//        deterministic; an unreliable one means a marginal connection.
module sqe_test_observer
  import mac10_pkg::*;
#(
  // Window after a transmission ends within which the heartbeat is
  // expected, in bit times.
  parameter int unsigned SQE_WINDOW_BITS = 15,
  // Whether SQE is expected at all. MUST be false when attached to a
  // repeater, and the design cannot work this out for itself.
  parameter bit SQE_EXPECTED = 1'b1,
  parameter int unsigned CNT_W = 16
) (
  input  logic clk,
  input  logic rst_n,
  input  logic clear,
 
  input  logic tx_done,
  input  logic collision_in,
  input  logic tx_active,
 
  output logic             heartbeat_seen,
  output logic             heartbeat_missing,
  // A collision indication outside both a transmission and the SQE
  // window. On a half-duplex medium this should not happen, and it
  // usually means the transceiver is asserting collision spuriously.
  output logic             spurious_collision,
 
  output logic [CNT_W-1:0] c_frames_sent,
  output logic [CNT_W-1:0] c_heartbeats,
  output logic [CNT_W-1:0] c_missing,
  output logic [CNT_W-1:0] c_spurious,
 
  // Sticky: a transceiver that has ever failed its own self-test is a
  // transceiver whose collision reports cannot be trusted, and that
  // fact outlives the counter.
  output logic             detector_suspect
);
 
  logic [4:0] window_q;
  logic       armed_q;
  logic       seen_q;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      window_q <= '0; armed_q <= 1'b0; seen_q <= 1'b0;
      heartbeat_seen <= 1'b0; heartbeat_missing <= 1'b0;
      spurious_collision <= 1'b0;
      c_frames_sent <= '0; c_heartbeats <= '0; c_missing <= '0; c_spurious <= '0;
      detector_suspect <= 1'b0;
    end else begin
      heartbeat_seen     <= 1'b0;
      heartbeat_missing  <= 1'b0;
      spurious_collision <= 1'b0;
 
      if (clear) begin
        c_frames_sent <= '0; c_heartbeats <= '0;
        c_missing <= '0; c_spurious <= '0;
        // detector_suspect deliberately survives.
      end
 
      if (tx_done) begin
        if (!(&c_frames_sent)) c_frames_sent <= c_frames_sent + 1'b1;
        armed_q  <= SQE_EXPECTED;
        window_q <= '0;
        seen_q   <= 1'b0;
      end else if (armed_q) begin
        if (collision_in && !seen_q) begin
          seen_q         <= 1'b1;
          heartbeat_seen <= 1'b1;
          if (!(&c_heartbeats)) c_heartbeats <= c_heartbeats + 1'b1;
        end
 
        if (window_q == 5'(SQE_WINDOW_BITS)) begin
          armed_q <= 1'b0;
          if (!seen_q) begin
            // The self-test did not run. With SQE_EXPECTED set, that
            // means the transceiver cannot prove its collision detector
            // works -- so nothing it reports about collisions can be
            // relied on.
            heartbeat_missing <= 1'b1;
            detector_suspect  <= 1'b1;
            if (!(&c_missing)) c_missing <= c_missing + 1'b1;
          end
        end else begin
          window_q <= window_q + 1'b1;
        end
      end else if (collision_in && !tx_active) begin
        // Collision asserted while not transmitting and outside the SQE
        // window. On a half-duplex medium a station cannot collide with
        // traffic it is not part of.
        spurious_collision <= 1'b1;
        detector_suspect   <= 1'b1;
        if (!(&c_spurious)) c_spurious <= c_spurious + 1'b1;
      end
    end
  end
 
endmodule

// SYNTHESIZABLE.
//
// Emits link integrity pulses when idle and maintains link state from
// pulses and data together.
//
// The subtleties are all in the timing constants, and each has a reason:
//
//   TX interval 16 ms   -- often enough that a real failure is noticed
//        quickly, rare enough to cost nothing on a busy link.
//   RX timeout > 2x     -- a single missed pulse is noise. A link that
//        drops on one missed pulse flaps continuously on a marginal
//        cable, which is worse than being slightly slow to notice.
//   data counts as life -- a busy link proves itself with traffic and
//        need not interrupt itself.
module link_integrity_pulse
  import mac10_pkg::*;
#(
  // Clock cycles per millisecond, so the timing constants can be stated
  // in the units the standard uses.
  parameter int unsigned CYCLES_PER_MS = 10_000,
  parameter int unsigned TX_INTERVAL_MS = 16,
  // Several intervals, so one missed pulse does not drop the link.
  parameter int unsigned RX_TIMEOUT_MS  = 100,
  parameter int unsigned CNT_W = 16
) (
  input  logic clk,
  input  logic rst_n,
  input  logic clear,
 
  input  logic tx_active,          // a frame is being sent
  input  logic rx_pulse,           // a link pulse was received
  input  logic rx_data,            // data was received
 
  output logic tx_pulse,
  output logic link_up,
 
  output logic [CNT_W-1:0] c_pulses_sent,
  output logic [CNT_W-1:0] c_pulses_rcvd,
  output logic [CNT_W-1:0] c_link_transitions,
  // Longest silence ever observed while the link stayed up. A link whose
  // worst gap approaches the timeout is one flap away from dropping, and
  // no counter of transitions says so.
  output logic [CNT_W-1:0] worst_silence_ms
);
 
  logic [31:0] tx_ctr_q;
  logic [31:0] rx_ctr_q;
  logic [31:0] ms_ctr_q;
  logic [CNT_W-1:0] silence_ms_q;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      tx_ctr_q <= '0; rx_ctr_q <= '0; ms_ctr_q <= '0; silence_ms_q <= '0;
      tx_pulse <= 1'b0; link_up <= 1'b0;
      c_pulses_sent <= '0; c_pulses_rcvd <= '0;
      c_link_transitions <= '0; worst_silence_ms <= '0;
    end else begin
      tx_pulse <= 1'b0;
 
      if (clear) begin
        c_pulses_sent <= '0; c_pulses_rcvd <= '0; c_link_transitions <= '0;
        // worst_silence_ms deliberately survives: it characterises the
        // cable, not the measurement window.
      end
 
      // TRANSMIT. A frame in flight restarts the interval -- the traffic
      // is itself the proof, so the pulse would be redundant.
      if (tx_active) begin
        tx_ctr_q <= '0;
      end else if (tx_ctr_q >= 32'(TX_INTERVAL_MS * CYCLES_PER_MS)) begin
        tx_pulse <= 1'b1;
        tx_ctr_q <= '0;
        if (!(&c_pulses_sent)) c_pulses_sent <= c_pulses_sent + 1'b1;
      end else begin
        tx_ctr_q <= tx_ctr_q + 1'b1;
      end
 
      // RECEIVE. Either a pulse or data resets the timeout, and the
      // symmetry with the transmit side is deliberate.
      if (rx_pulse || rx_data) begin
        if (rx_pulse && !(&c_pulses_rcvd)) c_pulses_rcvd <= c_pulses_rcvd + 1'b1;
        rx_ctr_q <= '0;
        if (silence_ms_q > worst_silence_ms) worst_silence_ms <= silence_ms_q;
        silence_ms_q <= '0;
        if (!link_up) begin
          link_up <= 1'b1;
          if (!(&c_link_transitions)) c_link_transitions <= c_link_transitions + 1'b1;
        end
      end else if (rx_ctr_q >= 32'(RX_TIMEOUT_MS * CYCLES_PER_MS)) begin
        if (link_up) begin
          link_up <= 1'b0;
          if (!(&c_link_transitions)) c_link_transitions <= c_link_transitions + 1'b1;
        end
      end else begin
        rx_ctr_q <= rx_ctr_q + 1'b1;
      end
 
      // Millisecond tick for the silence measurement.
      if (ms_ctr_q >= 32'(CYCLES_PER_MS - 1)) begin
        ms_ctr_q <= '0;
        if (!(&silence_ms_q)) silence_ms_q <= silence_ms_q + 1'b1;
      end else begin
        ms_ctr_q <= ms_ctr_q + 1'b1;
      end
    end
  end
 
endmodule

// ---------------------------------------------------------------------
// P1 -- THE CODING PROPERTY. A transition in every bit time, whatever
// the data. Everything Manchester buys follows from this.
// ---------------------------------------------------------------------
property p_transition_every_bit;
  @(posedge clk_2x) disable iff (!rst_n)
    (tx_active && phase_q) |-> (tx_level != $past(tx_level));
endproperty
a_transition_every_bit: assert property (p_transition_every_bit)
  else $error("no mid-bit transition -- the code is not self-clocking");
 
// ---------------------------------------------------------------------
// P2 -- EXACT DC BALANCE. Each bit emits one high half and one low half,
// which is what lets the signal cross a transformer.
// ---------------------------------------------------------------------
property p_dc_balanced_per_bit;
  @(posedge clk_2x) disable iff (!rst_n)
    (tx_active && phase_q) |-> ($past(tx_level) == ~tx_level);
endproperty
a_dc_balanced_per_bit: assert property (p_dc_balanced_per_bit);
 
// ---------------------------------------------------------------------
// P3 -- The encoding is the polarity convention. A low-to-high mid-bit
// transition is a one.
// ---------------------------------------------------------------------
property p_polarity_convention;
  @(posedge clk_2x) disable iff (!rst_n)
    (tx_active && phase_q) |-> (tx_level == bit_q);
endproperty
a_polarity_convention: assert property (p_polarity_convention);
 
// ---------------------------------------------------------------------
// P4 -- Encode then decode is the identity, WHEN the polarity is known.
// The qualifier is the point: without it the round trip inverts.
// ---------------------------------------------------------------------
property p_encode_decode_identity;
  @(posedge clk) disable iff (!rst_n)
    (bit_valid && polarity_known) |-> (bit_out == $past(bit_in, ENC_LATENCY));
endproperty
a_encode_decode_identity: assert property (p_encode_decode_identity);
 
// ---------------------------------------------------------------------
// P5 -- Polarity survives between frames: it is a property of the
// cabling, not of the frame.
// ---------------------------------------------------------------------
property p_polarity_persists;
  @(posedge clk) disable iff (!rst_n)
    (polarity_known && !carrier) |=> $stable(polarity_inverted);
endproperty
a_polarity_persists: assert property (p_polarity_persists);
 
// ---------------------------------------------------------------------
// P6 -- A missing mid-bit transition is a CODE VIOLATION, never a data
// value. Decoding it as data invents bits the transmitter never sent.
// ---------------------------------------------------------------------
property p_violation_not_decoded;
  @(posedge clk) disable iff (!rst_n)
    code_violation |-> !bit_valid;
endproperty
a_violation_not_decoded: assert property (p_violation_not_decoded);
 
// ---------------------------------------------------------------------
// P7 -- Deference: a transmission never starts while carrier is sensed.
// The "CS" of CSMA/CD, as a property.
// ---------------------------------------------------------------------
property p_defers_to_carrier;
  @(posedge clk) disable iff (!rst_n)
    ($rose(tx_enable)) |-> !$past(carrier_sense);
endproperty
a_defers_to_carrier: assert property (p_defers_to_carrier);
 
// ---------------------------------------------------------------------
// P8 -- A collision always produces a jam of exactly the specified
// length, so every station on the segment sees it long enough.
// ---------------------------------------------------------------------
property p_jam_length;
  @(posedge clk) disable iff (!rst_n)
    $rose(jam_active) |-> ##JAM_BITS $fell(jam_active);
endproperty
a_jam_length: assert property (p_jam_length);
 
// ---------------------------------------------------------------------
// P9 -- THE CLASSIFICATION. A collision after the slot time is a LATE
// collision, and the two classes are decided by the bit count alone.
// ---------------------------------------------------------------------
property p_late_collision_classified;
  @(posedge clk) disable iff (!rst_n)
    (collision_in && (state == C_XMIT) && (bits_q >= 10'(SLOT_BIT_TIMES)))
      |-> late_collision;
endproperty
a_late_collision_classified: assert property (p_late_collision_classified);
 
// ---------------------------------------------------------------------
// P10 -- A late collision is NOT retried. Retrying reproduces a physical
// fault and hides it behind a collision counter.
// ---------------------------------------------------------------------
property p_late_collision_not_retried;
  @(posedge clk) disable iff (!rst_n)
    late_collision |-> ##[1:JAM_BITS+2] frame_abandoned;
endproperty
a_late_collision_not_retried: assert property (p_late_collision_not_retried)
  else $error("a late collision was retried -- the network is over-length and this hides it");
 
// ---------------------------------------------------------------------
// P11 -- The backoff is truncated. Without the cap the final attempts
// wait for seconds.
// ---------------------------------------------------------------------
property p_backoff_truncated;
  @(posedge clk) disable iff (!rst_n)
    (state == C_BACKOFF) |-> (backoff_q <= 16'((1 << BACKOFF_LIMIT) - 1) * 16'(SLOT_BIT_TIMES));
endproperty
a_backoff_truncated: assert property (p_backoff_truncated);
 
// ---------------------------------------------------------------------
// P12 -- A frame is abandoned after at most MAX_ATTEMPTS.
// ---------------------------------------------------------------------
property p_attempts_bounded;
  @(posedge clk) disable iff (!rst_n)
    (attempts_q <= 5'(MAX_ATTEMPTS));
endproperty
a_attempts_bounded: assert property (p_attempts_bounded);
 
// ---------------------------------------------------------------------
// P13 -- The heartbeat, when expected, arrives within its window after
// every transmission. This is what makes the detector CHECKED rather
// than assumed -- compare the rejected property below.
// ---------------------------------------------------------------------
property p_heartbeat_follows_transmission;
  @(posedge clk) disable iff (!rst_n)
    (SQE_EXPECTED && tx_done) |-> ##[1:SQE_WINDOW_BITS] heartbeat_seen;
endproperty
a_heartbeat_follows_transmission: assert property (p_heartbeat_follows_transmission);
 
// ---------------------------------------------------------------------
// P14 -- A missing heartbeat makes the detector suspect, and the flag is
// sticky: a transceiver that once failed its self-test cannot be trusted
// about collisions afterwards.
// ---------------------------------------------------------------------
property p_missing_heartbeat_is_sticky;
  @(posedge clk) disable iff (!rst_n)
    heartbeat_missing |=> detector_suspect;
endproperty
a_missing_heartbeat_is_sticky: assert property (p_missing_heartbeat_is_sticky);
 
// ---------------------------------------------------------------------
// P15 -- A collision indication outside a transmission and outside the
// SQE window is spurious. A half-duplex station cannot collide with
// traffic it is not part of.
// ---------------------------------------------------------------------
property p_no_collision_while_idle;
  @(posedge clk) disable iff (!rst_n)
    (collision_in && !tx_active && !armed_q) |-> spurious_collision;
endproperty
a_no_collision_while_idle: assert property (p_no_collision_while_idle);
 
// ---------------------------------------------------------------------
// P16 -- Link pulses are suppressed while transmitting: the traffic is
// itself the proof of life.
// ---------------------------------------------------------------------
property p_no_pulse_during_traffic;
  @(posedge clk) disable iff (!rst_n)
    tx_active |-> !tx_pulse;
endproperty
a_no_pulse_during_traffic: assert property (p_no_pulse_during_traffic);
 
// ---------------------------------------------------------------------
// P17 -- The receive timeout is longer than several transmit intervals,
// so one missed pulse cannot drop the link.
// ---------------------------------------------------------------------
// synopsys translate_off
a_timeout_tolerates_a_miss: assert final (RX_TIMEOUT_MS >= 3 * TX_INTERVAL_MS)
  else $fatal(1, "link timeout is too short -- one missed pulse will drop the link");
// synopsys translate_on
 
// ---------------------------------------------------------------------
// P18 -- COVERAGE. A late collision, a missing heartbeat, a polarity
// inversion and an abandoned frame -- four states a healthy network
// never reaches and a verification run must.
// ---------------------------------------------------------------------
c_late_collision:   cover property (@(posedge clk) disable iff (!rst_n) late_collision);
c_missing_heartbeat:cover property (@(posedge clk) disable iff (!rst_n) heartbeat_missing);
c_polarity_flip:    cover property (@(posedge clk) disable iff (!rst_n) polarity_inverted);
c_abandoned:        cover property (@(posedge clk) disable iff (!rst_n) frame_abandoned);