ACK — Acknowledge

if (active_q && ack_i)  begin ... end     // correct: a level, per transfer
if ($rose(ack_i))       begin ... end     // wrong: assumes a gap

// ─────────────────────────────────────────────────────────────────────────
// wb_ack_fast_slave — the PERMISSION 3.10 slave, exactly.
//
//   PERMISSION 3.10 — "If the SLAVE guarantees it can keep pace with all
//   MASTER interfaces and if the [ERR_I] and [RTY_I] signals are not used,
//   then the SLAVE's [ACK_O] signal MAY be tied to the logical AND of the
//   SLAVE's [STB_I] and [CYC_I] inputs."
//
// Both preconditions hold here: it never waits, and it has no ERR_O/RTY_O.
// Adding an error output would move it under PERMISSION 3.15 instead.
//
// Against a master that holds STB_O across transfers, this slave's ACK_O
// NEVER FALLS. That is conformant (PERMISSION 3.35) and is what RULE 3.55
// requires masters to tolerate.
//
// Reset: SYNCHRONOUS, ACTIVE HIGH (RULES 2.30, 3.00).
// ─────────────────────────────────────────────────────────────────────────
module wb_ack_fast_slave #(
  parameter int unsigned OFF_AW = 4,
  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 [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 [7:0]        accepts_o        // side-effect count, for QA
);
  localparam int unsigned NL = DW/8;
  logic [DW-1:0] mem_q [16];

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

  // PERMISSION 3.10, literally. Note this is NOT ack_o = 1'b1: a tied-high
  // acknowledge would terminate transfers never presented to this slave,
  // violating RULE 3.35 — the distinction Chapter 5.1 Section 1 drew.
  assign ack_o = xfer;

  // Accepted == presented here, because this slave never waits. The ack_o
  // term is still written explicitly, for the reason Chapter 5.3 gave: it
  // is redundant now and load-bearing the moment a wait state appears.
  logic write_ok;
  assign write_ok = xfer & we_i & ack_o;

  always_ff @(posedge clk_i) begin
    if (rst_i) begin
      for (int unsigned i = 0; i < 16; i++) mem_q[i] <= '0;
      accepts_o <= '0;
    end else if (write_ok) begin
      for (int unsigned n = 0; n < NL; n++) begin
        if (sel_i[n]) mem_q[adr_i][n*8 +: 8] <= dat_i[n*8 +: 8];
      end
      accepts_o <= accepts_o + 8'd1;
    end
  end

  always_comb begin
    dat_o = '0;                              // RULE 3.65
    if (xfer && !we_i && ack_o) dat_o = mem_q[adr_i];
  end
endmodule

// ─────────────────────────────────────────────────────────────────────────
// wb_ack_block_master — holds STB_O across N transfers and counts
// terminations by LEVEL. This is the RULE 3.55-compliant shape.
//
// It exists to be pointed at wb_ack_fast_slave, where ACK_I is asserted
// continuously and never falls. Counting levels gets N; counting edges
// gets 1. The two differ by one line, and Section 7 simulates both.
//
// SCOPE NOTE. Holding STB_O across several transfers is a BLOCK cycle and
// Module 8 owns it properly. It appears here only because it is the
// simplest construction that makes ACK_I stay asserted, which is what
// RULE 3.55 is about.
//
// Reset: SYNCHRONOUS, ACTIVE HIGH (RULES 2.30, 3.00, 3.20).
// ─────────────────────────────────────────────────────────────────────────
module wb_ack_block_master #(
  parameter int unsigned AW = 30,
  parameter int unsigned DW = 32,
  parameter int unsigned CW = 8
) (
  input  logic            clk_i,
  input  logic            rst_i,

  input  logic            req_i,
  input  logic [AW-1:0]   base_i,
  input  logic [CW-1:0]   count_i,
  output logic            done_o,
  output logic [CW-1:0]   acked_o,           // transfers completed
  output logic [DW-1:0]   last_dat_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,
  output logic [DW/8-1:0] sel_o,
  input  logic [DW-1:0]   dat_i,
  input  logic            ack_i,
  input  logic            err_i,
  input  logic            rty_i
);
  logic          active_q;
  logic [AW-1:0] adr_q;
  logic [CW-1:0] left_q;

  assign cyc_o = active_q;                   // RULE 3.25: spans the block
  assign stb_o = active_q;                   // held across all transfers
  assign we_o  = 1'b0;                       // read block
  assign adr_o = adr_q;
  assign dat_o = '0;
  assign sel_o = '1;

  always_ff @(posedge clk_i) begin
    if (rst_i) begin
      active_q   <= 1'b0;                    // RULE 3.20
      adr_q      <= '0;
      left_q     <= '0;
      acked_o    <= '0;
      last_dat_o <= '0;
      done_o     <= 1'b0;
    end else begin
      done_o <= 1'b0;

      if (!active_q) begin
        if (req_i && (count_i != '0)) begin
          active_q <= 1'b1;
          adr_q    <= base_i;
          left_q   <= count_i;
          acked_o  <= '0;
        end
      end else if (ack_i) begin
        // ── RULE 3.55 COMPLIANCE, IN ONE LINE ─────────────────────────
        // ack_i is read as a LEVEL, every cycle the transfer is presented.
        // Nothing here asks whether it CHANGED, so a slave holding it
        // asserted across all N transfers is counted correctly.
        //
        // The bug this avoids:   if ($rose(ack_i)) ...
        // which sees one acknowledge instead of N and never finishes.
        last_dat_o <= dat_i;                 // RULE 3.65 window
        acked_o    <= acked_o + CW'(1);
        if (left_q == CW'(1)) begin
          active_q <= 1'b0;                  // last transfer: release
          done_o   <= 1'b1;
        end else begin
          left_q <= left_q - CW'(1);
          adr_q  <= adr_q + AW'(1);
        end
      end else if (err_i || rty_i) begin
        active_q <= 1'b0;
        done_o   <= 1'b1;
      end
    end
  end
endmodule

// ─────────────────────────────────────────────────────────────────────────
// wb_ack_edge_master — THE RULE 3.55 VIOLATION, isolated.
//
// NOT A REFERENCE DESIGN. Identical to wb_ack_block_master except that it
// advances on a RISING EDGE of ack_i instead of on the level. Against a
// slave that ever negates ACK_I between transfers it works perfectly.
// Against wb_ack_fast_slave it stalls after one transfer, with STB_O and
// ACK_I both asserted — a waveform that looks like success.
// ─────────────────────────────────────────────────────────────────────────
module wb_ack_edge_master #(
  parameter int unsigned AW = 30,
  parameter int unsigned DW = 32,
  parameter int unsigned CW = 8
) (
  input  logic            clk_i,
  input  logic            rst_i,
  input  logic            req_i,
  input  logic [AW-1:0]   base_i,
  input  logic [CW-1:0]   count_i,
  output logic            done_o,
  output logic [CW-1:0]   acked_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,
  output logic [DW/8-1:0] sel_o,
  input  logic [DW-1:0]   dat_i,
  input  logic            ack_i,
  input  logic            err_i,
  input  logic            rty_i
);
  logic          active_q;
  logic [AW-1:0] adr_q;
  logic [CW-1:0] left_q;
  logic          ack_q;                      // previous ack_i

  assign cyc_o = active_q;
  assign stb_o = active_q;
  assign we_o  = 1'b0;
  assign adr_o = adr_q;
  assign dat_o = '0;
  assign sel_o = '1;

  // ── THE BUG ───────────────────────────────────────────────────────────
  // A rising edge of ack_i. RULE 3.55 requires a master to operate normally
  // when a slave HOLDS ACK_I asserted; this one cannot, because a held
  // acknowledge produces exactly one rising edge no matter how many
  // transfers complete.
  logic ack_rise;
  assign ack_rise = ack_i & ~ack_q;

  always_ff @(posedge clk_i) begin
    if (rst_i) begin
      active_q <= 1'b0;
      adr_q    <= '0;
      left_q   <= '0;
      ack_q    <= 1'b0;
      acked_o  <= '0;
      done_o   <= 1'b0;
    end else begin
      done_o <= 1'b0;
      ack_q  <= ack_i;

      if (!active_q) begin
        if (req_i && (count_i != '0)) begin
          active_q <= 1'b1;
          adr_q    <= base_i;
          left_q   <= count_i;
          acked_o  <= '0;
        end
      end else if (ack_rise) begin
        acked_o <= acked_o + CW'(1);
        if (left_q == CW'(1)) begin
          active_q <= 1'b0;
          done_o   <= 1'b1;
        end else begin
          left_q <= left_q - CW'(1);
          adr_q  <= adr_q + AW'(1);
        end
      end else if (err_i || rty_i) begin
        active_q <= 1'b0;
        done_o   <= 1'b1;
      end
    end
  end
endmodule

                              level      edge
  transfers requested          3          3
  cycles CYC&STB&ACK true      3          40
  rising edges on ACK_I        1          1
  TRANSFERS COUNTED            3          1
  completed                   yes        STALLED
  slave still presenting?     no         yes

// ─────────────────────────────────────────────────────────────────────────
// wb_ack_checker — acknowledge properties, both sides.
//
// P1 and P2 are SPECIFICATION (RULES 3.35 and 3.50). P3 is also
// SPECIFICATION — from RULE 3.55 — but is a LIVENESS property about the
// MASTER'S BEHAVIOUR rather than a constraint on any wire, which is why it
// needs a white-box progress signal. P4 is LOCAL POLICY.
// ─────────────────────────────────────────────────────────────────────────
module wb_ack_checker (
  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 m_progress     // white-box: master advanced a transfer
);
  default disable iff (rst_i);

  // P1 — SPECIFICATION (RULE 3.35). The acknowledge is a RESPONSE: it may
  //      only be asserted when the transfer provoking it is present.
  //      Catches a tied-high ACK_O and one derived from STB_I alone.
  property p_ack_is_a_response;
    @(posedge clk_i) ack_o |-> (cyc_i && stb_i);
  endproperty
  a_ack_is_a_response : assert property (p_ack_is_a_response)
    else $error("RULE 3.35: ACK_O asserted without CYC_I & STB_I");

  // P2 — SPECIFICATION (RULE 3.50, OBSERVATION 3.10). Terminations are
  //      negated in response to the negation of STB_I.
  property p_ack_negates_with_stb;
    @(posedge clk_i) !stb_i |-> !ack_o;
  endproperty
  a_ack_negates_with_stb : assert property (p_ack_negates_with_stb)
    else $error("RULE 3.50: ACK_O still asserted after STB_I negated");

  // P3 — SPECIFICATION (RULE 3.55), as LIVENESS. If a transfer is
  //      presented and acknowledged, the master MUST make progress.
  //
  //      This is the ONLY way to catch edge detection. During the failure
  //      every bus signal is legal — qualifiers asserted, acknowledge
  //      asserted, all rules satisfied — and what is wrong is that nothing
  //      happens. "Nothing happens" is not a signal, so the property needs
  //      to see inside the master.
  property p_master_progresses_on_held_ack;
    @(posedge clk_i) (cyc_i && stb_i && ack_o) |-> m_progress;
  endproperty
  a_master_progresses_on_held_ack :
    assert property (p_master_progresses_on_held_ack)
    else $error("RULE 3.55: master did not advance on an asserted ACK_I");

  // P4 — LOCAL POLICY. The three terminations are mutually exclusive.
  //      RULE 3.45 makes this SPECIFICATION for any slave that supports
  //      ERR_O or RTY_O; wb_ack_fast_slave supports neither, so for THIS
  //      slave it is trivially true rather than a constraint. Kept so the
  //      checker can be reused against slaves that do.
  property p_terminations_exclusive;
    @(posedge clk_i) (int'(ack_o) + int'(err_o) + int'(rty_o)) <= 1;
  endproperty
  a_terminations_exclusive : assert property (p_terminations_exclusive)
    else $error("RULE 3.45: more than one termination asserted");
endmodule