CRC-32 Generation

x^32 + x^26 + x^23 + x^22 + x^16 + x^12 + x^11 + x^10
     + x^8 + x^7 + x^5 + x^4 + x^2 + x + 1

// SYNTHESIZABLE.
//
// Polynomial division, one message bit per clock. This is the entire
// mathematics of CRC-32 and it is thirty lines.
//
// It is NOT an Ethernet FCS engine. Four conventions are missing, and a
// design that stops here interoperates with nothing -- while passing
// every test that compares it against itself.
package crc32_pkg;
 
  // NORMATIVE. The generator, x^32 implicit: it is the bit that shifts
  // out and drives the feedback, so it is never stored.
  localparam logic [31:0] POLY_MSB = 32'h04C1_1DB7;
 
  // The same polynomial with its bit order reversed. NOT a different
  // polynomial -- Section 11 makes that precise. It is what an LSB-first
  // shift register needs, because reversing the shift direction reverses
  // which end the taps must be read from.
  localparam logic [31:0] POLY_LSB = 32'hEDB8_8320;
 
  // NORMATIVE, and all four are conventions rather than mathematics.
  localparam logic [31:0] INIT_VALUE  = 32'hFFFF_FFFF;
  localparam bit          REFLECT_IN  = 1'b1;
  localparam bit          REFLECT_OUT = 1'b1;
  localparam logic [31:0] XOR_OUT     = 32'hFFFF_FFFF;
 
  // The published check value for the nine ASCII characters "123456789"
  // under all four Ethernet conventions. Section 7 uses it as a self-test.
  localparam logic [31:0] CHECK_123456789 = 32'hCBF4_3926;
 
  function automatic logic [31:0] reflect32(input logic [31:0] v);
    for (int i = 0; i < 32; i++) reflect32[i] = v[31-i];
  endfunction
 
  function automatic logic [7:0] reflect8(input logic [7:0] v);
    for (int i = 0; i < 8; i++) reflect8[i] = v[7-i];
  endfunction
 
endpackage
 
module crc32_serial
  import crc32_pkg::*;
(
  input  logic clk,
  input  logic rst_n,
 
  // Load an arbitrary starting value. Exposed rather than hard-wired,
  // because WHICH value is a convention and this module holds none.
  input  logic        preset,
  input  logic [31:0] preset_value,
 
  input  logic        bit_valid,
  input  logic        bit_in,
 
  // The raw register. Not the FCS: no reflection, no complement.
  output logic [31:0] crc_reg
);
 
  // The feedback bit is the message bit exclusive-ored with the bit about
  // to leave the register. When it is set, the divisor "fits" and is
  // subtracted -- and subtraction here is exclusive-or, because there are
  // no carries in this field.
  wire feedback = bit_in ^ crc_reg[31];
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      crc_reg <= '0;
    end else if (preset) begin
      crc_reg <= preset_value;
    end else if (bit_valid) begin
      // Shift left by one, and conditionally subtract the generator.
      // Every tap position is a term of the polynomial; there is no
      // arithmetic here beyond that.
      crc_reg <= {crc_reg[30:0], 1'b0} ^ (feedback ? POLY_MSB : 32'h0);
    end
  end
 
endmodule

// SYNTHESIZABLE.
//
// The four conventions, applied around the division of Section 3.
//
// Order matters and is fixed:
//
//   1. preset the register to INIT
//   2. reflect each input octet, if REFLECT_IN
//   3. divide (the only mathematics)
//   4. reflect the 32-bit result, if REFLECT_OUT
//   5. exclusive-or with XOR_OUT
//
// Each is a parameter rather than a constant, so that ONE engine can be
// instantiated as the design's own and again as a differently-configured
// reference -- which is what Section 9 needs and what a hard-coded engine
// makes impossible.
module crc32_conventional
  import crc32_pkg::*;
#(
  parameter logic [31:0] INIT     = INIT_VALUE,
  parameter bit          REF_IN   = REFLECT_IN,
  parameter bit          REF_OUT  = REFLECT_OUT,
  parameter logic [31:0] FINAL_XOR = XOR_OUT
) (
  input  logic clk,
  input  logic rst_n,
 
  input  logic       frame_start,
  input  logic       oct_valid,
  input  logic [7:0] oct_data,
  input  logic       oct_last,
 
  output logic        fcs_valid,
  output logic [31:0] fcs,
 
  // The raw register, exposed for Section 12's discussion of why it must
  // not be asserted on.
  output logic [31:0] raw_reg
);
 
  logic [31:0] reg_q;
  logic [2:0]  bit_q;
  logic        busy_q;
  logic [7:0]  oct_q;
 
  assign raw_reg = reg_q;
 
  // Convention 2. Reflection is applied to the OCTET, not to the frame:
  // each octet is fed least-significant-bit first, which is the order the
  // bits go on the wire (Chapter 5.3's I/G bit is first for this reason).
  wire [7:0] oct_applied = REF_IN ? reflect8(oct_data) : oct_data;
 
  wire feedback = oct_q[7] ^ reg_q[31];
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      reg_q     <= INIT;
      bit_q     <= '0;
      busy_q    <= 1'b0;
      oct_q     <= '0;
      fcs_valid <= 1'b0;
      fcs       <= '0;
    end else begin
      fcs_valid <= 1'b0;
 
      if (frame_start) begin
        // Convention 1. The register starts at INIT, not at zero, and
        // Section 6 shows what that buys.
        reg_q  <= INIT;
        busy_q <= 1'b0;
      end else if (oct_valid && !busy_q) begin
        oct_q  <= oct_applied;
        bit_q  <= '0;
        busy_q <= 1'b1;
      end else if (busy_q) begin
        // The division, eight bits per octet.
        reg_q <= {reg_q[30:0], 1'b0} ^ (feedback ? POLY_MSB : 32'h0);
        oct_q <= {oct_q[6:0], 1'b0};
 
        if (bit_q == 3'd7) begin
          busy_q <= 1'b0;
          if (oct_last) begin
            // Conventions 3 and 4, in that order. Swapping them gives a
            // different value: reflecting a complemented word is not the
            // same as complementing a reflected one unless the mask is
            // symmetric -- which 0xFFFFFFFF happens to be, so Ethernet
            // survives the swap and other variants do not.
            automatic logic [31:0] div_result =
                {reg_q[30:0], 1'b0} ^ (feedback ? POLY_MSB : 32'h0);
            automatic logic [31:0] reflected =
                REF_OUT ? reflect32(div_result) : div_result;
            fcs       <= reflected ^ FINAL_XOR;
            fcs_valid <= 1'b1;
          end
        end else begin
          bit_q <= bit_q + 1'b1;
        end
      end
    end
  end
 
endmodule

// SYNTHESIZABLE SELF-TEST.
//
// Runs a fixed nine-octet message through the design's OWN engine and
// compares against the published check value.
//
// Why a built-in self-test rather than a simulation-only check: the
// conventions are configuration, and configuration survives into
// silicon. A parameter overridden in an integration wrapper, a variant
// instantiated by mistake, a synthesis constant that did not propagate --
// all of these produce a working CRC engine computing the wrong value,
// and none of them is visible until a peer rejects every frame.
//
// This runs once at reset and answers the question in nine octets.
module crc32_golden_selftest
  import crc32_pkg::*;
(
  input  logic clk,
  input  logic rst_n,
 
  input  logic start,
 
  output logic        drive_valid,
  output logic [7:0]  drive_data,
  output logic        drive_last,
  output logic        drive_start,
 
  input  logic        fcs_valid,
  input  logic [31:0] fcs,
 
  output logic        selftest_done,
  output logic        selftest_pass,
  // Kept on failure: the value the engine actually produced, which
  // Section 9 turns into a diagnosis rather than a bare failure.
  output logic [31:0] observed,
  output logic [31:0] expected
);
 
  // "123456789" -- the check message used by every published CRC
  // catalogue, so the expected value can be looked up rather than
  // derived, which is the point of a golden vector.
  localparam int unsigned N = 9;
  localparam logic [7:0] MSG [N] = '{
    8'h31, 8'h32, 8'h33, 8'h34, 8'h35, 8'h36, 8'h37, 8'h38, 8'h39
  };
 
  typedef enum logic [1:0] { T_IDLE, T_START, T_DRIVE, T_WAIT } t_e;
  t_e state_q;
  logic [3:0] idx_q;
 
  assign expected = CHECK_123456789;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      state_q       <= T_IDLE;
      idx_q         <= '0;
      drive_valid   <= 1'b0;
      drive_start   <= 1'b0;
      drive_last    <= 1'b0;
      drive_data    <= '0;
      selftest_done <= 1'b0;
      selftest_pass <= 1'b0;
      observed      <= '0;
    end else begin
      drive_valid <= 1'b0;
      drive_start <= 1'b0;
      drive_last  <= 1'b0;
 
      case (state_q)
        T_IDLE: if (start) begin
          state_q       <= T_START;
          idx_q         <= '0;
          selftest_done <= 1'b0;
        end
 
        T_START: begin
          drive_start <= 1'b1;
          state_q     <= T_DRIVE;
        end
 
        T_DRIVE: begin
          drive_valid <= 1'b1;
          drive_data  <= MSG[idx_q];
          drive_last  <= (idx_q == 4'(N-1));
          if (idx_q == 4'(N-1)) state_q <= T_WAIT;
          else                  idx_q   <= idx_q + 1'b1;
        end
 
        T_WAIT: if (fcs_valid) begin
          observed      <= fcs;
          selftest_pass <= (fcs == CHECK_123456789);
          selftest_done <= 1'b1;
          state_q       <= T_IDLE;
        end
 
        default: state_q <= T_IDLE;
      endcase
    end
  end
 
endmodule

// SYNTHESIZABLE DIAGNOSTIC.
//
// Turns "the check sequence disagrees" into "the peer's final complement
// is missing", which is a fix rather than a symptom.
//
// Method: hold the design's own computed value and the peer's received
// value, then apply the four candidate transformations and see which one
// reconciles them. Two of the four are pure transformations of the
// result; the other two need a recomputation, so a second engine
// instance is fed the same octets under an alternative configuration.
module convention_mismatch_identifier
  import crc32_pkg::*;
#(
  parameter int unsigned CNT_W = 16
) (
  input  logic clk,
  input  logic rst_n,
  input  logic clear,
 
  input  logic        result_valid,
  input  logic [31:0] computed,        // this design, Ethernet conventions
  input  logic [31:0] received,        // from the peer's FCS field
  input  logic [13:0] frame_octets,
 
  // A second engine over the same octets with INIT = 0. Everything else
  // identical. This is the recomputation the initial-value test needs.
  input  logic        alt_init_valid,
  input  logic [31:0] alt_init_result,
 
  // A third engine with REF_IN = 0, everything else identical.
  input  logic        alt_refin_valid,
  input  logic [31:0] alt_refin_result,
 
  output logic        verdict_valid,
  output logic        diff_complement,
  output logic        diff_out_reflect,
  output logic        diff_init,
  output logic        diff_in_reflect,
  output logic        unexplained,
 
  output logic [CNT_W-1:0] c_mismatch,
  // Sticky first verdict plus the evidence behind it.
  output logic             verdict_latched,
  output logic [31:0]      first_delta,
  output logic [13:0]      first_length
);
 
  wire [31:0] delta = computed ^ received;
 
  // TEST 1. A complement difference is an XOR with a constant applied
  // after everything else, so the delta is that constant -- for every
  // message, at every length. One frame settles it.
  wire t_complement = (delta == 32'hFFFF_FFFF);
 
  // TEST 2. An output-reflection difference means one value is the
  // bit-reversal of the other. Also decidable from one frame.
  wire t_out_reflect = (reflect32(computed) == received);
 
  // TEST 3. An initial-value difference is only detectable by
  // recomputing, because the delta depends on message content and length.
  wire t_init = alt_init_valid && (alt_init_result == received);
 
  // TEST 4. Likewise for input reflection, and note it cannot be
  // recovered by transforming the result at all -- it changed what was
  // divided, not how the answer was presented.
  wire t_in_reflect = alt_refin_valid && (alt_refin_result == received);
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      verdict_valid    <= 1'b0;
      diff_complement  <= 1'b0;
      diff_out_reflect <= 1'b0;
      diff_init        <= 1'b0;
      diff_in_reflect  <= 1'b0;
      unexplained      <= 1'b0;
      c_mismatch       <= '0;
      verdict_latched  <= 1'b0;
      first_delta      <= '0;
      first_length     <= '0;
    end else begin
      verdict_valid    <= 1'b0;
      diff_complement  <= 1'b0;
      diff_out_reflect <= 1'b0;
      diff_init        <= 1'b0;
      diff_in_reflect  <= 1'b0;
      unexplained      <= 1'b0;
 
      if (clear) begin
        c_mismatch <= '0;
        // The latched verdict deliberately survives: a convention
        // mismatch is a permanent property of a pairing, not a rate.
      end
 
      if (result_valid && (computed != received)) begin
        if (!(&c_mismatch)) c_mismatch <= c_mismatch + 1'b1;
        verdict_valid <= 1'b1;
 
        // Priority order is deliberate. The two single-frame tests come
        // first because they are decidable without a recomputation; the
        // recomputation-based tests follow. `unexplained` is the honest
        // default -- corruption on the wire also lands here, and calling
        // it a convention fault would be a worse error than saying
        // nothing.
        if      (t_complement)  diff_complement  <= 1'b1;
        else if (t_out_reflect) diff_out_reflect <= 1'b1;
        else if (t_init)        diff_init        <= 1'b1;
        else if (t_in_reflect)  diff_in_reflect  <= 1'b1;
        else                    unexplained      <= 1'b1;
 
        if (!verdict_latched) begin
          verdict_latched <= 1'b1;
          first_delta     <= delta;
          first_length    <= frame_octets;
        end
      end
    end
  end
 
endmodule

// SYNTHESIZABLE CONFORMANCE CHECKER.
//
// Verifies that this design's transmit and receive CRC engines are
// configured identically -- by construction rather than by inspection.
//
// The failure it catches: two instantiations of a parameterised engine
// where one override was applied and the other was not. That design
// transmits frames its own receiver rejects, and does it silently until
// something loops back.
//
// Note what this does NOT do: it does not compare parameters. It drives
// the same message through both engines and compares results, because a
// parameter that matches while a datapath differs is exactly the case a
// parameter comparison cannot see.
module convention_conformance_checker
  import crc32_pkg::*;
(
  input  logic clk,
  input  logic rst_n,
 
  input  logic start,
 
  // To the transmit engine.
  output logic        tx_start,
  output logic        tx_valid,
  output logic [7:0]  tx_data,
  output logic        tx_last,
  input  logic        tx_fcs_valid,
  input  logic [31:0] tx_fcs,
 
  // To the receive engine, driven with the identical octets.
  output logic        rx_start,
  output logic        rx_valid,
  output logic [7:0]  rx_data,
  output logic        rx_last,
  input  logic        rx_fcs_valid,
  input  logic [31:0] rx_fcs,
 
  output logic        check_done,
  output logic        engines_agree,
  output logic        matches_golden,
  output logic [31:0] tx_observed,
  output logic [31:0] rx_observed
);
 
  localparam int unsigned N = 9;
  localparam logic [7:0] MSG [N] = '{
    8'h31, 8'h32, 8'h33, 8'h34, 8'h35, 8'h36, 8'h37, 8'h38, 8'h39
  };
 
  typedef enum logic [1:0] { C_IDLE, C_START, C_DRIVE, C_WAIT } c_e;
  c_e         state_q;
  logic [3:0] idx_q;
  logic       tx_got_q, rx_got_q;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      state_q <= C_IDLE; idx_q <= '0;
      tx_start <= 1'b0; tx_valid <= 1'b0; tx_last <= 1'b0; tx_data <= '0;
      rx_start <= 1'b0; rx_valid <= 1'b0; rx_last <= 1'b0; rx_data <= '0;
      tx_got_q <= 1'b0; rx_got_q <= 1'b0;
      check_done <= 1'b0; engines_agree <= 1'b0; matches_golden <= 1'b0;
      tx_observed <= '0; rx_observed <= '0;
    end else begin
      tx_start <= 1'b0; tx_valid <= 1'b0; tx_last <= 1'b0;
      rx_start <= 1'b0; rx_valid <= 1'b0; rx_last <= 1'b0;
 
      case (state_q)
        C_IDLE: if (start) begin
          state_q <= C_START; idx_q <= '0;
          tx_got_q <= 1'b0; rx_got_q <= 1'b0; check_done <= 1'b0;
        end
 
        C_START: begin
          tx_start <= 1'b1; rx_start <= 1'b1;
          state_q  <= C_DRIVE;
        end
 
        C_DRIVE: begin
          tx_valid <= 1'b1; tx_data <= MSG[idx_q]; tx_last <= (idx_q == 4'(N-1));
          rx_valid <= 1'b1; rx_data <= MSG[idx_q]; rx_last <= (idx_q == 4'(N-1));
          if (idx_q == 4'(N-1)) state_q <= C_WAIT;
          else                  idx_q   <= idx_q + 1'b1;
        end
 
        C_WAIT: begin
          if (tx_fcs_valid) begin tx_observed <= tx_fcs; tx_got_q <= 1'b1; end
          if (rx_fcs_valid) begin rx_observed <= rx_fcs; rx_got_q <= 1'b1; end
          if (tx_got_q && rx_got_q) begin
            // TWO independent results, and both matter. Agreement without
            // matching the golden value means both engines are wrong the
            // same way -- which interoperates with nothing and passes
            // every loopback test in the suite.
            engines_agree  <= (tx_observed == rx_observed);
            matches_golden <= (tx_observed == CHECK_123456789) &&
                              (rx_observed == CHECK_123456789);
            check_done     <= 1'b1;
            state_q        <= C_IDLE;
          end
        end
 
        default: state_q <= C_IDLE;
      endcase
    end
  end
 
endmodule

// ---------------------------------------------------------------------
// P1 -- THE GOLDEN VECTOR. Nine known octets produce one published value.
// This single property pins the polynomial and all four conventions.
// ---------------------------------------------------------------------
property p_golden_check_value;
  @(posedge clk) disable iff (!rst_n)
    (selftest_done) |-> (observed == CHECK_123456789);
endproperty
a_golden_check_value: assert property (p_golden_check_value)
  else $error("golden vector failed -- polynomial or a convention differs");
 
// ---------------------------------------------------------------------
// P2 -- The register is preset at frame start, every frame. A register
// carried over from the previous frame produces a value that depends on
// history, which is correct for no specification at all.
// ---------------------------------------------------------------------
property p_preset_every_frame;
  @(posedge clk) disable iff (!rst_n)
    frame_start |=> (raw_reg == INIT);
endproperty
a_preset_every_frame: assert property (p_preset_every_frame);
 
// ---------------------------------------------------------------------
// P3 -- The result is produced exactly once per frame, on the last octet.
// ---------------------------------------------------------------------
property p_one_result_per_frame;
  @(posedge clk) disable iff (!rst_n)
    (oct_valid && oct_last) |-> ##[1:9] fcs_valid;
endproperty
a_one_result_per_frame: assert property (p_one_result_per_frame);
 
// ---------------------------------------------------------------------
// P4 -- No result without a frame. A value emitted outside a frame is a
// stale register being read.
// ---------------------------------------------------------------------
property p_no_result_outside_frame;
  @(posedge clk) disable iff (!rst_n)
    fcs_valid |-> $past(frame_active);
endproperty
a_no_result_outside_frame: assert property (p_no_result_outside_frame);
 
// ---------------------------------------------------------------------
// P5 -- REFLECTION IS AN INVOLUTION. Applying it twice is the identity.
// A reflect function with an off-by-one satisfies almost everything else
// and fails here immediately.
// ---------------------------------------------------------------------
property p_reflect32_involution;
  @(posedge clk) disable iff (!rst_n)
    (reflect32(reflect32(probe_word)) == probe_word);
endproperty
a_reflect32_involution: assert property (p_reflect32_involution);
 
property p_reflect8_involution;
  @(posedge clk) disable iff (!rst_n)
    (reflect8(reflect8(probe_octet)) == probe_octet);
endproperty
a_reflect8_involution: assert property (p_reflect8_involution);
 
// ---------------------------------------------------------------------
// P6 -- The two polynomial forms are bit reversals of one another. A
// constant relationship, asserted so an edit to either is caught at
// elaboration rather than by a peer.
// ---------------------------------------------------------------------
// synopsys translate_off
a_poly_forms_consistent: assert final (POLY_LSB == reflect32(POLY_MSB))
  else $fatal(1, "the two polynomial forms are not the same polynomial");
// synopsys translate_on
 
// ---------------------------------------------------------------------
// P7 -- The complement mask is bit-symmetric, which is the precondition
// that lets conventions 3 and 4 be applied in either order (Section 5).
// Asserted because a future variant with a different mask silently loses
// the property.
// ---------------------------------------------------------------------
// synopsys translate_off
a_final_mask_symmetric: assert final (XOR_OUT == reflect32(XOR_OUT))
  else $warning("final mask is not bit-symmetric: reflect and complement no longer commute");
// synopsys translate_on
 
// ---------------------------------------------------------------------
// P8 -- A complement difference produces exactly the mask as its delta.
// The single-frame diagnosis of Section 8.
// ---------------------------------------------------------------------
property p_complement_delta_is_mask;
  @(posedge clk) disable iff (!rst_n)
    diff_complement |-> ($past(computed) ^ $past(received)) == XOR_OUT;
endproperty
a_complement_delta_is_mask: assert property (p_complement_delta_is_mask);
 
// ---------------------------------------------------------------------
// P9 -- An output-reflection difference means one value is the other
// reversed. Also decidable from one frame.
// ---------------------------------------------------------------------
property p_out_reflect_delta_is_reversal;
  @(posedge clk) disable iff (!rst_n)
    diff_out_reflect |-> (reflect32($past(computed)) == $past(received));
endproperty
a_out_reflect_delta_is_reversal: assert property (p_out_reflect_delta_is_reversal);
 
// ---------------------------------------------------------------------
// P10 -- The verdicts are mutually exclusive, and `unexplained` is one of
// them rather than an absence. A classifier with no fallback forces
// ordinary wire corruption into whichever branch is last.
// ---------------------------------------------------------------------
property p_verdicts_onehot;
  @(posedge clk) disable iff (!rst_n)
    verdict_valid |-> $onehot({diff_complement, diff_out_reflect, diff_init,
                               diff_in_reflect, unexplained});
endproperty
a_verdicts_onehot: assert property (p_verdicts_onehot);
 
// ---------------------------------------------------------------------
// P11 -- A recomputation-based verdict requires the recomputation to have
// happened. Without it the test is comparing against a stale value.
// ---------------------------------------------------------------------
property p_init_verdict_needs_recompute;
  @(posedge clk) disable iff (!rst_n)
    diff_init |-> $past(alt_init_valid);
endproperty
a_init_verdict_needs_recompute: assert property (p_init_verdict_needs_recompute);
 
// ---------------------------------------------------------------------
// P12 -- The verdict is latched once and survives a clear: a convention
// mismatch is a property of a pairing, not a rate.
// ---------------------------------------------------------------------
property p_verdict_latched_stable;
  @(posedge clk) disable iff (!rst_n)
    verdict_latched |=> ($stable(first_delta) && $stable(first_length));
endproperty
a_verdict_latched_stable: assert property (p_verdict_latched_stable);
 
// ---------------------------------------------------------------------
// P13 -- Internal agreement does NOT imply conformance. Stated as a
// property so the weaker check cannot quietly stand in for the stronger.
// ---------------------------------------------------------------------
property p_agreement_is_not_conformance;
  @(posedge clk) disable iff (!rst_n)
    (check_done && matches_golden) |-> engines_agree;
endproperty
a_agreement_is_not_conformance: assert property (p_agreement_is_not_conformance);
 
// ---------------------------------------------------------------------
// P14 -- Both engines are checked against the golden value, not only
// against each other.
// ---------------------------------------------------------------------
property p_both_engines_golden;
  @(posedge clk) disable iff (!rst_n)
    (check_done && matches_golden)
      |-> ((tx_observed == CHECK_123456789) && (rx_observed == CHECK_123456789));
endproperty
a_both_engines_golden: assert property (p_both_engines_golden);
 
// ---------------------------------------------------------------------
// P15 -- The self-test drives exactly the golden message: nine octets,
// no more and no fewer. A self-test that drives eight produces a
// perfectly repeatable wrong value and reports a convention fault that
// does not exist.
// ---------------------------------------------------------------------
property p_selftest_drives_nine;
  @(posedge clk) disable iff (!rst_n)
    (drive_valid && drive_last) |-> (selftest_octets == 4'd9);
endproperty
a_selftest_drives_nine: assert property (p_selftest_drives_nine);
 
// ---------------------------------------------------------------------
// P16 -- Input reflection is applied if and only if configured. Written
// over the function rather than over a register, so it survives every
// restructuring the rejected property below does not.
// ---------------------------------------------------------------------
property p_input_reflection_applied_iff_configured;
  @(posedge clk) disable iff (!rst_n)
    oct_valid |-> (oct_applied == (REF_IN ? reflect8(oct_data) : oct_data));
endproperty
a_input_reflection_applied_iff_configured:
  assert property (p_input_reflection_applied_iff_configured);
 
// ---------------------------------------------------------------------
// P17 -- The diagnostic's alternative engines must have consumed THE
// SAME octets. Comparing against an engine fed different data produces a
// verdict from a coincidence.
// ---------------------------------------------------------------------
property p_alt_engines_same_octets;
  @(posedge clk) disable iff (!rst_n)
    (alt_init_valid || alt_refin_valid) |-> (alt_octet_count == main_octet_count);
endproperty
a_alt_engines_same_octets: assert property (p_alt_engines_same_octets);
 
// ---------------------------------------------------------------------
// P18 -- COVERAGE. Each of the four verdicts reached. A run that never
// produced a convention mismatch never tested Section 9 at all.
// ---------------------------------------------------------------------
c_verdict_complement:  cover property (@(posedge clk) disable iff (!rst_n) diff_complement);
c_verdict_out_reflect: cover property (@(posedge clk) disable iff (!rst_n) diff_out_reflect);
c_verdict_init:        cover property (@(posedge clk) disable iff (!rst_n) diff_init);
c_verdict_in_reflect:  cover property (@(posedge clk) disable iff (!rst_n) diff_in_reflect);
 
// ---------------------------------------------------------------------
// P19 -- COVERAGE. An UNEXPLAINED mismatch, which is what ordinary wire
// corruption looks like and what the fallback exists for.
// ---------------------------------------------------------------------
c_verdict_unexplained: cover property (@(posedge clk) disable iff (!rst_n) unexplained);