SEL_O

for each lane n:
    if (write is qualified) and (SEL_I[n]):
        storage[word][lane n] <= DAT_I[8n+7 : 8n]

// ─────────────────────────────────────────────────────────────────────────
// wb_sel_slave — a byte-addressable register file, correctly lane-gated.
//
// PURPOSE. This is the reference structure for every Wishbone slave that
// holds storage rather than fixed fields: a per-lane conditional write.
//
// LANE CONVENTION. sel_i[n] covers dat[8n+7 : 8n]. That is a WIRE fact and
// is fixed. Which BYTE ADDRESS lands in which lane is an endianness
// decision made by the MASTER (Section 2) and is not this module's business.
//
// Reset: SYNCHRONOUS, ACTIVE HIGH (RULES 2.30, 3.00).
// ─────────────────────────────────────────────────────────────────────────
module wb_sel_slave #(
  parameter int unsigned OFF_AW = 4,           // 16 words
  parameter int unsigned DW     = 32
) (
  input  logic                  clk_i,
  input  logic                  rst_i,
  input  logic                  cyc_i,
  input  logic                  stb_i,
  input  logic                  we_i,
  input  logic [(DW/8)-1:0]     sel_i,          // qualified with stb_i
  input  logic [OFF_AW-1:0]     adr_i,
  input  logic [DW-1:0]         dat_i,
  output logic [DW-1:0]         dat_o,
  output logic                  ack_o,
  output logic                  err_o
);
  localparam int unsigned NL    = DW / 8;       // lanes
  localparam int unsigned WORDS = 1 << OFF_AW;

  logic [DW-1:0] mem_q [WORDS];

  logic xfer;
  assign xfer = cyc_i & stb_i;                  // RULES 3.30 & 3.35

  // A write with SEL_I == 0 selects nothing. It is not an error in the
  // specification's terms, but it is almost always a master bug, so this
  // slave reports it rather than silently doing nothing — an EDUCATIONAL
  // IMPLEMENTATION CHOICE, flagged as such, not a specification rule.
  logic empty_sel;
  assign empty_sel = xfer & (sel_i == '0);

  assign err_o = empty_sel;
  assign ack_o = xfer & ~err_o;

  logic write_ok;
  assign write_ok = xfer & we_i & ~err_o;       // Chapter 4.6's single term

  // ── THE PER-LANE CONDITIONAL WRITE ─────────────────────────────────────
  // Each lane is gated INDEPENDENTLY. An unselected lane is not written at
  // all, so it keeps the neighbouring byte it already holds.
  //
  // The whole-word alternative —
  //     if (write_ok) mem_q[adr_i] <= dat_i;
  // — stores all NL lanes, taking unselected ones from whatever the master
  // left on dat_i. That destroys three neighbours on every byte write, and
  // the destroyed bytes belong to data the transfer never named.
  always_ff @(posedge clk_i) begin
    if (rst_i) begin
      for (int unsigned w = 0; w < WORDS; w++) mem_q[w] <= '0;
    end else if (write_ok) begin
      for (int unsigned n = 0; n < NL; n++) begin
        if (sel_i[n]) mem_q[adr_i][n*8 +: 8] <= dat_i[n*8 +: 8];
      end
    end
  end

  // ── READ PATH ──────────────────────────────────────────────────────────
  // On a read, unselected lanes carry nothing a master should believe.
  // Driving zero there is an educational choice that makes the discipline
  // VISIBLE in simulation: a master that ignores SEL on reads sees zeros
  // in the lanes it did not ask for, rather than plausible data that hides
  // the mistake. A slave returning the full word is equally conformant.
  always_comb begin
    dat_o = '0;
    if (xfer && !we_i && !err_o) begin
      for (int unsigned n = 0; n < NL; n++) begin
        if (sel_i[n]) dat_o[n*8 +: 8] = mem_q[adr_i][n*8 +: 8];
      end
    end
  end
endmodule

// ─────────────────────────────────────────────────────────────────────────
// wb_sel_master — converting a BYTE address and a SIZE into a word address
// plus a lane mask. This is where endianness actually lives.
//
// LITTLE-ENDIAN. Byte offset 0 within a word occupies lane 0. Stated here
// because it is a CHOICE, not a specification requirement (Section 2).
// ─────────────────────────────────────────────────────────────────────────
module wb_sel_master #(
  parameter int unsigned BYTE_AW = 32,
  parameter int unsigned DW      = 32
) (
  input  logic                    clk_i,
  input  logic                    rst_i,

  input  logic                    go_i,
  input  logic                    we_i,
  input  logic [BYTE_AW-1:0]      badr_i,       // BYTE address from the CPU
  input  logic [1:0]              size_i,       // 0=byte 1=half 2=word
  input  logic [DW-1:0]           wdat_i,       // right-justified payload
  output logic                    done_o,
  output logic                    misaligned_o,

  output logic                    cyc_o,
  output logic                    stb_o,
  output logic                    we_o,
  output logic [(DW/8)-1:0]       sel_o,
  output logic [BYTE_AW-3:0]      adr_o,        // WORD address
  output logic [DW-1:0]           dat_o,
  input  logic                    ack_i,
  input  logic                    err_i,
  input  logic                    rty_i
);
  localparam int unsigned NL = DW / 8;

  logic          active_q;
  logic [(NL)-1:0] sel_q;
  logic [BYTE_AW-3:0] adr_q;
  logic [DW-1:0] dat_q;
  logic          we_q;

  assign cyc_o = active_q;
  assign stb_o = active_q;
  assign we_o  = we_q;
  assign sel_o = sel_q;
  assign adr_o = adr_q;
  assign dat_o = dat_q;

  // ── LANE MASK FROM BYTE OFFSET AND SIZE ────────────────────────────────
  // Little-endian: offset 0 -> lane 0.
  logic [1:0] boff;
  assign boff = badr_i[1:0];

  function automatic logic [NL-1:0] mask_of(input logic [1:0] sz,
                                            input logic [1:0] off);
    unique case (sz)
      2'd0: mask_of = NL'(4'b0001) << off;              // one byte
      2'd1: mask_of = NL'(4'b0011) << off;              // half-word
      default: mask_of = {NL{1'b1}};                    // full word
    endcase
  endfunction

  // ── ALIGNMENT ──────────────────────────────────────────────────────────
  // A half-word at offset 1 or 3, or a word at any non-zero offset, would
  // need a mask that straddles two words. Wishbone has no such transfer.
  // Detecting this HERE, in the master, is the right place: the alternative
  // is a silently truncated mask and a corrupted neighbour.
  logic bad_align;
  always_comb begin
    unique case (size_i)
      2'd0:    bad_align = 1'b0;
      2'd1:    bad_align = boff[0];
      default: bad_align = (boff != 2'd0);
    endcase
  end

  // ── PAYLOAD PLACEMENT ──────────────────────────────────────────────────
  // The CPU hands over a right-justified value; the bus expects it in the
  // lanes SEL names. A byte destined for lane 2 must be shifted there.
  // Forgetting this shift is the "byte always lands in lane 0" bug.
  logic [DW-1:0] placed;
  assign placed = wdat_i << (8 * boff);

  logic terminated;
  assign terminated = ack_i | err_i | rty_i;

  always_ff @(posedge clk_i) begin
    if (rst_i) begin
      active_q     <= 1'b0;
      sel_q        <= '0;
      adr_q        <= '0;
      dat_q        <= '0;
      we_q         <= 1'b0;
      done_o       <= 1'b0;
      misaligned_o <= 1'b0;
    end else begin
      done_o       <= 1'b0;
      misaligned_o <= 1'b0;
      if (!active_q) begin
        if (go_i) begin
          if (bad_align) begin
            // Refuse locally. Never issue a transfer whose mask cannot
            // express what was asked for.
            done_o       <= 1'b1;
            misaligned_o <= 1'b1;
          end else begin
            active_q <= 1'b1;
            we_q     <= we_i;
            sel_q    <= mask_of(size_i, boff);
            adr_q    <= badr_i[BYTE_AW-1:2];
            dat_q    <= placed;
          end
        end
      end else if (terminated) begin
        active_q <= 1'b0;
        done_o   <= 1'b1;
      end
    end
  end
endmodule

// ─────────────────────────────────────────────────────────────────────────
// wb_sel_checker — byte-lane properties.
//
// P1 is the important one and is SPECIFICATION-derived: the SEL_O() signal
// description defines it as naming where valid data is PLACED on writes,
// which means an unselected lane carries nothing the slave may act on.
//
// P2 is SPECIFICATION-derived in the same way, for the read direction.
// P3 and P4 are LOCAL DESIGN POLICY — the specification does not forbid a
// zero mask, and the stability obligation is inherited by analogy with
// RULE 3.60's qualification requirement rather than stated as a stability
// rule for SEL in its own right.
// ─────────────────────────────────────────────────────────────────────────
module wb_sel_checker #(
  parameter int unsigned DW = 32,
  parameter int unsigned NL = 4
) (
  input logic           clk_i,
  input logic           rst_i,
  input logic           cyc_i,
  input logic           stb_i,
  input logic           we_i,
  input logic           ack_o,
  input logic           err_o,
  input logic [NL-1:0]  sel_i,
  input logic [DW-1:0]  word_q,        // the addressed word, white-box
  input logic [DW-1:0]  word_prev      // its value one cycle earlier
);
  default disable iff (rst_i);

  // P1 — SPECIFICATION-derived, and the property this chapter exists for.
  //      Every UNSELECTED lane of the addressed word must be unchanged.
  //      Generated per lane so a failure names WHICH lane was destroyed,
  //      which turns a vague "data corrupted" into a one-line diagnosis.
  generate
    for (genvar n = 0; n < NL; n++) begin : g_lane
      property p_unselected_lane_preserved;
        @(posedge clk_i)
          (word_q[n*8 +: 8] != word_prev[n*8 +: 8]) |-> $past(sel_i[n]);
      endproperty
      a_unselected_lane_preserved :
        assert property (p_unselected_lane_preserved)
        else $error("lane %0d changed while unselected", n);
    end
  endgenerate

  // P2 — SPECIFICATION-derived. No lane changes at all outside a qualified
  //      write, which is Chapter 4.6's P1 restated for this storage.
  property p_no_change_without_write;
    @(posedge clk_i) (word_q != word_prev) |-> $past(cyc_i && stb_i && we_i);
  endproperty
  a_no_change_without_write : assert property (p_no_change_without_write)
    else $error("stored word changed outside a qualified write");

  // P3 — LOCAL POLICY. A qualified transfer selects at least one lane.
  //      The specification does not require this; a zero mask is simply a
  //      transfer that moves nothing. It is asserted because in practice it
  //      is always a master bug, and a silent no-op is expensive to find.
  property p_nonempty_mask;
    @(posedge clk_i) (cyc_i && stb_i) |-> (sel_i != '0);
  endproperty
  a_nonempty_mask : assert property (p_nonempty_mask)
    else $error("qualified transfer with an empty byte-lane mask");

  // P4 — LOCAL POLICY, read out of RULE 3.60. SEL is stable while a
  //      transfer is outstanding. The end boundary is the termination, for
  //      exactly the reason Chapter 4.6 Section 10 set out.
  property p_sel_stable;
    @(posedge clk_i) (cyc_i && stb_i && !ack_o && !err_o) |=> $stable(sel_i);
  endproperty
  a_sel_stable : assert property (p_sel_stable)
    else $error("SEL changed while a transfer was outstanding");
endmodule