Data Transfer

for each lane n:
    if SEL[n]:
        register[lane n] <= write_data[lane n]
    // else: not assigned at all, so the lane keeps its value

lane_mask = {{8{SEL[3]}}, {8{SEL[2]}}, {8{SEL[1]}}, {8{SEL[0]}}}
next      = (write_data & lane_mask) | (register & ~lane_mask)

register <= write_data;        // ignores SEL entirely

// ─────────────────────────────────────────────────────────────────────────
// wb_write_lane — the byte-lane masked update, pulled out on its own.
//
// PURPOSE. This is stage 4 of Figure 1, isolated from the surrounding slave
// so the update rule is reviewable without the qualification logic around
// it. It is a pure function: old value + new value + lane mask -> result.
//
// NOT A WISHBONE SLAVE — no clock, no qualifiers, terminates nothing.
//
// Both formulations from Section 3 appear here so they can be compared,
// and an assertion-free equivalence check is left to Section 8's property.
// ─────────────────────────────────────────────────────────────────────────
module wb_write_lane #(
  parameter int unsigned DW = 32
) (
  input  logic [DW-1:0]   old_i,
  input  logic [DW-1:0]   wdat_i,
  input  logic [DW/8-1:0] sel_i,
  output logic [DW-1:0]   next_o,        // per-lane form (what we use)
  output logic [DW-1:0]   next_mask_o    // mask form (for comparison)
);
  localparam int unsigned NL = DW/8;

  // ── PER-LANE FORM ─────────────────────────────────────────────────────
  // next_o is seeded with the OLD value, then selected lanes are
  // overwritten. Seeding first is what makes the unselected lanes keep
  // their contents, and it is also what prevents a latch: every bit of
  // next_o is assigned on every path through the block.
  always_comb begin
    next_o = old_i;
    for (int unsigned n = 0; n < NL; n++) begin
      if (sel_i[n]) next_o[n*8 +: 8] = wdat_i[n*8 +: 8];
    end
  end

  // ── MASK FORM ─────────────────────────────────────────────────────────
  // Identical result, built from a replicated lane mask. Shown because it
  // appears in a great deal of production RTL and a reader should be able
  // to recognise it — but note how much harder it is to confirm by eye
  // that an unselected lane survives. Dropping the `~` on the second term
  // zeroes every unselected byte and still looks plausible.
  logic [DW-1:0] lane_mask;
  always_comb begin
    for (int unsigned n = 0; n < NL; n++) begin
      lane_mask[n*8 +: 8] = {8{sel_i[n]}};
    end
  end
  assign next_mask_o = (wdat_i & lane_mask) | (old_i & ~lane_mask);
endmodule

// ─────────────────────────────────────────────────────────────────────────
// wb_write_regs_lane — the running peripheral rebuilt around wb_write_lane.
//
// PURPOSE. Show the composition explicitly: qualification, a commit event,
// and a masked update that is now a separately reviewable block.
//
// Functionally identical to Chapter 7.1's wb_write_regs. The difference is
// that the update rule is no longer buried in a for-loop inside an
// always_ff, so it can be argued about — and tested — on its own.
//
// DECLARED COMMIT POLICY (LOCAL, unchanged from Chapter 7.1):
//   commits the addressed register on the same rising clock edge for which
//   it returns ACK_O for a qualified write.
//
// Reset: SYNCHRONOUS, ACTIVE HIGH (RULES 2.30, 3.00).
// ─────────────────────────────────────────────────────────────────────────
module wb_write_regs_lane #(
  parameter int unsigned OFF_AW = 4,
  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 [OFF_AW-1:0] adr_i,
  input  logic [DW-1:0]     dat_i,
  input  logic [DW/8-1:0]   sel_i,
  output logic [DW-1:0]     dat_o,
  output logic              ack_o,
  output logic              err_o,
  output logic [DW-1:0]     control_o,
  output logic [DW-1:0]     outdata_o
);
  localparam logic [OFF_AW-1:0] O_CTRL = 4'd2;
  localparam logic [OFF_AW-1:0] O_OUT  = 4'd6;
  localparam logic [OFF_AW-1:0] O_ID   = 4'd4;
  localparam logic [DW-1:0] ID_VALUE = 32'h5742_0701;

  logic [DW-1:0] ctrl_q, outdata_q;
  assign control_o = ctrl_q;
  assign outdata_o = outdata_q;

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

  logic writable, known_off;
  always_comb begin
    unique case (adr_i)
      O_CTRL, O_OUT: begin known_off = 1'b1; writable = 1'b1; end
      O_ID:          begin known_off = 1'b1; writable = 1'b0; end
      default:       begin known_off = 1'b0; writable = 1'b0; end
    endcase
  end

  logic illegal;
  assign illegal = ~known_off | (we_i & ~writable);
  assign err_o   = xfer &  illegal;
  assign ack_o   = xfer & ~illegal;

  logic commit;
  assign commit = xfer & we_i & ack_o;           // the declared policy

  // ── THE MASKED UPDATE, ONE INSTANCE PER REGISTER ──────────────────────
  // Each register gets its own lane block. The register's own current
  // value goes in as `old_i`, so a lane the write did not select comes
  // back out unchanged and the flop reloads what it already held.
  logic [DW-1:0] ctrl_next, out_next;
  wb_write_lane #(.DW(DW)) u_ctrl_lane (
    .old_i(ctrl_q), .wdat_i(dat_i), .sel_i(sel_i),
    .next_o(ctrl_next), .next_mask_o());
  wb_write_lane #(.DW(DW)) u_out_lane (
    .old_i(outdata_q), .wdat_i(dat_i), .sel_i(sel_i),
    .next_o(out_next), .next_mask_o());

  always_ff @(posedge clk_i) begin
    if (rst_i) begin
      ctrl_q    <= '0;
      outdata_q <= '0;
    end else if (commit) begin
      // Only the ADDRESSED register loads. The other lane block is still
      // computing a result every cycle — that costs nothing and is simply
      // not used, which is the normal shape for a small register file.
      unique case (adr_i)
        O_CTRL:  ctrl_q    <= ctrl_next;
        O_OUT:   outdata_q <= out_next;
        default: ;                                // unreachable under commit
      endcase
    end
  end

  always_comb begin
    dat_o = '0;                                   // RULE 3.65
    if (xfer && !we_i && ack_o) begin
      unique case (adr_i)
        O_CTRL:  dat_o = ctrl_q;
        O_OUT:   dat_o = outdata_q;
        O_ID:    dat_o = ID_VALUE;
        default: dat_o = '0;
      endcase
    end
  end
endmodule

// ─────────────────────────────────────────────────────────────────────────
// wb_write_regs_nosel — THE IGNORED-SEL BUG, isolated for simulation.
//
// NOT A REFERENCE DESIGN. Identical to wb_write_regs_lane except that the
// commit assigns the WHOLE WORD instead of the masked result:
//
//     ctrl_q <= dat_i;        instead of      ctrl_q <= ctrl_next;
//
// Every bus signal it produces is conformant. It acknowledges correctly,
// it refuses read-only offsets correctly, and for a FULL-WORD write it is
// indistinguishable from the correct slave. Only a narrow write exposes
// it, and what it destroys is data the transfer never named.
// ─────────────────────────────────────────────────────────────────────────
module wb_write_regs_nosel #(
  parameter int unsigned OFF_AW = 4,
  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 [OFF_AW-1:0] adr_i,
  input  logic [DW-1:0]     dat_i,
  input  logic [DW/8-1:0]   sel_i,
  output logic [DW-1:0]     dat_o,
  output logic              ack_o,
  output logic              err_o,
  output logic [DW-1:0]     control_o,
  output logic [DW-1:0]     outdata_o
);
  localparam logic [OFF_AW-1:0] O_CTRL = 4'd2;
  localparam logic [OFF_AW-1:0] O_OUT  = 4'd6;

  logic [DW-1:0] ctrl_q, outdata_q;
  assign control_o = ctrl_q;
  assign outdata_o = outdata_q;

  logic xfer; assign xfer = cyc_i & stb_i;
  logic writable;
  always_comb begin
    unique case (adr_i)
      O_CTRL, O_OUT: writable = 1'b1;
      default:       writable = 1'b0;
    endcase
  end
  assign err_o = xfer & we_i & ~writable;
  assign ack_o = xfer & ~(we_i & ~writable);

  logic commit; assign commit = xfer & we_i & ack_o;

  always_ff @(posedge clk_i) begin
    if (rst_i) begin
      ctrl_q <= '0; outdata_q <= '0;
    end else if (commit) begin
      // ── THE BUG: sel_i is never consulted ───────────────────────────
      unique case (adr_i)
        O_CTRL:  ctrl_q    <= dat_i;
        O_OUT:   outdata_q <= dat_i;
        default: ;
      endcase
    end
  end

  assign dat_o = '0;                              // read path omitted
endmodule

  === SIMULATION C - partial write ===
  CONTROL seeded              0x11223344
  write DAT=0xaabbccdd SEL=0010
    per-lane result           0x1122cc44
    mask-form result          0x1122cc44   (identical)
    CONTROL after commit      0x1122cc44
    bytes changed                      1
    bytes preserved                    3

  === the same write, SEL ignored ===
  CONTROL seeded              0x11223344
    CONTROL after commit      0xaabbccdd
    bytes changed                      4
    bytes destroyed that the write never named   3
  bus-trace differences between the two slaves:  0

// ─────────────────────────────────────────────────────────────────────────
// wb_write_data_checker — payload and masking properties.
//
// P1 is a DESIGN OBLIGATION derived from the SEL_O() signal description
// (SEL names where valid data is PLACED on a write) — the specification
// constrains what SEL MEANS, and "therefore an unselected lane must not
// change" is a sound inference about a slave's internal state rather than
// a stated rule. P2 and P3 are SPECIFICATION. P4 is LOCAL POLICY.
// ─────────────────────────────────────────────────────────────────────────
module wb_write_data_checker #(
  parameter int unsigned DW = 32,
  parameter int unsigned NL = 4
) (
  input logic          clk_i,
  input logic          rst_i,
  input logic          cyc_o,
  input logic          stb_o,
  input logic          we_o,
  input logic [DW-1:0] dat_o,
  input logic [NL-1:0] sel_o,
  input logic          ack_i,
  input logic          err_i,
  input logic          rty_i,
  // white-box, slave side
  input logic          commit,
  input logic [DW-1:0] ctrl_q,
  input logic [DW-1:0] ctrl_prev     // ctrl_q one cycle earlier
);
  default disable iff (rst_i);

  // P1 — DESIGN OBLIGATION, and the property this chapter exists for.
  //      An UNSELECTED lane of the committed register must be unchanged.
  //      Generated per lane so a failure names WHICH lane was destroyed,
  //      turning "the register is wrong" into a one-line diagnosis.
  generate
    for (genvar n = 0; n < NL; n++) begin : g_lane
      property p_unselected_lane_preserved;
        @(posedge clk_i)
          (ctrl_q[n*8 +: 8] != ctrl_prev[n*8 +: 8]) |-> $past(sel_o[n]);
      endproperty
      a_unselected_lane_preserved :
        assert property (p_unselected_lane_preserved)
        else $error("lane %0d of CONTROL changed while unselected", n);
    end
  endgenerate

  // P2 — SPECIFICATION (RULE 3.60, and §3.2.2 via RULE 3.75). The whole
  //      payload holds still while the write is outstanding. The end
  //      boundary is the termination: omitting it would forbid a legal
  //      back-to-back write on the next cycle, which is the over-strong
  //      trap Chapter 4.6 Section 10 described.
  property p_payload_stable;
    @(posedge clk_i) (cyc_o && stb_o && we_o && !(ack_i||err_i||rty_i))
      |=> ($stable(dat_o) && $stable(sel_o) && $stable(we_o));
  endproperty
  a_payload_stable : assert property (p_payload_stable)
    else $error("RULE 3.60 / 3.2.2: write payload moved while outstanding");

  // P3 — SPECIFICATION (RULE 3.60). A write presents a non-empty payload
  //      qualification. NOT a rule that SEL must be non-zero — an empty
  //      mask is legal and simply commits nothing — so this checks only
  //      that SEL is driven, never unknown, while qualified.
  property p_sel_driven;
    @(posedge clk_i) (cyc_o && stb_o) |-> !$isunknown(sel_o);
  endproperty
  a_sel_driven : assert property (p_sel_driven)
    else $error("SEL_O unknown while a transfer was presented");

  // P4 — LOCAL POLICY. State changes only at a commit event, checked
  //      against the slave's own declared term rather than against ACK_I
  //      (Chapter 7.1 Section 11 explains why that distinction matters).
  property p_state_only_on_commit;
    @(posedge clk_i) (ctrl_q != ctrl_prev) |-> $past(commit);
  endproperty
  a_state_only_on_commit : assert property (p_state_only_on_commit)
    else $error("LOCAL: register changed outside a commit event");
endmodule