Wait States

// ─────────────────────────────────────────────────────────────────────────
// wb_delayed_write_slave — the running peripheral, with latency and two
// side-effecting registers.
//
// PURPOSE. Make a write take LAT cycles, and give it state whose repeated
// update is OBSERVABLE — so the presented-versus-committed distinction
// stops being theoretical.
//
// ── DECLARED COMMIT POLICY (LOCAL, not Wishbone) ──────────────────────
//   Commits on the same rising clock edge for which it returns ACK_O for
//   a qualified write. Identical in wording to Chapter 7.1's slave; the
//   difference is that ACK_O now arrives LAT cycles later, so `commit` is
//   true for one cycle out of LAT+1 rather than one out of one.
//
// WHAT THE LATENCY MODEL IS. A counter — NOT realistic hardware latency.
// It is an EDUCATIONAL MODEL standing in for the real sources: a register
// file with a pipelined write port, a peripheral that must accept a
// command before it can be overwritten, a bridge to another clock domain,
// or a resource that is briefly busy. What matters for the protocol is
// only that the slave is not ready yet.
//
// Reset: SYNCHRONOUS, ACTIVE HIGH (RULES 2.30, 3.00).
// ─────────────────────────────────────────────────────────────────────────
module wb_delayed_write_slave #(
  parameter int unsigned OFF_AW = 4,
  parameter int unsigned DW     = 32,
  parameter int unsigned LAT    = 3          // cycles before terminating
) (
  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,
  // device side, all observable for QA
  input  logic [7:0]        event_set_i,     // events arriving from hardware
  output logic [DW-1:0]     control_o,
  output logic [7:0]        events_o,        // W1C status
  output logic              cmd_pulse_o,     // one-cycle command strobe
  output logic [7:0]        launches_o       // side-effect COUNT
);
  localparam int unsigned NL = DW/8;

  localparam logic [OFF_AW-1:0] O_CTRL   = 4'd2;   // byte 0x08  RW
  localparam logic [OFF_AW-1:0] O_ID     = 4'd4;   // byte 0x10  RO
  localparam logic [OFF_AW-1:0] O_EVENTS = 4'd8;   // byte 0x20  W1C
  localparam logic [OFF_AW-1:0] O_CMD    = 4'd9;   // byte 0x24  WO, pulses

  localparam logic [DW-1:0] ID_VALUE = 32'h5742_0701;

  logic [DW-1:0] ctrl_q;
  logic [7:0]    events_q;
  assign control_o = ctrl_q;
  assign events_o  = events_q;

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

  // ── LEGALITY ──────────────────────────────────────────────────────────
  logic known_off, writable;
  always_comb begin
    unique case (adr_i)
      O_CTRL, O_ID, O_EVENTS, O_CMD: known_off = 1'b1;
      default:                       known_off = 1'b0;
    endcase
  end
  always_comb begin
    unique case (adr_i)
      O_CTRL, O_EVENTS, O_CMD: writable = 1'b1;
      default:                 writable = 1'b0;   // ID is read-only
    endcase
  end

  logic illegal;
  assign illegal = ~known_off | (we_i & ~writable);

  // ── THE LATENCY COUNTER ───────────────────────────────────────────────
  // `ready` is declared and assigned BEFORE the block that uses it —
  // Icarus rejects a reference that precedes its declaration, and the
  // order reads better anyway.
  //
  // The counter resets the moment the transfer is not presented, which is
  // what satisfies RULE 3.50 structurally: when STB_I goes away the
  // counter returns to zero and no termination can be asserted.
  logic [7:0] waited_q;
  logic       ready;
  assign ready = (waited_q >= 8'(LAT));

  always_ff @(posedge clk_i) begin
    if (rst_i)       waited_q <= '0;
    else if (!xfer)  waited_q <= '0;
    else if (!ready) waited_q <= waited_q + 8'd1;
    else             waited_q <= '0;              // one termination per transfer
  end

  // ── TERMINATION ───────────────────────────────────────────────────────
  assign err_o = xfer & ready &  illegal;
  assign ack_o = xfer & ready & ~illegal;

  // ── THE COMMIT EVENT ──────────────────────────────────────────────────
  // ONE named term. It contains ack_o, so it is true for exactly one cycle
  // out of the LAT+1 the transfer is presented for.
  //
  // Replace `commit` with `xfer & we_i` in the block below and this slave
  // launches the command LAT+1 times, and clears EVENTS LAT+1 times —
  // Section 5 measures both.
  logic commit;
  assign commit = xfer & we_i & ack_o;

  always_ff @(posedge clk_i) begin
    if (rst_i) begin
      ctrl_q      <= '0;
      events_q    <= '0;
      cmd_pulse_o <= 1'b0;
      launches_o  <= '0;
    end else begin
      cmd_pulse_o <= 1'b0;                        // default: a ONE-CYCLE pulse

      // ── W1C EVENTS ──────────────────────────────────────────────────
      // Writing a 1 CLEARS that bit; writing a 0 preserves it. Only the
      // selected byte lane participates — an unselected lane must not
      // clear anything, which is why sel_i[0] gates it.
      //
      // The clear and the hardware set are combined into ONE assignment so
      // an event arriving in the same cycle as the commit is not lost: it
      // is OR-ed in after the mask is applied, and the NEXT write sees it.
      // Writing them as two separate statements would make the outcome
      // depend on statement order, which is the race Chapter 6.5 Section 11
      // described from the read side.
      if (commit && (adr_i == O_EVENTS) && sel_i[0]) begin
        events_q <= (events_q & ~dat_i[7:0]) | event_set_i;
      end else begin
        events_q <= events_q | event_set_i;
      end

      // ── COMMAND PULSE ───────────────────────────────────────────────
      // A write to COMMAND produces exactly one cycle of cmd_pulse_o and
      // increments a launch counter. launches_o is NOT a Wishbone signal;
      // it exists so a testbench can count the side effect. A production
      // peripheral would not export it.
      if (commit && (adr_i == O_CMD)) begin
        cmd_pulse_o <= 1'b1;
        launches_o  <= launches_o + 8'd1;
      end

      // ── ORDINARY MASKED REGISTER ────────────────────────────────────
      if (commit && (adr_i == O_CTRL)) begin
        for (int unsigned n = 0; n < NL; n++)
          if (sel_i[n]) ctrl_q[n*8 +: 8] <= dat_i[n*8 +: 8];
      end
    end
  end

  // ── READ PATH ─────────────────────────────────────────────────────────
  // RULE 3.65: qualified by the termination. COMMAND is write-only and
  // reads back zero; a design could equally refuse the read with ERR_O,
  // which is an implementation policy rather than a rule.
  always_comb begin
    dat_o = '0;
    if (xfer && !we_i && ack_o) begin
      unique case (adr_i)
        O_CTRL:   dat_o = ctrl_q;
        O_ID:     dat_o = ID_VALUE;
        O_EVENTS: dat_o = {24'd0, events_q};
        default:  dat_o = '0;
      endcase
    end
  end
endmodule

  === SIMULATION B - payload stability (LAT=3) ===
                                     correct      unlatched
    cycles the write was presented       4             4
    distinct ADR_O values on the bus     1             2
    distinct DAT_O values on the bus     1             2
    ADR_O at the commit edge           0x2           0x6
    DAT_O at the commit edge      0x0000000f    0xdeadbeef
    CONTROL after                 0x0000000f    0x00000000
    OUTPUT  after                 0x00000000    0xdeadbeef
    RULE 3.60 violation cycles           0             3

  === SIMULATION D - delayed write (LAT=3) ===
    cycles the transfer was presented       4
    ADR_O changes while outstanding         0
    DAT_O changes while outstanding         0
    SEL_O changes while outstanding         0
    WE_O  changes while outstanding         0
    CYC_O deasserted while outstanding      0
    STB_O deasserted while outstanding      0
    master completions before termination   0
    commit events                           1

  === SIMULATION E - repeated side effect (LAT=3) ===
                                   gated on COMMIT   gated on PRESENT
    cycles presented                      4                4
    terminations returned                 1                1
    COMMAND launches                      1                4
  --- W1C EVENTS, one write, event 0x02 arrives mid-wait ---
    events pending at the start        0x05             0x05
    write data (bits to clear)         0x07             0x07
    events after the write             0x00             0x00
    events lost                           1                1

// ─────────────────────────────────────────────────────────────────────────
// wb_write_wait_checker — properties for a waited write.
//
// P1 is SPECIFICATION (RULE 3.60, and §3.2.2 via RULE 3.75). P2 is
// SPECIFICATION (RULE 3.50). P3 and P4 are DESIGN OBLIGATIONS — the
// specification does not know what side effects a slave has, so it cannot
// require them to happen once.
// ─────────────────────────────────────────────────────────────────────────
module wb_write_wait_checker #(
  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            we_i,
  input logic [AW-1:0]   adr_i,
  input logic [DW-1:0]   dat_i,
  input logic [DW/8-1:0] sel_i,
  input logic            ack_o,
  input logic            err_o,
  // white-box
  input logic            commit,
  input logic [7:0]      launches_q,
  input logic            cmd_pulse
);
  default disable iff (rst_i);

  logic xfer, terminated;
  assign xfer       = cyc_i & stb_i;
  assign terminated = ack_o | err_o;

  // P1 — SPECIFICATION. The WHOLE payload holds still for the whole wait.
  //      This is the write-side form of Chapter 6.5's P1, extended with
  //      dat_i — the field whose lapse commits a wrong value rather than
  //      returning one. The end boundary is the termination; omitting it
  //      would forbid a legal back-to-back write.
  property p_payload_frozen_while_waiting;
    @(posedge clk_i) (xfer && we_i && !terminated)
      |=> ($stable(adr_i) && $stable(dat_i) && $stable(sel_i) &&
           $stable(we_i) && cyc_i && stb_i);
  endproperty
  a_payload_frozen_while_waiting :
    assert property (p_payload_frozen_while_waiting)
    else $error("RULE 3.60 / 3.2.2: write payload moved during the wait");

  // P2 — SPECIFICATION (RULE 3.50, OBSERVATION 3.10). A slow response
  //      cannot outlive the transfer that provoked it.
  property p_no_termination_without_strobe;
    @(posedge clk_i) !stb_i |-> !terminated;
  endproperty
  a_no_termination_without_strobe :
    assert property (p_no_termination_without_strobe)
    else $error("RULE 3.50: termination asserted with STB_I negated");

  // P3 — DESIGN OBLIGATION, and the one this chapter exists for. A side
  //      effect happens only at a COMMIT, never in a merely presented
  //      cycle. Fires on the FIRST extra launch rather than when a
  //      downstream symptom eventually surfaces.
  //
  //      No bus-level property can catch this: the bus is conformant
  //      throughout, so the checker needs the counter.
  property p_side_effect_once_per_commit;
    @(posedge clk_i) $changed(launches_q) |-> $past(commit);
  endproperty
  a_side_effect_once_per_commit :
    assert property (p_side_effect_once_per_commit)
    else $error("side effect fired outside a commit event");

  // P4 — DESIGN OBLIGATION. The command strobe is ONE cycle wide. Stated
  //      separately from P3 because a pulse and a counter fail
  //      differently: a stretched pulse may be harmless to an
  //      edge-detecting consumer and fatal to a level-sensitive one.
  property p_pulse_is_one_cycle;
    @(posedge clk_i) cmd_pulse |=> !cmd_pulse;
  endproperty
  a_pulse_is_one_cycle : assert property (p_pulse_is_one_cycle)
    else $error("command pulse wider than one cycle");
endmodule