Transaction Completion

// ─────────────────────────────────────────────────────────────────────────
// wb_completion_master — the termination edge, made explicit.
//
// PURPOSE. Chapter 5.5's wb_single_master handles completion correctly but
// compactly. This one separates the four obligations of Section 1 into
// named, individually reviewable steps, and distinguishes the three
// termination classes at the client interface instead of merging them.
//
// It is the Module 5 reference master. Everything Module 5 has established
// is present: latched metadata (5.5), level-sampled termination (5.4),
// PERMISSION 3.40 qualifiers (5.1), and a one-pulse local completion.
//
// Reset: SYNCHRONOUS, ACTIVE HIGH (RULES 2.30, 3.00, 3.20).
// ─────────────────────────────────────────────────────────────────────────
module wb_completion_master #(
  parameter int unsigned AW = 30,
  parameter int unsigned DW = 32
) (
  input  logic            clk_i,
  input  logic            rst_i,

  // ── local client side ───────────────────────────────────────────────
  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,       // ONE pulse per accepted request
  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;

  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;

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

  assign cyc_o = active_q;                     // PERMISSION 3.40
  assign stb_o = active_q;
  assign we_o  = we_q;                         // all from the private copy
  assign adr_o = adr_q;                        // (Chapter 5.5)
  assign dat_o = dat_q;
  assign sel_o = sel_q;

  // ── THE TERMINATION, DECODED ONCE ─────────────────────────────────────
  // RULE 3.45 makes these mutually exclusive at the slave, so at most one
  // is asserted. Decoding them in one place means the completion branch
  // cannot disagree with itself about which one arrived.
  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
      we_q     <= 1'b0;
      adr_q    <= '0;
      dat_q    <= '0;
      sel_q    <= '0;
      done_o   <= 1'b0;
      status_o <= ST_OK;
      rdat_o   <= '0;
    end else begin
      // ── OBLIGATION 4a: done_o defaults LOW every cycle ───────────────
      // This default is what makes done_o a PULSE structurally. A design
      // that sets done_o in the completion branch and clears it elsewhere
      // depends on the "elsewhere" being reachable; this one cannot fail
      // that way.
      done_o <= 1'b0;

      if (acc_o) begin
        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
        // ══ THE TERMINATION EDGE ═════════════════════════════════════════
        // All four obligations of Section 1, in one place.

        // ── 1. CAPTURE READ DATA ────────────────────────────────────────
        // Three conditions, each excluding a different wrong cycle:
        //   active_q : the slave is still driving the return path
        //   ack_i    : the termination SUCCEEDED (no defined value on
        //              ERR_I; nothing happened on RTY_I)
        //   !we_q    : this was a read
        // RULE 3.65 gives exactly one cycle in which dat_i is meaningful,
        // and this is it. Deferring by one cycle yields the previous
        // read's value on every read.
        if (ack_i && !we_q) rdat_o <= dat_i;

        // ── 2. RECORD WHICH TERMINATION ─────────────────────────────────
        // Kept DISTINCT rather than merged into a single error flag.
        // ERR and RTY oblige a client to do different things: an error
        // must not be retried, a retry should be (Chapters 4.11, 4.12).
        // Collapsing them here would discard the one bit of information
        // the third termination signal exists to carry.
        if      (ack_i) status_o <= ST_OK;
        else if (err_i) status_o <= ST_ERR;
        else            status_o <= ST_RTY;

        // ── 3. RELEASE THE BUS ──────────────────────────────────────────
        // Clearing active_q negates CYC_O and STB_O together, which is
        // correct for a single-transfer cycle (Chapter 5.2). The slave
        // then drops ACK_O in response, per RULE 3.50.
        active_q <= 1'b0;

        // ── 4. REPORT ONCE ──────────────────────────────────────────────
        // Guarded by active_q, so a termination the master did not
        // provoke cannot generate a completion.
        done_o <= 1'b1;
      end
    end
  end
endmodule

// ─────────────────────────────────────────────────────────────────────────
// wb_latecapture_master — THE OFF-BY-ONE, isolated for simulation.
//
// NOT A REFERENCE DESIGN. Identical to wb_completion_master except that
// the read-data capture is moved OUTSIDE the active_q guard, so it runs in
// the cycle AFTER the termination. By then the master has negated STB_O,
// the slave has stopped driving DAT_O per RULE 3.65, and the return path
// has reverted to zero.
//
// Everything on the bus remains fully conformant. Only the captured value
// is wrong, and it is wrong in the characteristic way: every read returns
// the PREVIOUS read's value.
// ─────────────────────────────────────────────────────────────────────────
module wb_latecapture_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, we_q, cap_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;
  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;

  always_ff @(posedge clk_i) begin
    if (rst_i) begin
      active_q <= 1'b0; we_q <= 1'b0; cap_q <= 1'b0;
      adr_q <= '0; dat_q <= '0; sel_q <= '0;
      done_o <= 1'b0; rdat_o <= '0;
    end else begin
      done_o <= 1'b0;
      cap_q  <= 1'b0;

      // ── THE BUG ─────────────────────────────────────────────────────
      // cap_q was set at the termination edge, so this runs ONE CYCLE
      // LATE. dat_i has already reverted — RULE 3.65 means the slave
      // stopped driving it when STB_O went away.
      if (cap_q) rdat_o <= dat_i;

      if (acc_o) begin
        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 && (ack_i || err_i || rty_i)) begin
        active_q <= 1'b0;
        done_o   <= 1'b1;
        if (ack_i && !we_q) cap_q <= 1'b1;      // defer the capture
      end
    end
  end
endmodule

// ─────────────────────────────────────────────────────────────────────────
// wb_completion_checker — termination-edge properties.
//
// P1 and P2 are DESIGN OBLIGATIONS derived from RULE 3.65: the
// specification says a slave qualifies DAT_O with its termination, from
// which it follows that a master must capture there — but the
// specification does not dictate master capture timing, so these are
// house policy built on a specification fact. P3 and P4 are LOCAL POLICY
// encoding the client contract.
// ─────────────────────────────────────────────────────────────────────────
module wb_completion_checker #(
  parameter int unsigned DW = 32
) (
  input logic          clk_i,
  input logic          rst_i,
  input logic          cyc_o,
  input logic          stb_o,
  input logic          ack_i,
  input logic          err_i,
  input logic          rty_i,
  input logic          we_o,
  input logic [DW-1:0] rdat_q,        // white-box: captured read data
  input logic          acc_o,         // white-box: acceptance
  input logic          busy_o,
  input logic          done_o
);
  default disable iff (rst_i);

  // P1 — DESIGN OBLIGATION (from RULE 3.65). The captured read register
  //      changes only at the edge of a successful READ termination.
  //      Catches BOTH the off-by-one and an unconditional capture.
  //
  //      $past is required because rdat_q changes AT the edge while the
  //      conditions authorising it were true BEFORE it — the shift
  //      Chapter 4.5 Section 10 warned about getting backwards.
  property p_capture_at_termination_only;
    @(posedge clk_i) $changed(rdat_q)
      |-> $past(cyc_o && stb_o && ack_i && !we_o);
  endproperty
  a_capture_at_termination_only :
    assert property (p_capture_at_termination_only)
    else $error("read data captured outside a successful read termination");

  // P2 — DESIGN OBLIGATION. A failed termination captures nothing. There
  //      is no defined read value on ERR_I and nothing happened on RTY_I.
  property p_no_capture_on_failure;
    @(posedge clk_i) (cyc_o && stb_o && (err_i || rty_i)) |=> $stable(rdat_q);
  endproperty
  a_no_capture_on_failure : assert property (p_no_capture_on_failure)
    else $error("read data captured from a failed termination");

  // P3 — LOCAL POLICY. done_o is a ONE-CYCLE PULSE and follows a real
  //      termination of an outstanding transfer. Catches a level-style
  //      done_o and a completion generated from the wrong condition.
  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");

  // P4 — LOCAL POLICY. Exactly one completion per acceptance, enforced as
  //      an alternation: an acceptance is always followed by a completion
  //      before the next acceptance. Catches both duplicated and dropped
  //      completions, which P3 alone would not.
  property p_one_done_per_accept;
    @(posedge clk_i) acc_o |=> (!acc_o throughout (done_o[->1]));
  endproperty
  a_one_done_per_accept : assert property (p_one_done_per_accept)
    else $error("a second acceptance occurred before the completion");
endmodule

  read   slave holds    correct     late
    1      0x11          0x11        0x0
    2      0x22          0x22        0x0
    3      0x33          0x33        0x0
  late-capture master final value: 0x0