ACK Generation

// ─────────────────────────────────────────────────────────────────────────
// wb_read_ack_comb — combinational read response.
//
// PURPOSE. The shape Chapters 6.1 and 6.3 have used, stated minimally so
// its timing structure is visible. ack_o and dat_o are produced by the same
// combinational logic in the same cycle, which is what makes them coherent
// by construction: there is no stored state that could disagree.
//
// PERMISSION 3.30 allows the combinatorial STB_I -> ACK_O path directly.
// OBSERVATION 3.40 credits it with one data transfer per clock cycle.
// OBSERVATION 3.50 names its cost: the master-to-slave-and-back loopback.
//
// Reset: SYNCHRONOUS, ACTIVE HIGH (RULES 2.30, 3.00).
// ─────────────────────────────────────────────────────────────────────────
module wb_read_ack_comb #(
  parameter int unsigned OFF_AW = 3,
  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 [OFF_AW-1:0] adr_i,
  output logic [DW-1:0]     dat_o,
  output logic              ack_o,
  output logic              err_o,
  input  logic [DW-1:0]     input_data_i,
  input  logic [7:0]        flags_i
);
  logic [DW-1:0] count_q;

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

  logic [DW-1:0] mux_value;
  logic          known_off;
  wb_read_mux #(.OFF_AW(OFF_AW), .DW(DW)) u_mux (
    .off_i(adr_i),
    .status_i({24'd0, flags_i}),
    .count_i(count_q),
    .ctrl_i('0),
    .input_data_i(input_data_i),
    .value_o(mux_value),
    .known_o(known_off)
  );

  // ── COHERENT BY CONSTRUCTION ──────────────────────────────────────────
  // Both outputs derive from the SAME combinational inputs in the SAME
  // cycle. There is no way for the acknowledge to describe a different
  // request than the data does, because neither is remembered.
  assign err_o = xfer & (~known_off | we_i);
  assign ack_o = xfer &   known_off & ~we_i;
  assign dat_o = ack_o ? mux_value : '0;        // RULE 3.65

  always_ff @(posedge clk_i) begin
    if (rst_i) count_q <= '0;
    else       count_q <= count_q + 32'd1;
  end
endmodule

// ─────────────────────────────────────────────────────────────────────────
// wb_read_ack_reg — registered read response, done correctly.
//
// PURPOSE. Break the combinational loopback by putting a flop between the
// request and the response. The cost is one cycle per read. The NEW
// obligation — and the whole reason this module is longer than the
// combinational one — is that a registered response must REMEMBER WHAT IT
// IS ANSWERING.
//
// A combinational slave cannot get the context wrong because it holds no
// context. This one holds an offset, and if that offset and the returned
// data ever disagree, the master captures a coherent-looking wrong value.
//
// Reset: SYNCHRONOUS, ACTIVE HIGH (RULES 2.30, 3.00).
// ─────────────────────────────────────────────────────────────────────────
module wb_read_ack_reg #(
  parameter int unsigned OFF_AW = 3,
  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 [OFF_AW-1:0] adr_i,
  output logic [DW-1:0]     dat_o,
  output logic              ack_o,
  output logic              err_o,
  input  logic [DW-1:0]     input_data_i,
  input  logic [7:0]        flags_i
);
  logic [DW-1:0] count_q;

  logic xfer;
  assign xfer = cyc_i & stb_i;

  // ── CAPTURED REQUEST CONTEXT ──────────────────────────────────────────
  // pend_q says a response is owed. off_q remembers WHICH offset it is
  // owed for. Both are loaded from the same cycle's inputs, so they cannot
  // describe different requests.
  logic                  pend_q;
  logic [OFF_AW-1:0]     off_q;
  logic                  was_read_q;

  // ── THE RESPONSE ──────────────────────────────────────────────────────
  // The multiplexer is driven by off_q — the REMEMBERED offset — not by
  // adr_i. That single choice is the correctness of this module:
  //
  //   driven by off_q : the data matches the request being answered
  //   driven by adr_i : the data matches whatever is on the bus NOW
  //
  // With a well-behaved master the two are identical, because RULE 3.60
  // requires the address to hold still. Driving from off_q means this
  // slave stays coherent even against a master that violates it — and,
  // more importantly, it is coherent BY CONSTRUCTION rather than by
  // relying on someone else's conformance.
  logic [DW-1:0] mux_value;
  logic          known_off;
  wb_read_mux #(.OFF_AW(OFF_AW), .DW(DW)) u_mux (
    .off_i(off_q),
    .status_i({24'd0, flags_i}),
    .count_i(count_q),
    .ctrl_i('0),
    .input_data_i(input_data_i),
    .value_o(mux_value),
    .known_o(known_off)
  );

  // The termination is asserted only while a response is pending AND the
  // master is still presenting a transfer. The second term matters: if the
  // master somehow withdrew, this slave must not terminate into a bus that
  // is no longer asking (RULES 3.30, 3.35).
  assign ack_o = pend_q & xfer &  known_off & ~was_read_q ? 1'b0 :
                 pend_q & xfer &  known_off &  was_read_q;
  assign err_o = pend_q & xfer & (~known_off | ~was_read_q);
  assign dat_o = ack_o ? mux_value : '0;        // RULE 3.65

  always_ff @(posedge clk_i) begin
    if (rst_i) begin
      pend_q     <= 1'b0;
      off_q      <= '0;
      was_read_q <= 1'b0;
      count_q    <= '0;
    end else begin
      count_q <= count_q + 32'd1;

      if (!pend_q) begin
        // Capture the request. From here the response is determined by
        // off_q alone, regardless of what the bus does next.
        if (xfer) begin
          pend_q     <= 1'b1;
          off_q      <= adr_i;
          was_read_q <= ~we_i;
        end
      end else begin
        // The response was presented this cycle. Clear the pending flag so
        // a held strobe cannot produce a second acknowledge for the same
        // request — and clear it too if the master withdrew, so a stale
        // response cannot outlive its transfer (RULE 3.50).
        pend_q <= 1'b0;
      end
    end
  end
endmodule

master flop → decode → slave mux → DAT_O gate → response merge → master flop

master flop → decode → slave flop          (leg 1)
slave flop  → mux → gate → merge → master flop   (leg 2)

// ─────────────────────────────────────────────────────────────────────────
// wb_read_ack_stale — THE LOST-CONTEXT BUG, isolated for simulation.
//
// NOT A REFERENCE DESIGN. Identical to wb_read_ack_reg except for ONE
// port connection: the read multiplexer is driven from adr_i — the bus
// address RIGHT NOW — instead of from off_q, the remembered offset.
//
// Against a conformant master the two are the same, because RULE 3.60
// requires ADR_O to hold still for the transfer's duration. The bug is
// therefore INVISIBLE in a well-behaved system.
//
// It appears the moment the address moves during an outstanding read —
// which Chapter 6.2 showed a walking master doing — and it converts that
// master's bug into a COHERENT-LOOKING wrong answer: the slave
// acknowledges, and the data it returns belongs to a different register
// than the one the transfer was for.
// ─────────────────────────────────────────────────────────────────────────
module wb_read_ack_stale #(
  parameter int unsigned OFF_AW = 3,
  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 [OFF_AW-1:0] adr_i,
  output logic [DW-1:0]     dat_o,
  output logic              ack_o,
  output logic              err_o,
  input  logic [DW-1:0]     input_data_i,
  input  logic [7:0]        flags_i
);
  logic [DW-1:0] count_q;
  logic xfer; assign xfer = cyc_i & stb_i;

  logic              pend_q;
  logic [OFF_AW-1:0] off_q;
  logic              was_read_q;

  logic [DW-1:0] mux_value;
  logic          known_off;
  // ── THE BUG: off_i is adr_i, not off_q ────────────────────────────────
  wb_read_mux #(.OFF_AW(OFF_AW), .DW(DW)) u_mux (
    .off_i(adr_i),                              // <-- should be off_q
    .status_i({24'd0, flags_i}),
    .count_i(count_q),
    .ctrl_i('0),
    .input_data_i(input_data_i),
    .value_o(mux_value),
    .known_o(known_off)
  );

  assign ack_o = pend_q & xfer & known_off & was_read_q;
  assign err_o = pend_q & xfer & (~known_off | ~was_read_q);
  assign dat_o = ack_o ? mux_value : '0;

  always_ff @(posedge clk_i) begin
    if (rst_i) begin
      pend_q <= 1'b0; off_q <= '0; was_read_q <= 1'b0; count_q <= '0;
    end else begin
      count_q <= count_q + 32'd1;
      if (!pend_q) begin
        if (xfer) begin
          pend_q <= 1'b1; off_q <= adr_i; was_read_q <= ~we_i;
        end
      end else begin
        pend_q <= 1'b0;
      end
    end
  end
endmodule

  === SIMULATION - combinational vs registered read response ===
                                   combinational   registered
    reads issued                         5             5
    total busy cycles                    5            10
    cycles per read                      1             2
    STATUS      (0x000000a5)        0x000000a5    0x000000a5
    COUNT       (moving)            0x00000007    0x00000008
    INPUT_DATA  (0xcafebabe)        0xcafebabe    0xcafebabe
    ID          (0x57420601)        0x57420601    0x57420601
    values matching expectation          4/4           4/4

  === lost context + walking address ===
    requested word                        3  (INPUT_DATA = 0xcafebabe)
    slave's remembered offset             3
    slave's mux input at ACK              4
    value returned                0x57420601
    terminated with                      ACK

// ─────────────────────────────────────────────────────────────────────────
// wb_read_ack_checker — read-side termination properties.
//
// P1 and P2 are SPECIFICATION (RULES 3.35 and 3.50). P3 is a DESIGN
// OBLIGATION that only EXISTS for a registered slave — a combinational one
// holds no context and cannot violate it. That is worth noting: choosing a
// registered response adds a property to the verification plan.
// ─────────────────────────────────────────────────────────────────────────
module wb_read_ack_checker #(
  parameter int unsigned OFF_AW = 3,
  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 [OFF_AW-1:0] adr_i,
  input logic              ack_o,
  input logic              err_o,
  input logic [DW-1:0]     dat_o,
  // white-box, registered slaves only
  input logic              pend_q,
  input logic [OFF_AW-1:0] off_q,
  input logic [OFF_AW-1:0] mux_off       // what the mux is actually indexing
);
  default disable iff (rst_i);

  // P1 — SPECIFICATION (RULE 3.35). The termination is a response to a
  //      qualified transfer. Catches a tied-high ACK_O, one derived from
  //      STB_I alone, and a registered response that outlives its request.
  property p_ack_is_a_response;
    @(posedge clk_i) (ack_o || err_o) |-> (cyc_i && stb_i);
  endproperty
  a_ack_is_a_response : assert property (p_ack_is_a_response)
    else $error("RULE 3.35: termination asserted without CYC_I & STB_I");

  // P2 — SPECIFICATION (RULE 3.50, OBSERVATION 3.10). Terminations are
  //      negated in response to STB_I negating. Contrapositive form.
  property p_ack_negates_with_stb;
    @(posedge clk_i) !stb_i |-> (!ack_o && !err_o);
  endproperty
  a_ack_negates_with_stb : assert property (p_ack_negates_with_stb)
    else $error("RULE 3.50: termination asserted with STB_I negated");

  // P3 — DESIGN OBLIGATION, REGISTERED SLAVES ONLY. The data returned
  //      describes the request being answered. Stated as: while a response
  //      is pending, the multiplexer indexes the REMEMBERED offset.
  //
  //      This property has no meaning for a combinational slave, which has
  //      no off_q to compare against. Adding a register to break a timing
  //      path therefore ADDS a correctness obligation — a trade worth
  //      making deliberately rather than by habit.
  property p_response_matches_request;
    @(posedge clk_i) (pend_q && ack_o) |-> (mux_off == off_q);
  endproperty
  a_response_matches_request : assert property (p_response_matches_request)
    else $error("registered response answered from the wrong offset");

  // P4 — SPECIFICATION (RULE 3.65), restated for the read path: no
  //      termination, no data. Protects the shared return path.
  property p_data_qualified;
    @(posedge clk_i) (!ack_o && !err_o) |-> (dat_o == '0);
  endproperty
  a_data_qualified : assert property (p_data_qualified)
    else $error("RULE 3.65: read data driven without a termination");
endmodule