A Parallel CRC-32 Engine in RTL

next = (reg << 1) XOR (poly if (reg[31] XOR bit) else 0)

next_state = F · current_state  XOR  H · input_data

// SYNTHESIZABLE. The matrices are computed at elaboration.
//
// F[i] is the state after running the serial step W times, starting from
// a state with only bit i set and feeding zeros.
// H[i] is the state after running it W times from a zero state, feeding
// a data word with only bit i set.
//
// Both are obtained by RUNNING THE SERIAL STEP. Nothing is transcribed,
// nothing is derived by hand, and the polynomial appears exactly once.
package crc_parallel_pkg;
  import crc32_pkg::*;
 
  // The serial step of Chapter 6.2 §3, verbatim. This function is the
  // single source of truth for the entire chapter.
  function automatic logic [31:0] serial_step(input logic [31:0] r,
                                              input logic        b);
    serial_step = {r[30:0], 1'b0} ^ ((r[31] ^ b) ? POLY_MSB : 32'h0);
  endfunction
 
  // W steps, consuming `d` most-significant-bit first.
  function automatic logic [31:0] serial_steps(input logic [31:0] r,
                                               input logic [63:0] d,
                                               input int unsigned W);
    logic [31:0] s;
    s = r;
    for (int unsigned i = 0; i < W; i++) s = serial_step(s, d[W-1-i]);
    serial_steps = s;
  endfunction
 
  // Column i of F: the response to state bit i alone.
  function automatic logic [31:0] f_col(input int unsigned i,
                                        input int unsigned W);
    f_col = serial_steps(32'h1 << i, 64'h0, W);
  endfunction
 
  // Column i of H: the response to data bit i alone.
  function automatic logic [31:0] h_col(input int unsigned i,
                                        input int unsigned W);
    h_col = serial_steps(32'h0, 64'h1 << i, W);
  endfunction
 
  // The wide next state, assembled by superposition. This IS the matrix
  // multiply -- each set input bit contributes its column.
  function automatic logic [31:0] next_state(input logic [31:0] r,
                                             input logic [63:0] d,
                                             input int unsigned W);
    logic [31:0] acc;
    acc = 32'h0;
    for (int unsigned i = 0; i < 32; i++) if (r[i]) acc ^= f_col(i, W);
    for (int unsigned i = 0; i < W;  i++) if (d[i]) acc ^= h_col(i, W);
    next_state = acc;
  endfunction
 
endpackage
 
// SYNTHESIZABLE. The generated network, as a block.
//
// Wrapping the function in a module is not ceremony: it gives the
// network a name in the netlist, a place to constrain timing, and a
// single instance that every width in the design shares. A design that
// calls next_state() inline in three places has three networks that
// synthesis may optimise differently and that no timing report names.
module crc32_next_state
  import crc32_pkg::*;
  import crc_parallel_pkg::*;
#(
  parameter int unsigned W = 8
) (
  input  logic [31:0] state_in,
  input  logic [W-1:0] data_in,
  output logic [31:0] state_out
);
 
  // Constant-folded at elaboration into a fixed XOR network: every output
  // bit is the parity of a subset of the 32 + W inputs, and nothing else.
  assign state_out = next_state(state_in, 64'(data_in), W);
 
endmodule

// SYNTHESIZABLE.
//
// Eight bits per clock, which is the width an xMII-class interface
// delivers and the smallest width worth parallelising.
//
// The datapath is one line. Everything else in this module exists for
// the frame's edges, which is the honest ratio for a CRC engine: the
// arithmetic is free and the boundaries are the work.
module crc32_byte_engine
  import crc32_pkg::*;
  import crc_parallel_pkg::*;
(
  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,
  output logic [31:0] crc_reg
);
 
  logic [31:0] reg_q;
  assign crc_reg = reg_q;
 
  // The input reflection of Chapter 6.2 §5, applied per octet before the
  // octet enters the network.
  wire [7:0] oct_applied = REFLECT_IN ? reflect8(oct_data) : oct_data;
 
  // THE DATAPATH. One combinational function, depth 4, 252 XOR terms
  // across the 32 outputs -- and no sequential dependence inside the
  // cycle, which is why it meets timing where a serial engine cannot.
  wire [31:0] next = next_state(reg_q, {56'h0, oct_applied}, 8);
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      reg_q     <= INIT_VALUE;
      fcs_valid <= 1'b0;
      fcs       <= '0;
    end else begin
      fcs_valid <= 1'b0;
 
      if (frame_start) begin
        reg_q <= INIT_VALUE;
      end else if (oct_valid) begin
        reg_q <= next;
        if (oct_last) begin
          // Output conventions applied to the value the last octet
          // produced -- `next`, not `reg_q`, because reg_q has not been
          // updated yet. Reading the wrong one is a one-octet-early
          // result and is the single most common bug in this module.
          fcs       <= (REFLECT_OUT ? reflect32(next) : next) ^ XOR_OUT;
          fcs_valid <= 1'b1;
        end
      end
    end
  end
 
endmodule

// SYNTHESIZABLE.
//
// Sixty-four bits per clock with byte enables, which is what a frame
// whose length is not a multiple of eight requires.
//
// The core idea: a transfer carrying k valid octets must advance the
// state by EXACTLY 8k bits. So the module instantiates the generated
// network at eight widths and selects among them.
//
// It does NOT mask the invalid octets to zero and run the full 64-bit
// network. Zero octets are not "no octets" -- feeding eight zero bits
// advances the state, and a zero octet is a perfectly ordinary input
// that changes the remainder. That mistake produces a frame whose CRC is
// computed over a longer message than was sent, and it is invisible on
// every frame whose length happens to be a multiple of eight.
module crc32_wide_engine
  import crc32_pkg::*;
  import crc_parallel_pkg::*;
#(
  parameter int unsigned LANES = 8            // octets per transfer
) (
  input  logic clk,
  input  logic rst_n,
 
  input  logic                 frame_start,
  input  logic                 xfer_valid,
  input  logic [8*LANES-1:0]   xfer_data,     // lane 0 is the FIRST octet
  // Number of valid octets in THIS transfer, 1..LANES. A count rather
  // than a mask, deliberately: valid octets are always contiguous from
  // lane 0, and a mask permits states that cannot occur and must then be
  // handled or excluded.
  input  logic [3:0]           xfer_octets,
  input  logic                 xfer_last,
 
  output logic                 fcs_valid,
  output logic [31:0]          fcs,
  output logic [31:0]          crc_reg,
  // Asserted if a transfer arrives with an octet count outside 1..LANES.
  // Not an error the engine can absorb -- it is an upstream fault, and
  // silently clamping it would produce a stable wrong check value.
  output logic                 bad_octet_count
);
 
  logic [31:0] reg_q;
  assign crc_reg = reg_q;
 
  // Reflect each octet independently, then present them most-significant
  // octet first, because the generated network consumes MSB-first.
  logic [8*LANES-1:0] applied;
  always_comb begin
    applied = '0;
    for (int unsigned i = 0; i < LANES; i++) begin
      automatic logic [7:0] o = xfer_data[8*i +: 8];
      applied[8*(LANES-1-i) +: 8] = REFLECT_IN ? reflect8(o) : o;
    end
  end
 
  // Eight candidate next states, one per possible valid-octet count.
  // Each is the generated network at a different width, and each consumes
  // the TOP 8k bits of `applied` -- which is why the octets were packed
  // most-significant first above.
  logic [31:0] cand [LANES+1];
  always_comb begin
    cand[0] = reg_q;                       // no octets: state unchanged
    for (int unsigned k = 1; k <= LANES; k++)
      cand[k] = next_state(reg_q,
                           64'(applied >> (8*(LANES-k))),
                           8*k);
  end
 
  wire count_ok = (xfer_octets >= 4'd1) && (xfer_octets <= 4'(LANES));
  wire [31:0] next = cand[count_ok ? xfer_octets : 4'd0];
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      reg_q           <= INIT_VALUE;
      fcs_valid       <= 1'b0;
      fcs             <= '0;
      bad_octet_count <= 1'b0;
    end else begin
      fcs_valid <= 1'b0;
 
      if (frame_start) begin
        reg_q           <= INIT_VALUE;
        bad_octet_count <= 1'b0;
      end else if (xfer_valid) begin
        if (!count_ok) begin
          // Report and do not advance. A clamped count computes a valid
          // check value over the wrong number of octets, which is the
          // worst available outcome: stable, repeatable and wrong.
          bad_octet_count <= 1'b1;
        end else begin
          reg_q <= next;
          if (xfer_last) begin
            fcs       <= (REFLECT_OUT ? reflect32(next) : next) ^ XOR_OUT;
            fcs_valid <= 1'b1;
          end
        end
      end
    end
  end
 
endmodule

// SYNTHESIZABLE.
//
// Packs an octet stream into LANES-wide transfers and produces the valid
// octet count for each -- including the final, partial one.
//
// Three failures live here and all three are invisible on frames whose
// length is a multiple of LANES:
//
//   1. the final partial word is never emitted, so the frame's last
//      octets are silently dropped from the computation
//   2. the final partial word is emitted with a count of LANES, so
//      stale octets from the previous frame are consumed
//   3. the final word is emitted twice -- once on the last octet and
//      again on the flush -- doubling the last octets
//
// Each produces a stable, repeatable, wrong check value.
module frame_word_packer
#(
  parameter int unsigned LANES = 8
) (
  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                 xfer_valid,
  output logic [8*LANES-1:0]   xfer_data,
  output logic [3:0]           xfer_octets,
  output logic                 xfer_last
);
 
  logic [8*LANES-1:0] acc_q;
  logic [3:0]         fill_q;
 
  // The accumulator is cleared at frame start, not merely the counter.
  // Clearing only the counter leaves the previous frame's octets in the
  // lanes -- harmless while the count is honoured and catastrophic the
  // moment a count is wrong, because the stale data is plausible.
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      acc_q       <= '0;
      fill_q      <= '0;
      xfer_valid  <= 1'b0;
      xfer_data   <= '0;
      xfer_octets <= '0;
      xfer_last   <= 1'b0;
    end else begin
      xfer_valid <= 1'b0;
      xfer_last  <= 1'b0;
 
      if (frame_start) begin
        acc_q  <= '0;
        fill_q <= '0;
      end else if (oct_valid) begin
        automatic logic [8*LANES-1:0] acc_next = acc_q;
        automatic logic [3:0]         fill_next = fill_q + 4'd1;
 
        acc_next[8*fill_q +: 8] = oct_data;
 
        if (oct_last) begin
          // The final transfer. Emitted with the ACTUAL count, which may
          // be anything from 1 to LANES -- and note it is emitted here,
          // on the last octet, rather than by a separate flush. A flush
          // is where failure 3 comes from: two paths that can both emit
          // the same word.
          xfer_data   <= acc_next;
          xfer_octets <= fill_next;
          xfer_valid  <= 1'b1;
          xfer_last   <= 1'b1;
          acc_q       <= '0;
          fill_q      <= '0;
        end else if (fill_next == 4'(LANES)) begin
          // A full transfer in the ordinary course.
          xfer_data   <= acc_next;
          xfer_octets <= 4'(LANES);
          xfer_valid  <= 1'b1;
          acc_q       <= '0;
          fill_q      <= '0;
        end else begin
          acc_q  <= acc_next;
          fill_q <= fill_next;
        end
      end
    end
  end
 
  // The frame must never end with octets still in the accumulator. This
  // is failure 1, stated as a property of the module's own state rather
  // than left to the engine to notice -- because the engine cannot: a
  // shorter message produces a perfectly valid check value.
  // synopsys translate_off
  always_ff @(posedge clk) begin
    if (rst_n && frame_start && (fill_q != 4'd0))
      $error("frame started with %0d octets still buffered from the previous frame", fill_q);
  end
  // synopsys translate_on
 
endmodule

// VERIFICATION COMPONENT. NOT FOR SYNTHESIS.
//
// Drives the same octets through the parallel engine and through the
// bit-serial engine, and requires identical results.
//
// The INDEPENDENCE of the two sides is the entire value:
//
//   the serial engine   -- written from the polynomial, one bit per step
//   the parallel engine -- a generated matrix, LANES octets per step
//
// They share the polynomial constant and nothing else. In particular the
// serial engine does NOT use crc_parallel_pkg's serial_step, because a
// shared step function would make a bug in that function invisible to
// this check -- which is precisely the failure Section 10 rejects.
module crc_equivalence_checker
  import crc32_pkg::*;
#(
  parameter int unsigned LANES     = 8,
  parameter int unsigned MAX_OCTETS = 1522
) (
  input  logic clk,
  input  logic rst_n,
 
  input  logic start,
  input  logic [13:0] octet_count,   // swept by the testbench
 
  // To the serial reference.
  output logic        ref_start,
  output logic        ref_valid,
  output logic [7:0]  ref_data,
  output logic        ref_last,
  input  logic        ref_fcs_valid,
  input  logic [31:0] ref_fcs,
 
  // To the parallel design under test, through the packer of Section 8.
  output logic        dut_start,
  output logic        dut_valid,
  output logic [7:0]  dut_data,
  output logic        dut_last,
  input  logic        dut_fcs_valid,
  input  logic [31:0] dut_fcs,
 
  output logic        compare_done,
  output logic        equivalent,
  output logic [31:0] ref_observed,
  output logic [31:0] dut_observed,
  output logic [13:0] failing_length,
  output logic        failure_seen,
  // Which residues modulo LANES have been exercised. A sweep that never
  // reaches all of them has not tested the partial-word paths.
  output logic [7:0]  residues_covered
);
 
  logic [13:0] idx_q;
  logic        ref_got_q, dut_got_q;
  typedef enum logic [1:0] { E_IDLE, E_DRIVE, E_WAIT, E_CMP } e_e;
  e_e state_q;
 
  // The same pseudo-random octet stream to both, so any difference is
  // the engines and not the stimulus.
  function automatic logic [7:0] pattern(input logic [13:0] i);
    pattern = i[7:0] ^ {i[13:8], 2'b10};
  endfunction
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      state_q <= E_IDLE; idx_q <= '0;
      ref_start <= 1'b0; ref_valid <= 1'b0; ref_last <= 1'b0; ref_data <= '0;
      dut_start <= 1'b0; dut_valid <= 1'b0; dut_last <= 1'b0; dut_data <= '0;
      ref_got_q <= 1'b0; dut_got_q <= 1'b0;
      compare_done <= 1'b0; equivalent <= 1'b0;
      ref_observed <= '0; dut_observed <= '0;
      failing_length <= '0; failure_seen <= 1'b0;
      residues_covered <= '0;
    end else begin
      ref_start <= 1'b0; ref_valid <= 1'b0; ref_last <= 1'b0;
      dut_start <= 1'b0; dut_valid <= 1'b0; dut_last <= 1'b0;
      compare_done <= 1'b0;
 
      case (state_q)
        E_IDLE: if (start) begin
          ref_start <= 1'b1; dut_start <= 1'b1;
          idx_q <= '0; ref_got_q <= 1'b0; dut_got_q <= 1'b0;
          state_q <= E_DRIVE;
        end
 
        E_DRIVE: begin
          ref_valid <= 1'b1; ref_data <= pattern(idx_q);
          dut_valid <= 1'b1; dut_data <= pattern(idx_q);
          ref_last  <= (idx_q == octet_count - 14'd1);
          dut_last  <= (idx_q == octet_count - 14'd1);
          if (idx_q == octet_count - 14'd1) state_q <= E_WAIT;
          else                              idx_q   <= idx_q + 14'd1;
        end
 
        E_WAIT: begin
          if (ref_fcs_valid) begin ref_observed <= ref_fcs; ref_got_q <= 1'b1; end
          if (dut_fcs_valid) begin dut_observed <= dut_fcs; dut_got_q <= 1'b1; end
          if (ref_got_q && dut_got_q) state_q <= E_CMP;
        end
 
        E_CMP: begin
          equivalent   <= (ref_observed == dut_observed);
          compare_done <= 1'b1;
          // Record which length-modulo-LANES class this run covered, so
          // the sweep's completeness is a reported fact rather than an
          // assumption about how the testbench was configured.
          residues_covered[octet_count % LANES] <= 1'b1;
          if ((ref_observed != dut_observed) && !failure_seen) begin
            failure_seen   <= 1'b1;
            failing_length <= octet_count;
          end
          state_q <= E_IDLE;
        end
 
        default: state_q <= E_IDLE;
      endcase
    end
  end
 
endmodule

next = (reg << 8) XOR T[(reg >> 24) XOR byte]

// ---------------------------------------------------------------------
// P1 -- THE SIGN-OFF PROPERTY. The parallel engine and the INDEPENDENT
// bit-serial reference produce identical values, at every length.
// ---------------------------------------------------------------------
property p_parallel_equals_serial;
  @(posedge clk) disable iff (!rst_n)
    compare_done |-> (dut_observed == ref_observed);
endproperty
a_parallel_equals_serial: assert property (p_parallel_equals_serial)
  else $error("parallel engine differs from the serial reference at length %0d", octet_count);
 
// ---------------------------------------------------------------------
// P2 -- The generated matrices reproduce direct serial evaluation. An
// elaboration-time check on the generator itself, independent of any
// frame ever being driven.
// ---------------------------------------------------------------------
// synopsys translate_off
a_matrix_matches_serial: assert final
  (next_state(32'h1234_5678, 64'h00AB, 8) ==
   serial_steps(32'h1234_5678, 64'h00AB, 8))
  else $fatal(1, "generated matrix disagrees with the serial step it was built from");
// synopsys translate_on
 
// ---------------------------------------------------------------------
// P3 -- The full-width network is the composition of narrower ones.
// Consuming eight octets in one step equals consuming four then four.
// This catches a width parameter that did not propagate.
// ---------------------------------------------------------------------
// synopsys translate_off
a_widths_compose: assert final
  (next_state(32'hDEAD_BEEF, 64'h0011_2233_4455_6677, 64) ==
   next_state(next_state(32'hDEAD_BEEF, 64'h0011_2233, 32), 64'h4455_6677, 32));
// synopsys translate_on
 
// ---------------------------------------------------------------------
// P4 -- The result is taken from `next`, not from the register. Written
// as a value relation, because the failure is a one-octet-early result
// that is otherwise perfectly stable.
// ---------------------------------------------------------------------
property p_result_from_next_not_reg;
  @(posedge clk) disable iff (!rst_n)
    fcs_valid |-> (fcs == ((REFLECT_OUT ? reflect32($past(next)) : $past(next)) ^ XOR_OUT));
endproperty
a_result_from_next_not_reg: assert property (p_result_from_next_not_reg);
 
// ---------------------------------------------------------------------
// P5 -- The octet count on a transfer is always in range. Out of range
// must be REPORTED, not clamped.
// ---------------------------------------------------------------------
property p_octet_count_in_range;
  @(posedge clk) disable iff (!rst_n)
    (xfer_valid && !bad_octet_count) |-> ((xfer_octets >= 4'd1) && (xfer_octets <= 4'(LANES)));
endproperty
a_octet_count_in_range: assert property (p_octet_count_in_range);
 
// ---------------------------------------------------------------------
// P6 -- A bad count does not advance the state. Clamping produces a
// valid check value over the wrong number of octets.
// ---------------------------------------------------------------------
property p_bad_count_does_not_advance;
  @(posedge clk) disable iff (!rst_n)
    (xfer_valid && !count_ok) |=> $stable(crc_reg);
endproperty
a_bad_count_does_not_advance: assert property (p_bad_count_does_not_advance);
 
// ---------------------------------------------------------------------
// P7 -- Only the FINAL transfer of a frame may be partial. A partial
// transfer mid-frame means the packer emitted early.
// ---------------------------------------------------------------------
property p_only_last_is_partial;
  @(posedge clk) disable iff (!rst_n)
    (xfer_valid && (xfer_octets != 4'(LANES))) |-> xfer_last;
endproperty
a_only_last_is_partial: assert property (p_only_last_is_partial);
 
// ---------------------------------------------------------------------
// P8 -- Exactly one last transfer per frame. Two is the double-emit
// failure of Section 8; zero is the dropped-tail failure.
// ---------------------------------------------------------------------
property p_one_last_per_frame;
  @(posedge clk) disable iff (!rst_n)
    (xfer_valid && xfer_last) |-> ##1 (!xfer_last throughout (!frame_start [*1:$]));
endproperty
a_one_last_per_frame: assert property (p_one_last_per_frame);
 
// ---------------------------------------------------------------------
// P9 -- The packer's accumulator is empty at frame start. Octets left
// over from the previous frame are plausible data, which makes any
// downstream count error invisible.
// ---------------------------------------------------------------------
property p_accumulator_empty_at_start;
  @(posedge clk) disable iff (!rst_n)
    frame_start |-> (fill_q == 4'd0);
endproperty
a_accumulator_empty_at_start: assert property (p_accumulator_empty_at_start);
 
// ---------------------------------------------------------------------
// P10 -- The octets driven into the engine over a frame equal the octets
// the client supplied. The end-to-end conservation property, and the one
// that catches a dropped or duplicated tail regardless of mechanism.
// ---------------------------------------------------------------------
property p_octet_conservation;
  @(posedge clk) disable iff (!rst_n)
    (xfer_valid && xfer_last) |-> (octets_consumed_this_frame == client_octets_this_frame);
endproperty
a_octet_conservation: assert property (p_octet_conservation);
 
// ---------------------------------------------------------------------
// P11 -- The register is preset at every frame start (Chapter 6.2 P2,
// restated here because a wide engine has a second place to get it
// wrong: the packer's own state).
// ---------------------------------------------------------------------
property p_engine_preset_every_frame;
  @(posedge clk) disable iff (!rst_n)
    frame_start |=> (crc_reg == INIT_VALUE);
endproperty
a_engine_preset_every_frame: assert property (p_engine_preset_every_frame);
 
// ---------------------------------------------------------------------
// P12 -- The byte-wide and wide engines agree on the same octet stream.
// A second equivalence, between two DIFFERENT widths of the same
// generator -- weaker than P1, and cheap.
// ---------------------------------------------------------------------
property p_widths_agree;
  @(posedge clk) disable iff (!rst_n)
    (byte_fcs_valid && wide_fcs_valid) |-> (byte_fcs == wide_fcs);
endproperty
a_widths_agree: assert property (p_widths_agree);
 
// ---------------------------------------------------------------------
// P13 -- The golden vector still holds at every width. Chapter 6.2's
// self-test is width-independent and is the cheapest conformance check
// available to a parallel engine.
// ---------------------------------------------------------------------
property p_golden_at_any_width;
  @(posedge clk) disable iff (!rst_n)
    selftest_done |-> (observed == CHECK_123456789);
endproperty
a_golden_at_any_width: assert property (p_golden_at_any_width);
 
// ---------------------------------------------------------------------
// P14 -- The residue is width-independent too: a wide checker tests for
// the same constant a serial one does.
// ---------------------------------------------------------------------
property p_residue_width_independent;
  @(posedge clk) disable iff (!rst_n)
    (check_valid && frame_was_valid) |-> (residue_observed == RESIDUE);
endproperty
a_residue_width_independent: assert property (p_residue_width_independent);
 
// ---------------------------------------------------------------------
// P15 -- Equivalence has been demonstrated at EVERY residue class before
// the sign-off is meaningful. Coverage as a property, because a sweep
// that missed a class has not tested that sub-network at all.
// ---------------------------------------------------------------------
property p_all_residues_covered_before_signoff;
  @(posedge clk) disable iff (!rst_n)
    signoff_asserted |-> (residues_covered == 8'hFF);
endproperty
a_all_residues_covered_before_signoff:
  assert property (p_all_residues_covered_before_signoff);
 
// ---------------------------------------------------------------------
// P16 -- The first failing length is captured once and kept. It is more
// informative than the values (Section 9).
// ---------------------------------------------------------------------
property p_failing_length_stable;
  @(posedge clk) disable iff (!rst_n)
    failure_seen |=> $stable(failing_length);
endproperty
a_failing_length_stable: assert property (p_failing_length_stable);
 
// ---------------------------------------------------------------------
// P17 -- The generated network is purely combinational. No output bit
// depends on anything but the current state and the current data, which
// is what makes the block retimeable and what a registered intermediate
// would silently break.
// ---------------------------------------------------------------------
property p_network_is_combinational;
  @(posedge clk) disable iff (!rst_n)
    (state_out == next_state(state_in, 64'(data_in), W));
endproperty
a_network_is_combinational: assert property (p_network_is_combinational);
 
// ---------------------------------------------------------------------
// P18 -- Consuming zero octets leaves the state unchanged. The identity
// case, which distinguishes "no octets" from "a zero octet" -- the
// distinction Section 6 is built on.
// ---------------------------------------------------------------------
property p_zero_octets_is_identity;
  @(posedge clk) disable iff (!rst_n)
    (xfer_valid && (xfer_octets == 4'd0) && count_ok_relaxed) |=> $stable(crc_reg);
endproperty
a_zero_octets_is_identity: assert property (p_zero_octets_is_identity);
 
// ---------------------------------------------------------------------
// P19 -- COVERAGE. Every partial-word width exercised, individually.
// ---------------------------------------------------------------------
c_partial_1: cover property (@(posedge clk) disable iff (!rst_n) (xfer_valid && xfer_last && xfer_octets == 4'd1));
c_partial_7: cover property (@(posedge clk) disable iff (!rst_n) (xfer_valid && xfer_last && xfer_octets == 4'd7));
c_partial_8: cover property (@(posedge clk) disable iff (!rst_n) (xfer_valid && xfer_last && xfer_octets == 4'(LANES)));
 
// ---------------------------------------------------------------------
// P20 -- COVERAGE. A frame shorter than one full transfer, which
// exercises the packer's start and end in the same cycle.
// ---------------------------------------------------------------------
c_frame_shorter_than_word: cover property (
  @(posedge clk) disable iff (!rst_n)
    (xfer_valid && xfer_last && (xfer_octets < 4'(LANES)) && first_xfer_of_frame)
);