AHB Assertions (SVA)

The previous chapter established the mindset — treat the spec as rules and hunt violations. This chapter writes the tool that encodes those rules: SystemVerilog Assertions (SVA). An assertion is a continuously-evaluated property that fires the instant a rule is broken — at the exact cycle and signal — which is exactly what the mindset demands. The anatomy is four parts: a clocking event (@(posedge HCLK) — when to evaluate), an antecedent (the trigger condition — e.g. !HREADY), an implication operator (|-> same cycle, or |=> next cycle), and a consequent (the property that must then hold — e.g. $stable(HADDR)). Read together: "at each clock edge, if the antecedent holds, then the consequent must hold — else fire." The chapter builds the core AHB assertion set — one per rule category from 17.1: address-phase stability (!HREADY |=> $stable(HADDR)), HREADY liveness (no hang), the two-cycle ERROR sequence, HRESP legality, no-X on a real transfer, and burst sequencing. Assertions are bound to the design without modifying the RTL, they catch violations at the source (not as downstream symptoms), and they double as cover properties (confirming scenarios were exercised). This chapter writes the rules as code.

1. What Is It?

AHB assertions are SVA properties that encode the protocol rules and fire at the exact cycle of a violation. Its parts:

• The anatomy — clocking event (@(posedge HCLK)), antecedent (trigger), implication (|-> same / |=> next cycle), consequent (must hold).
• The core set — address-phase stability, HREADY liveness, two-cycle ERROR, HRESP legality, no-X-on-real-transfer, burst sequencing (one per 17.1 rule category).
• Bound, not embedded — assertions are bound to the DUT (or in a checker module), checking it without modifying the RTL.
• Fire at the source — a violation fires immediately, at the exact cycle and signal — and assertions double as cover properties (did the scenario occur?).

So AHB assertions are the executable form of the protocol rules. The mindset (17.1) said "for each rule, know what violates it and catch it at the exact cycle"; an SVA assertion is that catch — a property the tool evaluates every cycle, firing (an error with the cycle/signal) the moment it's violated. The anatomy maps directly to a rule: the antecedent is when the rule applies (!HREADY — during a wait), the consequent is what must hold ($stable(HADDR) — the address unchanged), and the implication sets the timing (|=> — checked next cycle, because the address should be stable into the next wait cycle). You write one assertion per rule, name it (so failures and coverage are tracked), and bind it to the design (checking it non-intrusively — no RTL change). The assertions then run continuously during any simulation, catching violations whenever they occur. So AHB assertions are the protocol rules, written as continuously-checked properties. So they're how you encode the mindset.

2. Why Does It Exist?

AHB assertions exist because the protocol-checker mindset needs an executable, continuous, precise mechanism — assertions evaluate every cycle (catching violations whenever they occur), fire at the source (pinpointing the exact cycle/signal), and bind non-intrusively (checking the design without changing it) — which directed testing can't provide.

The continuous evaluation is the root: a protocol rule must hold on every cycle, forever — so the check must be continuous. An assertion is evaluated every clock edge, automatically, throughout any simulation — so it catches a violation whenever it occurs, no matter what stimulus triggered it. A directed check (e.g. "after this transfer, verify X") only checks at specific points and misses violations elsewhere. So assertions exist to provide continuous checking — the rule is watched always. So it's always-on. So continuity demands assertions.

The fire at the source drives the precision: when an assertion fires, it reports the exact cycle and signal of the violation — at the moment the rule broke. So debugging is immediate: you know exactly what rule broke, when, and where. A downstream check (e.g. a scoreboard catching wrong data later) tells you something is wrong but not where it started. So assertions exist to localize bugs at the source — turning a silent violation into a precisely-located failure (17.1). So it's source localization. So precision demands assertions.

The non-intrusive binding is the practicality: assertions can be bound to the design (via bind) or live in a checker module — checking the DUT without modifying its RTL. So you can add protocol checks to any design (even third-party IP) without touching it, and reuse a checker across many designs. So assertions exist as a non-intrusive, reusable checking layer. So it's clean separation. So practicality favors assertions. So AHB assertions exist because: protocol rules must be checked continuously (every cycle, forever — assertions evaluate every edge — the why); violations must be localized (fire at the exact cycle/signal — source debugging — the precision); and checks should be non-intrusive (bound to the DUT without RTL changes, reusable — the practicality). So AHB assertions are the executable, continuous, precise, non-intrusive encoding of the protocol rules — the primary tool of the protocol-checker mindset, catching silent violations the instant they occur. So this chapter writes them. So encode every rule as an assertion.

3. Mental Model

Model an SVA assertion as a tripwire alarm wired to a specific rule, watching every moment. Unlike a guard who patrols and might miss a break-in between rounds (a directed check at specific points), a tripwire is always armed: the instant someone crosses the line it's watching (the rule's violation), it sounds immediately, and it tells you exactly which tripwire tripped and when (the cycle and signal). You install one tripwire per rule, label each, and wire them in without rebuilding the room (bind, no RTL change).

A secured building (the design) you want to protect against rule violations. One approach is a patrolling guard (a directed check) who walks a route and inspects things at specific points — but between rounds, a violation could happen and be missed (the guard wasn't there). The better approach is a network of tripwire alarms (assertions), each wired to a specific rule and always armed. A tripwire across the fire exit (the "address stable during waits" rule) sounds the instant someone crosses the line it watches (the exact violation — the address changing while HREADY is low). It's continuous — it doesn't patrol; it watches its line every moment — so it catches the violation whenever it happens, not just when a guard passes by. When it trips, it sounds immediately and identifies itself: "tripwire #7 — east fire exit — tripped at 2:14" (the named assertion, the exact cycle and signal). So you know precisely what rule broke, when, and where — not just "something's wrong somewhere" (which a downstream alarm — like noticing missing inventory later — would give). You install one tripwire per rule you care about (one assertion per protocol rule), label each (name them), and — crucially — you wire them in without rebuilding the room (you bind them to the design without modifying its structure). And the same tripwires can double as traffic counters — confirming someone did walk through the exit (a cover property — the scenario occurred).

This captures SVA assertions: the patrolling guard missing things between rounds = a directed check at specific points (misses violations elsewhere); the always-armed tripwire = the continuously-evaluated assertion; wired to a specific rule = the antecedent/consequent encoding one rule; sounding the instant the line is crossed = firing at the exact cycle of the violation; identifying which tripwire and when = the named assertion reporting the cycle/signal; one tripwire per rule, labeled = one named assertion per protocol rule; wiring in without rebuilding the room = binding to the DUT without RTL changes; doubling as a traffic counter = the assertion as a cover property. Install one always-armed, labeled tripwire per rule, wired in non-intrusively, sounding precisely on violation.

Watch an assertion fire on a two-cycle-ERROR violation (a buggy one-cycle error):

The model's lesson: install one always-armed, labeled tripwire per rule, wired in non-intrusively, sounding precisely on violation. In the waveform, the two-cycle-ERROR assertion arms when the first error cycle is seen and fires at cycle 2 when HRESP is wrongly dropped — catching the bug at the exact cycle.

4. Real Hardware Perspective

In SVA, the assertions are written as named properties (often in a checker/interface bound to the DUT), using the implication operators and sampled-value functions ($stable, $rose, $past, $isunknown); they're concurrent (clocked, continuous); and they compile into checking logic the simulator (or formal tool) evaluates.

The named properties and implication: each rule is a named property and an assert: property p_addr_stable; @(posedge HCLK) !HREADY |=> $stable(HADDR); endproperty then a_addr_stable: assert property (p_addr_stable);. The naming (a_addr_stable) makes failures and coverage traceable. The implication (|->/|=>) is the core operator. So in SVA, rules are named, asserted properties. So it's structured. So that's the form.

The sampled-value functions: AHB assertions lean on sampled-value functions: $stable(x) (x unchanged from last cycle — for stability rules), $past(x) (x's value N cycles ago — for comparing across cycles), $rose/$fell (edge detection — e.g. $rose(HREADY)), $isunknown(x) (x has X/Z — for no-X rules). These let the property reason about signal behavior over time. So in SVA, the sampled-value functions express the temporal rules. So they're the building blocks. So temporal rules use them.

The concurrent, bound, dual-use: AHB protocol assertions are concurrent (clocked, evaluated continuously — vs immediate assertions inside procedural code). They're typically in an interface or a checker module bound to the DUT (bind ahb_slave ahb_protocol_checker chk(.*);) — checking without modifying the RTL. And the same properties serve as cover properties (c_waited_transfer: cover property (...)) — confirming a scenario (a wait, an error, a burst) was exercised (feeding coverage — 17.5). So in SVA, AHB assertions are concurrent, named properties (using implication + sampled-value functions), bound to the DUT non-intrusively, dual-use (assert + cover). The skill is writing each rule correctly (right antecedent, consequent, and timing operator) and completely (the full rule set). So in SVA, write each rule as a precise, named, bound property. So that's the implementation.

5. System Architecture Perspective

At the system level, AHB assertions are a reusable protocol-compliance checker — a single, verified checker IP that, bound to any AHB interface, enforces the protocol everywhere; they're also the bridge to formal verification and a living, executable form of the spec.

The reusable checker IP: a complete set of AHB assertions, packaged as a checker module/interface, is a reusable protocol-compliance checker — bind it to any AHB master, slave, or interconnect, and it enforces the AHB protocol there. So one verified checker protects every AHB interface in the SoC (and across projects). So at the system level, the assertions are reusable checker IP — the protocol-compliance layer. So it's reusable. So one checker, many interfaces.

The formal verification bridge: SVA assertions are the input to formal verification (model checking — chapter beyond this module). A formal tool proves an assertion holds for all possible inputs (exhaustive) — or finds a counterexample. So the same assertions used in simulation (catching violations on exercised stimulus) can be formally proven (exhaustive — no stimulus needed). So at the system level, assertions bridge simulation and formal — a single property serving both. So it's the formal input. So assertions enable formal.

The executable spec: a complete assertion set is, in effect, an executable, machine-checkable form of the AHB protocol spec. The prose spec says "the address is stable during waits"; the assertion !HREADY |=> $stable(HADDR) is that rule, executable. So the assertion set documents and enforces the protocol simultaneously — a living spec. So at the system level, AHB assertions are a reusable protocol-compliance checker (one verified checker, bound to every AHB interface — the compliance layer), the bridge to formal verification (the same properties proven exhaustively, not just simulated), and an executable form of the spec (documenting and enforcing the protocol at once). So AHB assertions are how the protocol's rules become a reusable, formal-ready, self-documenting enforcement layer — the foundation of trustworthy AHB IP, bound everywhere and proven where it matters. So write the checker once, bind it everywhere, prove it where it counts.

6. Engineering Tradeoffs

AHB assertions embody the continuous, source-localized, non-intrusive checking design.

• Assertions (continuous) vs directed checks (sampled). Assertions check every cycle (catch violations whenever they occur); directed checks only at specific points (miss them). Use assertions for protocol rules.
• Bound checker vs embedded checks. A bound checker (or interface) checks the DUT without modifying it (reusable, non-intrusive); embedding checks in the RTL couples them. Bind a reusable checker.
• |-> (same cycle) vs |=> (next cycle). Use |-> when the consequent must hold the same cycle as the antecedent; |=> when next cycle. Choosing wrong shifts the check by a cycle (false pass/fail). Match the operator to the rule's timing.
• Assert + cover (dual-use) vs assert only. Using properties as both asserts (catch violations) and covers (confirm exercised) maximizes value; assert-only leaves you unsure the check ever ran. Add cover properties.

The throughline: AHB assertions encode each protocol rule (17.1) as an SVA property — a clocking event + antecedent (trigger) + implication (|-> same / |=> next cycle) + consequent (must hold) — that fires at the exact cycle of a violation. The core set: address-phase stability (!HREADY |=> $stable(HADDR)...), HREADY liveness (!HREADY |-> ##[1:MAX] HREADY), the two-cycle ERROR ((HRESP==ERROR && !HREADY) |=> (HRESP==ERROR && HREADY)), HRESP legality (HRESP inside {OKAY, ERROR}), no-X on a real transfer, and burst sequencing. They use sampled-value functions ($stable, $past, $rose, $isunknown), are bound to the DUT non-intrusively, double as cover properties, and bridge to formal. They're the executable, continuous, precise form of the protocol rules — a reusable compliance checker.

7. Industry Example

Write and bind the core assertion set for the simple slave (16.1), and watch each catch a Module-16 bug.

You're adding an AHB protocol checker to verify the 16.1 slave. You write the core assertions and bind them.

• Address-phase stability → catches the un-gated capture (16.7). a_addr_stable: assert property (@(posedge HCLK) !HREADY |=> $stable(HADDR) && $stable(HWRITE));. If a waited transfer's address changes mid-wait (the bug), this fires at the exact cycle. (Paired with cover property (!HREADY) to confirm waits occurred.)
• Two-cycle ERROR → catches the dropped HRESP (16.6). a_err_2cycle: assert property (@(posedge HCLK) (HRESP==ERROR && !HREADY) |=> (HRESP==ERROR && HREADY));. If the slave drops HRESP to OKAY in the second cycle (the bug), the consequent fails and it fires.
• HREADY liveness → catches a stuck HREADYOUT (16.4). a_hready_live: assert property (@(posedge HCLK) !HREADY |-> ##[1:MAX] HREADY);. If HREADY never rises (a hung slave), it fires after MAX cycles.
• HRESP legality + no-X. a_hresp_legal: assert property (@(posedge HCLK) HRESP inside {OKAY, ERROR}); and a_no_x: assert property (@(posedge HCLK) real_transfer |-> !$isunknown(HADDR)); — catching an illegal response or an X on a real transfer.
• Binding. bind ahb_lite_slave ahb_protocol_checker u_chk (.HCLK, .HRESETn, .HADDR, .HWRITE, .HTRANS, .HREADY, .HRESP, ...); — the checker watches the slave without modifying its RTL.
• Verifying the checker. You inject each bug (a buggy slave variant) and confirm the corresponding assertion fires — proving the checks are real (not vacuous).

The example shows the assertions operationalized: each core assertion encodes a rule and catches the specific Module-16 bug that violates it — at the exact cycle — bound non-intrusively, paired with covers (and tested against known violations). This is how you'd actually protocol-check the 16.1 slave. This is the mindset as code.

8. Common Mistakes

9. Interview Insight

AHB assertions are a core verification interview topic — the anatomy (implication operators), the core rule set, and the vacuity/testing awareness are the signals.

The answer that lands gives the anatomy and the core set: "An SVA assertion encodes a protocol rule as a property that's evaluated every clock edge and fires at the exact cycle of a violation. It has four parts: a clocking event saying when to evaluate, like at the posedge of HCLK; an antecedent, the trigger condition, like HREADY being low; an implication operator — the overlapping arrow checks the consequent in the same cycle, the non-overlapping double arrow checks it in the next cycle; and the consequent, what must hold, like the address being stable. So address-phase stability is: if HREADY is low this cycle, then next cycle the address is stable — using the non-overlapping operator. The core AHB assertion set, one per rule category, is: address-phase stability while HREADY is low; HREADY liveness, that it rises within some bound so the bus doesn't hang; the two-cycle ERROR sequence — if HRESP is ERROR with HREADY low, then next cycle HRESP is still ERROR with HREADY high; HRESP legality — it's inside the legal set OKAY or ERROR; no unknowns on a real transfer; and burst sequencing — the address increments or wraps correctly and HTRANS stays legal mid-burst. I'd write these using sampled-value functions like $stable, $past, and $isunknown, name each one so failures and coverage are tracked, and bind them to the DUT so they check it without modifying the RTL. Two things I'm careful about: getting the implication operator right, because an off-by-one shifts the check by a cycle, and vacuity — an assertion whose antecedent never holds passes without ever checking, so I pair each assert with a cover of the antecedent and I test the assertions by injecting known violations to confirm they fire. The same properties also double as cover properties to confirm scenarios like waits and errors were actually exercised." The anatomy, the core set, and the vacuity/testing awareness are the senior signals.

10. Practice Challenge

Build and reason from AHB assertions.

1. The anatomy. Break down an assertion (clocking event, antecedent, implication, consequent) and read it in plain English.
2. The core set. Write (in SVA-like form) the core AHB assertions: address stability, HREADY liveness, two-cycle ERROR, HRESP legality, burst sequencing.
3. Read the waveform. From Figure 2, explain how the two-cycle-ERROR assertion arms and fires on a dropped HRESP.
4. Operator and functions. Explain |-> vs |=> and the use of $stable/$past/$isunknown, with a rule that needs each.
5. Vacuity and testing. Explain vacuous assertions, why they're dangerous, and how covering antecedents + injecting bugs guards against them.

11. Key Takeaways

• An SVA assertion encodes a protocol rule as a property: clocking event + antecedent (trigger) + implication (|-> same / |=> next cycle) + consequent (must hold) — firing at the exact cycle of a violation.
• The core AHB set: address-phase stability (!HREADY |=> $stable(HADDR)...), HREADY liveness (!HREADY |-> ##[1:MAX] HREADY), two-cycle ERROR ((HRESP==ERROR && !HREADY) |=> (HRESP==ERROR && HREADY)), HRESP legality (inside {OKAY, ERROR}), no-X on a real transfer, burst sequencing.
• Match the operator to the timing — |-> same cycle, |=> next; an off-by-one misses the violation. Use the right sampled-value function ($stable/$past/$rose/$isunknown).
• Guard against vacuity — an assertion whose antecedent never holds passes without checking. Cover the antecedents and test assertions against injected known violations.
• Bind, non-intrusive, dual-use — bind the checker to the DUT without changing RTL; assertions double as cover properties; they bridge to formal (proven exhaustively).
• They catch violations at the source — the exact cycle/signal — turning silent protocol breaks into located failures; a complete set is a reusable compliance checker and an executable spec.

12. What Comes Next

You now can write the assertions that encode the protocol rules. The next chapters build the transaction-level verification components:

• AHB Monitors (next) — build a passive monitor that reconstructs transfers from the bus signals (the foundation for scoreboards and coverage).
• Scoreboards, Functional Coverage, and the rest — check data integrity and measure completeness.

To revisit the rules these assertions encode, see The Protocol-Checker Mindset; for the slave behaviors they check, see HRESP Generation and Address / Control Capture.