Almost every PENABLE bug is the same bug wearing a different mask: PENABLE was treated as a decode output instead of a registered ACCESS strobe, so the SETUP→ACCESS sequence breaks somewhere. APB's entire timing contract rests on one rule — a transfer spends exactly one cycle in SETUP (PSEL=1, PENABLE=0) and then one or more cycles in ACCESS (PSEL=1, PENABLE=1) — and PENABLE is the single bit that draws the line between those two phases. Get PENABLE wrong and the phase boundary moves, vanishes, duplicates, or glitches, and the subordinate either samples address and data a cycle too early, misses a transfer entirely, commits on a pulse that was never a real ACCESS, or merges two transfers into one. The idea to carry through this chapter: PENABLE is not "the second select" and it is not a combinational function of PSEL — it is the registered output of a one-deep SETUP→ACCESS state machine, qualified by PSEL, and the six classic PENABLE bugs (asserted in SETUP, never deasserting, high without PSEL, glitching, held across back-to-back with no SETUP gap, driven one cycle late or early) are all failures to build it that way. Each has a distinct waveform signature on the bus, and once you can read the signature you can name the RTL mistake before you ever open the source.
1. Problem statement
The problem is recognising the recurring ways PENABLE is driven wrong in real APB RTL, reading each one's signature on a captured waveform, and tracing it back to the specific line of source that broke the SETUP→ACCESS sequence. PENABLE looks trivial — it is one bit — and that is exactly why it is mishandled so often: engineers reach for the simplest expression that "works" in the happy-path directed test and ship it, only for the boundary behaviour to be wrong.
The AMBA APB spec (IHI 0024C) §3.1 states the rule plainly: a transfer enters the SETUP state with PSEL asserted and PENABLE deasserted, and on the next rising clock edge moves to the ACCESS state with both PSEL and PENABLE asserted, holding there until PREADY is sampled high. PENABLE is therefore not free-running — it is a strict function of which phase the transfer is in. Three things make getting it right harder than it looks:
- The happy-path test does not exercise the boundary. A single isolated transfer with one wait state will pass even if PENABLE is combinationally tied to PSEL, because the slave still eventually sees
PSEL && PENABLEand completes. The bug only surfaces on the first sampling cycle, on back-to-back traffic, or when the address has not yet settled — none of which the trivial test reaches. - The legal-looking states hide the illegal ones.
PSEL=1, PENABLE=1is a legal ACCESS state. But the same waveform read one cycle earlier —PSEL=1, PENABLE=1on the first cycle of the transfer, with no SETUP in between — is a bug. PENABLE bugs are rarely a value that is "obviously wrong"; they are a correct-looking value at the wrong time. - PENABLE feeds the slave's commit logic. Because the subordinate uses
PSEL && PENABLE && PREADYto commit a write, any PENABLE that is high when it should be low — a glitch, a stuck-high, an early assertion — can drive a false commit. The cost of a PENABLE bug is not a cosmetic timing wobble; it is corrupted register state.
So the job is to build a mental index from symptom on the bus → root-cause RTL → fix, for each of the six PENABLE failure families, so that when a waveform shows the signature you reach straight for the broken line.
2. Why previous knowledge is insufficient
Earlier chapters told you what PENABLE should do; this chapter is about the gap between that ideal and the ways real RTL gets it wrong, which the earlier material does not enumerate.
- Knowing the two-phase rule is not the same as knowing its failure modes. Chapter — why two phases and the PENABLE deep dive teach the rule and the intent: SETUP gives the subordinate a guaranteed cycle to decode the address before the ACCESS strobe arrives. That is the correct behaviour. But a rule stated positively does not tell you what a violation looks like on a scope, nor which line of RTL produces it. The failure catalogue — PENABLE in SETUP, PENABLE stuck high, PENABLE without PSEL — is a separate body of knowledge from the rule itself, and it is what you actually use at 2 a.m. staring at a capture.
- The phase mechanics describe the manager's intent, not the bugs in its implementation. SETUP-phase mechanics and ACCESS-phase mechanics walk the clean sequence. Real managers, though, drive PENABLE from FSMs that have an extra state, a missing state, a combinational shortcut, or a back-to-back path that forgets to dip through SETUP. None of those appear in the idealised mechanics — they are implementation pathologies, and recognising them requires a different lens.
- The strobe semantics tell you what PENABLE means, not how it is mis-built. PENABLE as the enable strobe explains that PENABLE is the "go" pulse for the access. But "PENABLE is a strobe" is precisely the framing that leads to the most common bug: an engineer who thinks "strobe" reaches for a combinational decode or a pulse generator, when PENABLE must in fact be a registered FSM output that is deliberately held, not pulsed, across wait states. The semantic mental model and the correct RTL idiom can quietly diverge.
So the knowledge to add is the bug taxonomy itself: a named set of PENABLE failure families, each with a waveform signature and a root-cause RTL pattern, layered on top of the rule you already know — because the rule tells you the destination and this chapter tells you all the ways the road bends.
3. Mental model
The model: PENABLE is the registered output of a one-deep state machine with exactly two live states — SETUP and ACCESS — and it is asserted in, and only in, ACCESS, and only while PSEL is high. Picture a token that, when a transfer starts, lands on SETUP for exactly one cycle (PENABLE low) and then steps to ACCESS (PENABLE high), where it sits until PREADY lets it leave. PENABLE is just "is the token on ACCESS?" registered into a flop. Every PENABLE bug is the token doing something it must not: starting on ACCESS, never leaving ACCESS, sitting on ACCESS with no PSEL underneath it, flickering between cells within a cycle, or jumping ACCESS→ACCESS without passing back through SETUP.
Three refinements make the model precise and interview-ready:
- PENABLE is registered, never combinational. The cure for half the bug families is the same single rule: PENABLE comes out of an
always_ff, derived from the FSM state, not out of anassignthat decodes PSEL or the address. A combinational PENABLE inherits every glitch on its inputs and can rise the same cycle PSEL does — which is the skipped-SETUP bug. Registering PENABLE one cycle behind the SETUP entry is what guarantees the SETUP cycle exists. - Every new transfer must pass through SETUP, even back-to-back. Back-to-back is legal and common:
PSELstays high across the boundary, butPENABLEmust drop to 0 for exactly one cycle to mark the new SETUP, then rise again. The FSM must route ACCESS→SETUP→ACCESS, never ACCESS→ACCESS. A PENABLE that stays high across two accesses has skipped the SETUP of the second one — the subordinate either misses the new transfer or merges it with the old. See the transfer lifecycle for the full state walk. - PENABLE is meaningless without PSEL, and is only an ACCESS strobe when both are high.
PENABLE=1, PSEL=0is an illegal state — there is no transfer to enable. The FSM must qualify PENABLE on PSEL so it is structurally impossible for PENABLE to be high outside a selected transfer; see the PSEL select signal for why select must precede and bracket every enable.
4. Real SoC implementation
In real APB RTL the PENABLE bugs are small — often a single wrong line — and the fix is almost always "stop computing PENABLE combinationally and drive it from a registered SETUP→ACCESS FSM, qualified by PSEL." Below are the wrong-vs-correct pairs for the highest-frequency families, using the real APB signal names throughout.
Family 1 — PENABLE asserted in SETUP (the skipped SETUP cycle). This is the single most common PENABLE bug. A manager ties PENABLE to PSEL, so PENABLE rises on the same edge PSEL does and the bus enters ACCESS on cycle one — there is no SETUP cycle, and the subordinate has no guaranteed window to decode paddr before the access strobe.
// WRONG — PENABLE combinationally equal to PSEL. No SETUP cycle ever exists:
// PENABLE rises the same edge PSEL rises, so the very first cycle is ACCESS.
assign penable = psel; // <-- skips SETUP entirely
// CORRECT — PENABLE is a registered FSM output, one cycle behind SETUP entry.
// SETUP: psel=1, penable=0 for exactly one cycle. ACCESS: penable rises next.
typedef enum logic [1:0] {IDLE, SETUP, ACCESS} apb_state_t;
apb_state_t state;
always_ff @(posedge pclk or negedge presetn) begin
if (!presetn) begin
state <= IDLE;
psel <= 1'b0;
penable <= 1'b0; // reset value: deasserted
end else begin
case (state)
IDLE : if (req) begin
state <= SETUP;
psel <= 1'b1; // select asserted in SETUP
penable <= 1'b0; // <-- PENABLE LOW in SETUP (the key cycle)
end
SETUP : begin
state <= ACCESS;
penable <= 1'b1; // <-- PENABLE rises one cycle after PSEL
end
ACCESS: if (pready) begin
state <= IDLE;
psel <= 1'b0;
penable <= 1'b0; // deassert cleanly on completion
end
endcase
end
endFamily 2 — PENABLE high without PSEL. An FSM whose PENABLE flop is not gated by the select condition can leave PENABLE high after PSEL has dropped — an ACCESS strobe with no transfer under it. The slave should never see this, and a protocol assertion will flag it, but the root cause is the manager's RTL.
// WRONG — penable updated independently of psel; it can outlive the select.
always_ff @(posedge pclk or negedge presetn)
if (!presetn) penable <= 1'b0;
else if (in_access) penable <= 1'b1; // never tied back to psel
// (psel drops elsewhere, penable lingers high -> illegal PENABLE & !PSEL)
// CORRECT — penable can only be high when psel is also high; they fall together.
always_ff @(posedge pclk or negedge presetn)
if (!presetn) penable <= 1'b0;
else if (state == ACCESS) penable <= 1'b1;
else penable <= 1'b0; // any non-ACCESS state -> 0
// and psel is driven 1 in SETUP and ACCESS only, so PENABLE is bracketed by PSEL.Family 3 and 4 — PENABLE never deasserting / back-to-back with no SETUP gap. When a manager pipelines transfers, the dangerous shortcut is to keep PENABLE high from one ACCESS straight into the next. PENABLE must dip to 0 for exactly one cycle — the new SETUP — even though psel stays high across the boundary. See back-to-back sequencing in the transfer lifecycle.
// WRONG — on completion with another request pending, the FSM goes
// ACCESS -> ACCESS, holding penable high. The new transfer has NO SETUP cycle;
// the subordinate either misses it or merges it with the previous one.
ACCESS: if (pready)
state <= next_req ? ACCESS : IDLE; // <-- skips SETUP, penable stays 1
// CORRECT — back-to-back routes ACCESS -> SETUP -> ACCESS. PSEL holds high;
// PENABLE drops to 0 for the new SETUP cycle, then rises for the new ACCESS.
ACCESS: if (pready) begin
if (next_req) begin
state <= SETUP; // new transfer re-enters SETUP
psel <= 1'b1; // <-- PSEL stays high across the boundary
penable <= 1'b0; // <-- PENABLE dips to 0 for the new SETUP
paddr <= next_addr;
end else begin
state <= IDLE;
psel <= 1'b0;
penable <= 1'b0;
end
endFamily 5 — PENABLE glitch / not registered. A PENABLE produced by combinational decode can pulse mid-cycle as its inputs settle. Because the slave commits on psel && penable && pready, a glitch coincident with pready can drive a false commit. The fix is structural: PENABLE must be a flop output only.
// WRONG — combinational PENABLE decoded from address/state; glitches on inputs.
assign penable = (state == ACCESS) && addr_in_range(paddr); // hazardous decode
// CORRECT — PENABLE is purely a registered FSM output; no combinational decode.
// The address has already been latched; PENABLE depends only on the flopped state.
always_ff @(posedge pclk or negedge presetn)
if (!presetn) penable <= 1'b0;
else penable <= (state == ACCESS); // glitch-free, registeredTwo facts make this the right shape. First, the cure is one idiom, not six fixes: drive PENABLE from always_ff, derive it from the registered FSM state, qualify it on PSEL, and route every transfer (including back-to-back) through a one-cycle SETUP. That single discipline eliminates Families 1, 2, 4, 5 and the late/early Family 6 at once. Second, PENABLE is held, not pulsed, across wait states — during a long ACCESS the FSM stays in ACCESS and PENABLE stays high until pready; the deep dive on PENABLE behaviour and on PSEL select semantics covers why holding (not strobing) is correct, and why that distinction trips up engineers who model PENABLE as a one-cycle pulse generator.
5. Engineering tradeoffs
The PENABLE bug table is the engineering artifact: each row names a family, its waveform signature, the root-cause RTL pattern, what breaks downstream, and the fix. Building and internalising this table is what lets you debug from a capture instead of from the source.
| PENABLE bug family | Waveform signature | Root-cause RTL | What breaks | Fix |
|---|---|---|---|---|
| Asserted in SETUP (skipped SETUP) | PENABLE rises the same edge PSEL does; first transfer cycle is already ACCESS — no PENABLE=0 cycle | assign penable = psel; — combinational tie | Slave samples paddr/pwdata a cycle early; wrong region decoded; stale data | Register PENABLE one cycle behind SETUP entry from the FSM |
| Never deasserting | PENABLE stays 1 after PREADY, with no PENABLE=0 cycle before the next ACCESS | FSM loops ACCESS → ACCESS | Two transfers merge into one; second transfer lost or mis-addressed | Route ACCESS → SETUP → ACCESS; dip PENABLE to 0 each new transfer |
| High without PSEL | PENABLE=1 while PSEL=0 — an enable with no select | PENABLE flop not gated by select; lingers after PSEL drops | Illegal state; slave may decode an access that does not exist | Gate PENABLE so it is high only in ACCESS, falls with PSEL |
| Back-to-back, no SETUP gap | PENABLE held 1 across two accesses; PSEL high throughout, no dip | Pipelined path keeps PENABLE asserted between transfers | New transfer has no SETUP; slave misses it or re-uses stale paddr | Keep PSEL high but drop PENABLE for one SETUP cycle |
| Glitch / not registered | Brief PENABLE pulse mid-cycle, or a sliver coincident with PREADY | assign penable = <combinational decode>; | False commit on the glitch; corrupted register write | Drive PENABLE from always_ff only — never combinational |
| One cycle late / early | Extra PENABLE=0 cycle (SETUP stretched) or none (SETUP skipped) | Extra or missing FSM state before ACCESS | Throughput loss, or address sampled before stable | SETUP is exactly one cycle; one state between IDLE and ACCESS |
The throughline: five of the six families share one fix — registered PENABLE off a SETUP→ACCESS FSM qualified by PSEL — and the table's value is the signature column, because reading the signature off a capture is what lets you skip straight to the right row. The genuine tradeoff is back-to-back throughput versus simplicity: an FSM that always returns to IDLE between transfers is trivially correct but inserts an idle cycle; an FSM that supports zero-idle back-to-back is faster but is exactly where the "never deasserting" and "no SETUP gap" bugs live. Choosing back-to-back support means you owe the assertion that the new SETUP cycle is always present — performance bought with a verification obligation, not for free.
6. Common RTL mistakes
7. Debugging scenario
The signature PENABLE escape is a subordinate that intermittently reads or configures the wrong register, traced to a manager that skipped the SETUP cycle so the address was sampled a cycle before it settled.
- Observed symptom: a peripheral occasionally returns data from, or writes to, an address adjacent to the intended one —
0x40instead of0x44, say. It is sporadic, appears only at higher bus clock frequencies or when the previous transfer leftpaddrat a different value, and never reproduces in the slow, isolated directed tests. In silicon it looks like a flaky address-decode or a "marginal timing" problem. - Waveform clue: on the capture,
PSELandPENABLErise on the same clock edge — there is no cycle wherePSEL=1andPENABLE=0. The bus goes straight to ACCESS.paddris still transitioning to its new value on that same edge, so the subordinate's address sampler latches the address while it is changing, picking up the previous transfer's high bits. The missing low-PENABLE SETUP cycle is the tell. - Root cause: the manager drove
assign penable = psel;(or an FSM with no SETUP state — IDLE straight to ACCESS). Without the SETUP cycle the subordinate has no guaranteed window to see a stablepaddrbefore the access strobe; whether it decodes correctly depends on combinational settling, which is why it is frequency- and history-dependent. This violates APB (IHI 0024C) §3.1: SETUP must precede ACCESS by exactly one cycle. - Correct RTL: insert the SETUP state and register PENABLE one cycle behind PSEL, so the subordinate always sees a stable address before PENABLE rises:
// FIX: a real SETUP cycle. PSEL asserts with PENABLE low; PENABLE rises the
// NEXT edge. PADDR is registered in SETUP and is stable before ACCESS samples it.
always_ff @(posedge pclk or negedge presetn) begin
if (!presetn) begin
state <= IDLE; psel <= 1'b0; penable <= 1'b0;
end else case (state)
IDLE : if (req) begin state <= SETUP; psel <= 1'b1; penable <= 1'b0;
paddr <= req_addr; end // address latched in SETUP
SETUP : begin state <= ACCESS; penable <= 1'b1; end // strobe one cycle later
ACCESS: if (pready) begin state <= IDLE; psel <= 1'b0; penable <= 1'b0; end
endcase
end- Verification assertion: prove SETUP precedes ACCESS — that on the first cycle of select, PENABLE is low — and cover that the SETUP cycle was actually exercised so the proof is not vacuous:
// On the cycle PSEL first rises, PENABLE must be low (a real SETUP cycle exists).
a_setup_before_access: assert property (@(posedge pclk) disable iff (!presetn)
$rose(psel) |-> !penable);
// And PENABLE must rise exactly one cycle later (SETUP is exactly one cycle).
a_penable_next_cycle: assert property (@(posedge pclk) disable iff (!presetn)
($rose(psel) && !penable) |=> penable);
c_setup_cycle_seen: cover property (@(posedge pclk)
psel && !penable ##1 psel && penable);- Debug habit: when a peripheral decodes the almost-right address, do not start at the address decoder — start at PENABLE. On the capture, look for the cycle where
PSEL=1andPENABLE=0. If it is missing — ifPSELandPENABLErise together — the manager skipped SETUP and the address was sampled before it settled. The absence of the low-PENABLE cycle is the fingerprint, and it points straight at a combinational or stateless PENABLE in the manager.
8. Verification perspective
PENABLE is one of the cheapest signals to assert and one of the most valuable, because its correct behaviour is fully expressible as a small set of temporal properties on the SETUP→ACCESS sequence — and because PENABLE feeds the slave's commit, a PENABLE assertion that fires catches a bug before it corrupts data.
- The core property: SETUP must precede ACCESS, and PENABLE marks the boundary. Every transfer must show a cycle of
PSEL && !PENABLE(SETUP) beforePSEL && PENABLE(ACCESS). The single most useful PENABLE assertion proves PENABLE is low on the first cycle of select and rises exactly one cycle later — this catches the skipped-SETUP, late, and early families at once:
// PENABLE must be deasserted on the first cycle a transfer is selected (SETUP),
// then asserted on the very next cycle (ACCESS) — the two-phase rule, directly.
property p_setup_then_access;
@(posedge pclk) disable iff (!presetn)
($rose(psel) && !penable) |=> (psel && penable);
endproperty
a_setup_then_access: assert property (p_setup_then_access);- PENABLE must never be high without PSEL. A one-line assertion makes the illegal Family-2 state impossible to miss — it is the signal-stability and legality discipline applied to the enable:
// An ACCESS strobe with no select is illegal: PENABLE high implies PSEL high.
a_penable_implies_psel: assert property (@(posedge pclk) disable iff (!presetn)
penable |-> psel);- PENABLE must deassert after completion, even back-to-back. On a completion edge (
psel && penable && pready), the next cycle's PENABLE must be 0 — whether the bus goes idle or straight into the next SETUP. This is the Family-3/Family-4 guard, and it is exactly the legal/illegal transition check applied to the access phase:
// After a completed ACCESS, PENABLE must drop for one cycle (the next SETUP or idle).
// This catches "PENABLE never deasserts" and "back-to-back with no SETUP gap".
a_penable_falls_after_complete:
assert property (@(posedge pclk) disable iff (!presetn)
(psel && penable && pready) |=> !penable);- Cover the corners, not just the centre, so the assertions are non-vacuous. A
coverforpsel && !penable ##1 psel && penableproves a real SETUP cycle was exercised; acoverfor a zero-idle back-to-back ((psel && penable && pready) ##1 (psel && !penable)) proves the re-sequencing path was actually driven. Without these, the assertions can pass simply because the corner was never reached. The APB monitor reconstructs each transfer's phase sequence fromPSEL/PENABLE/PREADYand feeds these covers, while the assertions above run continuously alongside it.
The point: PENABLE correctness reduces to three temporal facts — SETUP precedes ACCESS by one cycle, PENABLE implies PSEL, PENABLE falls after completion — and a handful of covers that prove those facts were exercised. Three asserts and three covers catch all six bug families and fire before any false commit reaches a register.
9. Interview discussion
"Walk me through the ways PENABLE gets driven wrong, and how you'd debug one from a waveform" is a high-signal question because it separates engineers who memorised "PENABLE is high in ACCESS" from those who have actually debugged a manager.
Lead with the framing that unifies everything: almost every PENABLE bug is the same root cause — PENABLE was treated as a combinational decode or a second select instead of a registered output of a SETUP→ACCESS FSM qualified by PSEL. Then enumerate the families so the interviewer hears a list, each with its signature: PENABLE asserted in SETUP (rises the same edge as PSEL — no PENABLE=0 cycle, slave samples a cycle early; the most common one), PENABLE never deasserting (stays high after PREADY, FSM loops ACCESS→ACCESS, two transfers merge), PENABLE high without PSEL (an illegal enable-with-no-select), back-to-back with no SETUP gap (PSEL held high but PENABLE not dipped for the new SETUP), PENABLE glitching (combinational decode pulses mid-cycle and can drive a false commit), and PENABLE one cycle late or early (an extra or missing FSM state). The depth flourishes are three: why the happy-path test misses it — a lone directed transfer still eventually shows psel && penable, so it passes while the address was sampled early; the debug fingerprint — on a capture, look for the cycle where PSEL=1, PENABLE=0; if it is absent, the manager skipped SETUP; and why PENABLE must be held, not pulsed — across wait states the FSM stays in ACCESS and PENABLE stays high until PREADY, which is why a pulse-generator model is wrong. Closing with "and the fix is almost always one idiom — register PENABLE off the FSM state, qualify it on PSEL, route every transfer including back-to-back through one SETUP cycle — guarded by three assertions: SETUP precedes ACCESS, PENABLE implies PSEL, PENABLE falls after completion" shows you see PENABLE bugs as a family with a single cure, not six unrelated incidents. For more on the traps, see SETUP/ACCESS interview traps and the protocol rules catalogue.
10. Practice
- Enumerate the families. Without looking back, list the six PENABLE bug families, and for each give its one-line waveform signature and the root-cause RTL pattern in a phrase (e.g. "rises with PSEL →
assign penable = psel"). - Read the capture. You are handed a trace where
PSELandPENABLErise on the same edge and a peripheral occasionally decodes the wrong address. Name the bug, explain why it is frequency- and history-dependent, and write the one assertion that would have caught it. - Fix the back-to-back FSM. Given an
ACCESS: if (pready) state <= next_req ? ACCESS : IDLE;line, rewrite it so back-to-back transfers route through a one-cycle SETUP —PSELstays high,PENABLEdips to 0 — and state which family the original line causes. - Classify each PENABLE observation. For each, name the family and whether it is illegal-on-the-bus (a checker must reject) or a manager RTL defect that produces legal-looking-but-wrong timing: (a)
PENABLE=1, PSEL=0; (b)PENABLEhigh for two accesses with no dip; (c)PENABLErising the same edge asPSEL; (d) a one-cyclePENABLEglitch coincident withPREADY. - Write the assertion triad. Write the three SVA properties that together cover all six families — SETUP precedes ACCESS by one cycle, PENABLE implies PSEL, PENABLE falls after a completed access — and the two covers that make them non-vacuous (a real SETUP cycle, and a zero-idle back-to-back).
11. Q&A
12. Key takeaways
- PENABLE is the registered output of a one-deep SETUP→ACCESS FSM, qualified by PSEL — not a second select and not a combinational decode. Building it any other way is the root cause of nearly every PENABLE bug. The two-phase rule of APB (IHI 0024C) §3.1 is the contract PENABLE must implement.
- The six recurring families are: asserted in SETUP (skipped SETUP cycle), never deasserting, high without PSEL, back-to-back with no SETUP gap, glitching, and one cycle late/early — and each has a distinct waveform signature you can read off a capture before opening the source.
- The debug fingerprint for the most common bug is the absence of the
PSEL=1, PENABLE=0SETUP cycle: if PSEL and PENABLE rise on the same edge, the manager skipped SETUP and the subordinate sampled the address a cycle early — which is why wrong-address decodes are frequency- and history-dependent and invisible to slow directed tests. - PENABLE is held, not pulsed: across wait states the FSM stays in ACCESS and PENABLE stays high until
PREADY. Modelling it as a one-cycle strobe breaks every wait-stated transfer; a combinational PENABLE can glitch coincident withPREADYand drive a false write commit. - Five of the six families share one fix — register PENABLE off the FSM state, qualify it on PSEL, route every transfer (including back-to-back) through exactly one SETUP cycle — so the cure is an idiom, not six separate patches.
- PENABLE correctness reduces to three assertions plus covers: SETUP precedes ACCESS by one cycle (
$rose(psel) |-> !penable), PENABLE implies PSEL (penable |-> psel), and PENABLE falls after a completed access ((psel && penable && pready) |=> !penable) — caught continuously by APB assertions and made non-vacuous by covers the APB monitor feeds.