Arbitration Logic

Chapter 17.4 finished the last of the policy questions. Four chapters have shown pieces; none has shown how they go together without the policy reaching somewhere it should not.

How is arbitration logic built so that it stays correct under real transfer timing?

1. The Five Stages

Written as a pipeline, arbitration logic is five stages and the boundaries matter more than the stages.

The guard between stages three and four is the entire safety property. Remove it and the policy's combinational output drives the owner directly, which is Chapter 17.1 §5's defect and Chapter 16.3's before that.

The boundary between stages two and three is what makes the policy replaceable. wb_arb_policy has one output the owner register reads and one input — commit_i — telling it a grant was taken. Nothing else crosses.

2. RTL — The System

Three requesters, one arbitrating interconnect, one address split, one shared RAM and one DMA whose registers are a slave on that same shared path.

Four of the modules below are Module 16's, reused unchanged and not re-taught here: wb_cpu_master and wb_teaching_dma from Chapter 16.1, wb_split2 and wb_shared_ram from Chapter 16.4. The IO master is a second instance of wb_cpu_master — a third requester needed no new master, only a second copy of one.

// ─────────────────────────────────────────────────────────────────────────
// m17_system — Chapter 16.2's system, with a third requester and an
// arbitrating interconnect.
//
//   CPU master ─┐                        ┌─ shared RAM      0x000..0x0FF
//   DMA master ─┼─ wb_owner_arb3 ─ wb_split2
//   IO  master ─┘    (wb_arb_policy)     └─ DMA config regs 0x800..0x803
//
// Everything except the interconnect is Module 16's published RTL, reused
// unchanged: wb_cpu_master and wb_teaching_dma from Chapter 16.1,
// wb_split2 and wb_shared_ram from Chapter 16.4. The IO master is a second
// instance of wb_cpu_master - a third requester needs no new master, only
// a second copy of an existing one.
//
// WHY THREE. Chapter 17.1 measures a two-master system under sustained
// demand and finds zero contested arbitration events, because an event
// fires when the owner negates CYC_O and that master is then not asking.
// A contested decision needs a requester that is neither the owner nor the
// cause of the event.
//
// WORD ADDRESSES throughout - adr[11:0] selects a 32-bit word, never a
// byte. adr[11] chooses the RAM from the DMA's configuration registers.
// ─────────────────────────────────────────────────────────────────────────
module m17_system #(
  parameter int unsigned AW                 = 12,
  parameter int unsigned DW                 = 32,
  parameter int unsigned SW                 = DW/8,
  parameter int unsigned RAM_WAITS          = 0,
  parameter bit          POLICY             = 1'b0,  // 0 fixed, 1 round robin
  parameter bit          PREEMPT            = 1'b0,
  parameter bit          PTR_ON_REQUEST     = 1'b0,
  parameter bit          IGNORE_ELIGIBILITY = 1'b0
) (
  input  logic          clk_i,
  input  logic          rst_i,
  // CPU client contract - LOCAL, not Wishbone
  input  logic          cpu_req_i, cpu_we_i, cpu_lock_i, cpu_hold_i,
  input  logic [AW-1:0] cpu_adr_i,
  input  logic [DW-1:0] cpu_dat_i,
  input  logic [SW-1:0] cpu_sel_i,
  output logic          cpu_busy_o, cpu_done_o, cpu_ok_o,
  output logic [DW-1:0] cpu_rdat_o,
  // IO client contract
  input  logic          io_req_i, io_we_i, io_hold_i,
  input  logic [AW-1:0] io_adr_i,
  input  logic [DW-1:0] io_dat_i,
  output logic          io_busy_o, io_done_o, io_ok_o,
  output logic [DW-1:0] io_rdat_o,
  input  logic          ram_busy_i,
  // DMA observation
  output logic          dma_busy_o, dma_done_o, dma_failed_o,
  output logic [15:0]   dma_words_o, ram_writes_o,
  // master ports, for the monitors
  output logic          m0_cyc_o, m0_stb_o, m0_we_o, m0_ack_o,
  output logic [AW-1:0] m0_adr_o,
  output logic [DW-1:0] m0_dat_o,
  output logic [SW-1:0] m0_sel_o,
  output logic          m0_err_o, m0_rty_o,
  output logic          m1_cyc_o, m1_stb_o, m1_we_o, m1_ack_o,
  output logic [AW-1:0] m1_adr_o,
  output logic [DW-1:0] m1_dat_o,
  output logic [SW-1:0] m1_sel_o,
  output logic          m1_err_o, m1_rty_o,
  output logic          m2_cyc_o, m2_stb_o, m2_we_o, m2_ack_o,
  output logic [AW-1:0] m2_adr_o,
  output logic [DW-1:0] m2_dat_o,
  output logic [SW-1:0] m2_sel_o,
  output logic          m2_err_o, m2_rty_o,
  // shared downstream path
  output logic          s_cyc_o, s_stb_o, s_we_o, s_lock_o,
  output logic          s_ack_o, s_err_o, s_rty_o,
  output logic [AW-1:0] s_adr_o,
  output logic [DW-1:0] s_dat_o, s_rdat_o,
  output logic [SW-1:0] s_sel_o,
  output logic [1:0]    owner_o,
  // the arbitration event
  output logic [2:0]    elig_o,
  output logic          arb_event_o, commit_o,
  output logic [1:0]    grant_o, hist_o
);
  logic [DW-1:0] m0_rd, m1_rd, m2_rd;
  logic          m0_lock, m1_lock, m2_lock;
  logic          cpu_xe, cpu_xr, io_xe, io_xr;

  // ── requester 0: the CPU (Chapter 16.1, unchanged) ──
  wb_cpu_master #(.AW(AW), .DW(DW), .SW(SW)) u_cpu (
    .clk_i(clk_i), .rst_i(rst_i),
    .req_i(cpu_req_i), .req_we_i(cpu_we_i), .req_adr_i(cpu_adr_i),
    .req_dat_i(cpu_dat_i), .req_sel_i(cpu_sel_i), .req_lock_i(cpu_lock_i),
    .hold_i(cpu_hold_i),
    .busy_o(cpu_busy_o), .done_o(cpu_done_o), .ok_o(cpu_ok_o),
    .err_o(cpu_xe), .rty_o(cpu_xr), .rdat_o(cpu_rdat_o),
    .cyc_o(m0_cyc_o), .stb_o(m0_stb_o), .lock_o(m0_lock), .we_o(m0_we_o),
    .adr_o(m0_adr_o), .dat_o(m0_dat_o), .sel_o(m0_sel_o),
    .dat_i(m0_rd), .ack_i(m0_ack_o), .err_i(m0_err_o), .rty_i(m0_rty_o));

  // ── requester 1: the DMA (Chapter 16.1, unchanged) ──
  logic          cfg_cyc, cfg_stb, cfg_we;
  logic [AW-1:0] cfg_adr;
  logic [DW-1:0] cfg_dat, cfg_rdat;
  logic          cfg_ack, cfg_err;

  wb_teaching_dma #(.AW(AW), .DW(DW), .SW(SW)) u_dma (
    .clk_i(clk_i), .rst_i(rst_i),
    .c_cyc_i(cfg_cyc), .c_stb_i(cfg_stb), .c_we_i(cfg_we),
    .c_adr_i(cfg_adr[1:0]), .c_dat_i(cfg_dat),
    .c_dat_o(cfg_rdat), .c_ack_o(cfg_ack), .c_err_o(cfg_err),
    .cyc_o(m1_cyc_o), .stb_o(m1_stb_o), .lock_o(m1_lock), .we_o(m1_we_o),
    .adr_o(m1_adr_o), .dat_o(m1_dat_o), .sel_o(m1_sel_o),
    .dat_i(m1_rd), .ack_i(m1_ack_o), .err_i(m1_err_o), .rty_i(m1_rty_o),
    .busy_o(dma_busy_o), .done_o(dma_done_o), .failed_o(dma_failed_o),
    .words_done_o(dma_words_o));

  // ── requester 2: the IO engine, a second wb_cpu_master ──
  wb_cpu_master #(.AW(AW), .DW(DW), .SW(SW)) u_io (
    .clk_i(clk_i), .rst_i(rst_i),
    .req_i(io_req_i), .req_we_i(io_we_i), .req_adr_i(io_adr_i),
    .req_dat_i(io_dat_i), .req_sel_i({SW{1'b1}}), .req_lock_i(1'b0),
    .hold_i(io_hold_i),
    .busy_o(io_busy_o), .done_o(io_done_o), .ok_o(io_ok_o),
    .err_o(io_xe), .rty_o(io_xr), .rdat_o(io_rdat_o),
    .cyc_o(m2_cyc_o), .stb_o(m2_stb_o), .lock_o(m2_lock), .we_o(m2_we_o),
    .adr_o(m2_adr_o), .dat_o(m2_dat_o), .sel_o(m2_sel_o),
    .dat_i(m2_rd), .ack_i(m2_ack_o), .err_i(m2_err_o), .rty_i(m2_rty_o));

  // ── the arbitrating interconnect ──
  logic          s_cyc, s_stb, s_lock, s_we;
  logic [AW-1:0] s_adr;
  logic [DW-1:0] s_dat, s_rdat;
  logic [SW-1:0] s_sel;
  logic          s_ack, s_err, s_rty;

  wb_owner_arb3 #(
    .AW(AW), .DW(DW), .SW(SW), .POLICY(POLICY), .PREEMPT(PREEMPT),
    .PTR_ON_REQUEST(PTR_ON_REQUEST),
    .IGNORE_ELIGIBILITY(IGNORE_ELIGIBILITY)
  ) u_arb (
    .clk_i(clk_i), .rst_i(rst_i),
    .m0_cyc_i(m0_cyc_o), .m0_stb_i(m0_stb_o), .m0_lock_i(m0_lock),
    .m0_we_i(m0_we_o), .m0_adr_i(m0_adr_o), .m0_dat_i(m0_dat_o),
    .m0_sel_i(m0_sel_o), .m0_dat_o(m0_rd), .m0_ack_o(m0_ack_o),
    .m0_err_o(m0_err_o), .m0_rty_o(m0_rty_o),
    .m1_cyc_i(m1_cyc_o), .m1_stb_i(m1_stb_o), .m1_lock_i(m1_lock),
    .m1_we_i(m1_we_o), .m1_adr_i(m1_adr_o), .m1_dat_i(m1_dat_o),
    .m1_sel_i(m1_sel_o), .m1_dat_o(m1_rd), .m1_ack_o(m1_ack_o),
    .m1_err_o(m1_err_o), .m1_rty_o(m1_rty_o),
    .m2_cyc_i(m2_cyc_o), .m2_stb_i(m2_stb_o), .m2_lock_i(m2_lock),
    .m2_we_i(m2_we_o), .m2_adr_i(m2_adr_o), .m2_dat_i(m2_dat_o),
    .m2_sel_i(m2_sel_o), .m2_dat_o(m2_rd), .m2_ack_o(m2_ack_o),
    .m2_err_o(m2_err_o), .m2_rty_o(m2_rty_o),
    .s_cyc_o(s_cyc), .s_stb_o(s_stb), .s_lock_o(s_lock), .s_we_o(s_we),
    .s_adr_o(s_adr), .s_dat_o(s_dat), .s_sel_o(s_sel),
    .s_dat_i(s_rdat), .s_ack_i(s_ack), .s_err_i(s_err), .s_rty_i(s_rty),
    .owner_o(owner_o), .elig_o(elig_o), .arb_event_o(arb_event_o),
    .commit_o(commit_o), .grant_o(grant_o), .hist_o(hist_o));

  assign s_cyc_o = s_cyc;  assign s_stb_o = s_stb;  assign s_we_o = s_we;
  assign s_adr_o = s_adr;  assign s_dat_o = s_dat;  assign s_sel_o = s_sel;
  assign s_rdat_o = s_rdat; assign s_lock_o = s_lock;
  assign s_ack_o = s_ack;  assign s_err_o = s_err;  assign s_rty_o = s_rty;

  // ── downstream split (Chapter 16.4, unchanged) ──
  logic          r_cyc, r_stb, r_we;
  logic [AW-1:0] r_adr;
  logic [DW-1:0] r_dat, r_rdat;
  logic [SW-1:0] r_sel;
  logic          r_ack, r_rty;

  wb_split2 #(.AW(AW), .DW(DW), .SW(SW), .SEL_BIT(11)) u_dsplit (
    .m_cyc_i(s_cyc), .m_stb_i(s_stb), .m_lock_i(s_lock), .m_we_i(s_we),
    .m_adr_i(s_adr), .m_dat_i(s_dat), .m_sel_i(s_sel),
    .m_dat_o(s_rdat), .m_ack_o(s_ack), .m_err_o(s_err), .m_rty_o(s_rty),
    .a_cyc_o(r_cyc), .a_stb_o(r_stb), .a_lock_o(), .a_we_o(r_we),
    .a_adr_o(r_adr), .a_dat_o(r_dat), .a_sel_o(r_sel),
    .a_dat_i(r_rdat), .a_ack_i(r_ack), .a_err_i(1'b0), .a_rty_i(r_rty),
    .b_cyc_o(cfg_cyc), .b_stb_o(cfg_stb), .b_lock_o(), .b_we_o(cfg_we),
    .b_adr_o(cfg_adr), .b_dat_o(cfg_dat), .b_sel_o(),
    .b_dat_i(cfg_rdat), .b_ack_i(cfg_ack), .b_err_i(cfg_err),
    .b_rty_i(1'b0), .hit_b_o());

  wb_shared_ram #(.AW(AW), .DW(DW), .SW(SW), .WORDS(256), .WAITS(RAM_WAITS))
    u_ram (.clk_i(clk_i), .rst_i(rst_i), .cyc_i(r_cyc), .stb_i(r_stb),
           .we_i(r_we), .adr_i(r_adr), .dat_i(r_dat), .sel_i(r_sel),
           .busy_i(ram_busy_i), .dat_o(r_rdat), .ack_o(r_ack),
           .err_o(), .rty_o(r_rty), .writes_o(ram_writes_o));
endmodule

Reading it

The instance list is the argument. One wb_owner_arb3 sits between three master ports and the shared path; inside it, one wb_arb_policy. Everything below the arbiter is Module 16's system unchanged, which is what makes Section 3's comparison a controlled experiment rather than an impression.

POLICY is a parameter on the system and it reaches exactly one module. Nothing in the split, the RAM, the DMA or either master knows which policy is running. If changing it changed a bus invariant, the separation would be a lie, and Section 3 checks that it does not.

The address map is Chapter 16.2's, minus the private leg. adr[11] chooses the shared RAM from the DMA's configuration registers; there is no local split, because an arbitration study needs every access to cross the interconnect.

Here is the arbitration event, ten clocks of it, taken from the sustained-contention segment of Section 4's run:

Read the grant row against the arb event row. A grant is meaningful on three cycles out of ten. On the other seven the policy is still producing an output and nobody reads it — that is the guard, drawn.

Read the history row against the grant row one cycle earlier. History IO → grant CPU. History CPU → grant DMA. History DMA → grant IO. The scan starts one past the history, every time, and the history moves to the grant that was taken.

And read the owner row against the three CYC_O rows. At cycle 0 all of CPU and DMA are asking and the owner is still IO — the previous owner, whose CYC_O has just gone. Ownership is registered, so the grant taken at cycle 0 appears as an owner at cycle 1. That one-clock skew is the same one Chapter 16.2 measured as the structural cost of every acquisition.

The rows with no transition are the ones to notice. Cycles 1–3, 5–7: arb event low, owner unchanged, shared ACK arriving at the end of each. The IO master is asking throughout cycles 2 to 7 and is not selected, because no decision is being made. It is not losing. It is not being asked about.

3. Simulation — SIM I: The Same Stimulus, Two Policies

One client stimulus into two complete systems whose only difference is POLICY. If the separation in Section 1 is real, the service order changes and nothing else does.

  === SIM I - one client stimulus, two policies ===
    everything downstream of the owner register is identical.

    grant sequence
      fixed        CDCDCDCDCDCDCDCDCDCICIC
      round robin  ICDICDICDICDICDICDICDICD

    measure                          fixed  round robin
      arbitration events                53         53
      contested events                  19         23
      grants CPU                        22         18
      grants DMA                        16         15
      grants IO                          2          8
      longest run IO asked and lost     19          1
      DMA words copied                   8          7
      shared-bus ACKs                   40         40
      transfers with no owner            0          0
      non-owner terminations             0          0
      request context split              0          0
      owner changed mid-phase            0          0
      RULE 3.25 / 3.30 / 3.45         0/0/0      0/0/0

    -> the policy changed WHO ran. It changed nothing about
       what a Wishbone transfer is.

Reading it

The two grant sequences are different strings.

fixed        CDCDCDCDCDCDCDCDCDCICIC
round robin  ICDICDICDICDICDICDICDICD

Fixed priority alternates CPU and DMA and reaches the IO master twice, both times near the end when the others had finished. Round robin cycles all three. Grants to IO: 2 against 8. Longest run of IO asking and losing: 19 against 1.

Now the six rows underneath, which are the actual claim of this chapter.

Forty terminations under both policies, and every invariant clean under both. The arbitration policy changed who ran. It changed nothing whatsoever about what a Wishbone transfer is, which is what a replaceable policy is supposed to mean and what a parameter that leaked into the routing would have broken.

One number is not the same and should not be glossed over: DMA words copied, 8 against 7. The round-robin run did not finish the DMA's copy inside the window, because the IO master took six grants that fixed priority had given elsewhere. That is Chapter 17.3 §5 arriving in the system: equalising opportunities is not free, and the cost lands on whoever was previously winning. Neither column is "better" without a statement of what the system values.

4. Simulation — SIM J: The Integrated Audit

One deterministic trace through every situation this module has discussed, under round robin so the history is exercised, with two wait states so retention is exercised.

  === SIM J - integrated arbitration audit ===
    round robin, shared RAM with 2 wait states, all three
    requesters, every situation in one trace.

    ten clocks inside the sustained contention segment
      clk  I D C  event commit  history  grant  owner  STB ACK
      172  0 1 1    1     1      IO      CPU    IO     0   0
      173  0 1 1    0     0      CPU     -      CPU    1   0
      174  1 1 1    0     0      CPU     -      CPU    1   0
      175  1 1 1    0     0      CPU     -      CPU    1   1
      176  1 1 0    1     1      CPU     DMA    CPU    0   0
      177  1 1 0    0     0      DMA     -      DMA    1   0
      178  1 1 1    0     0      DMA     -      DMA    1   0
      179  1 1 1    0     0      DMA     -      DMA    1   1
      180  1 0 1    1     1      DMA     IO     DMA    0   0
      181  1 1 1    0     0      IO      -      IO     1   0
      history and owner use the same names; grant is the
      policy's choice and is meaningful only when commit is 1

    segment                             events  contested
      isolated CPU access                  4         0
      isolated IO access                   4         0
      simultaneous CPU and IO              6         1
      DMA running, CPU arrives mid-phase    28         0
      ERR from the DMA registers          16         0
      RTY from the shared RAM              7         0
      a locked CPU cycle, IO asking        5         0
      sustained three-way contention      41        26

    ARBITRATION AUDIT
      arbitration events                        112
      contested events                          27
      grants  CPU 23   DMA 22   IO 12
      grant to a requester that was not asking  0
      selection disagreed with reference model  0
      owner changed while a phase was unanswered 0
      longest losing run  CPU 1   DMA 1   IO 1

    BUS INVARIANTS (Chapter 16.3, three masters)
      transfer presented with no owner          0
      a master saw a termination it did not own 0
      shared request context split              0

    SPECIFICATION CONFORMANCE
      RULE 3.25  STB_O without CYC_O            0
      RULE 3.30  termination with CYC negated   0
      RULE 3.45  more than one termination      0
      terminations  ACK 55   ERR 1   RTY 1
      clocks LOCK_O was asserted downstream     3

    DMA words copied 6   failed 0   RAM writes 12

Reading it

The segment table is a coverage statement. Isolated access, isolated access by a different requester, simultaneous requests, a request arriving mid-phase, an ERR, an RTY, a locked cycle, and sustained three-way contention. Twenty-seven contested events out of 112 — the policy was genuinely asked to decide, twenty-seven times.

Read the three audits as three separate questions.

Arbitration. Grant to a requester that was not asking: 0. Selection disagreed with the reference model: 0. Owner changed while a phase was unanswered: 0. Longest losing run 1, 1, 1 — inside the structural bound of 2 for three requesters, on this trace.

Bus invariants — Chapter 16.3's three, restated for three masters. All zero. A policy change did not reintroduce a routing defect.

Specification conformance. RULE 3.25, RULE 3.30, RULE 3.45: all zero, across 55 ACKs, 1 ERR and 1 RTY. All three termination classes were exercised and all three routed to the owner.

clocks LOCK_O was asserted downstream: 3 — one locked three-clock phase, and Section 7 says exactly what it did and did not do.

The ERR and RTY rows are worth naming because neither is contrived. The ERR is the DMA's configuration slave refusing a write while its engine runs — Chapter 11.2's test, since the request is wrong for the device's state rather than deferred. The RTY is the shared RAM reporting its local resource busy, which is the specification's own example: "This signal is generally used for shared memory and bus bridges. In these cases SLAVE circuitry asserts [RTY_I] if the local resource is busy."

One thing the audit does not show, and it is deliberate. There is no row for "the arbiter violated a rule". There is no rule for it to violate, and Section 6 measures what that means.

5. The Negative-Control Gate

Four arbitration checkers against five arbiters. Three are broken by exactly one named term each; the fifth is correct fixed priority, and it is there for a reason Section 6 explains.

  === NEGATIVE-CONTROL GATE ===
    one stimulus, five arbiters. The first four are round robin;
    each broken rig differs from the correct one by one term.

    checker                      RR   preempt blind ptr-req  fixed
    NO PREEMPTION MID-TRANSFER  PASS   FAIL    PASS  PASS     PASS
    GRANT IMPLIES ELIGIBLE      PASS   PASS    FAIL  PASS     PASS
    SELECTION MATCHES POLICY    PASS   PASS    FAIL  FAIL     PASS
    LOSING RUN <= 2 (A1-A4)     PASS   PASS    PASS  PASS     FAIL

    The last column is CORRECT FIXED PRIORITY, not a defect.
    It is there because a bounded-wait property that no policy
    fails is not being checked. Fixed priority does not claim
    the property and must not pass the checker for it.

    raw counts      preempt  ineligible grant  wrong choice  worst run
      correct           0            0               0           2
      preempt          35            0               0           2
      blind rotation    0           22              22           2
      ptr on request    0            0               1           2

    ASSUMPTIONS BEHIND THE FOURTH CHECKER
      A1 every requester holds its request until served
      A2 the current owner eventually negates CYC_O
      A3 an arbitration event follows every release
      A4 the history is not reset between events
    Outside A1-A4 the bound is not claimed and is not checked.

    specification conformance, all five rigs
      rig            RULE 3.25  RULE 3.30  RULE 3.45
      correct             0          0          0
      preempt             0          0          0
      blind rotation      0          0          0
      ptr on request      0          0          0
      fixed priority      0          0          0
      -> every arbiter here is conformant, including the three
         that are wrong. B3 has no rule about selection.

    NEGATIVE-CONTROL CHECKERS REQUIRED:  >= 3
    CHECKERS PASS CORRECT DUT:           4/4
    CHECKERS FAIL TARGET BROKEN DUT:     3/3
      1 NO PREEMPTION MID-TRANSFER  <- PREEMPT
      2 GRANT IMPLIES ELIGIBLE      <- IGNORE_ELIGIBILITY
      3 SELECTION MATCHES POLICY    <- PTR_ON_REQUEST
    PROPERTY CHECKER VALIDATED AGAINST A POLICY THAT LACKS IT:
      4 LOSING RUN <= 2             <- fixed priority  PASS

Reading it

Three of the four rows are a clean diagonal, and the fourth is a different kind of entry entirely.

PREEMPT fails NO PREEMPTION MID-TRANSFER, 35 times. IGNORE_ELIGIBILITY fails GRANT IMPLIES ELIGIBLE, 22 times. PTR_ON_REQUEST fails SELECTION MATCHES POLICY — once.

Stop on that "once". One wrong choice, in a run with over a hundred arbitration events. A pointer that updates on the wrong event produced a system that agreed with the correct one 99% of the time, and it agreed on the service distribution, on the grant counts, and on every bus invariant. The only instrument that found it was a reference model that recomputed the decision independently. A service-distribution check would have passed it; so would a regression that counted grants.

That is the argument for reference models in one number. Chapter 17.2 §5 listed six ways a round-robin pointer goes wrong; this is what the first of them looks like from outside.

IGNORE_ELIGIBILITY failing two checkers is not a defect in the matrix. A policy that hands grants to absent requesters is both granting ineligibly and choosing wrongly. The requirement is that each checker fails for its intended reason, not that no checker ever overlaps.

The fourth row is the one that needed care. BOUNDED LOSING RUN is a property, not a defect check, and no broken rig violated it — the three defects happen not to produce a long denial. A property checker that nothing fails is not testing anything. So the fifth column is correct fixed priority, which does not claim the property and must not pass a checker for it. It fails, as it must.

Reporting that honestly matters. The gate says 3/3 broken DUTs caught — PREEMPT, IGNORE_ELIGIBILITY, PTR_ON_REQUEST — and reports the fourth checker separately as validated against a policy that lacks the property, not against a defect. Fixed priority is not broken. Calling it broken to make a matrix look symmetrical would be the same error as calling starvation a protocol violation.

6. Five Arbiters, and Nothing to Check Them Against

The bottom table is the most important result in Module 17.

RULE 3.25: 0. RULE 3.30: 0. RULE 3.45: 0. For all five.

Three of those arbiters are wrong. One displaces owners mid-transfer. One hands the shared path to masters that are not asking. One chooses the wrong requester. Every one of them satisfies every checkable rule in B3 completely.

This is not a gap in the monitor — those are the only rules there are. The specification describes a MASTER interface, a SLAVE interface, and what passes between them. It describes no arbiter, because it says so in as many words: "Arbitration methodology is defined by the end user." There is no rule an arbitration policy can violate, and the words fair, fairness, starve and starvation do not appear anywhere in the document.

So the practical statement for a design review is flat:

A Wishbone protocol checker cannot verify your arbiter. It will pass a preempting one, a blind-rotating one and a wrong-pointer one. The only instruments that find these are the ownership-aware and policy-aware ones — an event log, a reference model, a retention check and an eligibility check — and every one of them is something you build, because nothing in the specification asks for it.

Across Modules 9 to 17 the count of published defects a bus-level protocol checker would catch remains one — Chapter 10.2's ACK+ERR double termination.

7. Arbitration and LOCK_O

Module 15 established the semantics and they are not re-derived. What changes here is only the relationship to selection.

Ordinary ownership answers "who drives the bus now?". LOCK_O answers a different question — may the interconnect hand ownership to another master before this cycle ends? — in the words of its signal description:

Once the transfer has started, the INTERCON does not grant the bus to any other MASTER, until the current MASTER negates [LOCK_O] or [CYC_O].

That is the only sentence in B3 that constrains a grant decision, and it constrains retention rather than selection.

Under this module's retention rule the lock is structurally redundant, and the audit says so. An owner is held for the whole of its CYC_O, which already satisfies the requirement. SIM J asserted LOCK_O downstream for three clocks and nothing about the arbitration changed, because nothing could have. Chapter 15.4 measured the policy where the lock is load-bearing — one that re-evaluates ownership while an owner is idle mid-cycle — and that experiment is not rebuilt here.

What LOCK_O never does, in any policy:

The one design rule that follows: if your retention rule can release an owner mid-cycle, you need an explicit lock term; if it cannot, you do not. Knowing which kind you have is the question, and assuming either answer universally is how both mistakes get made.

8. Verification

Fourteen properties across two blocks, and the classification is the point.

Three of fourteen are spec-derived. Eleven are this system's policy. In Module 16 the ratio was four of thirteen; it has got worse, and it should have — an arbitration study is almost entirely local by construction, and inflating the specification's authority here would be the module's easiest mistake.

P12 is deliberately not written as an assertion. A bounded-losing-run property is a liveness claim conditional on four assumptions, and a clocked implication that looked like it would be worse than not writing one. It is checked procedurally instead, by wb_arb_probe's run counters, and Section 5's gate validates that checker against a policy that does not have the property.

SVA REVIEWED BY INSPECTION ONLY. Icarus Verilog does not execute concurrent assertions; the property file was run through iverilog -g2012 and rejected with "sorry: concurrent_assertion_item not supported". None of the fourteen was executed as an assertion. Every one has a named procedural equivalent that was executed: P2, P3, P4, P5, P6 and P7 are counters in wb_arb_probe; P8, P9, P10, P11, P13 and P14 are counters in wb_arb_bus_mon.

Elaboration is not synthesis. All published modules elaborate individually and together under iverilog -g2012 with no duplicate module names. Every always_comb assigns all of its outputs on every path, so none infers a latch; every output has one driver by inspection; and no combinational loop exists — one would not have produced eleven deterministic runs. No synthesis tool was run and no area, timing or frequency claim is made anywhere in this module.

9. Common Mistakes

"Priority logic can drive the owner mux directly."

Why it is dangerous: the policy is a pure function of the request lines, so the owner follows the request lines, so any arrival changes the owner — including during an unanswered phase. The PREEMPT rig is that design and it produced 35 mid-phase handovers.

"If the arbiter passes a protocol checker it is correct."

Why it is wrong: Section 6. Five arbiters, three of them broken, all conformant. There is no rule for an arbiter to break.

"Changing the arbitration policy is risky because it touches the bus."

Why it is wrong here, and worth generalising: if changing the policy can change a bus invariant, the policy is not separable and that is the defect. SIM I is the check: same ACKs, same invariants, different order.

"The reference model is redundant because we check the service distribution."

Why it is wrong: PTR_ON_REQUEST produced one wrong choice in over a hundred events, with a service distribution indistinguishable from correct. Aggregates hide single wrong decisions.

"LOCK_O gives a master higher priority."

Why it is wrong: it constrains whether an existing owner may be displaced. A waiting master asserting it gains nothing at all — it is not the owner, so there is nothing to protect.

"Our arbiter is fine, we ran it for a million cycles."

Why it is insufficient: how many of those were contested? Chapter 17.2 §4 measured a two-master system with twelve events and zero contested ones. A million uncontested events test eligibility, not selection.

10. Interview Reasoning

"Walk me through the stages of an arbiter."

Pending requests, selection, registered owner, retained ownership, release. Then the two boundaries: the policy is read only at an arbitration event, and the event fires only when nobody owns or the owner has released. Those two sentences are where every arbitration bug lives.

"Why keep the selection policy in a separate module?"

So it can be swapped and so it can be tested. Swapping it is a one-parameter experiment whose downstream invariants are provably unchanged; testing it needs no bus at all, which is how a three-requester eligibility trace was run at one decision per clock.

"How do you verify an arbiter?"

Four instruments, none of them a protocol checker. An event log — eligibility, history, choice, owner. A reference model that recomputes the choice independently. A retention check. An eligibility check on every grant. And then validate each of them against a deliberately broken arbiter, because a checker that has only ever passed has not been shown to check anything.

"What does LOCK_O change about arbitration?"

It constrains retention, not selection. It is the only sentence in B3 that constrains a grant decision, and under a retention rule that already holds an owner for the whole of its cycle, it is redundant — which is a statement about your policy, not about the signal.

"You are handed an arbiter and told it is round robin. What do you check first?"

Find the one line that writes the pointer and ask which event it is under. Then count contested events in the regression. Most round-robin bugs are in the update condition, and most round-robin test suites never contend.

11. Understanding Check

In the waveform, the IO master asserts CYC_O from cycle 2 and is not selected until cycle 8. Was it losing?

No — it was not being asked about. There was no arbitration event on cycles 1 to 3 or 5 to 7; the owner was retained. Losing requires an event at which you were eligible and not chosen, and there were two of those for IO, at cycles 0 and 4.

PTR_ON_REQUEST made one wrong choice in over a hundred events and passed every other checker. What does that tell you about your regression?

That an aggregate is not an invariant. Grant counts, service distribution and bus invariants were all indistinguishable from correct. Only a per-decision comparison found it.

SIM I shows 40 ACKs under both policies. Why does that number matter more than the grant counts?

Because it is the claim that the policy is separable. Different service order, identical transfer behaviour. If that number had moved, the policy parameter would have been reaching into the routing.

The bounded-losing-run checker passes all three broken arbiters. Is it a bad checker?

No — but it is untested by them, which is why the gate runs it against fixed priority, a correct policy that does not claim the property. A property checker must be shown to reject something, and the something does not have to be a defect.

12. What Module 17 Established

17.1 — selection, and when it happens. Three questions kept apart: eligibility, selection, retention. Fixed priority is a pure function with no memory, and priority is not preemption — the guard that makes that true is one term, and removing it produced 35 mid-phase handovers that corrupted nothing.

17.2 — history, and when it moves. One register, a scan that starts one past it, and a pointer convention written down once. Blind rotation handed four grants out of sixteen to requesters that were not asking. And the measurement that reshaped the module: two masters under sustained demand produced twelve events, zero contested — the policies were indistinguishable because neither was ever consulted.

17.3 — a property instead of an adjective. fair and fairness occur zero times in B3. The property this arbiter has is a bounded losing run of NREQ - 1, under four named assumptions, and A2 — that the owner eventually releases — is not about the arbiter at all. Equal grants are not equal bandwidth.

17.4 — denial without a bound. 63 opportunities, 1 grant, a longest run of 62 — and 68 completed transfers on the same bus. Starvation is not deadlock, arbitration wait is not slave wait, and a finite trace demonstrates a mechanism rather than proving an infinity.

17.5 — the assembly. One stimulus, two policies, 40 ACKs and zero invariant movement under both. And five arbiters, three of them wrong, all found perfectly conformant by every rule B3 contains.

The through-line is one sentence. The specification defines what a transfer is and delegates who gets to make one — and everything in this module lives on the delegated side.

13. What's Next

One shared path, three requesters, one policy. Every system in Modules 16 and 17 has had exactly one shared resource.

What happens when the fabric itself has structure — several paths, several targets, and a choice about how they connect?

Module 18 — Interconnect Design takes up the topology the specification named and this module deliberately did not enter: the shared bus as one of five interconnection means, crossbar switches, routing, and what scales. The full path is on the Wishbone curriculum index.