LPDDR4 Architecture

   16n prefetch on a x16 channel
   = 16 transfers x 16 bits
   = 256 bits
   = 32 bytes minimum per channel burst

// ---------------------------------------------------------------------
// lp4_ca_decoder -- assembles a command from 1, 2 or 4 consecutive
// positive-edge samples of a 6-bit CA bus.
//
// CLASSIFICATION: educational, synthesisable.
//
// VERIFIED STRUCTURE, ILLUSTRATIVE ENCODING. That commands span 1, 2
// or 4 cycles on a 6-bit bus sampled on the positive edge only is
// DEVICE-VERIFIED (§1). The specific opcode-to-length mapping below
// is ILLUSTRATIVE and is NOT reproduced from any datasheet's truth
// table -- §11's header says so and it matters.
//
// WHAT IT DOES NOT MODEL:
//   - the device, the electrical interface, or any timing parameter
//   - the real command set (Module 7 owns DDR's; this is not it)
//   - what the device does with a malformed command, which is not
//     defined to be a clean rejection
//
// WHY THE OCCUPANCY OUTPUT EXISTS: §2's callout. A 4-cycle command
// holds the bus for 4 clocks and cannot be interleaved, so the bus is
// a schedulable resource and a controller needs to see it.
// ---------------------------------------------------------------------
module lp4_ca_decoder #(
  parameter int CA_W    = 6,        // DEVICE-VERIFIED width
  parameter int MAX_CY  = 4,        // DEVICE-VERIFIED maximum length
  parameter int CMD_W   = CA_W * MAX_CY,
  parameter int CY_W    = $clog2(MAX_CY + 1),   // a COUNT, not an index
  parameter int CNT_W   = 20
) (
  input  logic              clk,
  input  logic              rst_n,

  // ── The interface. Sampled on the POSITIVE EDGE ONLY -- there is no
  //    negative-edge path in this block, deliberately (§1, §3).
  input  logic              cke,
  input  logic              cs,
  input  logic [CA_W-1:0]   ca,

  // ── Assembled output.
  output logic              cmd_valid,
  output logic [CMD_W-1:0]  cmd_bits,
  output logic [CY_W-1:0]   cmd_length,

  // ── Bus occupancy. §2's callout: the command bus is a resource.
  output logic              bus_busy,
  output logic [CY_W-1:0]   cycles_remaining,
  output logic [CNT_W-1:0]  cy_bus_occupied,
  output logic [CNT_W-1:0]  cnt_cmds_1cy,
  output logic [CNT_W-1:0]  cnt_cmds_2cy,
  output logic [CNT_W-1:0]  cnt_cmds_4cy,

  // ── Malformed assembly, reported by kind.
  output logic              err_truncated,     // CS dropped mid-command
  output logic              err_cke_low_mid,   // CKE dropped mid-command
  output logic              err_new_cmd_mid,   // a start arrived mid-command
  output logic              err_unknown_length,
  output logic              any_malformed
);

  // ILLUSTRATIVE length mapping, from the top two bits of the first
  // sample. NOT a datasheet truth table (§11's header).
  localparam logic [1:0] L_ONE  = 2'b00;
  localparam logic [1:0] L_TWO  = 2'b01;
  localparam logic [1:0] L_FOUR = 2'b10;

  initial begin
    if (CA_W != 6)
      // Not a functional requirement -- a warning that the block is
      // being used outside the width §1 verified.
      $display("lp4_ca_decoder: NOTE -- CA_W=%0d, device-verified width is 6",
               CA_W);
    if (MAX_CY != 4)
      $fatal(1, "lp4_ca_decoder: MAX_CY must be 4 (device-verified)");
    if (CMD_W != CA_W * MAX_CY)
      $fatal(1, "lp4_ca_decoder: CMD_W must be CA_W*MAX_CY");
  end

  logic [CMD_W-1:0] acc;
  logic [CY_W-1:0]  need, got;
  logic             active;
  logic [CNT_W-1:0] occ, n1, n2, n4;
  logic             v, e_tr, e_ck, e_nw, e_ul;
  logic [CY_W-1:0]  out_len;
  logic [CMD_W-1:0] out_bits;

  // A command STARTS when CS is asserted with CKE high. Declared above
  // the continuous assigns that read it.
  logic start;
  assign start = cke && cs;

  // Length of a starting command, from its first sample.
  logic [CY_W-1:0] len_of_start;
  logic            len_known;
  always_comb begin
    unique case (ca[CA_W-1 -: 2])
      L_ONE   : begin len_of_start = CY_W'(1); len_known = 1'b1; end
      L_TWO   : begin len_of_start = CY_W'(2); len_known = 1'b1; end
      L_FOUR  : begin len_of_start = CY_W'(4); len_known = 1'b1; end
      default : begin len_of_start = CY_W'(1); len_known = 1'b0; end
    endcase
  end

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      acc <= '0; need <= '0; got <= '0; active <= 1'b0;
      occ <= '0; n1 <= '0; n2 <= '0; n4 <= '0;
      v <= 1'b0; out_len <= '0; out_bits <= '0;
      e_tr <= 1'b0; e_ck <= 1'b0; e_nw <= 1'b0; e_ul <= 1'b0;
    end else begin
      v <= 1'b0;
      e_tr <= 1'b0; e_ck <= 1'b0; e_nw <= 1'b0; e_ul <= 1'b0;

      if (active) begin
        if (occ != {CNT_W{1'b1}}) occ <= occ + CNT_W'(1);

        // ── Mid-command hazards, each reported separately so a debug
        //    session learns WHICH way the assembly broke.
        if (!cke) begin
          // §1: CKE low mid-command. The remaining samples will not
          // arrive, so the partial command is abandoned rather than
          // completed with stale bits -- completing it would
          // fabricate a command the controller never sent.
          e_ck   <= 1'b1;
          active <= 1'b0;
          acc    <= '0;
          got    <= '0;
        end else if (start && (got != need)) begin
          // A new command asserted while one is still assembling. The
          // bus cannot carry two, so the new one is REJECTED and the
          // in-flight one continues. Dropping the in-flight one
          // instead would lose a command the controller believes it
          // issued.
          e_nw <= 1'b1;
          acc[got*CA_W +: CA_W] <= ca;
          got <= got + CY_W'(1);
          if ((got + CY_W'(1)) == need) begin
            v <= 1'b1; out_bits <= acc; out_len <= need; active <= 1'b0;
          end
        end else if (!cs && (got != need)) begin
          // §16's truncation row: the strobe went away before the
          // command finished.
          e_tr   <= 1'b1;
          active <= 1'b0;
          acc    <= '0;
          got    <= '0;
        end else begin
          acc[got*CA_W +: CA_W] <= ca;
          if ((got + CY_W'(1)) == need) begin
            v        <= 1'b1;
            // The final sample is folded in COMBINATIONALLY for the
            // output, not read back from acc -- acc's last write lands
            // on this same edge, so reading it would publish the
            // PRE-fold value. This is the stale-register hazard
            // Module 21 §10 names.
            out_bits <= acc | (CMD_W'(ca) << (got*CA_W));
            out_len  <= need;
            active   <= 1'b0;
            acc      <= '0;
            got      <= '0;
            unique case (need)
              CY_W'(1) : if (n1 != {CNT_W{1'b1}}) n1 <= n1 + CNT_W'(1);
              CY_W'(2) : if (n2 != {CNT_W{1'b1}}) n2 <= n2 + CNT_W'(1);
              CY_W'(4) : if (n4 != {CNT_W{1'b1}}) n4 <= n4 + CNT_W'(1);
              default  : ;
            endcase
          end else begin
            got <= got + CY_W'(1);
          end
        end
      end else if (start) begin
        if (!len_known) begin
          e_ul <= 1'b1;
        end else if (len_of_start == CY_W'(1)) begin
          // A one-cycle command completes on its own start edge and
          // never occupies the bus beyond it.
          v        <= 1'b1;
          out_bits <= CMD_W'(ca);
          out_len  <= CY_W'(1);
          if (occ != {CNT_W{1'b1}}) occ <= occ + CNT_W'(1);
          if (n1 != {CNT_W{1'b1}}) n1 <= n1 + CNT_W'(1);
        end else begin
          active <= 1'b1;
          need   <= len_of_start;
          got    <= CY_W'(1);
          acc    <= CMD_W'(ca);
          if (occ != {CNT_W{1'b1}}) occ <= occ + CNT_W'(1);
        end
      end
    end
  end

  assign cmd_valid        = v;
  assign cmd_bits         = out_bits;
  assign cmd_length       = out_len;
  assign bus_busy         = active;
  assign cycles_remaining = active ? (need - got) : CY_W'(0);
  assign cy_bus_occupied  = occ;
  assign cnt_cmds_1cy     = n1;
  assign cnt_cmds_2cy     = n2;
  assign cnt_cmds_4cy     = n4;
  assign err_truncated      = e_tr;
  assign err_cke_low_mid    = e_ck;
  assign err_new_cmd_mid    = e_nw;
  assign err_unknown_length = e_ul;
  assign any_malformed = e_tr | e_ck | e_nw | e_ul;
endmodule

out_bits <= acc | (CMD_W'(ca) << (got*CA_W));

out_bits <= acc;              // WRONG -- one sample short

// ---------------------------------------------------------------------
// lp4_channel_guard -- the §6 independence invariant as a checker,
// plus arbitration for the §7 shared resources.
//
// CLASSIFICATION: educational, synthesisable.
//
// WHAT IT DOES NOT MODEL:
//   - either channel's internal state. 24.2's lp_state_machine is
//     instantiated PER CHANNEL (§5) and this block sits beside two of
//     them rather than containing them.
//   - a legal address sent to the WRONG channel. §6's callout: that
//     is indistinguishable from a correct access at this level, and a
//     block claiming to catch it would be claiming the impossible.
//     What IS checkable is that selection depends only on the bits
//     assigned to it, which is the invariant that makes the bug
//     possible in the first place.
//
// WHY ARBITRATION IS HERE AND NOT PER CHANNEL: §7. RESET_n and ZQ are
// shared, so they are the ONE place where two independent channels
// must be serialised, and a per-channel block cannot do it.
// ---------------------------------------------------------------------
module lp4_channel_guard #(
  parameter int ADDR_W  = 34,
  // Address bit selecting the channel. On the named part the die is
  // split evenly between two channels (§5), so exactly one bit does
  // the selecting -- and WHICH bit is a controller mapping choice
  // with the §9 consequence.
  parameter int SEL_BIT = 33,
  parameter int CNT_W   = 20
) (
  input  logic              clk,
  input  logic              rst_n,

  // ── Per-channel activity. Two of everything, never one.
  input  logic              a_cmd_valid,
  input  logic              b_cmd_valid,
  input  logic [ADDR_W-1:0] a_addr,
  input  logic [ADDR_W-1:0] b_addr,
  input  logic              a_bus_busy,
  input  logic              b_bus_busy,

  // ── Shared-resource requests (§7).
  input  logic              a_zq_req,
  input  logic              b_zq_req,
  input  logic              reset_req,

  // ── Arbitrated shared-resource grants.
  output logic              a_zq_grant,
  output logic              b_zq_grant,
  output logic              reset_both,

  // ── Independence observation. Concurrency is the PROPERTY, so it
  //    is counted rather than merely permitted.
  output logic [CNT_W-1:0]  cy_both_busy,
  output logic [CNT_W-1:0]  cy_only_a,
  output logic [CNT_W-1:0]  cy_only_b,
  output logic [CNT_W-1:0]  cy_neither,
  output logic              concurrency_observed,

  // ── Violations.
  output logic              err_wrong_channel_a,
  output logic              err_wrong_channel_b,
  output logic              err_zq_both,
  output logic              err_reset_one_channel,
  output logic              any_violation
);

  initial begin
    if (SEL_BIT >= ADDR_W)
      $fatal(1, "lp4_channel_guard: SEL_BIT (%0d) outside ADDR_W (%0d)",
             SEL_BIT, ADDR_W);
  end

  logic [CNT_W-1:0] c_both, c_a, c_b, c_none;
  logic             e_wa, e_wb, e_zq, e_r1, saw_conc;
  logic             zq_last_a;

  // Declared above the assigns that read them.
  logic a_sel_ok, b_sel_ok;
  assign a_sel_ok = (a_addr[SEL_BIT] == 1'b0);
  assign b_sel_ok = (b_addr[SEL_BIT] == 1'b1);

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      c_both <= '0; c_a <= '0; c_b <= '0; c_none <= '0;
      e_wa <= 1'b0; e_wb <= 1'b0; e_zq <= 1'b0; e_r1 <= 1'b0;
      saw_conc <= 1'b0; zq_last_a <= 1'b0;
    end else begin
      e_wa <= 1'b0; e_wb <= 1'b0; e_zq <= 1'b0; e_r1 <= 1'b0;

      // ── Occupancy, four-way and exhaustive. §6: a controller that
      //    never reaches "both busy" has not built two channels.
      case ({a_bus_busy, b_bus_busy})
        2'b11 : begin
          if (c_both != {CNT_W{1'b1}}) c_both <= c_both + CNT_W'(1);
          saw_conc <= 1'b1;
        end
        2'b10 : if (c_a    != {CNT_W{1'b1}}) c_a    <= c_a    + CNT_W'(1);
        2'b01 : if (c_b    != {CNT_W{1'b1}}) c_b    <= c_b    + CNT_W'(1);
        2'b00 : if (c_none != {CNT_W{1'b1}}) c_none <= c_none + CNT_W'(1);
      endcase

      // ── The checkable half of §6's third rule: selection must be a
      //    function of the assigned bit and nothing else.
      if (a_cmd_valid && !a_sel_ok) e_wa <= 1'b1;
      if (b_cmd_valid && !b_sel_ok) e_wb <= 1'b1;

      // ── §7: ZQ is shared. Simultaneous requests are a real error
      //    and not merely arbitrated away silently -- a controller
      //    that issues both has not serialised its calibration.
      if (a_zq_req && b_zq_req) e_zq <= 1'b1;
      if (a_zq_req ^ b_zq_req)  zq_last_a <= a_zq_req;
    end
  end

  // Alternating priority, so neither channel starves the other when
  // both ask repeatedly.
  assign a_zq_grant = a_zq_req && (!b_zq_req || zq_last_a == 1'b0);
  assign b_zq_grant = b_zq_req && !a_zq_grant;
  // §7: RESET_n is shared, so it is a DEVICE action. There is no
  // per-channel reset, and the output name says so.
  assign reset_both  = reset_req;
  assign err_reset_one_channel = 1'b0;   // structurally impossible here

  assign cy_both_busy = c_both;
  assign cy_only_a    = c_a;
  assign cy_only_b    = c_b;
  assign cy_neither   = c_none;
  assign concurrency_observed = saw_conc;
  assign err_wrong_channel_a = e_wa;
  assign err_wrong_channel_b = e_wb;
  assign err_zq_both         = e_zq;
  assign any_violation = e_wa | e_wb | e_zq;
endmodule

// ---------------------------------------------------------------------
// lp4_prefetch_accountant -- bytes moved versus bytes requested,
// against the DEVICE-VERIFIED 16n prefetch granularity of §8.
//
// CLASSIFICATION: educational, synthesisable.
//
// WHAT IT CLOSES: 24.1 §11's terms_excluded bit 4, "wasted payload on
// small accesses", was permanently set because nothing in that
// chapter could compute it. A verified granularity makes it
// computable, and this block computes it.
//
// WHAT IT DOES NOT MODEL: energy. Waste is reported in BYTES, not in
// joules, because converting requires a per-bit energy figure no
// datasheet consulted in this module publishes. §14's header says so.
// ---------------------------------------------------------------------
module lp4_prefetch_accountant #(
  // DEVICE-VERIFIED for a x16 channel: 16 transfers x 16 bits = 32 B.
  parameter int GRAN_B  = 32,
  parameter int REQ_W   = 16,
  parameter int ACC_W   = 40,
  parameter int GRAN_SH = $clog2(GRAN_B)
) (
  input  logic              clk,
  input  logic              rst_n,

  input  logic              req_valid,
  input  logic [REQ_W-1:0]  req_bytes,

  // ── Totals. Reported as a PAIR, never as a ratio -- the caller
  //    states its denominator, the discipline every accountant in
  //    this module follows.
  output logic [ACC_W-1:0]  bytes_requested,
  output logic [ACC_W-1:0]  bytes_moved,
  output logic [ACC_W-1:0]  bytes_wasted,
  output logic [ACC_W-1:0]  bursts_issued,

  // ── Per-request, for the current request only.
  output logic [REQ_W+1:0]  this_moved,
  output logic [REQ_W+1:0]  this_wasted,
  output logic              this_is_partial,

  // Small-access classification. §8: a sub-granule request wastes
  // most of what it spends, and the count is the signal a system
  // needs in order to consider coalescing.
  output logic [ACC_W-1:0]  cnt_sub_granule,
  output logic [ACC_W-1:0]  cnt_exact,

  output logic              err_zero_length_req,
  output logic              any_saturated
);

  initial begin
    if (GRAN_B < 2 || (GRAN_B & (GRAN_B - 1)) != 0)
      // A non-power-of-two granule would need a divide to round up,
      // and no real prefetch granularity is one.
      $fatal(1, "lp4_prefetch_accountant: GRAN_B must be a power of two >= 2");
    if (ACC_W <= REQ_W)
      $fatal(1, "lp4_prefetch_accountant: ACC_W must exceed REQ_W");
  end

  logic [ACC_W-1:0] t_req, t_mov, t_bur, n_sub, n_exact;
  logic             e_zero, sat;

  // Round up to the granule by shifting -- no divide. Declared above
  // the assigns that read them.
  logic [REQ_W+1:0] nburst, moved;
  assign nburst = (req_bytes == '0) ? '0
                : (REQ_W+2)'(((req_bytes - REQ_W'(1)) >> GRAN_SH) + 1);
  assign moved  = nburst << GRAN_SH;

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      t_req <= '0; t_mov <= '0; t_bur <= '0;
      n_sub <= '0; n_exact <= '0;
      e_zero <= 1'b0; sat <= 1'b0;
    end else begin
      e_zero <= 1'b0;
      if (req_valid) begin
        if (req_bytes == '0) begin
          e_zero <= 1'b1;
        end else begin
          if (t_req > ({ACC_W{1'b1}} - ACC_W'(moved))) sat <= 1'b1;
          else begin
            t_req <= t_req + ACC_W'(req_bytes);
            t_mov <= t_mov + ACC_W'(moved);
            t_bur <= t_bur + ACC_W'(nburst);
          end
          if (req_bytes < REQ_W'(GRAN_B)) begin
            if (n_sub != {ACC_W{1'b1}}) n_sub <= n_sub + ACC_W'(1);
          end else if (moved == (REQ_W+2)'(req_bytes)) begin
            if (n_exact != {ACC_W{1'b1}}) n_exact <= n_exact + ACC_W'(1);
          end
        end
      end
    end
  end

  assign bytes_requested = t_req;
  assign bytes_moved     = t_mov;
  // Moved is always >= requested by construction, so the subtraction
  // cannot go negative -- P11 asserts the invariant that guarantees it.
  assign bytes_wasted    = (t_mov >= t_req) ? (t_mov - t_req) : '0;
  assign bursts_issued   = t_bur;
  assign this_moved      = moved;
  assign this_wasted     = moved - (REQ_W+2)'(req_bytes);
  assign this_is_partial = req_valid && (req_bytes < REQ_W'(GRAN_B));
  assign cnt_sub_granule = n_sub;
  assign cnt_exact       = n_exact;
  assign err_zero_length_req = e_zero;
  assign any_saturated   = sat;
endmodule

// Bind unit note: P1-P7 reference lp4_ca_decoder's internals, P8-P10
// lp4_channel_guard's, P11-P14 lp4_prefetch_accountant's. Each is
// written as though bound into its module.

// P1 -- a command is never longer than the device-verified maximum.
property p_length_bounded;
  @(posedge clk) disable iff (!rst_n)
    cmd_valid |-> (cmd_length inside {CY_W'(1), CY_W'(2), CY_W'(4)});
endproperty
assert property (p_length_bounded);

// P2 -- the bus cannot carry two commands. While one is assembling,
// no second command completes. §2: the bus is a serial resource.
property p_bus_is_exclusive;
  @(posedge clk) disable iff (!rst_n)
    (bus_busy && (cycles_remaining > CY_W'(1))) |-> !cmd_valid;
endproperty
assert property (p_bus_is_exclusive);

// P3 -- the countdown is monotone while a command assembles. Rules
// out a restart that would silently lengthen the command.
property p_countdown_monotone;
  @(posedge clk) disable iff (!rst_n)
    (bus_busy && $past(bus_busy, 1) && !any_malformed)
      |-> (cycles_remaining < $past(cycles_remaining, 1));
endproperty
assert property (p_countdown_monotone);

// P4 -- a truncated or CKE-interrupted command is NEVER published.
// §11: completing it with stale bits would fabricate a command the
// controller never issued, which is worse than losing one.
property p_malformed_never_published;
  @(posedge clk) disable iff (!rst_n)
    (err_truncated || err_cke_low_mid) |-> !cmd_valid;
endproperty
assert property (p_malformed_never_published);

// P5 -- a one-cycle command never occupies the bus past its own edge.
property p_one_cycle_does_not_occupy;
  @(posedge clk) disable iff (!rst_n)
    (cmd_valid && (cmd_length == CY_W'(1))) |-> !bus_busy;
endproperty
assert property (p_one_cycle_does_not_occupy);

// P6 -- the per-length counters partition the completed commands.
// A command that completed is counted exactly once.
property p_length_counters_partition;
  @(posedge clk) disable iff (!rst_n)
    (cmd_valid && (cmd_length == CY_W'(2)))
      |=> (cnt_cmds_2cy == $past(cnt_cmds_2cy, 1) + CNT_W'(1));
endproperty
assert property (p_length_counters_partition);

// P7 -- §12's hazard, as a property. The published command must carry
// the FINAL sample, which the stale-register bug would omit. Checked
// by requiring the top field of a 4-cycle command to be non-zero
// whenever the final sample was.
property p_final_sample_included;
  @(posedge clk) disable iff (!rst_n)
    (cmd_valid && (cmd_length == CY_W'(4)) && ($past(ca, 1) != '0))
      |-> (cmd_bits[CMD_W-1 -: CA_W] != '0);
endproperty
assert property (p_final_sample_included);

// P8 -- CHANNEL INDEPENDENCE. Neither channel's command validity
// constrains the other's. Asserted as the ABSENCE of an implication:
// both busy simultaneously must be reachable, which is what the
// concurrency cover checks -- and no violation may be raised for it.
property p_concurrency_is_legal;
  @(posedge clk) disable iff (!rst_n)
    (a_bus_busy && b_bus_busy) |-> !any_violation;
endproperty
assert property (p_concurrency_is_legal);

// P9 -- the four occupancy counters partition every cycle exactly.
property p_occupancy_partitions_cycles;
  @(posedge clk) disable iff (!rst_n)
    ((cy_both_busy + cy_only_a + cy_only_b + cy_neither) ==
     ($past(cy_both_busy,1) + $past(cy_only_a,1) +
      $past(cy_only_b,1)   + $past(cy_neither,1) + CNT_W'(1)));
endproperty
assert property (p_occupancy_partitions_cycles);

// P10 -- §7: ZQ is granted to at most one channel. The shared
// resource is genuinely serialised.
property p_zq_mutually_exclusive;
  @(posedge clk) disable iff (!rst_n) !(a_zq_grant && b_zq_grant);
endproperty
assert property (p_zq_mutually_exclusive);

// P11 -- bytes moved is never less than bytes requested. The
// invariant that makes §14's subtraction safe: a granule-rounded
// transfer can only be larger.
property p_moved_at_least_requested;
  @(posedge clk) disable iff (!rst_n) (bytes_moved >= bytes_requested);
endproperty
assert property (p_moved_at_least_requested);

// P12 -- bytes moved is always a whole number of granules. §8: 32 B
// is the smallest thing the channel can move, not the smallest
// efficient thing.
property p_moved_is_whole_granules;
  @(posedge clk) disable iff (!rst_n)
    ((bytes_moved & ACC_W'(GRAN_B - 1)) == '0);
endproperty
assert property (p_moved_is_whole_granules);

// P13 -- a sub-granule request always moves exactly one granule, and
// never zero. The 12.5%-useful row of §8's table, as a property.
property p_sub_granule_moves_one;
  @(posedge clk) disable iff (!rst_n)
    (req_valid && (req_bytes != '0) && (req_bytes < REQ_W'(GRAN_B)))
      |-> (this_moved == (REQ_W+2)'(GRAN_B));
endproperty
assert property (p_sub_granule_moves_one);

// P14 -- a zero-length request moves nothing and is reported. It is
// not silently rounded up to a granule, which would charge the
// system for a transfer it never asked for.
property p_zero_length_moves_nothing;
  @(posedge clk) disable iff (!rst_n)
    (req_valid && (req_bytes == '0)) |=> err_zero_length_req;
endproperty
assert property (p_zero_length_moves_nothing);

// ── Cover.
// All three command lengths actually assembled.
cover property (@(posedge clk) disable iff (!rst_n)
                  cmd_valid && (cmd_length == CY_W'(1)));
cover property (@(posedge clk) disable iff (!rst_n)
                  cmd_valid && (cmd_length == CY_W'(2)));
cover property (@(posedge clk) disable iff (!rst_n)
                  cmd_valid && (cmd_length == CY_W'(4)));
// Each malformed kind reached. A property forbidding something is
// vacuous until the testbench attempts it.
cover property (@(posedge clk) disable iff (!rst_n) err_truncated);
cover property (@(posedge clk) disable iff (!rst_n) err_cke_low_mid);
cover property (@(posedge clk) disable iff (!rst_n) err_new_cmd_mid);
cover property (@(posedge clk) disable iff (!rst_n) err_unknown_length);
// Back-to-back 4-cycle commands -- the 0.25 commands-per-clock
// ceiling of §2's callout, actually exercised.
cover property (@(posedge clk) disable iff (!rst_n)
                  cmd_valid && (cmd_length == CY_W'(4))
                  ##1 bus_busy [*3] ##1 cmd_valid);
// THE INDEPENDENCE COVER. Both channels busy at once. A suite that
// never hits this has not tested the architecture's whole purpose.
cover property (@(posedge clk) disable iff (!rst_n)
                  a_bus_busy && b_bus_busy);
// Both channels contending for ZQ -- §7's one genuine exception.
cover property (@(posedge clk) disable iff (!rst_n) err_zq_both);
// Each row of §8's table: sub-granule, exact, multi-granule.
cover property (@(posedge clk) disable iff (!rst_n) this_is_partial);
cover property (@(posedge clk) disable iff (!rst_n)
                  req_valid && (this_wasted == '0));
cover property (@(posedge clk) disable iff (!rst_n)
                  req_valid && (this_moved > (REQ_W+2)'(GRAN_B)));

// Independent CA reference. Assembles commands from a QUEUE of
// samples rather than from a state machine, so agreement between the
// two is evidence rather than a restatement of one implementation.
// SIMULATION-ONLY.
class ca_assembly_ref;
  bit [5:0] q[$];
  int       need;
  int       n_published;

  function void reset();
    q.delete(); need = 0; n_published = 0;
  endfunction

  function int length_of(bit [5:0] first);
    case (first[5:4])
      2'b00  : return 1;
      2'b01  : return 2;
      2'b10  : return 4;
      default: return -1;          // unknown
    endcase
  endfunction

  // Returns the assembled width in bits when a command completes,
  // 0 while assembling, -1 on a malformed sequence.
  function int sample(bit cke, bit cs, bit [5:0] ca);
    if (!cke && q.size() > 0) begin q.delete(); need = 0; return -1; end
    if (q.size() == 0) begin
      if (!(cke && cs)) return 0;
      need = length_of(ca);
      if (need < 0) return -1;
      q.push_back(ca);
    end else begin
      if (!cs) begin q.delete(); need = 0; return -1; end
      q.push_back(ca);
    end
    if (q.size() == need) begin
      int w = q.size() * 6;
      q.delete(); need = 0; n_published++;
      return w;
    end
    return 0;
  endfunction
endclass

  THE SERIALISED CONTROLLER THAT PASSES EVERY ASSERTION
    Two independent channels, one scheduler issuing to them in turn.

    assertions: P8  concurrency is legal        PASS
                P9  occupancy partitions        PASS
                P10 ZQ mutually exclusive       PASS
                all 14 properties               PASS

    coverage  : a_bus_busy && b_bus_busy        NEVER HIT

    occupancy : cy_both_busy      0
                cy_only_a    41,208
                cy_only_b    40,976
                cy_neither   17,816

    diagnosis : the design is CORRECT and the architecture is WASTED.
      Both channels work, neither ever works at the same time as the
      other, and the two extra CA pins of §4 bought nothing. Peak
      concurrency is 1 where the device offers 2.

    what makes it hard to catch : there is no error. Nothing is
      illegal, no property is violated, and every transaction
      completes. The only evidence is a zero in an occupancy counter
      and an unhit cover.

    the fix : cy_both_busy is a REQUIRED coverage goal, not a
      diagnostic. An LPDDR4 controller whose both-busy count is zero
      has built one channel with two data buses (§6).