Retry Concepts

  attempt 0     the ORIGINAL transfer          (not a retry)
  attempt 1     the first RE-ISSUED transfer   (retry 1)
  attempt N     the Nth re-issued transfer     (retry N)

// wb_retry_master — a master that re-issues a deferred request, bounded.
//
// THE CLIENT CONTRACT, extending Chapter 10.1's:
//
//   done_o    one clock per accepted client request. Means THE CLIENT
//             REQUEST IS FINISHED — not that any one bus attempt ended.
//             A request that took four attempts produces one done_o.
//
//   ok_o      valid with done_o. The request succeeded (an attempt was
//             terminated with ACK_I).
//   err_o     valid with done_o. The request failed (ERR_I).
//   exh_o     valid with done_o. The retry policy ran out: every allowed
//             attempt was terminated with RTY_I.
//
//   rdat_o    valid ONLY with done_o && ok_o on a read.
//
// EXACTLY ONE of ok_o / err_o / exh_o accompanies each done_o.
//
// NOTE WHAT exh_o IS NOT. It is not a Wishbone termination class. No slave
// ever asserted it; it is this master reporting that ITS OWN policy is
// spent. Chapter 11.5 separates it from ERR in debugging.
//
// ── MAX_RETRIES SEMANTICS ────────────────────────────────────────────────
// Stated once and measured in Chapter 11.2 Section 6 rather than assumed:
//
//   attempt 0        the original transfer
//   attempt 1        the first RE-issued transfer  (retry 1)
//   attempt N        the Nth re-issued transfer    (retry N)
//
//   MAX_RETRIES = N  ->  at most N RE-ISSUES are permitted, so the
//                        maximum number of bus attempts is N + 1.
//
//   MAX_RETRIES = 0  ->  no re-issues. One attempt. An RTY on it is
//                        reported immediately as exhaustion. This is a
//                        legal, useful configuration — it is "classify
//                        but do not retry" — and Section 6 measures it.
//   MAX_RETRIES = 1  ->  2 attempts maximum.
//   MAX_RETRIES = 3  ->  4 attempts maximum.
//
// retry_q counts RE-ISSUES, so it runs 0..MAX_RETRIES and the exhaustion
// test is `retry_q == MAX_RETRIES` on an RTY. There is no PARAM-1
// expression anywhere: Module 9 measured an unsigned `0 - 1` turning an
// off-by-one into a permanent hang, and this module does not repeat it.
//
// ── RETRY_DELAY SEMANTICS ────────────────────────────────────────────────
// Measured in Chapter 11.4 Section 6, and stated here as measured rather
// than as intended:
//
//   non-presented clocks between two attempts  =  RETRY_DELAY + 1
//
//   RETRY_DELAY = 0  ->  1 non-presented clock
//   RETRY_DELAY = 1  ->  2 non-presented clocks
//   RETRY_DELAY = N  ->  N + 1 non-presented clocks
//
// THE +1 IS NOT AN IMPLEMENTATION ARTEFACT AND CANNOT BE REMOVED. It is
// what makes the second attempt a SEPARATE TRANSFER.
//
// If STB_O never negated between the two presentations, the slave would
// see one continuously-presented transfer rather than two. RULE 3.50
// requires the slave to negate its termination in response to the
// negation of STB_I; with no negation there is no second qualification and
// no second termination — just one request being held while the slave goes
// on asserting RTY_O. That is the "retry as a wait state" mistake, in
// hardware.
//
// So one non-presented clock is the irreducible cost of a retry, exactly
// as one turnaround clock is the irreducible cost of a second bus cycle in
// Chapter 8.6. RETRY_DELAY adds to that floor; it cannot go below it.
//
// Wishbone imposes no retry delay at all. Both parameters are LOCAL POLICY.
//
// ── REQUEST IDENTITY ─────────────────────────────────────────────────────
// Every attempt presents the metadata latched when the CLIENT REQUEST was
// accepted. The client's live inputs are never re-read. This is the
// invariant Chapter 11.2 Section 5 measures against a master that gets it
// wrong, and it is what makes "retry" mean "the same operation again".
// ─────────────────────────────────────────────────────────────────────────
module wb_retry_master #(
  parameter int unsigned AW          = 30,
  parameter int unsigned DW          = 32,
  parameter int unsigned MAX_RETRIES = 2,
  parameter int unsigned RETRY_DELAY = 0
) (
  input  logic            clk_i,
  input  logic            rst_i,

  // ── 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            busy_o,
  output logic            done_o,
  output logic            ok_o,
  output logic            err_o,
  output logic            exh_o,
  output logic [DW-1:0]   rdat_o,

  // ── Wishbone side ──
  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,

  // ── observation only ──
  output logic [7:0]      attempt_o,      // 0 = original, 1.. = retries
  output logic [7:0]      retry_o,        // re-issues so far
  output logic            waiting_o       // in the retry gap
);
  typedef enum logic [1:0] { S_IDLE, S_XFER, S_GAP } state_e;
  state_e state_q;

  // ── THE LATCHED REQUEST. Written once, at client acceptance, and read
  //    by every attempt. Nothing else writes these.
  logic [AW-1:0]   adr_q;
  logic [DW-1:0]   dat_q;
  logic [DW/8-1:0] sel_q;
  logic            we_q;

  logic [7:0]  retry_q;
  logic [15:0] gap_q;
  logic        terminated;

  assign cyc_o = (state_q == S_XFER);
  assign stb_o = (state_q == S_XFER);
  assign adr_o = adr_q;
  assign dat_o = dat_q;
  assign sel_o = sel_q;
  assign we_o  = we_q;

  assign busy_o    = (state_q != S_IDLE);
  assign attempt_o = retry_q;
  assign retry_o   = retry_q;
  assign waiting_o = (state_q == S_GAP);

  assign terminated = cyc_o && stb_o && (ack_i || err_i || rty_i);

  always_ff @(posedge clk_i) begin
    if (rst_i) begin
      state_q <= S_IDLE;
      adr_q <= '0; dat_q <= '0; sel_q <= '0; we_q <= 1'b0;
      retry_q <= '0; gap_q <= '0;
      done_o <= 1'b0; ok_o <= 1'b0; err_o <= 1'b0; exh_o <= 1'b0;
      rdat_o <= '0;
    end else begin
      done_o <= 1'b0; ok_o <= 1'b0; err_o <= 1'b0; exh_o <= 1'b0;

      case (state_q)
        S_IDLE: if (req_i) begin
          // ── ACCEPTANCE. The only clock at which client inputs are read.
          adr_q   <= req_adr_i;
          dat_q   <= req_dat_i;
          sel_q   <= req_sel_i;
          we_q    <= req_we_i;
          retry_q <= '0;
          state_q <= S_XFER;
        end

        S_XFER: if (terminated) begin
          if (ack_i) begin
            if (!we_q) rdat_o <= dat_i;    // capture on ACK only
            ok_o    <= 1'b1;
            done_o  <= 1'b1;
            state_q <= S_IDLE;
          end else if (err_i) begin
            // An error is final for this master: retrying an ERR either
            // loops forever or converts a clean failure into a hang.
            err_o   <= 1'b1;
            done_o  <= 1'b1;
            state_q <= S_IDLE;
          end else begin
            // RTY. Either the policy has another re-issue left, or it does not.
            if (retry_q == 8'(MAX_RETRIES)) begin
              exh_o   <= 1'b1;
              done_o  <= 1'b1;
              state_q <= S_IDLE;
            end else begin
              retry_q <= retry_q + 8'd1;
              gap_q   <= 16'(RETRY_DELAY);
              state_q <= S_GAP;
            end
          end
        end

        // Nothing is presented here. The latched request is untouched, so
        // the next attempt carries the same identity as the first.
        S_GAP: begin
          if (gap_q == 16'd0) state_q <= S_XFER;
          else                gap_q   <= gap_q - 16'd1;
        end

        default: state_q <= S_IDLE;
      endcase
    end
  end
endmodule

// wb_retry_master_live — THE BUG, isolated. NOT A REFERENCE DESIGN.
//
// Identical to wb_retry_master except that the Wishbone outputs are driven
// from the CLIENT'S LIVE INPUTS instead of from the registers latched at
// acceptance:
//
//     assign adr_o = adr_q;        becomes      assign adr_o = req_adr_i;
//
// The retry counting, the delay, the classification and the completion
// reporting are all unchanged and all correct. The only defect is that the
// master does not remember what it accepted.
//
// WHY IT IS NOT AN OBVIOUS MISTAKE. Against a slave that never defers, this
// master is indistinguishable from the correct one: the transfer is
// presented and terminated before the client has any opportunity to change
// anything. Chapter 9.3 measured the same structural precondition for a
// single transfer under wait states — here the window is wider still,
// because it spans the gap BETWEEN attempts as well.
//
// WHAT IS STILL CORRECT. Everything on the bus, within each attempt. Each
// presentation is properly qualified, each termination is taken, the bus is
// released between attempts. A protocol checker watching its pins passes it.
//
// It also violates RULE 3.60 within an attempt if the client moves while
// the transfer is outstanding — but against a zero-wait slave that window
// is empty, and the damage measured in Chapter 11.2 happens entirely in the
// gap between attempts, where no Wishbone rule applies at all.
// ─────────────────────────────────────────────────────────────────────────
module wb_retry_master_live #(
  parameter int unsigned AW          = 30,
  parameter int unsigned DW          = 32,
  parameter int unsigned MAX_RETRIES = 2,
  parameter int unsigned RETRY_DELAY = 0
) (
  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            busy_o,
  output logic            done_o,
  output logic            ok_o,
  output logic            err_o,
  output logic            exh_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,
  output logic [7:0]      attempt_o,
  output logic [7:0]      retry_o,
  output logic            waiting_o
);
  typedef enum logic [1:0] { S_IDLE, S_XFER, S_GAP } state_e;
  state_e state_q;

  logic [7:0]  retry_q;
  logic [15:0] gap_q;
  logic        terminated;

  assign cyc_o = (state_q == S_XFER);
  assign stb_o = (state_q == S_XFER);

  // ── THE BUG. Four wires from the client straight to the bus. There is
  //    nothing to latch because nothing is remembered.
  assign adr_o = req_adr_i;
  assign dat_o = req_dat_i;
  assign sel_o = req_sel_i;
  assign we_o  = req_we_i;

  assign busy_o    = (state_q != S_IDLE);
  assign attempt_o = retry_q;
  assign retry_o   = retry_q;
  assign waiting_o = (state_q == S_GAP);

  assign terminated = cyc_o && stb_o && (ack_i || err_i || rty_i);

  always_ff @(posedge clk_i) begin
    if (rst_i) begin
      state_q <= S_IDLE; retry_q <= '0; gap_q <= '0;
      done_o <= 1'b0; ok_o <= 1'b0; err_o <= 1'b0; exh_o <= 1'b0; rdat_o <= '0;
    end else begin
      done_o <= 1'b0; ok_o <= 1'b0; err_o <= 1'b0; exh_o <= 1'b0;
      case (state_q)
        S_IDLE: if (req_i) begin
          retry_q <= '0;
          state_q <= S_XFER;      // nothing latched
        end
        S_XFER: if (terminated) begin
          if (ack_i) begin
            if (!req_we_i) rdat_o <= dat_i;
            ok_o <= 1'b1; done_o <= 1'b1; state_q <= S_IDLE;
          end else if (err_i) begin
            err_o <= 1'b1; done_o <= 1'b1; state_q <= S_IDLE;
          end else begin
            if (retry_q == 8'(MAX_RETRIES)) begin
              exh_o <= 1'b1; done_o <= 1'b1; state_q <= S_IDLE;
            end else begin
              retry_q <= retry_q + 8'd1;
              gap_q   <= 16'(RETRY_DELAY);
              state_q <= S_GAP;
            end
          end
        end
        S_GAP: begin
          if (gap_q == 16'd0) state_q <= S_XFER;
          else                gap_q   <= gap_q - 16'd1;
        end
        default: state_q <= S_IDLE;
      endcase
    end
  end
endmodule

  === SIM C - a retry that eventually succeeds ===
    slave defers 2 attempts then accepts; MAX_RETRIES = 3

    bus attempts presented      3
    RTY terminations            2
    ACK terminations            1
    master retry count          2
    client completions          1  (ok=1 err=0 exhausted=0)
    slave accepts               1

  === SIM D - retry exhaustion, swept ===
    slave never accepts. attempts = MAX_RETRIES + 1.

    MAX_RETRIES   attempts   RTY   retries   ok  err  exhausted
         0            1        1      0       0    0      1
         1            2        2      1       0    0      1
         3            4        4      3       0    0      1

  === SIM E - the client changes its request between attempts ===
    client asks to write 0xAAAA0001 to word 9, then switches its
    inputs to word 4 / 0xBBBB0002 while attempt 0 is being retried.

    master                  attempts  accepted offset  accepted data
    wb_retry_master             2           9            0xaaaa0001
    wb_retry_master_live        2           4            0xbbbb0002

// Properties for a retrying master. The split is stark here: exactly one
// is the specification's, because Wishbone says nothing about retry at all.
//
// NOTE ON EXECUTION: Icarus Verilog does not support SVA. These were
// reviewed by inspection and are NOT claimed to have been executed. The
// numbers in Sections 6 and 7 come from procedural checks, which Icarus
// does run.
// ─────────────────────────────────────────────────────────────────────────
module wb_retry_master_props #(
  parameter int unsigned AW          = 30,
  parameter int unsigned DW          = 32,
  parameter int unsigned MAX_RETRIES = 2
) (
  input logic            clk_i, rst_i,
  input logic            cyc_o, stb_o, 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, err_i, rty_i,
  input logic            req_i, busy_o,
  input logic            done_o, ok_o, err_rep_o, exh_o,
  input logic [7:0]      retry_o
);
  default clocking cb @(posedge clk_i); endclocking
  default disable iff (rst_i);

  logic terminated, accepted;
  assign terminated = cyc_o && stb_o && (ack_i || err_i || rty_i);
  assign accepted   = req_i && !busy_o;

  // M1 — SPECIFICATION (RULE 3.60). Within a presented attempt the
  //      qualified outputs are stable. This is the only property here the
  //      specification requires, and it says nothing about the gaps.
  M1_stable_in_attempt: assert property (
    (cyc_o && stb_o && !(ack_i||err_i||rty_i)) |=>
      ($stable(adr_o) && $stable(we_o) && $stable(sel_o))
  );

  // M2 — LOCAL POLICY, and the invariant this chapter is built on. The
  //      request presented by every attempt is the one latched at
  //      acceptance. Written as: the metadata does not change between
  //      acceptance and completion, INCLUDING across the gaps — which is
  //      strictly stronger than M1 and is not a Wishbone obligation.
  M2_identity_across_retries: assert property (
    (busy_o && !done_o) |=> ($stable(adr_o) && $stable(we_o) && $stable(sel_o))
  );

  // M3 — LOCAL POLICY. RTY ends the attempt: the master releases rather
  //      than holding the request. Without this, retry degenerates into a
  //      wait state and no progress is possible.
  M3_rty_releases: assert property (
    (cyc_o && stb_o && rty_i) |=> !stb_o
  );

  // M4 — LOCAL POLICY. The retry count never exceeds the configured
  //      maximum, so the bounded design cannot livelock.
  M4_bounded: assert property ( retry_o <= 8'(MAX_RETRIES) );

  // M5 — LOCAL POLICY. Exhaustion is reported only at the configured
  //      limit, so MAX_RETRIES means what Section 3 says it means.
  M5_exact_exhaustion: assert property (
    exh_o |-> $past(retry_o == 8'(MAX_RETRIES) && rty_i)
  );

  // M6 — LOCAL CONTRACT. One accepted client request produces exactly one
  //      completion, however many bus attempts occurred, and that
  //      completion carries exactly one outcome.
  M6_one_completion: assert property ( done_o |-> $onehot({ok_o, err_rep_o, exh_o}) );

  // M7 — LOCAL CONTRACT. Success is never reported for a deferral.
  M7_no_success_on_rty: assert property ( ok_o |-> $past(ack_i) );
endmodule