L5/04 — Power epochs

Background

Nothing in an ISA manual says what happens when you turn the computer off, because from the software's point of view nothing can happen — there is no software anymore. But a theorem about a physical chip has no such luxury: power arrives, wanders, sags, and vanishes on the environment's schedule, and the spec must be true through all of it. This chapter is about the machinery — physical and logical — that makes that possible, and it uses a vocabulary of small analog circuits that deserve introduction.

Start with what actually happens at power-on. The supply voltage does not appear; it ramps, over milliseconds, through every value between 0 and 1.8 V. During the ramp the chip's logic is in no valid state — flip-flops wake up holding arbitrary values, and below operating voltage the gates cannot even be trusted to compute. The standard remedy is a power-on reset (POR) circuit: a small analog block that holds the chip's reset line asserted from the moment any power exists until the supply has been stable for a while, then releases it once, cleanly. On release, every register with a reset connection loads its defined initial value, the program counter points at the boot address, and execution begins. One continuous run — from that release until power goes away — is what this book calls an epoch; the chip's lifetime is a concatenation of epochs separated by dark gaps, and the top-level theorem, which covers one epoch, must be composed across them.

The genuinely nasty case is not power loss but power sag — a brown-out. Flip-flops retain their state down to a voltage well below the minimum at which logic operates correctly. Between those two thresholds lies a gray band: a supply excursion that dips into it and recovers leaves the machine with silently corrupted state, still running, having triggered nothing — neither a clean death nor a valid continuation. The standard industrial defence is a brown-out reset (BOR) or supervisor: a cheap, self-contained part (on-board or on-die) that watches the supply rail with an analog comparator and asserts reset the moment the rail leaves the valid range, holding it until the rail has recovered and settled. Whether such a part actually closes the gray band — including the awkward regress that the watcher is powered by the rail it watches — is the substantive question this chapter answers.

Two more pieces of bench vocabulary. The decoupling capacitors ("decaps") scattered across the die in their tens of thousands are small charge reservoirs that smooth the supply against fast demand spikes; here they acquire a third formal job, as the energy store that guarantees the supervisor wins its race against a collapsing rail. And a hold-up capacitor is the same idea writ large at board level: a bulk capacitor storing enough energy that, when the input power fails, the chip has a known number of milliseconds of clean supply left — enough, if a warning signal fires, to finish the byte in flight and park somewhere quiet instead of dying mid-symbol.

Statement

The top-level statement covers one powered epoch: POR-released reset through T in-envelope cycles. The lifetime claim is a concatenation — obs = boot·trace₁ · gap · boot·trace₂ · … — and this file owns its composition: the per-boundary requirements, how power meets the ISA, and the brown-out resolution.

Per epoch boundary

  • V8 (L0/04): supply ramps follow the sequencing/rate constraints — the transitions between U and powered are trajectory conditions the steady-state envelope does not cover (multi-rail bring-up can forward-bias junctions and reach latch-up's branch while the wells are not yet protected).
  • The POR contract (X4-class): this design carries no analog POR block of its own — the arrangement lives in the pad-frame harness or on the board — so the contract is assumed, in its standard shape: reset asserted from power-good to supply-stable, released synchronously with a running clock, once.
  • Per-epoch X-elimination, refined by the spec: reset drives definite only what Sys(F) claims definite (pc, FSM, reset-defined state); elsewhere implementation-X is matched by the ISA's reset nondeterminism (L3/03's three-way split). The proof quantifies from all-X ⊇ arbitrary garbage, so brown-out recovery and SEU-recovery reset share this one obligation.
  • The boot-window promise: the pads have fixed functions and reset-defined drive states, so obs during boot is spec'd by hardware defaults, not demonic — the obligation is to extract and check those defaults from the RTL (UART TX idle-high, the serial link's valid lines deasserted, JTAG TDO passive).
  • How F persists. This chip has no writable persistent store: the boot ROM's contents are fixed at mask time (immutable by construction — the strongest possible answer to the F-evolution question), the data memory is volatile, and anything beyond the pads is X4's business. So the epoch-composition theorem carries one of two hypotheses: F is ROM-resident (immutability free), or F is loaded each epoch over the debug module or serial link — in which case "the same F arrives every epoch" is an explicit assumption on the environment, exactly the kind of clause that belongs in the composition rather than in anyone's intuition. Crash consistency, the deep problem writable persistence forces, simply does not arise on-die.
  • ε sums over powered time; aging (electromigration, NBTI, thermal cycling) scopes P4/P5 to the die's rated lifetime — the honest horizon of the whole theorem.

One power domain. The design has a single core rail — no mid-epoch domain switching, no power islands — which deletes the partial-cycling containment obligations that multi-domain chips carry. (The gap between core rail and IO rail still exists, and returns below as the partial-rail fault.)

How this meets the ISA — which is rightly silent

The ISA's two hooks suffice: its reset section is the power-on hook, and prefix-closed small-step refinement is the power-off hook — a machine that stops violates nothing. Three consequences with teeth:

  1. The epoch's end is prefix · demonic-ramp-down-tail · U (a dying UART TX can glitch a start bit), so prefix closure must hold at the physical alphabet with byte views derived — the constraint that forced 00's alphabet choice.
  2. All liveness is bounded progress ("if powered through cycle N, O by N") — power persistence becomes a per-claim P6 assumption, delivered free by the explicit T every statement already carries.
  3. Crash consistency is out of scope on-die (no writable persistence); whatever sits across the serial link owns its own persistency model (X4).

The brown-out gray band, and its resolution

Sudden full loss is the easy case. The epoch model is unsound against a slow sag below operating minimum but above state retention, recovering without reset — corrupted state, continued execution, neither epoch end nor valid continuation. An RC-ramp POR does not cover the band. The discharge is a supervisor (on-board, X4-class, jellybean part): (A) reset-clamp BOR — assert throughout the excursion, release on hysteresis + timeout — or (B) forced full discharge — load switch + bleed drains the die below retention on any sag, deleting the gray band from the reachable states rather than guarding it.

Rail faults do not go into ε — by category. ε's terms share one shape: continuation despite corruption (SEU, unresolved reads, evading droop) — the machine keeps running with traces that look valid but aren't. A rail fault is terminal, and termination is already free: prefix closure + the specified backstop tail make a fault death ⊑ Sys(F) with probability 1; adding a λ_fault·T term would pay probability for behaviour the spec can admit. (The claim is conditional correctness — while it runs, and however it stops, the trace is in-spec — not availability; component MTBF is a different document.) Three corner checks: the fast-collapse garbage burst (a short crossing the gray band faster than t_detect) is energy-bounded, hence deterministic — the tail admits "≤ t_burst of sub-symbol activity," filtered by the byte-view derivation, rate-independent; recovering transients that evade the BOR are exactly P_droop, which the supervisor shrinks rather than adds to; and the one real gap is the partial-rail fault (core dead, IO alive — level shifters float, output stages still driving): neither terminal nor bounded, engineered away by the fail-safe-IO property in its literal datasheet sense (pads hold safe state with the core unpowered) — an X4-class per-cell property of the sky130_fd_io macros — else it alone would genuinely need a component-FIT ε term.

The apparent regress (the detector is powered by the failing supply) terminates by range stacking + fail-safe polarity: the analog detector's validity range strictly contains the logic's gray band, and below the detector's own floor, deasserting reset requires drive headroom that no longer exists — a passive pull holds reset asserted. The requirement is "output monotone-safe in Vdd," one-sided, an easier computer-assisted-proof target than the oscillator (DC maps + latency bound; M8's interval machinery). Two checkable inequalities close it: traversal — t_detect + t_reset_prop < C·(V_thresh − V_fail)/I_max with C the decap total (the decaps' third formal job) — and hold — reset held past state-death or POR stabilisation. Residue: async-reset assertion effective at degraded voltage (one-sided DC-drive argument, not a timing race).

Hold-up energy makes the common death graceful. One rung above the tamed tail: a bulk capacitor plus an upstream power-fail warning (watching the input, before the storage — the BOR stays on the die rail as backstop) buys a bounded epilogue on stored energy: finish the symbol in flight, refuse new work, park at a quiescent state, then decay. The governing inequality t_holdup(C, I, ΔV) ≥ t_epilogue^max has its right-hand side derived from L3's exported WCET table (L3/08's quantitative reading of the measure): worst-case cycles over the epilogue path with IRQs masked, times a clock-period upper bound valid over the decaying-rail trajectory — the clock source slows as the supply sags, so the seconds-per-cycle factor is taken at the worst voltage the epilogue traverses (V8's temporal sibling). The refinement's own progress bound thus prices the capacitor (µF-scale at this design's draw; a UART byte at 9600 baud ≈ 1 ms ≈ tens of µF), and "we can finish the job in time" is a theorem, not a characterisation. Epilogue routes: warn→IRQ→firmware (drags firmware into the claim) or a hardware quiesce — gate issue at the next commit and drain — bounded by construction; a minor design modification of the kind the project's framing permits. The epoch end then refines once more, warn · epilogue · quiescent-end · decay: a spec event, not a truncation — B3 strengthens to "the last accepted byte is always fully emitted." Structurally this is the boundary ladder's move in the power domain: stored energy converts an asynchronous environmental event into a bounded-latency protocol event, price paid in board space instead of ε. Honest limit: gracefulness is conditional on the failure mode — upstream loss (the common case) goes graceful; a rail fault discharges the hold-up instantly, so the spec keeps a two-tier ending with the truncate-idle-decay tail as the rail-fault backstop.

Good BOR also tames the demonic ramp-down tail. The tail's demonic-ness came from one scenario — the core executing garbage in the gray band while driving pads — and the BOR threshold sitting above that band deletes it: normal operation ends at BOR assertion (in the valid band, pads driven to reset defaults correctly), and below the valid band the chip is already in reset with fail-safe polarity holding. The tail refines to (≤1 truncated symbol) · idle^k · monotone decay — specified, not demonic — under two pad-side conditions: (i) reset defaults are non-hazardous — to be checked in the RTL, with the expected answer that no output pad actively drives a hazardous level at reset (UART TX idles high, so the worst case is one framing error, never a spurious start bit); (ii) the IO cells are fail-safe under collapse — a constant-input driver must not glitch as rails die, with the core-before-IO level-shifter float as the known hazard — an X4-class per-cell property, plus V8 extended to the down-ramp rail ordering. Under architecture (B) even the decay profile is board-controlled (the bleed sets dV/dt). Irreducible residue: truncation timing (environmental), the analog decay (specifiable, not digital), and the fail-safe-IO property itself. The B3 payoff: "under power loss at any point, at most one framing error and never a spurious character" becomes provable rather than caveated.

Obligations

  1. The epoch-composition theorem over 00's alphabet: per-epoch refinement + the boundary requirements ⟹ the lifetime claim.
  2. The F-persistence hypothesis: state the ROM-resident and reloaded-per-epoch variants, and for the latter the environment clause that carries it.
  3. The supervisor's two inequalities, computed from datasheet + decap numbers; the monotone-safe property as a CAP target.
  4. The pad reset-default check against the RTL (the boot-window promise's evidence).

Effort

The composition theorem: weeks once 00 exists. The checks: days each. The supervisor CAP proof: optional depth, L0-machinery.