Transaction Initiation

// ─────────────────────────────────────────────────────────────────────────
// wb_single_master — the reference initiation design for Module 5.
//
// PURPOSE. Convert a local client request, which may be transient and may
// change at any time, into a Wishbone transfer that satisfies RULE 3.60
// for as many cycles as the slave needs.
//
// This is Chapter 5.1's wb_hs_master with the initiation boundary made
// explicit and defended: an accept handshake toward the client, a full
// metadata capture, and an explicit refusal of overlapping requests.
//
// CLIENT CONTRACT (this is LOCAL POLICY, not Wishbone — and per RULE 2.15
// it is the kind of thing a datasheet must state):
//   * req_i is a request; it is ACCEPTED only in a cycle where acc_o is
//     also asserted. The client must hold its metadata valid in that cycle
//     and is free to change it from the next cycle onward.
//   * Exactly one transaction is outstanding at a time.
//   * done_o pulses for one cycle per accepted transaction.
//
// Reset: SYNCHRONOUS, ACTIVE HIGH (RULES 2.30, 3.00, 3.20).
// ─────────────────────────────────────────────────────────────────────────
module wb_single_master #(
  parameter int unsigned AW = 30,
  parameter int unsigned DW = 32
) (
  input  logic            clk_i,
  input  logic            rst_i,

  // ── local client side (NOT Wishbone) ────────────────────────────────
  input  logic            req_i,
  input  logic            req_we_i,
  input  logic [AW-1:0]   req_adr_i,
  input  logic [DW-1:0]   req_dat_i,
  input  logic [DW/8-1:0] req_sel_i,
  output logic            acc_o,        // request accepted THIS cycle
  output logic            busy_o,
  output logic            done_o,       // one pulse per accepted request
  output logic            err_o,        // terminated with ERR or RTY
  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
);
  // ── STATE ─────────────────────────────────────────────────────────────
  // active_q says a transaction is outstanding. The four metadata
  // registers are the master's PRIVATE COPY of the request — the thing
  // that makes RULE 3.60 satisfiable across an unbounded wait.
  logic            active_q;
  logic            we_q;
  logic [AW-1:0]   adr_q;
  logic [DW-1:0]   dat_q;
  logic [DW/8-1:0] sel_q;

  // ── THE ACCEPTANCE BOUNDARY ───────────────────────────────────────────
  // acc_o is asserted only when a request is offered AND the master is
  // free. Exposing it lets the client know which cycle its metadata was
  // read in — the alternative, an implicit "we took it if busy_o rose",
  // forces the client to infer the boundary and is where ambiguity starts.
  assign acc_o  = req_i & ~active_q;
  assign busy_o = active_q;

  // ── BUS OUTPUTS: ENTIRELY FROM THE PRIVATE COPY ───────────────────────
  // Not one of these reads a req_* input. That is the whole defence: once
  // active_q is set, the client is disconnected from the bus.
  //
  // PERMISSION 3.40 lets both qualifiers share active_q, since this master
  // never negates STB_O mid-transfer.
  assign cyc_o = active_q;
  assign stb_o = active_q;
  assign we_o  = we_q;
  assign adr_o = adr_q;
  assign dat_o = dat_q;
  assign sel_o = sel_q;

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

  // ── SEQUENTIAL ────────────────────────────────────────────────────────
  always_ff @(posedge clk_i) begin
    if (rst_i) begin
      active_q <= 1'b0;                  // RULE 3.20
      we_q     <= 1'b0;
      adr_q    <= '0;
      dat_q    <= '0;
      sel_q    <= '0;
      done_o   <= 1'b0;
      err_o    <= 1'b0;
      rdat_o   <= '0;
    end else begin
      done_o <= 1'b0;                    // pulses
      err_o  <= 1'b0;

      if (acc_o) begin
        // ── CAPTURE ─────────────────────────────────────────────────────
        // Every signal RULE 3.60 qualifies with STB_O is copied here, in
        // one edge. Omitting any one of them would leave that signal
        // driven by a client input for the life of the transfer.
        active_q <= 1'b1;
        we_q     <= req_we_i;
        adr_q    <= req_adr_i;
        dat_q    <= req_dat_i;
        sel_q    <= req_sel_i;
      end else if (active_q && terminated) begin
        // ── COMPLETION ──────────────────────────────────────────────────
        // Chapter 5.6 takes this edge apart. Note the guard: acc_o cannot
        // be true here because acc_o requires ~active_q, so a new request
        // can never be captured in the same edge that completes the old
        // one. That ordering is what keeps exactly one transaction live.
        active_q <= 1'b0;
        done_o   <= 1'b1;
        err_o    <= err_i | rty_i;
        if (ack_i && !we_q) rdat_o <= dat_i;
      end
    end
  end
endmodule

// ─────────────────────────────────────────────────────────────────────────
// wb_unlatched_master — THE INITIATION BUG, isolated for simulation.
//
// NOT A REFERENCE DESIGN. Identical in structure to wb_single_master
// except that adr_o, we_o, dat_o and sel_o are driven DIRECTLY from the
// client inputs instead of from captured copies.
//
// Against a zero-wait-state slave this behaves identically to the correct
// master and passes every test. Against a slave that waits, the address on
// the bus follows the client and RULE 3.60 is violated from the second
// cycle of every transfer onward.
// ─────────────────────────────────────────────────────────────────────────
module wb_unlatched_master #(
  parameter int unsigned AW = 30,
  parameter int unsigned DW = 32
) (
  input  logic            clk_i,
  input  logic            rst_i,
  input  logic            req_i,
  input  logic            req_we_i,
  input  logic [AW-1:0]   req_adr_i,
  input  logic [DW-1:0]   req_dat_i,
  input  logic [DW/8-1:0] req_sel_i,
  output logic            acc_o,
  output logic            busy_o,
  output logic            done_o,
  output logic [DW-1:0]   rdat_o,

  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
);
  logic active_q;

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

  // ── THE BUG ───────────────────────────────────────────────────────────
  // Straight through from the client. There is no private copy, so the
  // bus reflects whatever the client is presenting RIGHT NOW — which,
  // after the first cycle, is usually the next request.
  assign we_o  = req_we_i;
  assign adr_o = req_adr_i;
  assign dat_o = req_dat_i;
  assign sel_o = req_sel_i;

  always_ff @(posedge clk_i) begin
    if (rst_i) begin
      active_q <= 1'b0;
      done_o   <= 1'b0;
      rdat_o   <= '0;
    end else begin
      done_o <= 1'b0;
      if (acc_o) begin
        active_q <= 1'b1;
      end else if (active_q && (ack_i || err_i || rty_i)) begin
        active_q <= 1'b0;
        done_o   <= 1'b1;
        if (ack_i) rdat_o <= dat_i;
      end
    end
  end
endmodule

// ─────────────────────────────────────────────────────────────────────────
// wb_init_checker — initiation properties.
//
// P1 is SPECIFICATION (RULE 3.60 read across a multi-cycle presentation)
// and is the one that catches the unlatched master. P2, P3 and P4 are
// LOCAL POLICY encoding this master's single-outstanding client contract —
// exactly the material RULE 2.15 requires a datasheet to state.
// ─────────────────────────────────────────────────────────────────────────
module wb_init_checker #(
  parameter int unsigned AW = 30,
  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 [AW-1:0]   adr_o,
  input logic [DW-1:0]   dat_o,
  input logic [DW/8-1:0] sel_o,
  input logic            ack_i,
  input logic            err_i,
  input logic            rty_i,
  input logic            acc_o,        // white-box: acceptance boundary
  input logic            busy_o
);
  default disable iff (rst_i);

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

  // P1 — SPECIFICATION (RULE 3.60). Everything the strobe qualifies holds
  //      still while the transfer is outstanding. This is THE property of
  //      this chapter: it fires on the first cycle the unlatched master's
  //      address moves, rather than when a downstream symptom appears.
  //
  //      The end boundary is the termination. Writing the antecedent
  //      without `!terminated` would forbid a master from presenting a
  //      DIFFERENT transfer the cycle after one completes, which is legal
  //      and normal — the over-strong-property trap from Chapter 4.6.
  property p_request_stable_until_terminated;
    @(posedge clk_i) (cyc_o && stb_o && !terminated)
      |=> ($stable(adr_o) && $stable(we_o) &&
           $stable(dat_o) && $stable(sel_o) && stb_o);
  endproperty
  a_request_stable_until_terminated :
    assert property (p_request_stable_until_terminated)
    else $error("RULE 3.60: a qualified signal moved while outstanding");

  // P2 — LOCAL POLICY. A request is never accepted while one is
  //      outstanding. Catches an overlapping accept that would silently
  //      overwrite the live transaction's metadata.
  property p_no_accept_while_busy;
    @(posedge clk_i) acc_o |-> !busy_o;
  endproperty
  a_no_accept_while_busy : assert property (p_no_accept_while_busy)
    else $error("LOCAL: request accepted while a transaction was outstanding");

  // P3 — LOCAL POLICY. The bus goes active only because a request was
  //      accepted. Catches a master that asserts its qualifiers from some
  //      other condition — a reset artefact, or a spurious state entry.
  property p_active_only_after_accept;
    @(posedge clk_i) ($rose(stb_o)) |-> $past(acc_o);
  endproperty
  a_active_only_after_accept : assert property (p_active_only_after_accept)
    else $error("LOCAL: STB_O asserted without a preceding acceptance");

  // P4 — LOCAL POLICY. Metadata is valid in the cycle the strobe first
  //      asserts, i.e. capture and presentation happen at the same edge.
  //      Catches a master that asserts the strobe a cycle before its
  //      registers are loaded, presenting the PREVIOUS transfer's address.
  property p_metadata_valid_at_first_strobe;
    @(posedge clk_i) $rose(stb_o) |-> !$isunknown({adr_o, we_o, sel_o});
  endproperty
  a_metadata_valid_at_first_strobe :
    assert property (p_metadata_valid_at_first_strobe)
    else $error("LOCAL: metadata not valid in the first strobe cycle");
endmodule

  Scenario 1 - client holds one cycle, then moves:
                                      good       bad
    cycles transfer presented          4          4
    ADR_O changes while presented      0          1
    cycles ADR_O != requested (0xa)    0          3
    ADR_O at termination edge        0xa        0xb

  Scenario 2 - client moves immediately on acceptance:
                                      good       bad
    cycles transfer presented          4          4
    ADR_O changes while presented      0          0
    cycles ADR_O != requested (0xa)    0          4
    ADR_O at termination edge        0xa        0xb