CRC Checking and the Residue

// SYNTHESIZABLE.
//
// Checks a frame by feeding EVERYTHING -- data and check sequence alike --
// through the division, and testing the final register against a constant.
//
// What makes this work: the transmitter appended exactly the remainder
// that makes the codeword divisible, so the result of dividing the whole
// codeword does not depend on the message. Every valid frame lands on the
// same value.
//
// Note the constant is a PARAMETER derived elsewhere (Section 7), not a
// literal. Section 12 explains at length why that distinction is the
// subject of this chapter's rejected property.
module crc32_residue_checker
  import crc32_pkg::*;
#(
  // The value a valid frame leaves in the register, given this design's
  // conventions and this sample point. DERIVED, not quoted.
  parameter logic [31:0] RESIDUE = 32'hDEBB_20E3
) (
  input  logic clk,
  input  logic rst_n,
 
  input  logic       frame_start,
  input  logic       oct_valid,
  input  logic [7:0] oct_data,
  // Asserted on the last octet of the FRAME, not of the payload. The
  // receiver never needs to know where the payload ended.
  input  logic       frame_end,
 
  output logic        check_valid,
  output logic        fcs_ok,
  output logic [31:0] residue_observed
);
 
  logic [31:0] reg_q;
  logic [7:0]  oct_q;
  logic [2:0]  bit_q;
  logic        busy_q;
  logic        end_q;
 
  wire [7:0] oct_applied = REFLECT_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_VALUE;
      oct_q            <= '0;
      bit_q            <= '0;
      busy_q           <= 1'b0;
      end_q            <= 1'b0;
      check_valid      <= 1'b0;
      fcs_ok           <= 1'b0;
      residue_observed <= '0;
    end else begin
      check_valid <= 1'b0;
 
      if (frame_start) begin
        reg_q  <= INIT_VALUE;
        busy_q <= 1'b0;
        end_q  <= 1'b0;
      end else if (oct_valid && !busy_q) begin
        oct_q  <= oct_applied;
        bit_q  <= '0;
        busy_q <= 1'b1;
        end_q  <= frame_end;
      end else if (busy_q) begin
        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 (end_q) begin
            automatic logic [31:0] final_reg =
                {reg_q[30:0], 1'b0} ^ (feedback ? POLY_MSB : 32'h0);
            // The whole check. One 32-bit equality against a constant --
            // and crucially, against a constant known at elaboration
            // rather than a value captured during the frame.
            residue_observed <= final_reg;
            fcs_ok           <= (final_reg == RESIDUE);
            check_valid      <= 1'b1;
          end
        end else begin
          bit_q <= bit_q + 1'b1;
        end
      end
    end
  end
 
endmodule

// SYNTHESIZABLE.
//
// The symmetric receiver: divide over the DATA only, hold the result,
// capture the arriving check sequence, compare at end of frame.
//
// Algebraically identical to Section 4 in what it detects. Structurally
// it needs three things Section 4 does not:
//
//   1. a four-octet delay line, because the engine must stop four octets
//      before the frame ends and the frame's end is not known in advance
//   2. a capture register for the arriving check sequence
//   3. a holding register for the computed value
//
// The delay line is the expensive one, and it is the one that does not
// appear in a naive gate count.
module crc32_compare_checker
  import crc32_pkg::*;
(
  input  logic clk,
  input  logic rst_n,
 
  input  logic       frame_start,
  input  logic       oct_valid,
  input  logic [7:0] oct_data,
  input  logic       frame_end,
 
  output logic        check_valid,
  output logic        fcs_ok,
  output logic [31:0] computed,
  output logic [31:0] received
);
 
  // (1) The delay line. Four octets, plus their valid bits, so that when
  // frame_end arrives the four octets still in flight can be recognised
  // as the check sequence rather than as payload.
  logic [7:0] dly_q [4];
  logic [2:0] fill_q;
 
  logic [31:0] reg_q;
  logic [7:0]  oct_q;
  logic [2:0]  bit_q;
  logic        busy_q;
 
  wire [7:0] oct_applied = REFLECT_IN ? reflect8(dly_q[3]) : dly_q[3];
  wire       feedback    = oct_q[7] ^ reg_q[31];
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      for (int i = 0; i < 4; i++) dly_q[i] <= '0;
      fill_q      <= '0;
      reg_q       <= INIT_VALUE;
      oct_q       <= '0;
      bit_q       <= '0;
      busy_q      <= 1'b0;
      check_valid <= 1'b0;
      fcs_ok      <= 1'b0;
      computed    <= '0;
      received    <= '0;
    end else begin
      check_valid <= 1'b0;
 
      if (frame_start) begin
        reg_q  <= INIT_VALUE;
        fill_q <= '0;
        busy_q <= 1'b0;
      end else if (oct_valid && !busy_q) begin
        // Shift the delay line. Only once four octets are resident does
        // the oldest one become payload rather than a possible FCS octet.
        dly_q[3] <= dly_q[2];
        dly_q[2] <= dly_q[1];
        dly_q[1] <= dly_q[0];
        dly_q[0] <= oct_data;
 
        if (fill_q != 3'd4) begin
          fill_q <= fill_q + 1'b1;
        end else begin
          oct_q  <= oct_applied;
          bit_q  <= '0;
          busy_q <= 1'b1;
        end
 
        if (frame_end) begin
          // (2) The four octets still in the delay line ARE the check
          // sequence -- and note the octet order, which is a fifth
          // convention this receiver has to get right and Section 4's
          // never encounters.
          received <= {dly_q[0], dly_q[1], dly_q[2], dly_q[3]};
          // (3) The held value, with the output conventions applied.
          computed <= (REFLECT_OUT ? reflect32(reg_q) : reg_q) ^ XOR_OUT;
          fcs_ok      <= ((REFLECT_OUT ? reflect32(reg_q) : reg_q) ^ XOR_OUT)
                          == {dly_q[0], dly_q[1], dly_q[2], dly_q[3]};
          check_valid <= 1'b1;
        end
      end else if (busy_q) begin
        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) busy_q <= 1'b0;
        else               bit_q  <= bit_q + 1'b1;
      end
    end
  end
 
endmodule

// SYNTHESIZABLE, and the work happens at elaboration.
//
// Derives the residue rather than quoting it, by doing exactly what a
// valid frame does: take an arbitrary message, compute its check
// sequence under this design's conventions, append it, and run the whole
// thing back through. Whatever comes out IS the residue -- by
// construction, for this configuration.
//
// The message is arbitrary because the residue does not depend on it.
// That is the property being relied on, and the module checks it rather
// than assuming it: two different messages must produce the same answer.
package residue_pkg;
  import crc32_pkg::*;
 
  // A constant-function model of the design's own engine. Not a second
  // implementation -- it applies the SAME parameters, so it cannot drift
  // from the datapath in the way an independently written reference can.
  function automatic logic [31:0] crc_raw(input logic [7:0] msg [],
                                          input int unsigned n);
    logic [31:0] r;
    logic [7:0]  o;
    r = INIT_VALUE;
    for (int unsigned i = 0; i < n; i++) begin
      o = REFLECT_IN ? reflect8(msg[i]) : msg[i];
      for (int unsigned b = 0; b < 8; b++) begin
        r = {r[30:0], 1'b0} ^ ((o[7] ^ r[31]) ? POLY_MSB : 32'h0);
        o = {o[6:0], 1'b0};
      end
    end
    crc_raw = r;
  endfunction
 
  function automatic logic [31:0] fcs_of(input logic [7:0] msg [],
                                         input int unsigned n);
    fcs_of = (REFLECT_OUT ? reflect32(crc_raw(msg, n)) : crc_raw(msg, n)) ^ XOR_OUT;
  endfunction
 
  // The derivation. Build message || FCS and run it all through.
  function automatic logic [31:0] derive_residue(input logic [7:0] msg [],
                                                 input int unsigned n);
    logic [7:0]  full [];
    logic [31:0] f;
    f = fcs_of(msg, n);
    full = new[n + 4];
    for (int unsigned i = 0; i < n; i++) full[i] = msg[i];
    // Octet order matters here and ONLY here -- it is the transmitter's
    // convention for laying the value onto the wire, and getting it wrong
    // yields a residue that is stable and wrong, which is the worst kind.
    full[n+0] = f[7:0];
    full[n+1] = f[15:8];
    full[n+2] = f[23:16];
    full[n+3] = f[31:24];
    derive_residue = crc_raw(full, n + 4);
  endfunction
 
endpackage
 
module residue_constant_verifier
  import crc32_pkg::*;
  import residue_pkg::*;
(
  input  logic clk,
  input  logic rst_n,
  output logic [31:0] residue_derived,
  output logic        residue_consistent
);
 
  // Two unrelated messages of different lengths. If the residue depends
  // on the message, these disagree -- which would mean the derivation is
  // wrong, or a convention is applied in the wrong place.
  localparam logic [7:0] MSG_A [3] = '{8'h61, 8'h62, 8'h63};
  localparam logic [7:0] MSG_B [9] = '{8'h31, 8'h32, 8'h33, 8'h34, 8'h35,
                                       8'h36, 8'h37, 8'h38, 8'h39};
 
  localparam logic [31:0] RES_A = derive_residue(MSG_A, 3);
  localparam logic [31:0] RES_B = derive_residue(MSG_B, 9);
 
  assign residue_derived    = RES_A;
  assign residue_consistent = (RES_A == RES_B);
 
  // The two checks that make this a verifier rather than a calculator.
  // synopsys translate_off
  // (1) The residue really is message-independent. If this fails, the
  //     whole approach of Section 4 is invalid for this configuration.
  a_residue_message_independent: assert final (RES_A == RES_B)
    else $fatal(1, "residue depends on the message -- derivation or conventions are wrong");
 
  // (2) And, for Ethernet's conventions specifically, it lands on the
  //     published value. This catches a derivation that is
  //     self-consistent and wrong -- two errors that cancel.
  a_residue_matches_published: assert final
    ((INIT_VALUE  != 32'hFFFF_FFFF) ||
     (REFLECT_IN  != 1'b1)          ||
     (REFLECT_OUT != 1'b1)          ||
     (XOR_OUT     != 32'hFFFF_FFFF) ||
     (RES_A       == 32'hDEBB_20E3))
    else $fatal(1, "Ethernet conventions but the derived residue is not 0xDEBB20E3");
  // synopsys translate_on
 
endmodule

// SYNTHESIZABLE.
//
// Detects, DURING a frame, that it cannot end validly -- and does so for
// one specific, useful case.
//
// The general question is not decidable: any register value can still be
// steered to the residue by the octets that follow, because the FCS the
// transmitter appended is exactly what steers it. So there is no
// mid-frame test for "this frame is doomed" in general.
//
// What IS decidable is the case that matters in practice: a receiver that
// already knows how many octets remain -- from a length field
// (Chapter 5.5) or from a store-and-forward buffer -- can ask whether the
// remaining octets are enough. Zero octets left and a register that is
// not the residue is a definite answer, available before end of frame.
//
// The value is latency: a cut-through path can stop forwarding at the
// moment the answer is known rather than at the frame's end.
module early_terminate_detector
  import crc32_pkg::*;
#(
  parameter logic [31:0] RESIDUE = 32'hDEBB_20E3
) (
  input  logic clk,
  input  logic rst_n,
 
  input  logic        frame_start,
  input  logic        oct_consumed,
  input  logic [31:0] crc_reg,        // the live register, Section 4's
 
  // Remaining octets, where known. Held low when unknown, which is the
  // common case on a pure streaming receiver and must be distinguishable
  // from "zero remaining".
  input  logic        remaining_valid,
  input  logic [13:0] remaining_octets,
 
  output logic        doomed,          // cannot end validly
  output logic        doomed_valid,
  output logic [13:0] octets_saved     // how early the answer came
);
 
  logic [13:0] consumed_q;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      consumed_q   <= '0;
      doomed       <= 1'b0;
      doomed_valid <= 1'b0;
      octets_saved <= '0;
    end else begin
      doomed_valid <= 1'b0;
 
      if (frame_start) begin
        consumed_q <= '0;
        doomed     <= 1'b0;
      end else begin
        if (oct_consumed) consumed_q <= consumed_q + 1'b1;
 
        // The one decidable case, and the guard on remaining_valid is
        // what keeps it honest: without it, an unknown remaining count
        // reads as zero and every frame is declared doomed at its start.
        if (remaining_valid && (remaining_octets == '0) &&
            (crc_reg != RESIDUE) && !doomed) begin
          doomed       <= 1'b1;
          doomed_valid <= 1'b1;
          octets_saved <= '0;
        end
      end
    end
  end
 
endmodule

// SYNTHESIZABLE MONITOR.
//
// Runs the residue check and the comparison check side by side and
// asserts they always agree.
//
// Why bother, when Section 2 argues they are algebraically equivalent:
// because the equivalence is a property of the MATHEMATICS and the two
// implementations are different CIRCUITS. The comparison path has a
// delay line, an octet-assembly order and a payload/FCS decision that the
// residue path does not; each is a place to be wrong.
//
// And when they disagree, the monitor says WHICH is likely wrong, from
// the shape of the disagreement:
//
//   residue rejects, compare accepts  -> the residue constant is wrong
//        for this configuration, OR the compare path assembled the FCS
//        octets in the wrong order and got lucky
//   residue accepts, compare rejects  -> almost always the compare path's
//        octet order or delay-line alignment
module residue_vs_compare_monitor
#(
  parameter int unsigned CNT_W = 32
) (
  input  logic clk,
  input  logic rst_n,
  input  logic clear,
 
  input  logic        res_valid,
  input  logic        res_ok,
  input  logic [31:0] res_observed,
 
  input  logic        cmp_valid,
  input  logic        cmp_ok,
  input  logic [31:0] cmp_computed,
  input  logic [31:0] cmp_received,
 
  output logic             disagree,
  output logic             suspect_residue_constant,
  output logic             suspect_compare_path,
  output logic [CNT_W-1:0] c_disagree,
 
  // The single most useful diagnostic in the module: when the residue
  // path rejects everything, is the observed value CONSTANT? A constant
  // wrong value is a configuration error; a varying one is real
  // corruption.
  output logic             observed_is_constant,
  output logic [31:0]      first_observed,
  output logic             first_observed_valid
);
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      disagree                 <= 1'b0;
      suspect_residue_constant <= 1'b0;
      suspect_compare_path     <= 1'b0;
      c_disagree               <= '0;
      observed_is_constant     <= 1'b1;
      first_observed           <= '0;
      first_observed_valid     <= 1'b0;
    end else begin
      disagree                 <= 1'b0;
      suspect_residue_constant <= 1'b0;
      suspect_compare_path     <= 1'b0;
 
      if (clear) begin
        c_disagree <= '0;
        // The observed-value evidence deliberately survives: it is the
        // thing that distinguishes a configuration error from a link
        // fault, and it is destroyed by a routine counter clear.
      end
 
      if (res_valid && cmp_valid) begin
        if (res_ok != cmp_ok) begin
          disagree <= 1'b1;
          if (!(&c_disagree)) c_disagree <= c_disagree + 1'b1;
          if (!res_ok && cmp_ok) suspect_residue_constant <= 1'b1;
          if (res_ok && !cmp_ok) suspect_compare_path     <= 1'b1;
        end
 
        // Track whether the residue path's observed value ever varies.
        if (!res_ok) begin
          if (!first_observed_valid) begin
            first_observed       <= res_observed;
            first_observed_valid <= 1'b1;
          end else if (res_observed != first_observed) begin
            observed_is_constant <= 1'b0;
          end
        end
      end
    end
  end
 
endmodule

// ---------------------------------------------------------------------
// P1 -- THE CENTRAL PROPERTY, and note it does not mention a value. The
// residue is the same for every valid frame, whatever the frame
// contained. Written this way it survives every convention change.
// ---------------------------------------------------------------------
property p_residue_is_message_independent;
  @(posedge clk) disable iff (!rst_n)
    (check_valid && frame_was_valid) |-> (residue_observed == $past(last_valid_residue));
endproperty
a_residue_is_message_independent: assert property (p_residue_is_message_independent);
 
// ---------------------------------------------------------------------
// P2 -- The residue is length-independent too. A separate property,
// because a design can be message-independent and length-dependent if a
// convention is applied per-octet where it should be per-frame.
// ---------------------------------------------------------------------
property p_residue_is_length_independent;
  @(posedge clk) disable iff (!rst_n)
    (check_valid && frame_was_valid && (frame_octets != $past(frame_octets)))
      |-> (residue_observed == $past(residue_observed));
endproperty
a_residue_is_length_independent: assert property (p_residue_is_length_independent);
 
// ---------------------------------------------------------------------
// P3 -- A valid frame is accepted. The residue constant matches what the
// derivation produced -- and RESIDUE is the DERIVED parameter, not a
// literal, which is what makes this property meaningful.
// ---------------------------------------------------------------------
property p_valid_frame_accepted;
  @(posedge clk) disable iff (!rst_n)
    (check_valid && frame_was_valid) |-> fcs_ok;
endproperty
a_valid_frame_accepted: assert property (p_valid_frame_accepted);
 
// ---------------------------------------------------------------------
// P4 -- The derived residue is message-independent at ELABORATION. If it
// were not, Section 4's whole approach would be invalid.
// ---------------------------------------------------------------------
// synopsys translate_off
a_derivation_consistent: assert final (RES_A == RES_B)
  else $fatal(1, "derived residue depends on the message");
// synopsys translate_on
 
// ---------------------------------------------------------------------
// P5 -- And, for Ethernet's conventions specifically, the derivation
// lands on the published number. GUARDED, so the module stays usable for
// other configurations rather than asserting a value they do not have.
// ---------------------------------------------------------------------
// synopsys translate_off
a_derivation_matches_published: assert final
  ((INIT_VALUE != 32'hFFFF_FFFF) || (REFLECT_IN != 1'b1) ||
   (REFLECT_OUT != 1'b1) || (XOR_OUT != 32'hFFFF_FFFF) ||
   (RES_A == 32'hDEBB_20E3));
// synopsys translate_on
 
// ---------------------------------------------------------------------
// P6 -- The three published readings are one value. Constant
// relationships, asserted so an edit to any of them is caught here.
// ---------------------------------------------------------------------
// synopsys translate_off
a_readings_consistent: assert final
  ((reflect32(32'hDEBB_20E3) == 32'hC704_DD7B) &&
   ((32'h2144_DF1C ^ 32'hFFFF_FFFF) == 32'hDEBB_20E3));
// synopsys translate_on
 
// ---------------------------------------------------------------------
// P7 -- The residue checker holds no captured value. Written over the
// interface: there is no port carrying an assembled received FCS,
// because the design never assembles one.
// ---------------------------------------------------------------------
property p_no_captured_fcs;
  @(posedge clk) disable iff (!rst_n)
    check_valid |-> !fcs_capture_register_written;
endproperty
a_no_captured_fcs: assert property (p_no_captured_fcs);
 
// ---------------------------------------------------------------------
// P8 -- The register is preset every frame. Carry-over from the previous
// frame makes the residue history-dependent, which is the one way it can
// stop being constant.
// ---------------------------------------------------------------------
property p_preset_every_frame;
  @(posedge clk) disable iff (!rst_n)
    frame_start |=> (crc_reg == INIT_VALUE);
endproperty
a_preset_every_frame: assert property (p_preset_every_frame);
 
// ---------------------------------------------------------------------
// P9 -- A truncated frame is rejected by the ORDINARY path, with no
// special case. This is Section 8's structural claim, asserted.
// ---------------------------------------------------------------------
property p_truncated_frame_rejected;
  @(posedge clk) disable iff (!rst_n)
    (check_valid && frame_truncated) |-> !fcs_ok;
endproperty
a_truncated_frame_rejected: assert property (p_truncated_frame_rejected);
 
// ---------------------------------------------------------------------
// P10 -- A truncated frame is not reported as a mismatch by the layer
// above (Chapter 5.8 §4). The residue path must not manufacture one.
// ---------------------------------------------------------------------
property p_truncation_not_a_mismatch;
  @(posedge clk) disable iff (!rst_n)
    frame_truncated |-> !report_fcs_mismatch;
endproperty
a_truncation_not_a_mismatch: assert property (p_truncation_not_a_mismatch);
 
// ---------------------------------------------------------------------
// P11 -- The early-terminate detector never condemns a frame while the
// remaining count is unknown. Without this guard every frame is doomed
// at its start.
// ---------------------------------------------------------------------
property p_no_doom_without_remaining;
  @(posedge clk) disable iff (!rst_n)
    doomed_valid |-> $past(remaining_valid);
endproperty
a_no_doom_without_remaining: assert property (p_no_doom_without_remaining);
 
// ---------------------------------------------------------------------
// P12 -- Doom is sticky within a frame and cleared at the next start. A
// frame declared doomed cannot un-doom itself.
// ---------------------------------------------------------------------
property p_doom_sticky_within_frame;
  @(posedge clk) disable iff (!rst_n)
    (doomed && !frame_start) |=> doomed;
endproperty
a_doom_sticky_within_frame: assert property (p_doom_sticky_within_frame);
 
// ---------------------------------------------------------------------
// P13 -- THE EQUIVALENCE. Residue and comparison agree on every frame.
// The property that makes running both worthwhile.
// ---------------------------------------------------------------------
property p_residue_equals_compare;
  @(posedge clk) disable iff (!rst_n)
    (res_valid && cmp_valid) |-> (res_ok == cmp_ok);
endproperty
a_residue_equals_compare: assert property (p_residue_equals_compare)
  else $error("residue and comparison disagree -- one path is misconfigured");
 
// ---------------------------------------------------------------------
// P14 -- The disagreement verdicts are exclusive and complete.
// ---------------------------------------------------------------------
property p_disagree_verdicts_exclusive;
  @(posedge clk) disable iff (!rst_n)
    disagree |-> $onehot({suspect_residue_constant, suspect_compare_path});
endproperty
a_disagree_verdicts_exclusive: assert property (p_disagree_verdicts_exclusive);
 
// ---------------------------------------------------------------------
// P15 -- A constant observed residue across rejected frames is evidence
// of misconfiguration, not corruption. Asserted as an implication so the
// monitor cannot report both.
// ---------------------------------------------------------------------
property p_constant_observed_implies_config;
  @(posedge clk) disable iff (!rst_n)
    (observed_is_constant && (c_disagree != '0)) |-> suspect_residue_constant;
endproperty
a_constant_observed_implies_config: assert property (p_constant_observed_implies_config);
 
// ---------------------------------------------------------------------
// P16 -- The evidence survives a counter clear.
// ---------------------------------------------------------------------
property p_evidence_survives_clear;
  @(posedge clk) disable iff (!rst_n)
    clear |=> ($stable(first_observed) && $stable(observed_is_constant));
endproperty
a_evidence_survives_clear: assert property (p_evidence_survives_clear);
 
// ---------------------------------------------------------------------
// P17 -- The residue checker never needs to know where the payload
// ended. Written over the interface: no signal marking the payload's
// last octet reaches this module at all.
// ---------------------------------------------------------------------
property p_no_payload_end_dependency;
  @(posedge clk) disable iff (!rst_n)
    check_valid |-> !payload_end_used_by_checker;
endproperty
a_no_payload_end_dependency: assert property (p_no_payload_end_dependency);
 
// ---------------------------------------------------------------------
// P18 -- A frame with an appended octet is rejected. The trailing-zero
// case of Chapter 6.2 §6, which the final complement exists to catch and
// which a residue checker inherits for free.
// ---------------------------------------------------------------------
property p_appended_octet_rejected;
  @(posedge clk) disable iff (!rst_n)
    (check_valid && frame_had_trailing_octet) |-> !fcs_ok;
endproperty
a_appended_octet_rejected: assert property (p_appended_octet_rejected);
 
// ---------------------------------------------------------------------
// P19 -- The observed residue is reported on every check, pass or fail.
// A checker that exposes it only on failure cannot establish that the
// value is CONSTANT across failures, which is Section 10's diagnostic.
// ---------------------------------------------------------------------
property p_observed_always_reported;
  @(posedge clk) disable iff (!rst_n)
    check_valid |-> !$isunknown(residue_observed);
endproperty
a_observed_always_reported: assert property (p_observed_always_reported);
 
// ---------------------------------------------------------------------
// P20 -- COVERAGE. Valid frames at several lengths, which is what makes
// P2 meaningful rather than vacuous.
// ---------------------------------------------------------------------
c_lengths_swept: cover property (
  @(posedge clk) disable iff (!rst_n) three_distinct_valid_lengths_seen
);
 
// ---------------------------------------------------------------------
// P21 -- COVERAGE. A disagreement between the two paths. A run that
// never produced one never tested Section 10.
// ---------------------------------------------------------------------
c_paths_disagreed: cover property (
  @(posedge clk) disable iff (!rst_n) disagree
);