L1 — The electrical circuit and its constraint system

Node — the EE circuit and its constraint system: the extracted netlist N with per-net RC enclosures (00–02), the timed contract model (03), the SDC constraint set (04), and the crosstalk/IR budgets (05); at this node ε has been traded for a deterministic constraint system. Edge up — the digital crossing: timing closure, the combinatorial geometry/interference checks, and gain-driven restoration together turn the transfer functions into a Boolean machine Mealy(N) — the digital abstraction (06), the bridge theorem (07), verified STA (08), corners (09), the clock (10), boundaries (11), and the geometric checks (12). This edge carries the second of the overview's two † conditioning marks (P1).

This layer is the merge of two bodies of work that share one object. The geometry half (00–02, and its continuous-field enclosures, which live in L0's electrical-abstraction edge) is what defines the EE circuit: the drawn polygons realise exactly the intended netlist, for every chip in the tolerance family, and extraction reads the circuit back out with certified RC. The timing half (03–12) is the digital crossing: given that circuit, the synchronous discipline lifts it to a discrete machine. The node is the circuit; the edge up is the crossing.

Background

The design is a stack of 2D polygon layers; the chip is what a fab printed from them — imprecisely, but within published tolerances. The first job of this layer is to connect the two: the drawn geometry realises exactly the intended circuit, for every chip in the tolerance family rather than the ideal one. The sandwich theorem (01) is what makes design-rule checking on the drawing sound for the fabricated silicon; extraction and LVS (02) read the circuit back out of the polygons; the capacitance enclosures (09) turn geometry into certified electrical intervals; the screening argument (10) is the open problem that makes any of that computable at all; and the geometric checks (12) discharge safety conditions that other layers can only state. 00 opens with how a chip is physically built and what a layout formally is.

The second job is the digital crossing. Everything above this layer treats the chip as a discrete machine stepping once per clock; the circuit this layer defines is a continuous system in which signals race through gates at analog speeds and arrive when they arrive. The synchronous discipline — storage elements that sample only at clock edges, given a full period for the racing to settle — is what connects the two pictures, and the edge up proves that it does: the bridge theorem (07) turns "the design meets timing" into "the discrete abstraction is sound," checked by a verified static timing analysis (08) over certified delay tables (09), conditional on the human-asserted path exceptions being justified (04). The edges of the story get their own chapters: the clock's generation and distribution (10), the boundaries where the world's timing meets the chip's (11) — one of the two places genuine probability enters the project — and the analog interference terms kept out of every interface (05).

The node: the EE circuit

One theorem with three faces defines the circuit, decomposed in the geometry subcomponents:

1. The layout implements the netlist. Ext(M(A)) ≅ N for all A in the family — the sandwich theorem (01) plus extraction/LVS (02).
2. The layout determines RC enclosures, valid over the whole family (09, 10).
3. DRC rules are the hypotheses, not an unstructured pile of manufacturing constraints — (H1)(H2), (D1)–(D3), G1–G6.

On top of that geometric netlist sits the constraint system that replaces ε with something deterministic: each cell carries its timed contract (03), the design carries an SDC — the human-asserted timing exceptions (04) — and the analog residue (crosstalk, IR drop) is absorbed as budgets with a single entry point (05). This is the largest and least-charted node in the tower. On the FPGA alternative the geometry half disappears entirely; the timing half remains.

The edge up: the digital crossing

The bridge theorem. If every cell stays inside its contract's domain, STA certifies setup and hold at every flop at every corner, every excluded path carries a justified exception, the combinatorial geometry checks discharge L0's interference budgets, and no fault event or unresolved synchroniser read occurs in [0,T] — then over [0,T] the physical circuit implements Mealy(N). Full statement and proof sketch in 07; the hypotheses are not yet established for this design — the flow's multi-corner signoff is the F-series' live frontier (axioms).

The crossing has three ingredients, all of the same "combinatorial check over an analog budget" flavour: timing closure (clean sampling instants), the geometry/interference checks (12, discharging L0's budgets), and restoration (gain > 1 collapses each cell's transfer function to a Boolean function — the digital abstraction, 06, which migrates up from the physics). Everything above L1 presupposes this edge and nobody has written it down. It is the highest value-per-effort novel contribution in the project.

Subcomponents

The continuous-field enclosures the geometry face depends on — the two-sided capacitance bounds (09) and the screening exponent (10) — now live in L0's electrical-abstraction edge, because they are analog field arguments; L1 consumes their intervals.

Interfaces

Consumes: GDS, process stack, DRC deck; from L0, the per-cell interval Liberty contracts and the RC enclosures + coupling graph that make up Contracts(N); from L2, the netlist with registers/clock/reset identified; the generated SDC. Exports: the netlist N — the shared object of the overview's tower, the same N this layer times and L2 compares — with per-net RC enclosures and a sparse coupling graph plus one aggregate ε; and, from the edge up, the licence to reason discretely — for the multi-domain design a network of Mealy machines with gadget-bounded channels (11) that collapses to nearly one machine here. Nothing numeric propagates upward except one outward artifact: the derived AC-timing table handed to L5.

The refinement proof never touches RC. Electrical data exists solely to discharge the digital crossing's hypotheses — the cleanest seam in the stack, preserved deliberately: any net that would need a functional coupling constraint is a layout bug, because it would entangle the noise argument with L3's invariant (05).

Axioms introduced

From the geometry face: E7 (as-fabricated geometry within the tolerance family — now also carrying the sandwich's (H3)), P4 (variation within corners), P5 (defect coverage), X3 (T→theorem: retires when M2 lands). From the edge up: P1 (synchronisers resolve — the per-boundary ledger is 11's), P6 (environment — now carrying the whole clock-generation contract, since the clock is board-supplied, 10). Formerly also E3 (discharged — the capacitance enclosures are its route), E6 (retired: yield, not per-die correctness), E4 (split: empirical half → P4, mathematical half → M4), and E5 (subsumed by E2's and E3's discharge routes); see Axioms. The F-series rows are unestablished hypotheses of the bridge theorem, not axioms.

Two things precisification turned up

The sandwich theorem needs a third hypothesis. With only "erosion connected" and "dilations disjoint" it is false: the fabricated set may contain a spurious island inside N ⊕ B_r that meets no eroded net, i.e. a net that does not exist in the drawn layout. The missing hypothesis (H3) — every component of Cond(A) meets Cond(D) ⊖ B_r — is not checkable, since it quantifies over A. It is an assumption about the process and belongs to E7. (No dual hypothesis is needed for voids: extra material creates nets, missing material cannot destroy them, because the eroded net is already connected.)

01's conclusion overclaims. Its statement says the net bijection preserves device-terminal incidence, but its proof handles only nets. Devices are components of poly ∩ active and perturb under their own sandwich; the missing device-level hypotheses (D1)–(D3) are stated in 02. (D3) — terminals stay attached — is exactly where line-end pullback bites, so the enclosure rules are its hypotheses, not the net-level theorem's.

Established during scoping (the geometry face)

The right model of a layout is a coloured image plus a fixed z-extrusion.

d = F(L)                          derived layers; F = booleans + morphology
c : ℝ² → 2^Layer                  pointwise colour
M : ℝ³ → Material,  M(x,y,z) = Z(c(x,y), z)

This is literally what DRC/extraction decks compute (gate = poly AND diff). Two refinements: the algebra is booleans plus morphology (grow/shrink), because self-alignment and diffusion mean the doped extent is the boolean then sized; and the vertical stack is a process constant, which is exactly why a finite extraction pattern library is possible at all. If z varied per design, no library would exist.

The model is exact for interconnect, lossy for devices. BEOL is conductors and dielectrics in fixed geometry — R and C are functionals of M via Laplace, nothing lost. FEOL doping is a continuous 3D concentration profile; the colour only identifies that there is an NMOS here, and (W,L) come from geometry while behaviour comes from a fitted compact model. So verified extraction is available for interconnect and not for devices.

The morphological sandwich, and why DRC is a theorem's hypotheses.

∀ mask m:  erode(D_m + d_m, r_m) ⊆ A_m ⊆ dilate(D_m + d_m, r_m),  |d_m| ≤ overlay_m
           r_m = bias_m(density) + k·σ_m

(a) ∀ nets n: erode(D_n, r) connected              [min width, neck/notch rules]
(b) ∀ n≠n':  dist(D_n,D_n') ≥ r + r' + overlay     [colour-aware spacing rules]
(c) ∀ vias:  enclosure ≥ pullback + overlay        [enclosure rules]
⟹ connectivity_graph(A) = connectivity_graph(D)

Proof is one line each way (erosion spans the net ⟹ connected; dilations disjoint ⟹ no shorts). Min-width and min-spacing rules are precisely (a) and (b). This is self-contained computational geometry — no PDEs, no Sobolev spaces — and converts a large fraction of a DRC deck from folklore into hypotheses. If one piece of the geometry face is formalised first, it should be this.

Caveats: bias is density-dependent so r = r(x); line-end pullback and corner rounding are systematic and are why (c) exists; vias are the dominant open mechanism and are not bounded in-plane at all; multiple patterning makes overlay a rigid per-mask displacement, a different perturbation class, hence colour-aware spacing.

Sub-resolution mask features do not transmit — lithography is a low-pass filter. A gap much smaller than the resolution limit prints as a slight narrowing or nothing. Proof that this is real: sub-resolution assist features work precisely by not printing. So the geometry family to propagate is band-limited, not arbitrary polygon perturbation. Another restoration-like property.

LER does not sever wires; defects do. Severing requires roughness to consume the full width — Gaussian-tail suppressed. The sandwich with r = bias + 4σ is effectively deterministic. Topology changes are Poisson defects handled by test (P5). Same continuous/discrete split as L0.

Extraction is pattern matching against a field-solver-characterised library — template matching on cross-sectional images, with the rule deck as a trained model. The replacement is rigorous enclosures: Dirichlet principle gives upper bounds from any trial potential, Thomson's principle gives lower bounds from any trial flux field, so any pair of trial fields yields a two-sided bracket. Verified-numerics machinery for elliptic BVPs is mature (Nakao, Plum, Watanabe). And the accuracy requirement is soft: ~5% vs field solver, against 10–20% derates already carried — so crude-but-rigorous bounds suffice, which is unusual and makes this viable.

2D may be exactly solvable. Schwarz–Christoffel mapping gives closed-form multiconductor capacitance for piecewise-linear 2D cross-sections in terms of elliptic integrals; verified numerics then only handles the 3D corrections. Better decomposition than treating everything as a 3D PDE.

Corner singularities are the real obstacle. Charge density diverges like r^(−1/3) at a right-angle conductor corner, exactly where the capacitance concentrates. Exponents are analytically known, so graded meshes work — but verified quadrature must handle integrable singularities.

You want enclosures over a geometry family anyway. As-fabricated ≠ drawn (etch bias, LER, CMP). So the right object is "∀ geometries within tolerance, C ∈ [lo,hi]" — which interval methods give naturally and which is arguably more faithful than the point-geometry field solve it replaces.

Below extraction it becomes image processing for real: DRC is polygon booleans; LVS is extraction + graph isomorphism; OPC is literal inverse imaging (simulate partially-coherent image formation, iteratively adjust mask polygons); fracturing is rasterisation, and multi-beam mask writers take a bitmap. Note E7 sits between LVS and the fab: the mask is deliberately not the drawn layout, so LVS-verified geometry is not what prints.

GDS is a clean formal object with dirty corners. A finite set of layer-tagged integer-coordinate polygons plus a hierarchy — far cleaner than Verilog. But: layer numbers are semantically empty (need an external layer map); PATH endcap type 1 is a semicircle so the format isn't purely polygonal; self-intersecting polygons and same-layer overlap semantics are unspecified. Restrict to a well-formed subset. Encouragingly, OpenROAD-era routing streams out as BOUNDARY polygons — so production output lives in a much cleaner subset than the format permits (pinned per layout by the checker).

The geometric combinatorial obligations

L1 owns a set of finite, decidable checks — the discharge points for conditions L0's operating envelope only states (L0/06 has the dispatch table). These are the combinatorial, relational geometry (spacing, taps, "≥ N apart") that make up the geometry ingredient of the digital crossing, as opposed to the continuous field geometry that stays in L0's edge. Stated precisely as G1–G6 in 12: tap coverage, ECC interleaving, antenna ratio, width/spacing/enclosure, shielding coverage, and tied fill.

Two of the six are not properties of the geometry alone — interleaving needs the ECC word structure from L3/L5, and the antenna check quantifies over prefixes of the process order rather than over the finished layout. That is worth carrying as a general caution: some geometric obligations need inputs a layout tool does not record.

The recurring structure, seen from this layer

Three of the project's global patterns surface here in their sharpest forms. The clock edge is a restoration point in time — the induction invariant is fully re-established every cycle, so nothing accumulates (07). The boundary gadgets are phase restorers — the window hypothesis is manufactured on-die, never imposed on the world (11). And the analog residue is confined to single entry points: the power grid enters once as an impedance bound, coupling enters once as an interval widening plus a geometric rule (05) — with the red line that any net needing a functional coupling constraint is a layout bug.

Open problems

From the geometry face:

1. The screening exponent — the load-bearing open problem of the geometry face. The far-field coupling sum does not obviously converge: the count of nets at distance d grows polynomially while unscreened coupling decays only logarithmically. Truncation is justified not by "distant things are small" but by screening making the decay fast enough. The mechanism is a mesh of apertures in series, giving multiplicative attenuation and hence C_far(d) ≲ C_adj · α^(d/p) — exponential in grid cells traversed. The rigorous object is harmonic measure of the aperture set, bounded via the maximum principle (complete enclosure ⟹ exactly zero; this case is topological, not metric, and so combinatorially checkable). Deriving α is a genuine analysis problem and everything in local extraction depends on it (10).
2. Formalising the variational characterisations of capacity — Sobolev machinery, well outside current Mathlib-scale infrastructure.
3. Verified quadrature with r^(−1/3) singularities.
4. Whether metal fill must be tied rather than floating: floating conductors do not screen, they relay, shortcutting an aperture chain. Should be a requirement, not an option.

From the edge up:

5. Write the bridge theorem (07) — bounded-delay model, window rule, per-cycle induction, multi-domain composition (11).
6. A verified STA engine with the three soundness deviations (08): four-corner interpolation, slew intervals, in-pass domain checks.
7. Prove the constraint set complete — every domain declared or its absence a named finding (04).
8. The monotonicity census and the tier model (09) — decides whether M4 is a footnote or a project.

First experiments

This layer holds the whole project's tractable entry point — 04's work plan: census the domains, diff against the generated constraints, and complete or record each gap. Weeks, needs only the flow's own artifacts, and either outcome is worth having. Alongside it, two mechanical censuses that other files consume: library-wide table monotonicity (08/09) and the clock-network cleanliness check (10).

On the geometry face:

• Formalise the sandwich theorem. Self-contained, no analysis, converts DRC into hypotheses. Highest value per effort in the geometry face by a wide margin.
• Run magic/netgen LVS on inv_1 and check the extracted netlist against the intended one; measure what a per-cell LVS obligation costs.
• Sanity-check the screening claim numerically on a toy 2D mesh before committing to open problem 1.

Effort

3–5.5 years for the merged layer: 2–4 years for the geometry face (the widest error bars in the project — open problem 1 could be six months or could be a thesis; the FPGA alternative deletes it entirely) plus 1–1.5 years for the edge up (the theory concentrated in the bridge theorem and the digital abstraction, the rest verified-algorithm work and measurement). The entry-point experiments are weeks.

Reading

Pólya & Szegő, Isoperimetric Inequalities in Mathematical Physics (1951) — rigorous capacity bounds. Nakao, Plum, Watanabe, Numerical Verification Methods and Computer-Assisted Proofs for PDEs. Driscoll on Schwarz–Christoffel. Lööw's HOL4 Verilog semantics and the Silver/Lutsig stack — closest prior art for a verified path from RTL to netlist; note it stops short of the bridge statement. Standard STA texts for the algorithm — none state the soundness bridge. McGeer & Brayton for the false-path/viability criterion (04). Zgliczyński, Galias, Demir–Mehrotra–Roychowdhury for 10's oscillator contract; Marino for why 11's ε is irreducible.