Wishbone · Module 26

Assertions

A property with zero failures and zero activations was never asked a question. Measured on one design under two stimulus regimes: activation 0 versus 8, both reporting perfectly clean.

Chapter 26.1 produced a plan. This chapter makes it executable — and then spends most of its length on the result that makes assertion suites dangerous:

A property that reports zero failures has told you one of two things, and you cannot tell which from the failure count alone: that the design obeyed it, or that its antecedent never occurred.

1. An Assertion Is An Implication

Azvya Education Pvt. Ltd.VLSI Mentor

Snippet

    ASSERTION = CONDITION THAT MUST HOLD WHEN ITS ANTECEDENT IS RELEVANT

Three parts, and the first one does the work:

part	Wishbone example
antecedent	a phase is presented and unanswered
implication	then, on the next clock…
consequent	`[ADR_O]` has not changed

A property fires only when the antecedent holds. If the antecedent never holds, the property is vacuously true — and reports exactly the same zero as a property that held under heavy stress.

Overlapped versus non-overlapped

The distinction matters for a bus, because "stable" is inherently about the next clock:

Azvya Education Pvt. Ltd.VLSI Mentor

Snippet

  // VR-02  RULE 3.60 — the qualified signals hold still while the phase
  //        is open. NOTE THE NON-OVERLAPPED IMPLICATION: the consequent
  //        is about the NEXT clock, which is what "stable" means here.
  p_adr_stable: assert property (
    (present && !term) |=> $stable(adr_i))
    else $error("VR-02 RULE 3.60: ADR_O moved while the phase was open");

|-> would assert the consequent on the same clock as the antecedent, which for a stability property is meaningless — the value cannot have changed relative to itself.

2. What This Simulator Actually Does — Re-tested

Modules 22 through 25 carried a blanket claim: Icarus cannot parse SVA. That was re-tested this session with minimal probe sources rather than repeated, and it is too coarse:

construct	Icarus Verilog 13.0
`default clocking … endclocking`	syntax error — "Invalid module item"
`assert property (@(posedge clk) a \|=> b)`	"Error in property_spec of concurrent assertion item"
the same, with `-gsupported-assertions`	notice suppressed, syntax errors remain
the same, with `-gassertions`	unchanged
immediate `assert (expr) else $error(…)`	ACCEPTED, compiles, executes

Concurrent (temporal) assertions are unsupported. Immediate assertions are not. The flag -gsupported-assertions suppresses the notice about the former, not the limitation.

So this module has three evidence tiers, and they are never conflated:

tier	compiled?	executed?	can report activation?
concurrent SVA (`props26.sv`)	rejected	no	no
immediate assertions	yes	yes	no
procedural counters	yes	yes	yes

Azvya Education Pvt. Ltd.VLSI Mentor

Snippet

// ── IMMEDIATE ASSERTIONS ARE EXECUTED HERE ──────────────────────────────
// Re-tested this session: Icarus 13.0 rejects CONCURRENT assertions
// (`assert property`) but ACCEPTS IMMEDIATE ones. So the immediate
// assertions in this file genuinely run, and props26.sv's concurrent
// equivalents genuinely do not. Three tiers, never conflated.

"SVA reviewed", "SVA compile attempted", "SVA executed" and "procedural equivalent executed" are four different statements, and only the last two are true of the properties in this module.

3. Why The Checker Counts Activations

Azvya Education Pvt. Ltd.VLSI Mentor

Snippet

// ── WHY THIS IS NOT MODULE 23'S wb_conformance ──────────────────────────
// wb_conformance counts FAILURES. That is half a checker.
//
// A property reports zero failures for two completely different reasons:
//   (a) the design obeyed it, or
//   (b) THE ANTECEDENT NEVER OCCURRED.
//
// Those are indistinguishable from a failure count alone, and (b) is
// worth nothing. So every property here exports TWO numbers:
//
//   act_*   how many times the antecedent held  -> was it EXERCISED?
//   fail_*  how many times the consequent broke -> was it VIOLATED?
//
//   act = 0, fail = 0   ->  VACUOUS. NOT VERIFIED. Say so.
//   act > 0, fail = 0   ->  exercised and held. Evidence.
//   act > 0, fail > 0   ->  violated.

Every property is written in that two-counter shape:

Azvya Education Pvt. Ltd.VLSI Mentor

Snippet

      // ── VR-02  SPEC  RULE 3.60 ──────────────────────────────────────
      // antecedent: a phase was open last clock and is still presented.
      if (open_phase && present) begin
        a2 <= a2 + 16'd1;
        if ((adr_i !== adr_q) || (sel_i !== sel_q) || (we_i !== we_q) ||
            (we_i && (wdat_i !== wdat_q)))
          f2 <= f2 + 16'd1;
      end

4. Vacuity, Measured

The same property. The same design. Two stimulus regimes — one with wait states, one without:

Azvya Education Pvt. Ltd.VLSI Mentor

Snippet

      rig                VR-02 act  VR-02 fail   verdict
      no wait states             0           0   VACUOUS - NOT VERIFIED
      with wait states           8           0                exercised

Azvya Education Pvt. Ltd.VLSI Mentor

Snippet

      -> BOTH ROWS REPORT ZERO FAILURES. They do not mean
         the same thing.

         With no wait states every phase completes on the
         clock it is presented, so a phase is NEVER open
         and unanswered. VR-02's ANTECEDENT NEVER HOLDS.
         The property was never asked a question, and its
         zero is worth nothing.

ZERO ASSERTION FAILURES IS NOT EVIDENCE. ZERO FAILURES WITH A NON-ZERO ACTIVATION COUNT IS.

5. The Full Activation Audit

An aggregate "0 errors" line hides the distinction, so every property publishes both numbers:

Azvya Education Pvt. Ltd.VLSI Mentor

Snippet

      property  class          activations  failures  verdict
      VR-01     SPEC  R3.25             13         0  exercised
      VR-02     SPEC  R3.60              8         0  exercised
      VR-03     SPEC  R3.35              5         0  exercised
      VR-04     SPEC  R3.45              5         0  exercised
      VR-05     SPEC  R3.50              5         0  exercised
      VR-07     SPEC  R3.65              4         0  exercised
      VR-12     LOCAL POLICY             8         0  exercised

Every row is exercised, so every zero is worth something. A row reading 0 0 VACUOUS would be reported as unverified, not folded into a pass.

6. Observation Point Is Part Of The Property

Here is the same property, the same run, at two boundaries — with the fault injected between them:

Azvya Education Pvt. Ltd.VLSI Mentor

Snippet

      OBSERVED AT THE MASTER PORT (upstream of the fault):
      rig             VR-02 act  VR-02 fail  SPEC fails
      correct                 8           0           0
      MOVING_REQUEST          8           0           0

      OBSERVED AT THE SLAVE-FACING BOUNDARY:
      rig             VR-02 act  VR-02 fail  SPEC fails
      correct                 8           0           0
      MOVING_REQUEST          8           4           4

Azvya Education Pvt. Ltd.VLSI Mentor

Snippet

         The fault is injected BETWEEN the two points, so
         the upstream checker is watching a bus on which
         nothing is wrong. A property catches only what it
         can OBSERVE, and choosing the observation point is
         a verification decision as real as writing the
         property itself.

And note the activation column: 8 at both points. The upstream property genuinely ran and genuinely had nothing to report. That is not the same as being unexercised, and only the two-number report distinguishes the three states.

7. A Local-Policy Violation That Stays Wishbone-Legal

Two negative controls break SPEC rules. The third breaks nothing B3 defines:

Azvya Education Pvt. Ltd.VLSI Mentor

Snippet

      rig               VR-04 act  VR-04 fail  SPEC fails
      correct                   7           0           0
      DUAL_TERMINATION          7           6           6

That one is RULE 3.45, and the antecedent matters:

Azvya Education Pvt. Ltd.VLSI Mentor

Snippet

    RULE 3.45, quoted with the antecedent Module 24 found:
    "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: [ACK_O], [ERR_O] or
    [RTY_O]."

But Chapter 26.4's WRONG_READ_DATA breaks no rule at all — B3 says when [DAT_O()] is valid and never what it should contain — and it is caught by no property in this chapter. Assertions are the wrong tool for that class of defect, and no amount of writing more of them helps.

8. How The Defects Are Injected

The negative controls in this module do not edit the design. Modules 23 through 25 are published and frozen, so the faults live in a transparent wrapper on the wire:

Azvya Education Pvt. Ltd.VLSI Mentor

Snippet

// ── WHY A WRAPPER RATHER THAN EDITED RTL ────────────────────────────────
// The DUT here is built from Modules 23, 24 and 25, which are FROZEN.
// Injecting defects by editing them would change published, verified
// designs. So the defects live in a wrapper that sits on the wire and is
// transparent when every parameter is off.
//
// That is not only a repository rule - it is how fault injection is
// normally done in a real environment, because it keeps the thing under
// test identical between the correct and broken runs. The ONLY
// difference between the rigs below is this wrapper's parameters.

MOVING_REQUEST disturbs the address only after a wait state, because a zero-wait target never leaves a phase open to disturb:

Azvya Education Pvt. Ltd.VLSI Mentor

Snippet

  // ── MOVING_REQUEST ────────────────────────────────────────────────────
  // After one wait state the address flips a bit. Against a zero-wait
  // slave this never happens, which is why the rigs that use it give the
  // target wait states.
  logic disturb;
  assign disturb = MOVING_REQUEST && present && !term && (held_q >= 8'd1);

And DUAL_TERMINATION is one line — the smallest possible RULE 3.45 violation:

Azvya Education Pvt. Ltd.VLSI Mentor

Snippet

  // ── DUAL_TERMINATION ──────────────────────────────────────────────────
  assign m_ack_o = s_ack_i;
  assign m_err_o = DUAL_TERMINATION ? (s_err_i || s_ack_i) : s_err_i;
  assign m_rty_o = s_rty_i;

Keeping the DUT byte-identical between the correct and broken runs is what makes the comparison a measurement. If the correct rig and the broken rig differed in any other way, a difference in the results would not tell you which change caused it.

9. The Property You Must Not Write, In Code

Azvya Education Pvt. Ltd.VLSI Mentor

Snippet

  // ══ NOT A WISHBONE PROPERTY — AND THIS IS THE POINT ════════════════
  //
  // It is tempting to write:
  //
  //     p_eventual_ack: assert property (present |-> ##[1:$] term);
  //
  // DO NOT. B3 BOUNDS NO LATENCY. PERMISSION 3.15 lets a slave's own
  // state decide when it terminates and nothing in the specification
  // says when that must be. A liveness property here would be asserting
  // a LOCAL POLICY as protocol law, and would fire on a perfectly
  // conformant slow slave.

The bounded version is legitimate because it is labelled:

Azvya Education Pvt. Ltd.VLSI Mentor

Snippet

  p_local_timeout: assert property (
    present |-> ##[1:64] term)
    else $error("LOCAL POLICY: no termination within 64 clocks");

10. Cover Directives, And Why The Counters Exist

SVA has a construct for exactly the vacuity problem — cover property — and this environment cannot run it:

Azvya Education Pvt. Ltd.VLSI Mentor

Snippet

  // ── COVERAGE. A property that never saw its antecedent is not
  //    evidence, and cover directives are how SVA says so. The
  //    procedural act_* counters in wb_vplan_checker exist because
  //    THESE CANNOT RUN HERE.
  c_wait_state:     cover property ((present && !term)[*2]);
  c_partial_write:  cover property (present && we_i && (sel_i != 4'hF));
  c_rty_then_ack:   cover property ((present && rty_i) ##[1:$]
                                    (present && ack_i));

The act_* counters are the procedural stand-in for these, and the mapping is one-to-one: every required property has a counter, and every counter is exercised by a named simulation.

11. Reset, Unknowns, And The Two Ways A Property Lies

Two mechanics decide whether a property is telling you anything, and both are easy to get wrong in a way that produces a clean report.

Reset. A property evaluated during reset fires on signals that mean nothing yet:

Azvya Education Pvt. Ltd.VLSI Mentor

Snippet

  default disable iff (rst_i);

The procedural equivalent is the same idea written as control flow — every counter lives inside the else of the reset branch, so neither activations nor failures accumulate while the design is held in reset. A property that counted activations during reset would report itself exercised on evidence that does not exist.

Unknowns. This is the subtler one. An X in an input makes a comparison neither true nor false:

Azvya Education Pvt. Ltd.VLSI Mentor

Snippet

      // ── TB INTEGRITY. An X in an input makes every comparison below
      //    unknown, which silently SKIPS checks. Detect it instead.
      if ((cyc_i === 1'bx) || (stb_i === 1'bx) || (ack_i === 1'bx) ||
          (err_i === 1'bx) || (rty_i === 1'bx) ||
          (present && ((^adr_i === 1'bx) || (^sel_i === 1'bx))))
        unk_q <= 1'b1;

Note === rather than ==. Case equality is what lets the checker detect an X instead of being defeated by one — x == 1'bx is itself unknown, so the naive test cannot fire.

So a property has three ways to report clean and only one of them is evidence: the design obeyed it; the antecedent never held; or an unknown input made the comparison unevaluable. The activation counter separates the first two, and unknown_o separates the third.

12. The Immediate Tier, In Practice

The immediate assertions execute and give a message at the clock the failure happened:

Azvya Education Pvt. Ltd.VLSI Mentor

Snippet

  always @(posedge clk_i) begin
    if (!rst_i && LOUD) begin
      assert (!(stb_i && !cyc_i))
        else $error("VR-01 RULE 3.25: STB_O with CYC_O negated");
      assert (!(term && !present))
        else $error("VR-03 RULE 3.35: termination with no request");
      assert (!(onehot_applies && multi))
        else $error("VR-04 RULE 3.45: two terminations at once");
    end
  end

They duplicate the counters deliberately, and the division of labour is worth stating: the counters supply activation evidence, which is what a vacuity audit needs; the assertions supply an immediate, located failure message, which is what debugging needs. Neither replaces the other.

What immediate assertions cannot express is anything temporal. $stable, $past and any multi-clock sequence require the concurrent form — which is why VR-02, the one property in this chapter that genuinely spans two clocks, exists only as a counter and as unexecuted SVA.

13. What This Chapter Did Not Build

No formal proof. These are simulation properties; an unexercised property stays unproven no matter how it is written.
No assertion library. The properties are written out, not parameterised into a reusable package.
No executed concurrent SVA. props26.sv is published, its rejection captured, and marked inspection-only.
No data checking. Deliberately: Chapter 26.4 shows why no property can do it.

Next: Chapter 26.3 — Monitors turns clocks into transactions — and finds that a broken observer makes a correct design look broken, which is a failure mode assertions cannot warn you about.

Continue learning

Standards & specifications

Governing standard: Wishbone SoC Interconnection Architecture (OpenCores)(opens OpenCores in a new tab)
Defines the Wishbone signal set, the bus cycles built from it and the interface rules a portable IP core must follow. It deliberately leaves interconnect topology, address map and arbitration policy to the integrator, so those are system decisions rather than requirements of the specification.

This page also covers RTL structure, verification approach and debugging technique. Those are engineering practice built on the standard, not requirements the standard itself imposes.

Where this fits

Part of the Wishbone curriculum.

Assertions

1. An Assertion Is An Implication

Overlapped versus non-overlapped

2. What This Simulator Actually Does — Re-tested

3. Why The Checker Counts Activations

4. Vacuity, Measured

5. The Full Activation Audit

6. Observation Point Is Part Of The Property

7. A Local-Policy Violation That Stays Wishbone-Legal

8. How The Defects Are Injected

9. The Property You Must Not Write, In Code

10. Cover Directives, And Why The Counters Exist

11. Reset, Unknowns, And The Two Ways A Property Lies

12. The Immediate Tier, In Practice

13. What This Chapter Did Not Build

Continue learning

Related tutorials

Master Design

Wait-State Bugs

UCIe Assertions

CXL Assertions

Standards & specifications

Where this fits