CYC_O

assign cyc_o = active_q;
assign stb_o = active_q;

// ─────────────────────────────────────────────────────────────────────────
// wb_cyc_master — a master that holds CYC_O across MULTIPLE transfers.
//
// PURPOSE. Every previous master in this module drove cyc_o and stb_o from
// one register. This one separates them, which is the point: cyc_o spans
// the tenure, stb_o is asserted once per transfer within it.
//
// RULE 3.25: CYC_O asserted for the duration of the cycle, and no later
// than the rising edge that qualifies STB_O. Here cyc_o is asserted in the
// same edge as the first stb_o and held until the last transfer ends.
//
// Reset: SYNCHRONOUS, ACTIVE HIGH (RULES 2.30, 3.00, 3.20).
// ─────────────────────────────────────────────────────────────────────────
module wb_cyc_master #(
  parameter int unsigned AW = 30,
  parameter int unsigned DW = 32,
  parameter int unsigned CW = 8                 // burst-count width
) (
  input  logic          clk_i,
  input  logic          rst_i,

  input  logic            go_i,
  input  logic [AW-1:0]   base_i,
  input  logic [CW-1:0]   count_i,              // transfers in this block
  output logic            busy_o,
  output logic            done_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] { S_IDLE, S_XFER, S_GAP } state_e;
  state_e state_q;

  logic [AW-1:0] adr_q;
  logic [CW-1:0] left_q;
  logic [DW-1:0] last_q;

  // ── THE SEPARATION ─────────────────────────────────────────────────────
  // cyc_o is asserted in S_XFER *and* S_GAP. stb_o only in S_XFER.
  // S_GAP is the state that cannot exist in a single-transfer master: the
  // bus is HELD but no transfer is presented. That is the legal combination
  // CYC_O asserted with STB_O negated.
  assign cyc_o  = (state_q == S_XFER) || (state_q == S_GAP);
  assign stb_o  = (state_q == S_XFER);
  assign we_o   = 1'b0;                          // read block
  assign adr_o  = adr_q;
  assign dat_o  = '0;
  assign busy_o = (state_q != S_IDLE);

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

  always_ff @(posedge clk_i) begin
    if (rst_i) begin
      state_q <= S_IDLE;                         // RULE 3.20 via cyc/stb
      adr_q   <= '0;
      left_q  <= '0;
      last_q  <= '0;
      done_o  <= 1'b0;
    end else begin
      done_o <= 1'b0;
      unique case (state_q)
        S_IDLE: begin
          if (go_i && (count_i != '0)) begin
            state_q <= S_XFER;
            adr_q   <= base_i;
            left_q  <= count_i;
          end
        end

        S_XFER: begin
          if (terminated) begin
            if (ack_i) last_q <= dat_i;          // Chapter 4.5's capture
            // An error or retry ABANDONS the block here. Deciding that is
            // this master's policy, not a rule — Chapters 4.11 and 4.12
            // examine what else a master might legitimately do.
            if (!ack_i) begin
              state_q <= S_IDLE;
              done_o  <= 1'b1;
            end else if (left_q == CW'(1)) begin
              state_q <= S_IDLE;                 // last transfer: drop CYC
              done_o  <= 1'b1;
            end else begin
              left_q  <= left_q - CW'(1);
              adr_q   <= adr_q + AW'(1);
              // Deliberately pass through S_GAP rather than presenting the
              // next transfer immediately. It is not required — a master
              // may hold stb_o continuously across a block — but it makes
              // the held-bus-without-a-transfer state observable.
              state_q <= S_GAP;
            end
          end
        end

        S_GAP: begin
          state_q <= S_XFER;                     // CYC_O never dropped
        end

        default: state_q <= S_IDLE;
      endcase
    end
  end
endmodule

// ─────────────────────────────────────────────────────────────────────────
// wb_rmw_master — read-modify-write as ONE tenure.
//
// The atomicity mechanism is a single fact: cyc_o is asserted from the
// start of the read until the end of the write, and is never negated in
// between. RULE 3.25 names RMW as one of the cycle types CYC_O must span.
//
// WHAT THIS DOES NOT DO (Section 2): it does not lock the slave against a
// second port, and it depends on an arbiter that honours the request. Both
// are system properties outside this module.
// ─────────────────────────────────────────────────────────────────────────
module wb_rmw_master #(
  parameter int unsigned AW = 30,
  parameter int unsigned DW = 32
) (
  input  logic          clk_i,
  input  logic          rst_i,

  input  logic          go_i,
  input  logic [AW-1:0] adr_i,
  input  logic [DW-1:0] setmask_i,               // bits to OR in
  output logic          done_o,
  output logic          failed_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] { R_IDLE, R_READ, R_WRITE } rstate_e;
  rstate_e state_q;

  logic [AW-1:0] adr_q;
  logic [DW-1:0] mask_q, wdat_q;

  // ── CYC_O SPANS BOTH TRANSFERS ─────────────────────────────────────────
  // This single line is the atomicity. Compare with stb_o, which is also
  // asserted in both states here only because this master presents the
  // write in the cycle immediately after the read terminates. If it needed
  // a cycle to compute, cyc_o would stay high and stb_o would drop — and
  // the bus would still be held.
  assign cyc_o = (state_q != R_IDLE);
  assign stb_o = (state_q != R_IDLE);
  assign we_o  = (state_q == R_WRITE);
  assign adr_o = adr_q;
  assign dat_o = wdat_q;

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

  always_ff @(posedge clk_i) begin
    if (rst_i) begin
      state_q  <= R_IDLE;
      adr_q    <= '0;
      mask_q   <= '0;
      wdat_q   <= '0;
      done_o   <= 1'b0;
      failed_o <= 1'b0;
    end else begin
      done_o   <= 1'b0;
      failed_o <= 1'b0;
      unique case (state_q)
        R_IDLE: begin
          if (go_i) begin
            state_q <= R_READ;
            adr_q   <= adr_i;
            mask_q  <= setmask_i;
          end
        end

        R_READ: begin
          if (ack_i) begin
            // Modify. The read value never leaves this master, and the bus
            // is still held, so no other master can have changed the word.
            wdat_q  <= dat_i | mask_q;
            state_q <= R_WRITE;
          end else if (err_i || rty_i) begin
            // Abandoning here is safe: nothing has been written, so the
            // location is exactly as it was. Abandoning after the read has
            // succeeded but before the write is also safe for the same
            // reason. There is no half-completed RMW to unwind.
            state_q  <= R_IDLE;
            done_o   <= 1'b1;
            failed_o <= 1'b1;
          end
        end

        R_WRITE: begin
          if (terminated) begin
            state_q  <= R_IDLE;
            done_o   <= 1'b1;
            failed_o <= ~ack_i;
          end
        end

        default: state_q <= R_IDLE;
      endcase
    end
  end
endmodule

// ─────────────────────────────────────────────────────────────────────────
// wb_cyc_checker — tenure properties.
//
// P2 and P3 are SPECIFICATION-derived from RULE 3.25. P1 is ATOMICITY
// POLICY for a particular master — the specification requires CYC_O to
// span an RMW cycle, but whether a given master is performing one is not
// visible on the bus, so the property needs a white-box signal.
// ─────────────────────────────────────────────────────────────────────────
module wb_cyc_checker (
  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 rmw_active      // white-box: master is mid read-modify-write
);
  default disable iff (rst_i);

  // P1 — ATOMICITY POLICY, checked white-box. CYC_O must not be negated
  //      while an RMW is in progress. Cannot be written from bus signals
  //      alone: an observer cannot tell a held tenure from two adjacent
  //      single cycles without knowing the master's intent.
  property p_rmw_holds_cyc;
    @(posedge clk_i) rmw_active |-> cyc_o;
  endproperty
  a_rmw_holds_cyc : assert property (p_rmw_holds_cyc)
    else $error("CYC_O negated during a read-modify-write");

  // P2 — RULE 3.25. CYC_O is asserted no later than the edge that
  //      qualifies STB_O. Stated as the simple implication: a strobe
  //      without a cycle is never legal.
  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");

  // P3 — RULE 3.25, the duration half. CYC_O may not be negated in the
  //      same cycle a transfer is still outstanding: the cycle lasts at
  //      least as long as the transfer inside it.
  property p_cyc_spans_outstanding;
    @(posedge clk_i)
      (cyc_o && stb_o && !(ack_i || err_i || rty_i)) |=> cyc_o;
  endproperty
  a_cyc_spans_outstanding : assert property (p_cyc_spans_outstanding)
    else $error("CYC_O negated with a transfer still outstanding");

  // P4 — LOCAL POLICY. A tenure does not stay open indefinitely with no
  //      transfer presented. Not a Wishbone rule — the specification sets
  //      no limit — but an open cycle with no strobes starves every other
  //      master, and the bound belongs in the verification plan.
  property p_no_idle_tenure;
    @(posedge clk_i) (cyc_o && !stb_o) |-> ##[1:32] (stb_o || !cyc_o);
  endproperty
  a_no_idle_tenure : assert property (p_no_idle_tenure)
    else $error("CYC_O held for 32 cycles with no transfer presented");
endmodule