Read Cycle Flow

// ─────────────────────────────────────────────────────────────────────────
// wb_read_master — the Module 6 running master.
//
// PURPOSE. Turn a local client read request into a Wishbone read and return
// the value. It is Chapter 5.6's wb_completion_master specialised for reads:
// the same client contract, the same acceptance boundary, the same
// level-sampled termination and the same one-pulse completion.
//
// WHAT IS NEW HERE is only that WE_O is driven low and that the captured
// value is the point of the exercise rather than a detail of it.
//
// CLIENT CONTRACT (LOCAL POLICY, not Wishbone — RULE 2.15 would require a
// datasheet to state it):
//   * 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; rdat_o is then valid and held.
//
// Reset: SYNCHRONOUS, ACTIVE HIGH (RULES 2.30, 3.00, 3.20).
// ─────────────────────────────────────────────────────────────────────────
module wb_read_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/8-1:0] req_sel_i,
  output logic            acc_o,
  output logic            busy_o,
  output logic            done_o,
  output logic [1:0]      status_o,        // 0=ok 1=error 2=retry
  output logic [DW-1:0]   rdat_o,

  // ── 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 [DW-1:0]   dat_i,
  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 ─────────────────────────────────────────────────────────────
  // active_q: a read is outstanding. adr_q / sel_q: the PRIVATE COPY that
  // makes RULE 3.60 satisfiable across an unbounded wait (Chapter 5.5).
  logic            active_q;
  logic [AW-1:0]   adr_q;
  logic [DW/8-1:0] sel_q;

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

  // ── BUS OUTPUTS ───────────────────────────────────────────────────────
  // 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 sel_o = sel_q;

  // WE_O held low for the whole transfer. RULE 3.60 qualifies it with
  // STB_O, so it must be stable while the transfer is presented — here it
  // is a constant, which satisfies that trivially and makes the read
  // direction impossible to corrupt mid-transfer.
  assign we_o = 1'b0;

  // DAT_O is a master OUTPUT even on a read, and RULE 3.60 qualifies it.
  // Driving zero is an EDUCATIONAL CHOICE, not a requirement: the
  // specification's SINGLE READ figure shows it undefined, and Chapter 4.6
  // showed a master legally leaving stale write data here. Zero makes
  // simulation traces easier to read and hides nothing, because a correct
  // slave ignores DAT_I entirely when WE_I is negated.
  assign dat_o = '0;

  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;
      sel_q    <= '0;
      done_o   <= 1'b0;
      status_o <= ST_OK;
      rdat_o   <= '0;
    end else begin
      done_o <= 1'b0;                      // done_o is a PULSE

      if (acc_o) begin
        // ── READ START ──────────────────────────────────────────────────
        // Metadata captured once. From the next edge the client may change
        // its inputs freely; the bus is driven from adr_q / sel_q.
        active_q <= 1'b1;
        adr_q    <= req_adr_i;
        sel_q    <= req_sel_i;
      end else if (active_q && terminated) begin
        // ── TERMINATION EDGE ────────────────────────────────────────────
        // Chapter 5.6's four obligations. The capture condition needs only
        // two terms here rather than three, because this master never
        // writes — there is no `!we_q` to check.
        //
        //   active_q : the transfer is still presented, so the selected
        //              slave is still driving the return path
        //   ack_i    : a SUCCESSFUL termination. RULE 3.65 ties the slave's
        //              DAT_O to its termination; on ERR or RTY there is no
        //              defined read value.
        if (ack_i) rdat_o <= dat_i;

        status_o <= ack_i ? ST_OK : (err_i ? ST_ERR : ST_RTY);
        active_q <= 1'b0;                  // release CYC_O and STB_O
        done_o   <= 1'b1;                  // report exactly once
      end
    end
  end
endmodule

// ─────────────────────────────────────────────────────────────────────────
// wb_read_regs — the running peripheral, read path only.
//
// PURPOSE. Turn a local word offset into a register value, and terminate.
// This is stage 4, 5 and part of 6 of Figure 1.
//
// TERMINATION STYLE. 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. Chapter 6.4
// builds the registered alternative and weighs them.
//
// Reset: SYNCHRONOUS, ACTIVE HIGH (RULES 2.30, 3.00).
// ─────────────────────────────────────────────────────────────────────────
module wb_read_regs #(
  parameter int unsigned OFF_AW = 3,       // 8 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,
  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 inputs: genuinely external, change on their own
  input  logic [DW-1:0]     input_data_i,
  input  logic [7:0]        flags_i
);
  // Word offsets. The byte offsets a datasheet would quote are 4x these.
  localparam logic [OFF_AW-1:0] O_STATUS = 3'd0;   // byte 0x00
  localparam logic [OFF_AW-1:0] O_COUNT  = 3'd1;   // byte 0x04
  localparam logic [OFF_AW-1:0] O_CTRL   = 3'd2;   // byte 0x08
  localparam logic [OFF_AW-1:0] O_INPUT  = 3'd3;   // byte 0x0C
  localparam logic [OFF_AW-1:0] O_ID     = 3'd4;   // byte 0x10

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

  logic [DW-1:0] ctrl_q;
  logic [DW-1:0] count_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;

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

  // A write to a read-only offset is refused. Module 6 is about reads, so
  // the write path exists only to keep CONTROL genuinely writable and to
  // keep the read/write distinction honest.
  logic illegal;
  assign illegal = ~known_off | (we_i & (adr_i != O_CTRL));

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

  // ── THE READ MULTIPLEXER ──────────────────────────────────────────────
  // RULE 3.65 requires a slave to qualify DAT_O() with its termination, so
  // ack_o appears in the condition. Driving '0 otherwise also keeps a
  // merged return path clean (Chapter 3.5) — Chapter 6.3 develops both.
  //
  // dat_o is assigned unconditionally first, so every path through this
  // block writes it. That is what prevents an inferred latch.
  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;    // sampled combinationally
        O_ID:     dat_o = ID_VALUE;
        default:  dat_o = '0;
      endcase
    end
  end

  // ── STATE ─────────────────────────────────────────────────────────────
  // count_q free-runs: it is a genuinely moving value, which makes it a
  // useful read target for detecting a master that captures at the wrong
  // edge (Chapter 6.3).
  always_ff @(posedge clk_i) begin
    if (rst_i) begin
      ctrl_q  <= '0;
      count_q <= '0;
    end else begin
      count_q <= count_q + 32'd1;
      // The only write path. Gated on ack_o, not merely on xfer — the
      // distinction is invisible here because this slave never waits, and
      // load-bearing the moment it does (Chapters 5.3 and 6.5).
      if (xfer && we_i && ack_o && (adr_i == O_CTRL)) begin
        for (int unsigned n = 0; n < DW/8; n++) begin
          if (sel_i[n]) ctrl_q[n*8 +: 8] <= dat_i[n*8 +: 8];
        end
      end
    end
  end
endmodule

// ─────────────────────────────────────────────────────────────────────────
// wb_read_flow_checker — the read-path invariants introduced here.
//
// P1 and P2 are SPECIFICATION. P3 is a DESIGN OBLIGATION derived from
// RULE 3.65 — the rule constrains the SLAVE's DAT_O, and what the master
// does with that window is the master's design (Chapter 5.8 Section 11).
// P4 is LOCAL POLICY for this master's client contract.
// ─────────────────────────────────────────────────────────────────────────
module wb_read_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 [DW-1:0] rdat_q,       // white-box: captured result
  input logic          busy_o,
  input logic          done_o
);
  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). WE_O is qualified by
  //      STB_O, so the DIRECTION of a presented transfer cannot change
  //      while it is outstanding. A read must stay a read.
  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 transfer was outstanding");

  // P3 — DESIGN OBLIGATION (from RULE 3.65). The captured result changes
  //      only at the edge of a SUCCESSFUL termination of a presented read.
  //      Catches both the off-by-one capture and an unconditional one.
  //      $past is required: rdat_q changes AT the edge, while the
  //      conditions authorising it were true BEFORE it.
  property p_capture_on_successful_read;
    @(posedge clk_i) $changed(rdat_q) |-> $past(cyc_o && stb_o && ack_i && !we_o);
  endproperty
  a_capture_on_successful_read :
    assert property (p_capture_on_successful_read)
    else $error("read data captured outside a successful read termination");

  // P4 — LOCAL POLICY. One completion per bus termination, and 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 read ===
  off  register       expected     captured   status  ADR_O  WE_O  done
    0  STATUS         0x000000a5   0x000000a5   OK       0x0     0     1
    1  COUNT          (moving)     0x00000006   OK       0x1     0     1
    2  CONTROL        0x00000000   0x00000000   OK       0x2     0     1
    3  INPUT_DATA     0xcafebabe   0xcafebabe   OK       0x3     0     1
    4  ID             0x57420601   0x57420601   OK       0x4     0     1
    7  (unmapped)     -            0x57420601   ERR      0x7     0     1
  completions: 6 requests -> 6 done pulses
  WE_O asserted at any point: 0