L0/02 — Device models: the nonlinear part

Background

The MOSFET — the transistor of which this chip contains tens of millions — is, to first approximation, a voltage-controlled switch: voltage on the gate terminal creates or removes a thin conducting channel in the silicon between the source and drain terminals. Below a threshold voltage, (almost) no channel and (almost) no current; above it, a conducting path whose strength grows with gate drive. CMOS logic wires these switches in complementary pairs — for every input combination, either a path to the high rail or a path to the low rail, never both — so a gate's output is always actively driven to one rail.

The property that makes digital computation possible is gain: in its transition region, a small change in a MOSFET's input produces a larger change in its output. Gain greater than one is what lets each gate clean up its input — an input at 90% of the rail voltage produces an output at 99.9% — making the rail values attracting fixed points of the gate dynamics. This is the restoration that every layer above has been invoking: noise does not accumulate through a million-gate chain, because each stage snaps its signal back toward the rails. The interconnect, being linear, could never do this; all restoration in the machine comes from the devices, which is why this file calls them "the reason the digital abstraction exists" and why their model bears more epistemic weight than their share of the delay numbers would suggest.

How is the device's current-voltage behaviour actually known? Not by solving the drift–diffusion PDE — the chapter walks through why that route is barred (no uniqueness theorem, hopeless cost). Industry's answer is the compact model: a large fitted formula — BSIM4, the standard used by this process, has hundreds of parameters — calibrated against measured silicon until it reproduces the terminal currents across the operating range. It is an excellent description and in no sense a derivation, and the assumption "the fitted model faithfully describes the physical device" is the project's deepest empirical axiom (E1) — the one 05 later argues is irreducible no matter how deep one digs. Above the compact model sits one more abstraction this chapter needs: the switch-level model (Bryant's MOSSIM tradition), where the transistor is just a switch with a strength and the analysis tracks which nodes get driven, fought over, or left floating — the coarse level at which "this cell computes NAND" is actually read off. The load-bearing chain is switch-level resting on compact model resting on measurement, and the chapter's job is to make each link an explicit enclosure rather than a point-value trust.

A crash course in Bayesian inference

One tool the later sections lean on deserves its own introduction, because it is what turns "a model fitted to measurements" from a hand-wave into a bounded statement: Bayesian inference, the arithmetic of updating belief with data.

The setup is always the same. There is an unknown you care about — here, the device's physical parameters θ (a doping profile, a few mobility and recombination coefficients), fixed but unmeasured. You have data D — terminal I–V and C–V curves, a SIMS trace — each reading carrying measurement noise. And you have a forward model that, given parameters, predicts what those measurements should read. Three ingredients combine:

  • The prior p(θ): what is known about θ before this data — physical constraints, not guesses. Doping is positive; it varies smoothly on the scale of a Debye length; mobilities sit in a known band. The prior is where physics that isn't in the data enters.
  • The likelihood p(D | θ): how probable the observed data is if θ were the truth — the forward model's prediction compared against D through the measurement-noise model (a reading many σ off nominal is exponentially unlikely). This is where the data pulls.
  • The posterior p(θ | D) ∝ p(D | θ)·p(θ): belief about θ after the data, by Bayes' rule — the prior reshaped by the likelihood, sharpened wherever the data is informative, left at the prior wherever it is silent.

The normaliser (the integral of the numerator over all θ, the evidence) is what makes this a probability, and computing the posterior it defines is the whole practical difficulty: for a few parameters with conjugate structure it is a formula, but for a PDE forward model it is a high-dimensional integral, done either by sampling (MCMC — draw θ's in proportion to the posterior; cheap, but the answer carries Monte-Carlo error) or, when you need a bound rather than an estimate, by validated integration over θ-space (rigorous, expensive).

The payoff is the credible interval: for any quantity Q(θ) you actually want — a delay, an I–V at an unmeasured bias, a stress response — push the posterior through Q and read off a region that holds it with posterior probability ≥ 1 − δ ("the true delay lies in [a, b] with probability 0.999"). That is the object the reforged E1 below produces, and it is why a fitted model can say something bounded about points it never measured: the forward model carries belief from the measured points into the unmeasured ones, and the prior keeps the extrapolation honest. Two cautions travel with it, developed below — the answer depends on the prior, so it must be declared; and the likelihood silently assumes the forward model is correct, so an approximate model needs an explicit discrepancy term or its posterior will be confidently wrong. (The one place the project already needs probabilistic machinery — ECC sufficiency, 03 — is a cousin of this; the reasoning layer is shared.)

Statement

Give each transistor a terminal I-V relation valid over the operating range, as an enclosure rather than a point value, and identify what that relation rests on.

This is where the nonlinearity lives, where restoration comes from, and where the project's deepest empirical axiom sits.

Why devices are special

The interconnect is linear: superposition applies, the network has a rational transfer function, model order reduction is exact, and rigorous enclosures are available (L1).

Devices are nonlinear, and they are the reason the digital abstraction exists — gain

1 in the transition region is what makes the rails attracting fixed points. So they carry disproportionate importance relative to their contribution to the numbers (which is smaller than interconnect's at any modern node).

Three routes, and their costs

Route A — solve drift–diffusion. The van Roosbroeck system. Existence established; uniqueness not known in general and genuinely false where latch-up or snapback occur (see 00). Even setting that aside, a per-device PDE solve is computationally hopeless at 400 cells × operating range × corners.

Route B — compact models (what industry does). BSIM or PSP: fitted algebraic relations with hundreds of parameters, calibrated against measured silicon. Deterministic, fast, composable. Cost: axiom E1, unfalsifiable in principle, and it gets thicker at smaller nodes as quantum confinement, quasi-ballistic transport and self-heating are folded into the fit.

Route C — switch-level abstraction. Model the MOSFET as a bidirectional switch with strength and charge sharing (Bryant's MOSSIM lineage; Melham's HOL CMOS work). This is the target abstraction for producing Boolean functions, and it is far coarser than either of the above.

The chain actually used is C resting on B: the switch abstraction's justification is the device's I-V characteristic, which comes from a fitted model. There is no route to a Boolean function that avoids either a non-unique PDE or an underived fit.

With foundry-level control there is a fourth option worth noting: define the cell library at transistor level and prove cell → Boolean via switch-level modelling, pushing the axiom down to "the switch-level MOSFET abstraction is sound." That covers the whole library at once instead of per-cell characterisation, and is a strictly better axiom. Not available for validating someone else's shipped design.

What must actually be proved

For each cell, the obligation is not "the device model is right" but:

Given the device model as an enclosure over the operating range and corners, the cell's terminal behaviour lies within a region from which the Boolean function can be read off with positive noise margin.

Two things follow. First, the device model enters as an interval, so E1's fidelity claim is "the true I-V lies in the enclosure," which is weaker and more defensible than "the model is correct." Second, the switch-level abstraction only has to be valid coarsely — you need the ON/OFF distinction and enough gain, not accurate currents.

For the interval representation itself, plain intervals will be too loose — terminal currents share the same underlying parameters, and naive intervals count that uncertainty independently at every use. The standard remedies are affine arithmetic (de Figueiredo & Stolfi), which tracks first-order correlations, and Taylor models (Makino & Berz) for higher order; both are mature and both have validated implementations.

Route A, reconsidered — and E1 as a credible enclosure

"Three routes" filed Route A under barred, on two objections; both are softer than they look, and what remains reshapes E1 rather than forbidding it.

The uniqueness objection is already handled — one level up. 00 does not assume the device PDE has a unique solution; it quantifies every downstream claim over all solutions, converting non-uniqueness from a blocking assumption into a reachability obligation. An enclosure that holds for every solution branch does not need uniqueness. (The parasitic branch — latch-up — is then excluded not by a uniqueness theorem but by the tap-coverage side condition below.) So the first objection bites only if you demand a single trajectory; for the enclosure it is a red herring.

The data objection is dischargeable by measurement. Route A is "blocked by data" (axioms.md, D4) because the doping profiles are unpublished. But you do not need the foundry's numbers — you identify them from the fabricated die: C–V profiling for net doping versus depth, I–V families across geometries for channel doping and V_th, SIMS for the chemical profile on a sacrifice, and standard TCAD inverse calibration to fit the model's parameter fields to that data. This is the project's own per-die stance applied to the device: measure the object, don't trust the spec sheet. The data floor becomes bulk material data measured on this process — exactly where 05 already places it.

Why you would want it, not merely tolerate it. This is the argument that makes Route A worth its cost, and it is 07's own argument moved down a level. A compact model fit to measurements is a point cloud with an interpolant: it asserts values where it was characterised and whatever its basis functions invent between, and goes vacuous outside the box (finding F2). A drift–diffusion solve over identified parameters is a physically-constrained continuum: once a handful of physical fields (doping, mobility, recombination) are fixed, the model's value at an unmeasured bias, corner, or disturbance is a consequence of Poisson-plus-transport, not a choice of spline. That is a low-capacity, well-validated prior, and evaluating it everywhere is principled generalisation — the same reason 07 prefers a derived interval-Liberty with an inter-sample derivative bound over the shipped point .lib, which "asserts values at the sample points and nothing in between." Points cannot bound between samples; a model can. The project already stakes this for the cell DAE; consistency demands it for the device. And it is the only vehicle for the disturbance response the envelope now quantifies over — no measurement visits every mechanical stress (04, V9) or every injected forcing (V10), so bounding those requires a model that carries the physics into regions no probe reaches.

What actually remains is validated numerics: rigorous enclosures for the nonlinear van Roosbroeck system at device scale (harder than L1's linear elliptic enclosures, and genuinely frontier), plus a conservative interval identification of the feasible parameter set. Hard, partly open — but mathematics, not a barred door.

E1, reforged. The inverse problem is ill-posed: many parameter fields fit the same terminal data and may disagree off-sample. So the honest object is not one trajectory but a set — one physical solution per parameter field consistent with the measurements — and the enclosure is their envelope. Two ways to close it, and the second is the natural one here:

  • Deterministic (interval). Take the union of DD solves over the whole measurement-consistent parameter set: a guaranteed hard enclosure, no probability, as loose as the feasible set is wide. Composes with E1 in its present "the true I–V lies in the enclosure" form.
  • Bayesian (credible). Put a posterior p(θ | D) on the parameters — a physical prior times a likelihood built from the forward model and the measurement-noise model — and push it through the (validated) DD solve. Every downstream quantity gets a credible enclosure: "the true I–V lies in this interval with posterior probability ≥ 1 − δ." Tighter than the worst-case union, and — the point — it composes with a conclusion that is already probabilistic. The tower ends in obs ⊑ Sys with probability ≥ 1 − ε(T); a credible E1 stops being a hard axiom propping up a probabilistic conclusion and becomes one more term in ε (the epistemic term of 03). The silent "modulo E1" asterisks become a number.

Rigour here is more than running a sampler, and each requirement drags a hidden assumption into the open — which is the gain:

  1. The prior is declared. Credible sets depend on it. State the physical prior as an explicit, tunable assumption (positivity and smoothness of the doping field, physical ranges) — an honest replacement for the brute "BSIM contains the truth" — or robustify: imprecise-prior Bayes over a set of priors gives interval-valued posteriors, and conformal calibration gives distribution-free coverage with no prior at all.
  2. Model discrepancy is mandatory. Calibrate an approximate model without a discrepancy term and the posterior is overconfident (the Kennedy–O'Hagan trap): tight, wrong intervals. So 05's "DD is only regime-valid" residue reappears here as an explicit, quantified discrepancy prior — small at 130 nm, but carried, and bounding it is the honest quantitative form of "how good is drift–diffusion here."
  3. The posterior is computed with validated numerics, not sampled. MCMC yields an estimate with Monte-Carlo error; a theorem needs validated posterior integration or a rigorous coverage bound (PAC-Bayes), composed with the validated forward enclosure. This is the frontier piece.

None of this eliminates the axiom; it relocates E1 to a smaller, better-structured base — the drift–diffusion regime (cheap at 130 nm, 05), the measured material closures, and a declared prior-plus-discrepancy — and turns it from a deterministic hedge into a quantified, composable, data-shrinkable contribution to ε(T). That is 05's thesis — the axiom relocates, it does not vanish — made probabilistic and honest about its size.

The uniqueness side condition

Latch-up is a second solution branch of the device PDE, and the design rule that eliminates it is tap coverage: every device within a bounded distance of a well tie.

So the layout rule normally filed under "reliability" is really the side condition making the single-branch assumption valid — i.e. a hypothesis of well-posedness, not a manufacturing constraint. It belongs in the same category as L1's min-width rules, which turned out to be hypotheses of a topology-preservation theorem.

This is worth stating as a general pattern: several DRC rules are secretly the side conditions of theorems nobody has written.

Open problems

  1. Uniqueness for stationary drift–diffusion under operating bias, or a characterisation of when the parasitic branch is reachable. Genuinely open.
  2. Turn tap-coverage rules into a proved sufficient condition for single-branch operation.
  3. Formalise a switch-level model with strengths and charge sharing, and prove it sound with respect to an interval-valued compact model. Nobody has done this for a real library.
  4. Self-heating: at advanced nodes it enters the functional path. Absent at 130 nm; record as a scope boundary.

First experiments

  • Take inv_1: extract its transistor netlist (magic/netgen), attach an interval-valued device model, and derive the terminal enclosure. This is the unit that gets multiplied by 400 — measuring it decides where in its one-to-three-year range L0 lands.
  • Check how coarse the device enclosure can be while still yielding positive noise margin. If the margin is large (it should be, at 1.8 V), E1's precision requirement is weak, which materially reduces what must be assumed.

Effort

The inv_1 experiment: days — and it prices the whole layer (see 07). The switch-level formalisation (route C): months.

Reading

Markowich, The Stationary Semiconductor Device Equations. Bryant, "A switch-level model and simulator for MOS digital systems" (IEEE Trans. Computers 1984) — the MOSSIM II model: strengths, charge sharing, and the ternary algebra. Melham, Higher Order Logic and Hardware Verification (1993) — transistor-level CMOS in HOL, the closest existing formalisation of Route C. The BSIM4 technical manual (Berkeley) for what E1 actually asserts — the SKY130 PDK models are BSIM4, evaluated under ngspice; Gildenblat et al. for PSP, the surface-potential alternative. de Figueiredo & Stolfi on affine arithmetic; Makino & Berz on Taylor models.