Atomic Operations

// ─────────────────────────────────────────────────────────────────────────
// wb_counter_slave — one shared word that two masters both want to increment.
//
// IT DOES NOT KNOW HOW TO INCREMENT, AND THAT IS THE POINT. A slave with an
// "add one" command would make the whole module vanish: the operation would
// be a single transfer and nothing could interleave. The increment here is
// built out of a bus READ and a bus WRITE, which is what makes the interval
// between them exist at all.
//
// IT ALSO DOES NOT KNOW IT IS INSIDE AN RMW. Nothing in the Classic profile
// tells it. RECOMMENDATION 3.15 advises an optional TGC_O() cycle tag named
// [RMW_O] that could identify the cycle type, but it is advisory and this
// slave does not receive one. It sees a read transfer, and later a write
// transfer, exactly as it would see two unrelated cycles.
//
// COMMIT SEMANTICS, inherited from Module 7 and used unchanged since:
// the register changes on an acknowledged write and at no other time. The
// commit is gated on `wr_fire`, which is true for exactly one clock per
// answered write phase — a held ACK cannot produce two increments, which
// would make every measurement in this module meaningless.
//
// THE EVENT INPUT IS REAL HARDWARE, NOT SCAFFOLDING. A shared counter in a
// real peripheral usually has something that also increments it — a packet
// arriving, a timer wrapping, an interrupt being posted. Chapter 15.3 uses
// it to separate BUS exclusivity from RESOURCE exclusivity, and it needs a
// deterministic priority:
//
//   LOCAL SLAVE POLICY: a bus write and an event on the same clock both
//   apply, with the event added to the written value. Neither is dropped.
//   This is a choice; another slave could let the write win and lose the
//   event. It is written as one expression so the precedence cannot drift.
// ─────────────────────────────────────────────────────────────────────────
module wb_counter_slave #(
  parameter int unsigned OFF_AW = 4,
  parameter int unsigned DW     = 32,
  parameter int unsigned WAITS  = 0,      // wait states per transfer
  parameter logic [31:0] RESET  = 32'd10,
  // THE DEFECT, available as a parameter so that Chapter 15.4's checker
  // can be shown to detect something. With it set, the commit is gated on
  // the transfer being PRESENTED rather than on its being ANSWERED - so a
  // phase that spans several clocks commits on every one of them.
  //
  // This is the repeated-side-effect failure Modules 5, 7, 9 and 11 each
  // measured in their own way. It is included here because an RMW built
  // on a slave that executes a write more than once is meaningless, and
  // because a commit-count checker that has never failed proves nothing.
  parameter bit COMMIT_EVERY_CLOCK = 1'b0
) (
  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,
  input  logic [DW/8-1:0]   sel_i,
  output logic [DW-1:0]     dat_o,
  output logic              ack_o,
  output logic              err_o,
  // an internal hardware source that also updates the counter
  input  logic              event_i,
  // write-protect. While asserted a write phase is answered with ERR and
  // commits nothing; reads are unaffected. A real shared register often
  // has one, and Chapter 15.4 uses it to produce a genuine error on the
  // write half of an RMW without building a special faulty slave.
  input  logic              wr_block_i,
  // observation only — not part of the Wishbone interface
  output logic [DW-1:0]     count_o,
  output int unsigned       wr_commits_o,
  output int unsigned       rd_serviced_o,
  output int unsigned       events_o
);
  localparam logic [OFF_AW-1:0] O_COUNT = OFF_AW'('h0);

  logic [DW-1:0] count_q;
  logic [7:0]    held_q;
  int unsigned   nwr_q, nrd_q, nev_q;

  logic xfer, mapped, ready, rd_fire, wr_fire;
  assign xfer   = cyc_i && stb_i;                 // RULE 3.30: CYC_I qualifies
  assign mapped = (adr_i == O_COUNT);
  // The slave throttles by withholding its termination, which is the
  // specification's mechanism. held_q counts clocks this phase has gone
  // unanswered and is cleared on the answer, so each phase of a two-phase
  // RMW gets its own latency.
  assign ready  = xfer && (held_q >= 8'(WAITS));

  // A write while write-protected is refused, exactly as an unmapped
  // offset is. The commit is gated on the same condition as the
  // acknowledgement, so a refused write cannot change the register -
  // LOCAL SLAVE POLICY, and the reason Chapter 15.4 can say the counter
  // is unchanged after an error without appealing to the specification.
  logic refused;
  assign refused = !mapped || (we_i && wr_block_i);

  assign ack_o  = ready && !refused;
  assign err_o  = ready &&  refused;

  assign rd_fire = ready && !refused && !we_i;
  assign wr_fire = ready && !refused &&  we_i;    // exactly one clock

  // The commit condition. Correct: the answered edge, once per phase.
  // Defective: every clock the write is presented.
  logic commit_now;
  logic presented_wr;
  assign presented_wr = xfer && mapped && we_i && !wr_block_i;
  assign commit_now   = COMMIT_EVERY_CLOCK ? presented_wr : wr_fire;

  always_comb begin
    dat_o = '0;
    if (rd_fire) dat_o = count_q;
  end

  always_ff @(posedge clk_i) begin
    if (rst_i) begin
      count_q <= DW'(RESET);
      held_q  <= 8'd0; nwr_q <= 0; nrd_q <= 0; nev_q <= 0;
    end else begin
      if (!xfer || ready) held_q <= 8'd0;
      else                held_q <= held_q + 8'd1;

      // One expression, so a bus write and a simultaneous event cannot
      // race: the write supplies the base and the event adds to it.
      if (commit_now) count_q <= dat_i   + (event_i ? DW'(1) : DW'(0));
      else            count_q <= count_q + (event_i ? DW'(1) : DW'(0));

      if (commit_now) nwr_q <= nwr_q + 1;
      if (rd_fire) nrd_q <= nrd_q + 1;
      if (event_i) nev_q <= nev_q + 1;
    end
  end

  assign count_o       = count_q;
  assign wr_commits_o  = nwr_q;
  assign rd_serviced_o = nrd_q;
  assign events_o      = nev_q;
endmodule

// ─────────────────────────────────────────────────────────────────────────
// wb_incr_master — reads the shared counter, adds one, writes it back.
//
// THE HOLD POLICY IS A PARAMETER, and that is the whole experimental design.
// Chapters 15.1 and 15.2 compare four policies against identical stimulus,
// so every measured difference has exactly one cause. Nothing else in the
// module changes between them.
//
//   HOLD_NONE   two independent cycles. CYC_O drops between read and write.
//   HOLD_CYC    one cycle across both halves. CYC_O retained, no LOCK_O.
//               This is the B3 RMW cycle as §3.4 defines it.
//   HOLD_LOCK   CYC_O retained AND LOCK_O asserted across both halves.
//   HOLD_WRITE  LOCK_O asserted for the write half only.
//   HOLD_READ   LOCK_O released after the read, before the write.
//
// WHAT §3.4 ACTUALLY SAYS, because HOLD_CYC is named after it:
//   "During the first half of the cycle a single read data transfer is
//    performed. During the second half of the cycle a write data transfer
//    is performed. The [CYC_O] signal remains asserted during both halves
//    of the cycle."
// and RULE 3.25 requires CYC_O for the duration of SINGLE, BLOCK and RMW
// cycles. LOCK_O appears nowhere in the RMW section and nowhere in its
// normative figure — which is why HOLD_CYC and HOLD_LOCK are different
// parameters rather than the same one.
//
// THE SAVED READ IS THE OTHER HALF OF CORRECTNESS. `saved_q` captures
// DAT_I at the read phase's answered edge, and the write data is derived
// from `saved_q` — never from live DAT_I, which by RULE 3.65 is meaningful
// only while the slave is terminating and belongs to a phase that is over.
// A master that recomputed from the wire would be reading whatever the
// second phase's bus carries.
//
// ONE CLIENT REQUEST PRODUCES ONE CLIENT COMPLETION. `done_o` pulses once,
// with `ok_o` or `err_o`, whatever happened on the bus.
// ─────────────────────────────────────────────────────────────────────────
module wb_incr_master #(
  parameter int unsigned AW   = 30,
  parameter int unsigned DW   = 32,
  // 0 NONE, 1 CYC, 2 LOCK, 3 WRITE-only, 4 READ-only
  parameter int unsigned HOLD = 2
) (
  input  logic            clk_i,
  input  logic            rst_i,
  input  logic            start_i,
  input  logic [AW-1:0]   adr_i,
  output logic            busy_o,
  output logic            done_o,
  output logic            ok_o,
  output logic            err_o,
  // Wishbone master port
  output logic            cyc_o,
  output logic            stb_o,
  output logic            lock_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,
  // observation only
  output logic [DW-1:0]   saved_o,
  output logic [2:0]      state_o
);
  localparam int unsigned HOLD_NONE  = 0;
  localparam int unsigned HOLD_CYC   = 1;
  localparam int unsigned HOLD_LOCK  = 2;
  localparam int unsigned HOLD_WRITE = 3;
  localparam int unsigned HOLD_READ  = 4;

  initial begin
    if (HOLD > 4) $fatal(1, "wb_incr_master: HOLD must be 0..4");
  end

  typedef enum logic [2:0] {
    S_IDLE, S_READ, S_GAP, S_WRITE, S_DONE
  } state_e;
  state_e state_q;

  logic [DW-1:0] saved_q;
  logic [AW-1:0] adr_q;
  logic          err_q;

  logic phase_done;
  assign phase_done = cyc_o && stb_o && (ack_i || err_i);

  // CYC_O spans both halves except under HOLD_NONE, where the cycle ends
  // after the read and a second cycle begins for the write. S_GAP exists
  // only for HOLD_NONE and is the clock in which CYC_O is low.
  assign cyc_o = (state_q == S_READ) || (state_q == S_WRITE) ||
                 ((HOLD != HOLD_NONE) && (state_q == S_GAP));
  assign stb_o = (state_q == S_READ) || (state_q == S_WRITE);

  // LOCK_O per the policy under test.
  always_comb begin
    case (HOLD)
      HOLD_LOCK:  lock_o = cyc_o;                        // whole cycle
      HOLD_WRITE: lock_o = (state_q == S_WRITE);         // write half only
      HOLD_READ:  lock_o = (state_q == S_READ);          // read half only
      default:    lock_o = 1'b0;                         // NONE and CYC
    endcase
  end

  assign we_o  = (state_q == S_WRITE);
  assign adr_o = adr_q;
  assign sel_o = '1;
  assign dat_o = saved_q + DW'(1);      // derived from the SAVED read

  assign busy_o  = (state_q != S_IDLE);
  assign done_o  = (state_q == S_DONE);
  assign ok_o    = (state_q == S_DONE) && !err_q;
  assign err_o   = (state_q == S_DONE) &&  err_q;
  assign saved_o = saved_q;
  assign state_o = state_q;

  always_ff @(posedge clk_i) begin
    if (rst_i) begin
      state_q <= S_IDLE; saved_q <= '0; adr_q <= '0; err_q <= 1'b0;
    end else begin
      case (state_q)
        S_IDLE: begin
          err_q <= 1'b0;
          if (start_i) begin adr_q <= adr_i; state_q <= S_READ; end
        end

        S_READ: if (phase_done) begin
          if (err_i) begin
            // LOCAL MASTER POLICY: an error on the read abandons the
            // compound operation. No write phase is presented, so nothing
            // is committed and there is nothing to undo.
            err_q   <= 1'b1;
            state_q <= S_DONE;
          end else begin
            saved_q <= dat_i;            // captured at the answered edge
            state_q <= S_GAP;
          end
        end

        // One clock between the halves. Under HOLD_NONE CYC_O is low here
        // and the write becomes a separate cycle; under every other policy
        // CYC_O is retained and this is the master wait state the
        // specification's own RMW walkthrough shows between the halves.
        S_GAP: state_q <= S_WRITE;

        S_WRITE: if (phase_done) begin
          // LOCAL MASTER POLICY: an error on the write is reported as a
          // failure. Whether the slave committed before answering ERR is
          // the slave's business - nothing here rolls anything back, and
          // Wishbone provides no mechanism that would.
          if (err_i) err_q <= 1'b1;
          state_q <= S_DONE;
        end

        S_DONE: state_q <= S_IDLE;
        default: state_q <= S_IDLE;
      endcase
    end
  end
endmodule

  === SIM A - two increments, no protection ===
    each master does a read cycle, then a separate write
    cycle. Every transfer is protocol-correct.

    policy                HOLD_NONE - CYC drops between read and write
    counter before        10
    A read                10
    B read                10
    A wrote               11
    B wrote               11
    read phases served    2
    write commits         2
    counter after         11
    expected after two    12
    result                LOST UPDATE

    Both masters read the same value, both computed the same
    result, and both wrote it. Two increments, one increment
    of effect. Nothing on the bus went wrong.

  === SIM B - the RMW cycle, with and without a lock ===
    Both rows keep CYC_O asserted across the read half and the
    write half, which is what section 3.4 requires. They differ
    only in whether LOCK_O is asserted with it.

    policy                    A read  B read  after  expected  result
    CYC retained, no LOCK       10      10     11      12     LOST UPDATE
    CYC retained + LOCK         10      11     12      12       preserved

    owner changes inside a protected interval:
      CYC only    0
      CYC + LOCK  0

    write commits   CYC only 2   CYC + LOCK 2

// ─────────────────────────────────────────────────────────────────────────
// wb_rmw_props — what a read-modify-write promises, and who promises it.
//
// NOTE ON EXECUTION: Icarus Verilog does not support SVA. These properties
// were reviewed by inspection and are NOT claimed to have been executed.
// The numbers in this module come from procedural checks, which Icarus
// does run — and three of those checks were additionally validated against
// targeted broken designs (Chapter 15.4), because a checker that has only
// ever passed has not been shown to check anything.
//
// ONE of these is SPEC-DERIVED. The rest are local, and that ratio is the
// honest picture: §3.4 fixes the structure of the cycle and says nothing
// about exclusion.
// ─────────────────────────────────────────────────────────────────────────
module wb_rmw_props #(
  parameter int unsigned AW = 30,
  parameter int unsigned DW = 32
) (
  input logic          clk_i,
  input logic          rst_i,
  input logic          cyc_i,
  input logic          stb_i,
  input logic          lock_i,
  input logic          we_i,
  input logic          ack_i,
  input logic          err_i,
  input logic [DW-1:0] dat_i,
  input logic [DW-1:0] dat_o,
  input logic [DW-1:0] saved_i,
  input logic [2:0]    state_i,      // 0 IDLE 1 READ 2 GAP 3 WRITE 4 DONE
  input logic          done_i,
  input logic          ok_i,
  input logic          err_rep_i
);
  default disable iff (rst_i);

  localparam logic [2:0] S_IDLE = 3'd0, S_READ = 3'd1, S_GAP = 3'd2,
                         S_WRITE = 3'd3, S_DONE = 3'd4;

  logic phase_end;
  assign phase_end = cyc_i && stb_i && (ack_i || err_i);

  // P1 — SPEC-DERIVED. §3.4: "During the first half of the cycle a single
  // read data transfer is performed. During the second half of the cycle a
  // write data transfer is performed. The [CYC_O] signal remains asserted
  // during both halves of the cycle." Plus RULE 3.25, which requires
  // CYC_O for the duration of SINGLE, BLOCK and RMW cycles.
  // Stated as: a presented phase always carries CYC_O, and the write half
  // is never presented before the read half has been answered.
  property p_write_after_read;
    @(posedge clk_i) (state_i == S_WRITE) |-> cyc_i;
  endproperty
  a_write_after_read: assert property (p_write_after_read);

  property p_read_precedes_write;
    @(posedge clk_i) $rose(state_i == S_WRITE) |-> $past(state_i == S_GAP);
  endproperty
  a_read_precedes_write: assert property (p_read_precedes_write);

  // P2 — LOCAL MASTER POLICY. The write data is derived from the SAVED
  // read, never from live DAT_I. RULE 3.65 makes a slave's DAT_O()
  // meaningful only while it is terminating, and by the write half the
  // read's termination is long over — a master recomputing from the wire
  // would be using whatever the second phase happens to carry.
  property p_write_derived_from_saved;
    @(posedge clk_i) (state_i == S_WRITE) |-> (dat_o == saved_i + DW'(1));
  endproperty
  a_write_derived_from_saved: assert property (p_write_derived_from_saved);

  // P3 — LOCAL MASTER POLICY. The saved value does not move once captured,
  // for the whole of the write half.
  property p_saved_stable;
    @(posedge clk_i) (state_i == S_GAP || state_i == S_WRITE) |=>
      (state_i == S_WRITE) -> $stable(saved_i);
  endproperty
  a_saved_stable: assert property (p_saved_stable);

  // P4 — LOCAL MASTER POLICY, and the definition of the protected
  // interval. LOCK_O is asserted from the start of the read half through
  // the answered write. Under the HOLD_LOCK policy this is what the
  // ownership guarantee is built on; under the other policies it is
  // deliberately false, which is the subject of Chapters 15.1 and 15.2.
  property p_lock_spans_operation;
    @(posedge clk_i) (state_i == S_READ || state_i == S_GAP ||
                      state_i == S_WRITE) |-> lock_i;
  endproperty
  a_lock_spans_operation: assert property (p_lock_spans_operation);

  // P5 — LOCAL MASTER POLICY. No early release: the operation does not
  // drop CYC_O between the halves. This is what separates an RMW cycle
  // from two transfers with a data dependency.
  property p_no_release_between_halves;
    @(posedge clk_i) (state_i == S_GAP) |-> cyc_i;
  endproperty
  a_no_release_between_halves: assert property (p_no_release_between_halves);

  // P6 — LOCAL MASTER POLICY. Metadata holds still while a phase waits.
  property p_metadata_stable_in_wait;
    @(posedge clk_i) (cyc_i && stb_i && !(ack_i || err_i)) |=>
      (cyc_i && stb_i) -> ($stable(we_i) && $stable(dat_o));
  endproperty
  a_metadata_stable_in_wait: assert property (p_metadata_stable_in_wait);

  // P7 — LOCAL MASTER POLICY. One client request, one client completion,
  // classified. Never both, never neither.
  property p_one_completion;
    @(posedge clk_i) done_i |-> (ok_i ^ err_rep_i);
  endproperty
  a_one_completion: assert property (p_one_completion);

  // P8 — LOCAL MASTER POLICY. An error anywhere in the operation is
  // reported as a failure. NOT a rollback claim: nothing here undoes a
  // write the slave may already have committed.
  property p_err_not_reported_as_success;
    @(posedge clk_i) (phase_end && err_i) |=> ##[0:2] (done_i -> err_rep_i);
  endproperty
  a_err_not_reported_as_success: assert property (p_err_not_reported_as_success);
endmodule