Protocol Rules

You know how Wishbone works. Twenty-five modules built masters, slaves, interconnects, register banks, memory controllers and a DMA engine. This module asks a different question:

How do we know the design is correct?

And it opens where Module 25 ended. That module produced a DMA engine that scored zero protocol violations, zero local-invariant violations and perfect accounting — and moved the wrong bytes in every single item.

That is not a curiosity. It is the organising fact of verification:

      rig                  PROTOCOL  LOCAL  ACCOUNT  SCORE
      correct                     0      0       ok      0
      LIVE_READ_DATA              0      0       ok      6

A conformance suite passes that design. Something else has to catch it, and knowing what that something is — and what it can and cannot see — is the whole of Module 26.

1. Four Layers, Four Questions

ASSERTIONS ≠ SCOREBOARD ≠ COVERAGE. They are not degrees of rigour on one axis; they answer questions that do not overlap. A design can be perfect on any three and broken on the fourth.

2. From Prose To Evidence

A requirement is not a check. The chain has five links and skipping any of them produces a verification plan that looks complete and proves nothing:

    prose requirement
        ↓
    verification intent      what would it mean to violate this?
        ↓
    observable condition     which signals, at which boundary?
        ↓
    checker / property       executable
        ↓
    evidence it ACTIVATED    did the antecedent ever hold?

The last link is the one most plans omit, and Chapter 26.2 is about why.

3. Not Every Important Check Is A Wishbone Rule

This is the classification that keeps a verification plan honest:

A LOCAL POLICY presented as protocol law is a lie that survives review, because it is enforced by real code that really fires. The reader cannot tell the difference from the failure message alone — so the class travels with the check:

// ── THE FOUR CLASSES, KEPT APART ────────────────────────────────────────
//   SPEC              a quoted B3 rule, with its scope preserved
//   LOCAL POLICY      this system's choice; legal to violate under B3
//   FUNCTIONAL INTENT the design does what it was meant to do
//   TB INTEGRITY      the checker's own inputs are trustworthy
//
// Only the SPEC rows may be called protocol violations. Presenting a
// LOCAL POLICY check as protocol law is the mistake this class system
// exists to prevent.

And the aggregates are reported separately, never summed:

  output logic [15:0] spec_fails_o,
  output logic [15:0] local_fails_o,

4. The Verification Plan

Twelve requirements, each traced from an authority to a checker to a positive test to a negative control. VR-09, VR-10 and VR-11 are the interesting rows: they are requirements whose check is not a protocol property at all.

5. Scope Is Part Of The Rule

Three of the SPEC rows carry a scope qualifier, and dropping it turns a correct checker into one that fails conformant designs.

RULE 3.45 has a conditional antecedent, which Chapter 24.4 established:

"If a SLAVE supports the [ERR_O] or [RTY_O] signals, then the SLAVE MUST NOT assert more than one of the following signals at any time."

So the checker carries the antecedent as a parameter rather than assuming it:

  // RULE 3.45's antecedent, made explicit rather than assumed
  logic onehot_applies;
  assign onehot_applies = SLAVE_HAS_ERR_RTY;

RULE 3.50 has PERMISSION 3.35's point-to-point carve-out — Chapter 24.4 measured a legal design scoring 58 violations against a checker applied outside its scope.

RULE 3.35 is Classic-only; PERMISSION 4.15 relaxes it for registered-feedback cycles.

// RULE 3.50's negation obligation has PERMISSION 3.35's point-to-point
// carve-out; TIED_OK disables that property for such a rig rather than
// reporting violations that are not violations.
//
// RULE 3.35 is CLASSIC-ONLY; PERMISSION 4.15 relaxes it for registered
// feedback. This checker is a Classic checker and says so.

6. The Property You Must Not Write

The tempting one:

    stb |-> eventually ack

That is not a Wishbone requirement. PERMISSION 3.15 lets a slave's own state participate in the termination decision, and B3 bounds no latency anywhere. A slow slave is conformant; a slave that waits a thousand clocks is conformant.

// ── NO LIVENESS PROPERTY IS CLAIMED AS A B3 REQUIREMENT ─────────────────
// B3 bounds no latency. `stb |-> eventually ack` is NOT a Wishbone rule.
// The timeout below is LOCAL POLICY, informed by RECOMMENDATION 3.10
// ("a watchdog timer function that monitors the MASTER's [STB_O] signal"),
// and it is classed accordingly.

A bounded timeout is legitimate — as LOCAL POLICY. Chapter 24.5 established that B3 is not silent about deadlock: RECOMMENDATION 3.10 recommends a watchdog and places it in the interconnect. A recommendation is not a rule, and VR-11 is classed accordingly.

7. Where To Observe

A property catches only what it can see, and the observation point is a verification decision as real as the property itself. Chapter 26.2 measures this directly: the same property, the same run, scoring 0 at one boundary and 16 at another.

The running system carries two checker instances for exactly this reason:

  // a SECOND checker, at the slave-facing boundary. A property catches
  // only what it can OBSERVE, and a defect injected between the two
  // boundaries is invisible at one of them.

8. Choosing Where To Look, Concretely

The observation point decides what a check can possibly see, so it belongs in the plan rather than in the code. Four boundaries exist in this system, and each answers a different question:

A defect injected between two boundaries is invisible at one of them — Chapter 26.2 measures the same property scoring 0 upstream and 4 downstream in the same run.

The practical rule the plan uses:

Put a property where the obligation lives. RULE 3.60 constrains what a master drives, so VR-02 belongs at every point where a master's request is visible — which in a system with an active fabric means more than one point.

9. Failure Modes The Plan Anticipates

Verification plans that list only requirements miss the failures that come from the plan itself. These are the four classes Modules 23–25 actually produced:

The third and fourth are failures of the verification environment, not of the design, and no amount of adding checkers finds them. Chapter 26.3 and Chapter 26.2 build the gates that do.

10. The Baseline

Seven operations, every layer watching, nothing to report:

      layer        measurement                     value
      CHECKER      SPEC failures                       0
      CHECKER      LOCAL POLICY failures               0
      MONITOR      transactions                        7
      MONITOR      unknown-field transactions          0
      SCOREBOARD   compared                            7
      SCOREBOARD   mismatches                          0
      SCOREBOARD   outstanding expectations            0
      TB INTEGRITY checker/sb/cov unknown          000

      -> ALL FOUR LAYERS QUIET. That is the baseline, and
         on its own it proves almost nothing - SIM I shows
         why a silent checker may simply never have been
         asked a question.

A green baseline is where verification starts, not where it ends. The rest of this module is spent establishing what each silence is worth.

11. What This Chapter Did Not Build

• No checkers yet. The plan names them; Chapter 26.2 writes them.
• No transaction model. Chapter 26.3 defines what a transaction is.
• No formal verification. Every check here is simulation-based; formal is a different curriculum.
• No constrained-random methodology. The stimulus in this module is targeted and deterministic on purpose — Chapter 26.5 explains why for a teaching environment.

Next: Chapter 26.2 — Assertions makes these properties executable, and then demonstrates the single most dangerous result in verification: a property that reports zero failures because it was never asked a question.