L3/03 — X and initialisation
Background
When a chip powers up, its flip-flops hold arbitrary values — physically, whichever way each bistable circuit happened to tip as the supply ramped. Hardware practice represents this ignorance with a third logic value, X, meaning "unknown: could be 0, could be 1." A freshly powered design is all-X, and a reset sequence exists precisely to fight X: registers with a reset connection get driven to definite values, and definiteness then propagates as the machine runs. But not every register has a reset connection — adding one costs area and wiring, so designers deliberately leave uninitialised any register whose value provably doesn't matter until first written (a register file is the classic case: garbage in a register you haven't written yet is harmless, because reading it was never meaningful). The result is that a real design's early life is a mixed X-and-definite state, converging toward definiteness at a rate the designer controlled by choosing which resets to pay for.
Reasoning about this uses ternary simulation (industrially, "X-propagation" or X-prop analysis): run the design's logic over the three-valued domain {0, 1, X}, where each gate maps unknown inputs to unknown outputs except where a known input forces the answer (0 AND X = 0 — the X never mattered). A ternary run of the reset sequence starting from all-X computes, conservatively, exactly which bits are guaranteed definite afterward — and because it starts from all-X, its conclusion holds from arbitrary pre-reset garbage, which is what lets one proof serve power-on, brown-out recovery, and post-upset reset alike.
The chapter's actual subject is a mismatch this creates. The semantics defined in 00 is two-valued — every register always holds a definite bitvector — because two-valued semantics is vastly more tractable for the refinement proof above. That is a strengthening of reality, and unjustified strengthenings are how proofs come to be about the wrong machine. The resolution below splits the gap three ways — prove X is eliminated where the spec claims definiteness, match X against the spec's own reset nondeterminism where the standard itself says "unspecified," and prove the residue never influences anything observable — with the second arm being the elegant one: the ISA's deliberate underspecification (choice C1 in L4/02) turns out to be exactly shaped to absorb the hardware's uninitialised registers.
Statement
⟦RTL⟧ as defined is two-valued — every register holds a definite bitvector — which is a strengthening of reality: power-up state is all-X (L1/03's value lattice), and real cores deliberately leave registers unset. The obligation is to justify the strengthening exactly where it is used and refine it where it is not justifiable.
The resolution, in three parts
Where the spec claims definiteness, prove X-elimination. pc, the FSM state, and reset-defined CSRs must be definite after reset. The obligation: the reset sequence, run in ternary semantics from the all-X state, drives these bits definite. This is checkable by ternary symbolic simulation (industrial "X-prop" verification), and its quantification over the all-X start state means it covers arbitrary pre-reset garbage — so brown-out recovery and SEU-recovery reset ride on the same proof (L5's epoch model consumes exactly this).
Where the spec permits nondeterminism, refine into it. RISC-V leaves general registers unspecified at reset. Implementation-X on those bits is not eliminated but matched: the refinement maps untracked implementation state into the spec's own reset nondeterminism. The register file simply never needs an X-elimination argument — a large saving discovered by aligning the obligation with what the spec actually claims.
Where neither applies, prove value-independence. Any remaining uninitialised bit must never flow to an observation before being written. In ternary terms: X from that bit never reaches a definite-claimed output. These are the classical value-independence lemmas, now stated as X-flow properties — per-bit, mechanical, and expected few after the first two parts have consumed the bulk.
The initial blocks and the X idioms
The census found 212 initial blocks — overwhelmingly one machine idiom, the compiler's register-randomization initializer, whose entire body sits behind simulation-only macro guards. With those macros undefined (every synthesis run), the blocks are empty: no register in the design carries a power-up value, which is exactly the all-X starting point this chapter's ternary story wants, stated by the emitter itself. The idiom exists so that simulation can start from randomized rather than zeroed state — the ecosystem's own defence against code that accidentally relies on uninitialised registers reading zero, i.e. a fuzzer for precisely this chapter's third obligation.
The design's 23 'bx literals are also one idiom: behavioural memory models yield X on a read with the enable low (read_data = en ? mem[addr] : 'bx). Per site, that is a declared don't-care — the generator asserting that disabled-read data is never consumed — which converts directly into a value-independence obligation: X from a disabled read never reaches a definite-claimed output. (In the hardened netlist these models are replaced by SRAM macros whose disabled-read behaviour is the macro contract's business — the RTL X-site and the macro contract must agree, a small cross-layer check.)
Interfaces
This file is where three layers meet, deliberately thin: L1/03 supplies the value lattice and the claim that reset is an X-elimination event; L2/03's ρ requires the reset-state correspondence this file establishes; L5's epoch model consumes "X-elimination from arbitrary state" as its per-epoch base case. The proof lives once, here.
Obligations
- The ternary reset simulation for the definite-claimed set (pc, FSM, CSRs).
- The spec-nondeterminism matching clause in the refinement statement (with L3/L4: which architectural state is reset-unspecified).
- The residual value-independence sweep.
- The disabled-read value-independence sweep over the 23 memory X-sites, and its agreement with the SRAM macro contracts.
Effort
Weeks, mostly tooling for the ternary simulation; the conceptual work was done when the obligation was split three ways.