RTY_I

// ─────────────────────────────────────────────────────────────────────────
// wb_rty_slave — a mailbox FIFO that RETRIES rather than waits when full.
//
// WHY RETRY AND NOT A WAIT STATE (Section 1): this FIFO's readiness depends
// on ANOTHER master draining it. Holding the bus while waiting for space
// would prevent the drain and deadlock the system. Terminating with RTY_O
// releases the bus so the drain can happen.
//
// A single-master version of this same FIFO could safely use wait states.
// The RTL would be correct in one system and deadlock the other, which is
// why the choice belongs in the datasheet (RULE 2.15).
//
// Reset: SYNCHRONOUS, ACTIVE HIGH (RULES 2.30, 3.00).
// ─────────────────────────────────────────────────────────────────────────
module wb_rty_slave #(
  parameter int unsigned OFF_AW = 2,
  parameter int unsigned DW     = 32,
  parameter int unsigned DEPTH  = 4
) (
  input  logic                  clk_i,
  input  logic                  rst_i,
  input  logic                  cyc_i,
  input  logic                  stb_i,
  input  logic                  we_i,
  input  logic [OFF_AW-1:0]     adr_i,
  input  logic [DW-1:0]         dat_i,
  output logic [DW-1:0]         dat_o,
  output logic                  ack_o,
  output logic                  err_o,
  output logic                  rty_o,
  output logic [3:0]            level_o
);
  localparam logic [OFF_AW-1:0] W_DATA  = 'd0;    // push (W) / pop (R)
  localparam logic [OFF_AW-1:0] W_LEVEL = 'd1;    // read-only occupancy

  logic [DW-1:0] mem_q [DEPTH];
  logic [3:0]    lvl_q;
  assign level_o = lvl_q;

  logic xfer;
  assign xfer = cyc_i & stb_i;                    // RULES 3.30 & 3.35

  logic full, empty;
  assign full  = (lvl_q == 4'(DEPTH));
  assign empty = (lvl_q == 4'd0);

  // ── TERMINATION SELECTION ──────────────────────────────────────────────
  // Three conditions, three different answers, and the distinction between
  // the last two is the chapter:
  //
  //   e_perm : this can NEVER work        -> ERR_O  (permanent)
  //   r_now  : this cannot work RIGHT NOW -> RTY_O  (transient)
  //   else                                -> ACK_O
  //
  // A full FIFO is not an error. The same write will succeed once a drain
  // happens, so reporting ERR_O would turn a transient condition into a
  // permanent failure and the master would correctly never try again.
  logic e_perm, r_now;

  always_comb begin
    unique case (adr_i)
      W_DATA:  e_perm = 1'b0;
      W_LEVEL: e_perm = we_i;                     // level is read-only
      default: e_perm = 1'b1;                     // unmapped offset
    endcase
  end

  always_comb begin
    r_now = 1'b0;
    if (!e_perm && (adr_i == W_DATA)) begin
      r_now = we_i ? full : empty;                // full: no space to push
    end                                           // empty: nothing to pop
  end

  // RULE 3.45: mutually exclusive by construction. Exactly one is asserted
  // for any qualified transfer, and none otherwise.
  assign err_o = xfer &  e_perm;
  assign rty_o = xfer & ~e_perm &  r_now;
  assign ack_o = xfer & ~e_perm & ~r_now;

  // ── A RETRIED TRANSFER CHANGES NOTHING ─────────────────────────────────
  // The same obligation an errored transfer carries (Chapter 4.11 Sec. 2),
  // and for a sharper reason: the master WILL come back. A retry that
  // half-completed would apply its effect once per attempt.
  logic push, pop;
  assign push = ack_o &  we_i & (adr_i == W_DATA);
  assign pop  = ack_o & ~we_i & (adr_i == W_DATA);

  always_ff @(posedge clk_i) begin
    if (rst_i) begin
      lvl_q <= 4'd0;
      for (int unsigned i = 0; i < DEPTH; i++) mem_q[i] <= '0;
    end else begin
      if (push) begin
        mem_q[lvl_q[1:0]] <= dat_i;
        lvl_q             <= lvl_q + 4'd1;
      end else if (pop) begin
        for (int unsigned i = 0; i < DEPTH-1; i++) mem_q[i] <= mem_q[i+1];
        lvl_q <= lvl_q - 4'd1;
      end
    end
  end

  always_comb begin
    dat_o = '0;                                   // RULE 3.65
    if (xfer && !we_i && ack_o) begin
      dat_o = (adr_i == W_LEVEL) ? {{(DW-4){1'b0}}, lvl_q} : mem_q[0];
    end
  end
endmodule

// ─────────────────────────────────────────────────────────────────────────
// wb_rty_master — bounded retry with backoff.
//
// POLICY (the material RULE 2.15 requires in a datasheet):
//   * RTY_I releases the bus completely — CYC_O is negated, not just STB_O.
//   * The transfer is re-presented after a backoff delay.
//   * Backoff grows with each attempt, and is seeded from MASTER_ID so two
//     masters do not retry in lock-step.
//   * After MAX_TRIES attempts the transfer is abandoned and reported as a
//     failure, so a never-clearing condition cannot livelock the system.
//   * ERR_I is NOT retried (Chapter 4.11).
// ─────────────────────────────────────────────────────────────────────────
module wb_rty_master #(
  parameter int unsigned AW        = 30,
  parameter int unsigned DW        = 32,
  parameter int unsigned MAX_TRIES = 8,
  parameter int unsigned MASTER_ID = 0
) (
  input  logic          clk_i,
  input  logic          rst_i,

  input  logic          go_i,
  input  logic          we_i,
  input  logic [AW-1:0] adr_i,
  input  logic [DW-1:0] wdat_i,
  output logic          done_o,
  output logic          ok_o,
  output logic          gave_up_o,
  output logic [3:0]    tries_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,
  input  logic [DW-1:0] dat_i,
  input  logic          ack_i,
  input  logic          err_i,
  input  logic          rty_i
);
  typedef enum logic [1:0] { T_IDLE, T_XFER, T_BACKOFF } tstate_e;
  tstate_e state_q;

  logic [AW-1:0] adr_q;
  logic [DW-1:0] wdat_q;
  logic          we_q;
  logic [7:0]    wait_q;

  // ── THE BUS IS GENUINELY RELEASED IN T_BACKOFF ─────────────────────────
  // cyc_o is low there, not merely stb_o. Holding CYC_O across a backoff
  // would keep the arbiter's grant and recreate the deadlock the retry
  // exists to break — while looking like correct retry handling.
  assign cyc_o = (state_q == T_XFER);
  assign stb_o = (state_q == T_XFER);
  assign we_o  = we_q;
  assign adr_o = adr_q;
  assign dat_o = wdat_q;

  // Backoff grows with the attempt count. MASTER_ID offsets it so two
  // masters retrying the same resource do not collide every time — the
  // lock-step hazard of Section 3, which only appears with more than one.
  function automatic logic [7:0] backoff_of(input logic [3:0] n);
    backoff_of = 8'((32'(n) << 2) + 32'(MASTER_ID) + 1);
  endfunction

  always_ff @(posedge clk_i) begin
    if (rst_i) begin
      state_q   <= T_IDLE;                        // RULE 3.20 via cyc/stb
      adr_q     <= '0;
      wdat_q    <= '0;
      we_q      <= 1'b0;
      wait_q    <= '0;
      tries_o   <= '0;
      rdat_o    <= '0;
      done_o    <= 1'b0;
      ok_o      <= 1'b0;
      gave_up_o <= 1'b0;
    end else begin
      done_o <= 1'b0;

      unique case (state_q)
        T_IDLE: begin
          if (go_i) begin
            state_q   <= T_XFER;
            adr_q     <= adr_i;
            wdat_q    <= wdat_i;
            we_q      <= we_i;
            tries_o   <= 4'd1;
            gave_up_o <= 1'b0;
          end
        end

        T_XFER: begin
          if (ack_i) begin
            if (!we_q) rdat_o <= dat_i;           // Chapter 4.5's capture
            state_q <= T_IDLE;
            done_o  <= 1'b1;
            ok_o    <= 1'b1;
          end else if (err_i) begin
            // Permanent. Retrying would loop forever (Chapter 4.11).
            state_q <= T_IDLE;
            done_o  <= 1'b1;
            ok_o    <= 1'b0;
          end else if (rty_i) begin
            if (tries_o >= 4'(MAX_TRIES)) begin
              // ── THE BOUND ────────────────────────────────────────────
              // Escalate rather than retry forever. A condition that has
              // not cleared in MAX_TRIES attempts is reported upward,
              // where a caller can decide. Without this, a never-clearing
              // condition livelocks the bus while looking healthy.
              state_q   <= T_IDLE;
              done_o    <= 1'b1;
              ok_o      <= 1'b0;
              gave_up_o <= 1'b1;
            end else begin
              state_q <= T_BACKOFF;               // release the bus
              wait_q  <= backoff_of(tries_o);
              tries_o <= tries_o + 4'd1;
            end
          end
        end

        T_BACKOFF: begin
          if (wait_q == 8'd0) state_q <= T_XFER;  // re-present unchanged
          else                wait_q  <= wait_q - 8'd1;
        end

        default: state_q <= T_IDLE;
      endcase
    end
  end
endmodule

// ─────────────────────────────────────────────────────────────────────────
// wb_rty_checker — retry properties.
//
// P1 is SPECIFICATION (RULES 3.35, 3.45). P2, P3 and P4 are DESIGN
// OBLIGATIONS — the specification says when and how a cycle is retried is
// supplier-defined, so these encode THIS system's documented policy, which
// is the material RULE 2.15 requires in the datasheet.
// ─────────────────────────────────────────────────────────────────────────
module wb_rty_checker #(
  parameter int unsigned MAX_TRIES = 8
) (
  input logic       clk_i,
  input logic       rst_i,
  input logic       cyc_i,
  input logic       stb_i,
  input logic       ack_o,
  input logic       err_o,
  input logic       rty_o,
  input logic [3:0] lvl_q,
  input logic [3:0] tries_q
);
  default disable iff (rst_i);

  // P1 — SPECIFICATION. RULE 3.35: generated from the qualified transfer.
  //      RULE 3.45: exclusive with the other two.
  property p_rty_legal;
    @(posedge clk_i) rty_o |-> ((cyc_i && stb_i) && !ack_o && !err_o);
  endproperty
  a_rty_legal : assert property (p_rty_legal)
    else $error("RTY_O unqualified or asserted with another termination");

  // P2 — DESIGN OBLIGATION, and the one this chapter exists for. A retry
  //      must RELEASE THE BUS: cyc_i is negated the cycle after RTY_O.
  //      A master that keeps the tenure recreates the deadlock the retry
  //      was meant to break, while its strobe waveform looks correct.
  property p_rty_releases_bus;
    @(posedge clk_i) (cyc_i && stb_i && rty_o) |=> !cyc_i;
  endproperty
  a_rty_releases_bus : assert property (p_rty_releases_bus)
    else $error("CYC_I still asserted the cycle after RTY_O");

  // P3 — DESIGN OBLIGATION. A retried transfer changes nothing. Sharper
  //      than the errored case: the master WILL come back, so an effect
  //      applied per attempt is applied repeatedly.
  property p_rty_changes_nothing;
    @(posedge clk_i) $changed(lvl_q) |-> !$past(rty_o);
  endproperty
  a_rty_changes_nothing : assert property (p_rty_changes_nothing)
    else $error("slave state changed on a transfer terminated with RTY_O");

  // P4 — DESIGN OBLIGATION, as LIVENESS. Attempts are BOUNDED. Nothing at
  //      the signal level forbids infinite retry, and livelock produces a
  //      bus that looks entirely healthy — so this is the only place the
  //      failure is visible.
  property p_tries_bounded;
    @(posedge clk_i) tries_q <= 4'(MAX_TRIES);
  endproperty
  a_tries_bounded : assert property (p_tries_bounded)
    else $error("retry attempts exceeded the documented bound");
endmodule