Write Cycle Flow

// ─────────────────────────────────────────────────────────────────────────
// wb_write_master — the Module 7 running master.
//
// PURPOSE. Turn a local client write request into a Wishbone write and
// report completion. It is Chapter 6.1's wb_read_master with the payload
// added: where the read master latched an address and byte selects, this
// one latches a data word as well, and drives WE_O high.
//
// THAT EXTRA REGISTER IS THE CHAPTER. On a read, a master that loses its
// payload gets a wrong answer. On a write, it CORRUPTS THE DEVICE — and
// Chapter 7.4 measures exactly that.
//
// CLIENT CONTRACT (LOCAL POLICY, not Wishbone — RULE 2.15 requires a
// datasheet to state this kind of thing):
//   * req_i is accepted only in a cycle where acc_o is also asserted;
//   * one transaction outstanding at a time;
//   * done_o pulses once per accepted request, with status_o valid.
//
// Reset: SYNCHRONOUS, ACTIVE HIGH (RULES 2.30, 3.00, 3.20).
// ─────────────────────────────────────────────────────────────────────────
module wb_write_master #(
  parameter int unsigned AW = 30,            // WORD address width
  parameter int unsigned DW = 32
) (
  input  logic            clk_i,
  input  logic            rst_i,

  // ── local client side (not Wishbone) ────────────────────────────────
  input  logic            req_i,
  input  logic [AW-1:0]   req_adr_i,         // WORD address
  input  logic [DW-1:0]   req_dat_i,         // value to write
  input  logic [DW/8-1:0] req_sel_i,         // which byte lanes
  output logic            acc_o,
  output logic            busy_o,
  output logic            done_o,
  output logic [1:0]      status_o,          // 0=ok 1=error 2=retry

  // ── Wishbone MASTER interface ───────────────────────────────────────
  output logic            cyc_o,
  output logic            stb_o,
  output logic            we_o,
  output logic [AW-1:0]   adr_o,
  output logic [DW-1:0]   dat_o,
  output logic [DW/8-1:0] sel_o,
  input  logic            ack_i,
  input  logic            err_i,
  input  logic            rty_i
);
  localparam logic [1:0] ST_OK = 2'd0, ST_ERR = 2'd1, ST_RTY = 2'd2;

  // ── STATE ─────────────────────────────────────────────────────────────
  // The PRIVATE COPY of the whole transaction. RULE 3.60 qualifies all four
  // of these with STB_O, and §3.2.2 requires them to stay valid until the
  // edge following STB_O's negation — neither is satisfiable across an
  // unbounded wait unless they come from registers.
  logic            active_q;
  logic [AW-1:0]   adr_q;
  logic [DW-1:0]   dat_q;
  logic [DW/8-1:0] sel_q;

  assign acc_o  = req_i & ~active_q;
  assign busy_o = active_q;

  // ── BUS OUTPUTS, ALL FROM THE PRIVATE COPY ────────────────────────────
  // PERMISSION 3.40 lets both qualifiers share one signal: this master
  // never negates STB_O mid-transfer.
  assign cyc_o = active_q;
  assign stb_o = active_q;
  assign adr_o = adr_q;
  assign dat_o = dat_q;
  assign sel_o = sel_q;

  // WE_O is a CONSTANT here, not a register. This master only writes, so
  // the direction cannot drift mid-transfer — which satisfies RULE 3.60's
  // stability obligation structurally rather than by promise. Chapter 6.1's
  // read master tied it low for the mirror-image reason.
  assign we_o = 1'b1;

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

  always_ff @(posedge clk_i) begin
    if (rst_i) begin
      active_q <= 1'b0;                      // RULE 3.20
      adr_q    <= '0;
      dat_q    <= '0;
      sel_q    <= '0;
      done_o   <= 1'b0;
      status_o <= ST_OK;
    end else begin
      done_o <= 1'b0;                        // done_o is a PULSE

      if (acc_o) begin
        // ── WRITE START ─────────────────────────────────────────────────
        // Address, DATA and byte enables captured together, once. From the
        // next edge the client may change all three freely.
        active_q <= 1'b1;
        adr_q    <= req_adr_i;
        dat_q    <= req_dat_i;
        sel_q    <= req_sel_i;
      end else if (active_q && terminated) begin
        // ── TERMINATION ─────────────────────────────────────────────────
        // A write has nothing to capture — that is the whole asymmetry
        // with Chapter 6.1, whose master captured dat_i here. All this
        // master does is record which termination arrived and release.
        status_o <= ack_i ? ST_OK : (err_i ? ST_ERR : ST_RTY);
        active_q <= 1'b0;
        done_o   <= 1'b1;
      end
    end
  end
endmodule

// ─────────────────────────────────────────────────────────────────────────
// wb_write_regs — the running peripheral, write path included.
//
// PURPOSE. Turn a qualified write into a committed register update, and
// terminate. This is stages 4, 5 and 6 of Figure 1.
//
// ── DECLARED COMMIT POLICY (LOCAL, not Wishbone) ──────────────────────
//   This slave commits the addressed register on the SAME rising clock
//   edge for which it is returning ACK_O for a qualified write.
//
//   Both effects are therefore driven by one combinational term, `commit`.
//   They cannot disagree, because there is nothing to disagree WITH — no
//   stored context, no second schedule. Chapter 7.3 builds a slave that
//   separates them and shows what that costs.
//
// TERMINATION TIMING. Combinational, which PERMISSION 3.30 explicitly
// allows ("i.e. there is a combinatorial logic path between [STB_I] and
// [ACK_O]") and OBSERVATION 3.40 credits with one transfer per clock.
//
// Reset: SYNCHRONOUS, ACTIVE HIGH (RULES 2.30, 3.00).
// ─────────────────────────────────────────────────────────────────────────
module wb_write_regs #(
  parameter int unsigned OFF_AW = 4,         // 16 word offsets
  parameter int unsigned DW     = 32
) (
  input  logic              clk_i,
  input  logic              rst_i,
  // Wishbone SLAVE interface
  input  logic              cyc_i,
  input  logic              stb_i,
  input  logic              we_i,
  input  logic [OFF_AW-1:0] adr_i,           // LOCAL word offset
  input  logic [DW-1:0]     dat_i,           // the value being written
  input  logic [DW/8-1:0]   sel_i,
  output logic [DW-1:0]     dat_o,
  output logic              ack_o,
  output logic              err_o,
  // device side
  input  logic [DW-1:0]     input_data_i,
  input  logic [7:0]        flags_i,
  output logic [DW-1:0]     control_o,       // observable committed state
  output logic [DW-1:0]     outdata_o
);
  localparam int unsigned NL = DW/8;

  localparam logic [OFF_AW-1:0] O_STATUS = 4'd0;   // byte 0x00  RO
  localparam logic [OFF_AW-1:0] O_COUNT  = 4'd1;   // byte 0x04  RO
  localparam logic [OFF_AW-1:0] O_CTRL   = 4'd2;   // byte 0x08  RW
  localparam logic [OFF_AW-1:0] O_INPUT  = 4'd3;   // byte 0x0C  RO
  localparam logic [OFF_AW-1:0] O_ID     = 4'd4;   // byte 0x10  RO
  localparam logic [OFF_AW-1:0] O_OUT    = 4'd6;   // byte 0x18  RW

  localparam logic [DW-1:0] ID_VALUE = 32'h5742_0701;  // "WB", module 7 rev 1

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

  // ── THE QUALIFIED TRANSFER ────────────────────────────────────────────
  // RULE 3.30 forbids responding to any slave signal while CYC_I is
  // negated; RULE 3.35 requires the termination to be generated from the
  // AND of CYC_I and STB_I.
  logic xfer;
  assign xfer = cyc_i & stb_i;

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

  // A write to a read-only offset is REFUSED rather than ignored. Silently
  // dropping it would tell the client the write succeeded — Chapter 4.11's
  // argument that an error is the honest answer and silence never is.
  logic illegal;
  assign illegal = ~known_off | (we_i & ~writable);

  // RULE 3.35 both; RULE 3.45 mutually exclusive by construction.
  assign err_o = xfer &  illegal;
  assign ack_o = xfer & ~illegal;

  // ── THE COMMIT EVENT ──────────────────────────────────────────────────
  // ONE named term, used for every state-changing path below. It contains
  // ack_o, so it is true for exactly one cycle per transfer — which is the
  // declared policy above, made structural.
  //
  // This slave never waits, so `commit` and `xfer & we_i` happen to
  // coincide. Writing ack_o in anyway is deliberate: the moment a wait
  // state appears the two diverge, and Chapter 7.4 measures a slave that
  // learned this the hard way.
  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;
      count_q   <= '0;
    end else begin
      count_q <= count_q + 32'd1;

      if (commit) begin
        // ── BYTE-LANE MASKED UPDATE ─────────────────────────────────────
        // Each lane is gated independently, so an unselected lane is not
        // written at all and keeps whatever it held. Chapter 7.2 takes
        // this apart; Chapter 4.7 established why SEL exists.
        unique case (adr_i)
          O_CTRL: begin
            for (int unsigned n = 0; n < NL; n++)
              if (sel_i[n]) ctrl_q[n*8 +: 8] <= dat_i[n*8 +: 8];
          end
          O_OUT: begin
            for (int unsigned n = 0; n < NL; n++)
              if (sel_i[n]) outdata_q[n*8 +: 8] <= dat_i[n*8 +: 8];
          end
          default: ;                        // unreachable: commit needs writable
        endcase
      end
    end
  end

  // ── READ PATH ─────────────────────────────────────────────────────────
  // Unchanged in shape from Chapter 6.3: RULE 3.65 qualifies a slave's
  // DAT_O with its termination, and driving '0 otherwise keeps a merged
  // return path clean. Present here so the same device still reads.
  always_comb begin
    dat_o = '0;
    if (xfer && !we_i && ack_o) begin
      unique case (adr_i)
        O_STATUS: dat_o = {24'd0, flags_i};
        O_COUNT:  dat_o = count_q;
        O_CTRL:   dat_o = ctrl_q;
        O_INPUT:  dat_o = input_data_i;
        O_ID:     dat_o = ID_VALUE;
        O_OUT:    dat_o = outdata_q;
        default:  dat_o = '0;
      endcase
    end
  end
endmodule

// ─────────────────────────────────────────────────────────────────────────
// wb_write_flow_checker — the write-path invariants introduced here.
//
// P1 and P2 are SPECIFICATION. P3 and P4 are LOCAL DESIGN POLICY: the
// specification says nothing about when a slave's flops load, so a commit
// property can only be checked against a slave's DECLARED policy.
// ─────────────────────────────────────────────────────────────────────────
module wb_write_flow_checker #(
  parameter int unsigned DW = 32
) (
  input logic          clk_i,
  input logic          rst_i,
  input logic          cyc_o,
  input logic          stb_o,
  input logic          we_o,
  input logic          ack_i,
  input logic          err_i,
  input logic          rty_i,
  input logic          busy_o,
  input logic          done_o,
  // white-box, slave side
  input logic          commit,
  input logic [DW-1:0] ctrl_q
);
  default disable iff (rst_i);

  // P1 — SPECIFICATION (RULE 3.25). A strobe never exists outside a cycle.
  property p_stb_implies_cyc;
    @(posedge clk_i) stb_o |-> cyc_o;
  endproperty
  a_stb_implies_cyc : assert property (p_stb_implies_cyc)
    else $error("RULE 3.25: STB_O asserted without CYC_O");

  // P2 — SPECIFICATION (RULE 3.60, as stability across a presentation).
  //      WE_O is qualified by STB_O, so a presented write stays a write.
  //      Holds trivially here because we_o is a constant — which is the
  //      point of making it one.
  property p_direction_stable;
    @(posedge clk_i) (cyc_o && stb_o && !(ack_i||err_i||rty_i)) |=> $stable(we_o);
  endproperty
  a_direction_stable : assert property (p_direction_stable)
    else $error("RULE 3.60: WE_O changed while the write was outstanding");

  // P3 — LOCAL POLICY (this slave's declared commit rule). Application
  //      state changes only at a commit event. Catches a register enable
  //      that is gated on something looser than `commit`.
  property p_state_only_on_commit;
    @(posedge clk_i) $changed(ctrl_q) |-> $past(commit);
  endproperty
  a_state_only_on_commit : assert property (p_state_only_on_commit)
    else $error("LOCAL: register changed outside a commit event");

  // P4 — LOCAL POLICY. One completion per bus termination, never without
  //      an outstanding transaction.
  property p_done_follows_termination;
    @(posedge clk_i) done_o
      |-> $past(busy_o && cyc_o && stb_o && (ack_i || err_i || rty_i));
  endproperty
  a_done_follows_termination : assert property (p_done_follows_termination)
    else $error("completion pulse without a matching bus termination");
endmodule

  === SIMULATION A - basic write ===
  word  register      wrote       CONTROL     OUTPUT    status  WE  SEL  done
     2  CONTROL     0x0000000f  0x0000000f  0x00000000   OK     1  1111   1
     6  OUTPUT_DATA 0xdeadbeef  0x0000000f  0xdeadbeef   OK     1  1111   1
     0  STATUS      0x11111111  0x0000000f  0xdeadbeef  ERR    1  1111   1
     4  ID          0x22222222  0x0000000f  0xdeadbeef  ERR    1  1111   1
     7  (unmapped)  0x33333333  0x0000000f  0xdeadbeef  ERR    1  1111   1
  completions: 5 requests -> 5 done pulses
  commit events: 2   (one per writable target)