APB Assertions

The rules catalogue told you what legal APB is; assertions make a tool check it, continuously, on every edge. The single idea to carry: an APB assertion is a 1:1 encoding of one catalogue rule into a concurrent SVA property — clocked on pclk, disabled during reset, gated by an antecedent and obligated by a consequent — bind-ed non-intrusively to the bus so it fails the instant the rule breaks. You are not re-deriving the rules (they were enumerated in 15.1); you are turning each one into a property that an always-on simulation or formal engine evaluates. Get the property structure right — the clocking event, the disable iff, the antecedent/consequent split, $stable, and the bind — and the catalogue becomes a live protocol monitor. Get it subtly wrong — a vacuous antecedent, a missing reset disable — and the assertion reports green while the rule goes unchecked.

1. Problem statement

The problem is rendering each catalogue rule as a concurrent SystemVerilog Assertion (SVA) property that an engine evaluates on every clock, so a protocol violation fails an assertion the moment it occurs — and doing so non-intrusively, so the checker attaches to any APB bus without editing the DUT.

A rule in prose — "the address is held stable from SETUP through completion" — cannot fail a simulation. It has to become an executable proposition with three things made precise: when it is sampled (which clock edge), when it applies (the gating condition, or antecedent), and what must then hold (the obligation, or consequent). SVA is the language that expresses exactly this, and the encoding has hard requirements:

• It must be a temporal proposition, not a combinational if. Protocol rules span cycles — "if PSEL is high and the transfer isn't completing this cycle, then next cycle PADDR is unchanged." That "next cycle" is temporal; it needs a clocking event and an implication operator, not a procedural conditional.
• It must be disabled during reset. While PRESETn is low the bus is not running a protocol; a property that keeps evaluating in reset fires spurious failures (or, worse, gets waived and masks a real one). Every property carries disable iff (!presetn).
• It must be non-intrusive and reusable. The checker cannot live inside the DUT — it has to attach from outside, to the interface signals, so the same checker works on any APB slave and ships nothing into silicon. That is what bind is for.

So the job is to take a complete catalogue and produce a complete, syntactically correct, idiomatic set of SVA properties — one per rule — bound to the bus as an always-on monitor.

2. Why previous knowledge is insufficient

Chapter 15.1 gave you the rulebook: phase, select, stability, ready, error and reset rules, each atomic and numbered. But a rule list is a document — it does not run. What you are missing is the language and structure that turns a written rule into something an engine checks:

• A rule statement is not a property. "PENABLE is low in SETUP and high in ACCESS" is English. The property is @(posedge pclk) disable iff(!presetn) (psel && !penable) |=> penable — and writing it forces decisions the prose hides: which edge samples, whether the obligation is same-cycle (|->) or next-cycle (|=>), and what arms the check. The catalogue does not teach SVA; this chapter does.
• Assertions are not the procedural monitor. Chapter 15.3 (the monitor) reconstructs transactions in procedural code — a class sampling the bus, building transaction objects, comparing in a scoreboard. SVA is declarative: you state the obligation and the engine proves or refutes it every cycle, with no sampling loop to write. The two are complementary — assertions are the dense, always-on rule checks; the monitor is the transaction reconstructor. Confusing them is a classic gap.
• Reachability is not coverage. This chapter uses cover to confirm an assertion's antecedent actually fires (reachability — did the scenario happen at all). The functional coverage model — bins for every wait-count, every error case, every back-to-back pattern — is Chapter 15.5. cover property here answers "did this property ever arm?"; the coverage model answers "did we exercise the whole space?"

So the model to add is SVA structure: clocking, reset-disable, antecedent/consequent, sequences, $stable/$isunknown, and bind — the machinery that makes the catalogue executable.

3. Mental model

The model: an SVA property is a contract with a trigger and a clause. The antecedent is the trigger ("if this situation arises on the bus"); the consequent is the clause that then becomes legally binding ("then this must hold"). The clocking event says when the contract is read (which edge samples the signals); disable iff(!presetn) says the contract is void during reset. The engine re-reads the contract on every clock and the instant the trigger fires but the clause is broken, the assertion fails — pointing at the exact cycle and signal.

Four refinements make it precise and interview-ready:

• |-> is same-cycle; |=> is next-cycle. antecedent |-> consequent means the consequent must hold in the same cycle the antecedent matched. antecedent |=> consequent means it must hold one cycle later — exactly |-> ##1 consequent. Stability rules use |=> ("if held this cycle, next cycle the value is unchanged"); a same-cycle combinational rule like "PENABLE high ⇒ PSEL high" uses |->. Choosing wrong shifts the check by a cycle and either fires falsely or misses the violation.
• $stable / $past / $isunknown are the sampled-value functions. $stable(sig) is true when sig has the same sampled value as the previous clock — the natural encoding of every stability rule. $isunknown(sig) is true if any bit is X/Z — the encoding of "never-X" rules (e.g. PSLVERR must not be unknown at completion). $past(sig, n) reaches back n cycles. These operate on sampled values (preponed to the clock edge), which is why glitches between edges don't trip them.
• The antecedent must actually fire, or the pass is vacuous. If the antecedent is never true on the trace, the implication is trivially satisfied every cycle — the property reports PASS while never once testing the consequent. A vacuous pass is an unasked question. The defence is cover property on the antecedent: if it never covers, the assertion never armed.
• bind attaches the checker from outside. You write the properties in a separate module (or checker), then bind it to the APB interface or DUT instance. The checker sees the bus signals as if it were inside, but the DUT source is untouched and the checker ships nothing into the netlist. One checker, bound to every APB slave.

4. Real SoC implementation

In a real environment the properties live in a dedicated checker module — one property per catalogue rule, each commented with its rule ID — and a bind statement attaches it to the APB interface so it monitors every transfer without touching the DUT. A representative checker:

// apb_protocol_checker.sv — concurrent SVA encoding of the APB rules catalogue.
// Non-intrusive: bound to the APB interface, ships nothing into the netlist.
// One property per catalogue rule; each assert/cover names the rule ID it owns.
module apb_protocol_checker #(
  parameter int ADDR_W   = 32,
  parameter int DATA_W   = 32,
  // Worst-case wait cycles this subordinate is permitted, from its datasheet.
  // Used to make the completion rule falsifiable in simulation.
  parameter int MAX_WAIT = 16
) (
  input logic              pclk,
  input logic              presetn,
  input logic              psel,      // single-slave view; one-hot handled at the fabric
  input logic              penable,
  input logic              pwrite,
  input logic [ADDR_W-1:0] paddr,
  input logic [DATA_W-1:0] pwdata,
  input logic [DATA_W-1:0] prdata,
  input logic [DATA_W/8-1:0] pstrb,
  input logic              pready,
  input logic              pslverr
);
 
  // A transfer is "active and not yet completing" when PSEL is high and we are
  // not on the completing edge (PENABLE & PREADY). Reused by the stability rules.
  let in_held_transfer = psel && !(penable && pready);
 
  // ---- PHASE rules -------------------------------------------------------
  // PHASE-2: PENABLE is LOW during SETUP - the first cycle of every transfer.
  //
  // Getting the antecedent right matters more than it looks. Writing
  //     ($rose(psel) && !penable) |-> !penable
  // is a TAUTOLOGY: !penable appears in both halves, so the property can never
  // fail no matter what the design does. It arms happily, its cover HITs, and
  // it still checks nothing - a failure mode distinct from vacuity and just as
  // silent. See the Debug Lab in beat 7b.
  //
  // The first cycle of a transfer is one where PSEL is high and the previous
  // cycle was either unselected or a completing ACCESS. Both cases start a
  // new SETUP, which covers back-to-back transfers where PSEL never drops.
  property p_setup_penable_low;
    @(posedge pclk) disable iff (!presetn)
      (psel && (!$past(psel) || $past(penable && pready))) |-> !penable;
  endproperty
  a_setup_penable_low: assert property (p_setup_penable_low);   // PHASE-2 (SETUP)
 
  // PHASE-1 + PHASE-2: SETUP is followed by ACCESS next cycle, i.e. once PSEL
  //          is high with PENABLE low, the NEXT cycle PENABLE must be high
  //          (assuming PSEL stays asserted). Next-cycle obligation → |=>.
  property p_setup_to_access;
    @(posedge pclk) disable iff (!presetn)
      (psel && !penable) |=> (penable);
  endproperty
  a_setup_to_access: assert property (p_setup_to_access);   // PHASE-1/2
 
  // ---- SELECT rules ------------------------------------------------------
  // SEL-1: PENABLE is never high unless PSEL is high (combinational → |->).
  property p_enable_implies_sel;
    @(posedge pclk) disable iff (!presetn)
      penable |-> psel;
  endproperty
  a_enable_implies_sel: assert property (p_enable_implies_sel);  // SEL-1
  // (SEL-2 one-hot PSEL is checked at the fabric level over the PSEL vector:
  //  assert ($onehot0(psel_vec)); — bound where all PSELx are visible.)
 
  // ---- STABILITY rules ---------------------------------------------------
  // STAB-1/2: address, control and write data are held stable across a transfer
  //           that has not yet completed. Next-cycle → |=> with $stable.
  property p_request_stable;
    @(posedge pclk) disable iff (!presetn)
      in_held_transfer |=> ($stable(paddr) && $stable(pwrite) &&
                            $stable(pwdata) && $stable(pstrb));
  endproperty
  a_request_stable: assert property (p_request_stable);     // STAB-1/2
 
  // ---- READY rules -------------------------------------------------------
  // RDY-1: PREADY is only meaningful (sampled) in ACCESS; outside ACCESS it
  //        must not falsely signal completion. Encoded as: completion edge
  //        (PSEL & PENABLE & PREADY) only occurs when PENABLE is high.
  // RDY-2: bounded completion - once in ACCESS, PREADY must rise within
  //        MAX_WAIT cycles, taken from the subordinate's worst-case wait spec.
  //
  // The bound is not a convenience. Written as
  //     (psel && penable) |-> ##[0:$] pready
  // the property is UNBOUNDED liveness, and a simulator cannot falsify it: an
  // attempt that never completes simply stays pending until the run ends, so
  // the assertion reports no failure however long the subordinate stalls. A
  // stuck PREADY - the exact bug this rule exists for - passes.
  //
  // True liveness needs formal. In simulation, assert the engineering
  // requirement instead, which is a real number the datasheet gives you.
  property p_bounded_completion;
    @(posedge pclk) disable iff (!presetn)
      (psel && penable && !pready) |-> ##[1:MAX_WAIT] pready;
  endproperty
  a_bounded_completion: assert property (p_bounded_completion)   // RDY-2
    else $error("PREADY did not rise within %0d cycles of ACCESS", MAX_WAIT);
 
  // ---- ERROR rules -------------------------------------------------------
  // ERR-1: PSLVERR is only VALID at completion (PSEL & PENABLE & PREADY), and
  //        at that edge it must be a known 0/1, never X.
  //
  // Note the strength of the first property below. AMBA *recommends* that
  // PSLVERR is driven low when it is not being sampled; it does not require
  // it. So this asserts a house rule rather than a protocol rule, and it will
  // flag a compliant subordinate that leaves PSLVERR as a don't-care outside
  // the completing cycle. Keep it where the project mandates the tie-low, and
  // downgrade it to a warning when qualifying third-party IP.
  property p_pslverr_only_at_completion;
    @(posedge pclk) disable iff (!presetn)
      pslverr |-> (psel && penable && pready);
  endproperty
  a_pslverr_only_at_completion: assert property (p_pslverr_only_at_completion); // ERR-1
 
  property p_pslverr_known_at_completion;
    @(posedge pclk) disable iff (!presetn)
      (psel && penable && pready) |-> !$isunknown(pslverr);
  endproperty
  a_pslverr_known: assert property (p_pslverr_known_at_completion);  // ERR-1 (never-X)
 
  // ---- COVER: prove the antecedents actually fire (anti-vacuity) ----------
  c_held_transfer: cover property (@(posedge pclk) in_held_transfer);
  c_wait_state:    cover property (@(posedge pclk) (psel && penable && !pready));
  c_error_resp:    cover property (@(posedge pclk) (psel && penable && pready && pslverr));
 
endmodule
 
// ---- BIND: attach the checker to the DUT's APB interface, non-intrusively --
// The checker is instantiated against apb_if without editing the slave RTL.
bind apb_slave apb_protocol_checker #(.ADDR_W(32), .DATA_W(32), .MAX_WAIT(16)) u_apb_chk (
  .pclk    (pclk),    .presetn (presetn),
  .psel    (psel),    .penable (penable), .pwrite (pwrite),
  .paddr   (paddr),   .pwdata  (pwdata),  .prdata (prdata),
  .pstrb   (pstrb),   .pready  (pready),  .pslverr(pslverr)
);

Two facts make this the right shape. First, each property names its catalogue rule ID, so the assertion set is an auditable derivation from 15.1 — a sign-off review walks rule IDs and confirms each has a property (and that each property non-vacuously fires via its cover). Second, bind keeps the checker non-intrusive and reusable: the same apb_protocol_checker binds to every APB slave in the SoC, lives only in the verification compile, and ships nothing into the netlist — which is precisely why assertions and the procedural monitor can both watch the same bus without interfering.

5. Engineering tradeoffs

Writing the SVA is a sequence of structural choices — operator, gating, where each construct fits.

The second axis is how each rule category maps to property style:

The throughline: assert checks, assume constrains inputs (in formal), cover proves reachability — three different jobs, not three strengths of the same thing. And the operator follows the rule's timing: same-cycle relationships are |->, "next cycle / held" rules are |=>, completion is bounded liveness. Pick the operator from the rule, not from habit.

6. Common RTL mistakes

7. Debugging scenario

The signature SVA failure is not a noisy false fail — it is a silent vacuous pass: an assertion that reports green on every run because its antecedent never once armed, so a real protocol bug it was meant to catch sailed straight through.

• Observed symptom: a slave passes its full assertion suite, every property reports PASS, sign-off says "assertions clean." In integration the slave intermittently corrupts write data under back-to-back traffic with wait states — the exact failure the stability assertion was written to catch. The assertion that should have screamed never fired.
• Waveform clue: on the failing trace, PWDATA changes during a wait state (manager holding the transfer with PREADY low). Yet the assertion log shows a_stab: PASS. Pulling the assertion's coverage reveals the tell: the property's antecedent has 0% coverage — it never evaluated non-vacuously, not once, across the entire regression.
• Root cause: the stability property's antecedent was written too narrowly — it gated on (psel && penable && !pready && pwrite==0), i.e. it only armed on a read wait, while write data only matters on writes. The condition was never true on a write transfer, so the property was vacuously satisfied every cycle and the $stable(pwdata) consequent was never checked. The assertion existed, compiled, and "passed" — but it was an empty contract whose trigger could never fire.
• Correct RTL (corrected SVA): widen the antecedent to arm on every held transfer beat, and pair it with a cover so a non-firing antecedent is visible:

// FIX: arm on any held transfer (read or write), and prove the antecedent fires.
property p_request_stable;
  @(posedge pclk) disable iff (!presetn)
    (psel && !(penable && pready)) |=> ($stable(pwdata) && $stable(paddr) &&
                                        $stable(pwrite) && $stable(pstrb));
endproperty
a_request_stable: assert property (p_request_stable);
c_held_transfer:  cover  property (@(posedge pclk) (psel && !(penable && pready)));

• Verification assertion: beyond fixing this property, add a sign-off gate: every assert must have a paired cover on its antecedent, and the regression report must show every such cover HIT. An assertion whose antecedent cover is 0% is treated as a failure of the suite, not a pass — vacuity is a coverage hole, not a clean result.
• Debug habit: when a "fully verified" slave fails on a rule its assertion supposedly checks, do not assume the assertion is wrong — check whether it ever fired. Read the non-vacuous evaluation count and the antecedent cover. A PASS with zero non-vacuous evaluations means the property never tested anything; the bug is a too-narrow or mistyped antecedent, and the fix is to make the trigger reachable and prove it with cover.

7b. Two ways an assertion passes without checking anything

Beat 7 covers vacuity: an antecedent that never arms. There are two further failure modes with the same symptom — a green report from a property that tests nothing — and both were present in earlier revisions of the checker above.

A tautology arms and still cannot fail. The original PHASE-2 property read:

// ✗ !penable appears on BOTH sides. This can never fail.
($rose(psel) && !penable) |-> !penable;

Its antecedent fires on every transfer, so an antecedent cover HITs and the standard vacuity check reports it healthy. It is nonetheless an empty contract: the consequent restates part of the antecedent, so the property is true by construction regardless of the design. Vacuity coverage cannot see this, because the property is not vacuous — it is trivially satisfiable.

Unbounded liveness cannot be falsified in simulation. The original completion property read:

// ✗ Unbounded. A simulator can never report this as failing.
(psel && penable) |-> ##[0:$] pready;

##[0:$] says "eventually". If PREADY never rises, the attempt simply remains pending until the run ends — there is no cycle at which the tool can declare it failed, because a later cycle might still satisfy it. A permanently stuck PREADY, which is exactly the bug this rule exists to catch, produces no failure. Only a formal engine can discharge true liveness; in simulation you assert the bounded engineering requirement instead.

// Comment claims bounded; code is unbounded.
// RDY-2: bounded completion — PREADY must rise within N cycles.
property p_bounded_completion;
  @(posedge pclk) disable iff (!presetn)
    (psel && penable) |-> ##[0:$] pready;
endproperty
a_bounded_completion: assert property (p_bounded_completion);

  a_bounded_completion   attempts: 4127   failures: 0   incomplete: 1
  c_wait_state           hits: 3891

// Bound it with the subordinate's worst-case wait specification.
parameter int MAX_WAIT = 16;
 
property p_bounded_completion;
  @(posedge pclk) disable iff (!presetn)
    (psel && penable && !pready) |-> ##[1:MAX_WAIT] pready;
endproperty
a_bounded_completion: assert property (p_bounded_completion)
  else $error("PREADY did not rise within %0d cycles of ACCESS", MAX_WAIT);

7c. Qualifying the checker

A protocol checker is itself a design, and the way you verify a checker is to feed it known-bad traffic and confirm it objects. This harness drives one deliberate violation per rule and fails if the corresponding assertion stays silent.

module apb_checker_qual_tb;
  logic pclk = 0, presetn = 0;
  logic psel = 0, penable = 0, pwrite = 0, pready = 1, pslverr = 0;
  logic [31:0] paddr = '0, pwdata = '0, prdata = '0;
  logic [3:0]  pstrb = '1;
 
  apb_protocol_checker #(.ADDR_W(32), .DATA_W(32), .MAX_WAIT(4)) chk (.*);
 
  always #5 pclk = ~pclk;
 
  // Count failures per rule by hooking the assertion action blocks through a
  // shared counter. In a real flow this comes from the tool's assertion API;
  // here an explicit counter keeps the example self-contained.
  int unsigned fired [string];
  int unsigned expected_fires;
 
  task automatic expect_fire (input string rule);
    expected_fires++;
    if (!fired.exists(rule) || fired[rule] == 0)
      $fatal(1, "QUALIFICATION FAILED: %s did not fire on its own violation",
             rule);
    else
      $display("PASS %-24s fired on injected violation", rule);
  endtask
 
  initial begin
    repeat (2) @(negedge pclk); presetn = 1;
 
    // ---- Violation 1: PENABLE high during SETUP (PHASE-2) ---------------
    @(negedge pclk) psel = 1; penable = 1;      // illegal: SETUP with PENABLE
    @(negedge pclk) psel = 0; penable = 0;
    repeat (2) @(negedge pclk);
    expect_fire("a_setup_penable_low");
 
    // ---- Violation 2: PADDR changes mid-transfer (STAB-1) ---------------
    @(negedge pclk) psel = 1; penable = 0; paddr = 32'h100; pready = 0;
    @(negedge pclk) penable = 1;
    @(negedge pclk) paddr = 32'h200;            // illegal: address moved
    @(negedge pclk) pready = 1;
    @(negedge pclk) psel = 0; penable = 0; pready = 1;
    repeat (2) @(negedge pclk);
    expect_fire("a_request_stable");
 
    // ---- Violation 3: PREADY held low past MAX_WAIT (RDY-2) -------------
    // Against the OLD unbounded property this injection produced no failure
    // at all - which is precisely why the qualification harness exists.
    @(negedge pclk) psel = 1; penable = 0; paddr = 32'h300; pready = 0;
    @(negedge pclk) penable = 1;
    repeat (8) @(negedge pclk);                 // 8 > MAX_WAIT of 4
    @(negedge pclk) pready = 1;
    @(negedge pclk) psel = 0; penable = 0;
    repeat (2) @(negedge pclk);
    expect_fire("a_bounded_completion");
 
    // ---- Violation 4: PENABLE without PSEL (SEL-1) ----------------------
    @(negedge pclk) psel = 0; penable = 1;      // illegal
    @(negedge pclk) penable = 0;
    repeat (2) @(negedge pclk);
    expect_fire("a_enable_implies_sel");
 
    $display("Checker qualification passed: %0d rules proven falsifiable.",
             expected_fires);
    $finish;
  end
endmodule

Violation 3 is the point of the whole harness. Run it against the unbounded version of the completion property and the injected stall produces no failure, so expect_fire reports the checker itself as broken. That is the only mechanical way to distinguish a rule that holds from a rule that cannot fail — and it costs one directed stimulus per property.

8. Verification perspective

Assertions are not "set and forget" — their own completeness is a verification deliverable, measured by non-vacuity and coverage of antecedents, and the choice between simulation and formal changes what they buy you.

• Vacuity is the first thing you verify about your assertions. A passing assertion proves nothing unless it armed. So every assert is paired with a cover property on its antecedent, and sign-off requires every such cover to be HIT — a 0% antecedent cover means the property never tested its rule. This is assertion coverage: not "did any assertion fail" but "was every property exercised non-vacuously." It is the single highest-value check on the assertion suite, because a vacuous property is indistinguishable from a passing one in the failure log.
• Formal and simulation use the same properties differently. In simulation, properties are checked against the stimulus you happen to drive — they fail only on traces you generate, and vacuity is a real risk (an antecedent you never stimulated). In formal, the engine explores all legal input traces: you assume the manager drives legal APB (constraining inputs), and the tool proves each assert holds for every reachable state or returns a counterexample. Formal turns "passed on my tests" into "cannot be violated" — invaluable for the dense, local APB rules (stability, phase, select) that are fully provable, while bounded-liveness ready rules may need a depth bound.
• bind reuse makes the checker an SoC-wide asset. Because the properties are written against interface signals and attached by bind, one apb_protocol_checker binds to every APB slave in the design — and, in formal, to the same RTL under a different harness. The checker is authored once, audited once against the catalogue, and reused everywhere, which is what keeps the assertion set consistent across dozens of peripherals instead of drifting per-block. It also coexists cleanly with the procedural monitor and feeds the same sign-off as the coverage model: assertions prove the rules, the monitor reconstructs transactions, coverage confirms the space was exercised.

The point: verify the assertions by non-vacuity and antecedent coverage, exploit formal to turn passes into proofs, and use bind to make one audited checker watch every APB bus — because an assertion that never fires is worse than none, since it reads as green.

9. Interview discussion

"Walk me through how you'd write an APB protocol checker in SVA" is a critical verification question, and the answer that signals real experience moves from structure to non-vacuity to bind.

Lead with the structure: every concurrent property has a clocking event (@(posedge pclk)), a disable iff(!presetn) so it is void in reset, an antecedent that arms the check, and a consequent obligated by |-> (same cycle) or |=> (next cycle). Then show you can map the catalogue: a same-cycle relationship like "PENABLE ⇒ PSEL" is penable |-> psel; a stability rule is (psel && !(penable && pready)) |=> $stable(paddr); "PSLVERR only at completion" is pslverr |-> (psel && penable && pready); the never-X rule uses !$isunknown(...). The depth flourishes are three: assert vs assume vs cover — assert checks the DUT, assume constrains inputs in formal, cover proves reachability, three different jobs not three strengths; vacuity — a green assertion means nothing unless its antecedent fired, so you pair every assert with a cover on its antecedent and treat a 0% antecedent cover as a suite failure; and bind — the checker is a separate module bound to the interface so it is non-intrusive, ships nothing into the netlist, and the one audited checker reuses across every APB slave. Closing with "in formal I assume legal manager stimulus and the tool proves the stability and phase properties for all reachable states — turning 'passed my tests' into 'cannot be violated'" demonstrates you understand assertions as both a simulation monitor and a formal contract.

10. Practice

1. Encode three rules. Write SVA properties for: "PENABLE is high in ACCESS one cycle after SETUP," "PADDR is stable across a held transfer," and "PSLVERR is only asserted at completion." State the operator (|-> vs |=>) for each and why.
2. Spot the vacuity. Given (psel && penable && !pready && pwrite==0) |=> $stable(pwdata), explain why it can pass vacuously on every write transfer, and rewrite the antecedent so it arms on every held beat. Add the cover you'd pair with it.
3. Assert vs assume vs cover. For each of these, say which construct fits and why: (a) the DUT must never assert PSLVERR outside completion; (b) in a formal run, the manager only ever drives legal APB; (c) confirm the wait-state-with-error scenario was reached.
4. Reset discipline. Show what goes wrong if a stability property omits disable iff(!presetn), and how a waived reset-time failure can later mask a real bug.
5. Bind it. Write a bind statement attaching an apb_protocol_checker to an apb_slave instance, and explain in one sentence why bind keeps the checker non-intrusive and reusable.

11. Q&A

11b. Where This Is Specified

• Arm AMBA APB Protocol Specification (ARM IHI 0024). The IDLE → SETUP → ACCESS model; PSEL asserted with PENABLE low for exactly one SETUP cycle; PENABLE asserted throughout ACCESS; the transfer completing only when PSEL && PENABLE && PREADY; address, direction and write data held stable for the duration of a transfer; and PSLVERR being valid only on the completing cycle — with driving it low elsewhere stated as a recommendation rather than a requirement.
• IEEE 1800-2023 §16 — Assertions. Concurrent property syntax, the overlapping (|->) and non-overlapping (|=>) implication operators, $past, $stable, $isunknown, and cover property.
• IEEE 1800-2023 §16.9.2 — Cycle delay ranges. The ##[m:n] bounded range and the ##[m:$] unbounded form whose eventuality a simulator cannot falsify.
• IEEE 1800-2023 §16.12.2 — Property evaluation. Attempts that neither succeed nor fail before end of simulation, reported as incomplete.
• IEEE 1800-2023 §23.11 — bind. Attaching the checker to the subordinate without editing its RTL.

12. Key takeaways

• An APB assertion is a 1:1 encoding of one catalogue rule into a concurrent SVA property — clocking event, disable iff(!presetn), antecedent, and |->/|=> consequent — and the full suite is a complete, auditable derivation from the rules catalogue.
• |-> is same-cycle, |=> is next-cycle (|=> ≡ |-> ##1); pick the operator from the rule's timing — combinational relationships use |->, "held / next-cycle" stability and phase rules use |=>, and bounded completion is liveness (##[1:N]).
• $stable encodes stability rules, $isunknown encodes never-X rules, both on sampled values at the clock edge — which is why glitches between edges don't trip them.
• assert checks, assume constrains inputs (in formal), cover proves reachability — three different jobs, not three strengths of one construct.
• A green assertion means nothing unless it fired non-vacuously — pair every assert with a cover on its antecedent and treat a 0% antecedent cover as a suite failure; vacuity is the dominant silent-escape mode.
• bind makes the checker non-intrusive and reusable — one audited apb_protocol_checker, written against the interface, binds to every APB slave and ships nothing into the netlist, and in formal the same properties turn "passed my tests" into "cannot be violated."