L1/00 — The layout as a formal object

Background

A chip is built, not carved: it starts as a blank silicon wafer and grows upward through a few dozen processing steps, each one adding, doping, or removing material across the whole wafer at once. The repeating move is photolithography: coat the wafer with a light-sensitive resist, project a pattern onto it through a mask (a stencil, one per patterned step), develop away the exposed resist, and then let the step's real action — etching material away, implanting dopant atoms, depositing metal — act only where the resist is gone. Repeat per layer: first the transistor-forming layers (doped wells in the silicon, the active/diffusion regions, the polysilicon gate material), then, above them, an alternating stack of insulating oxide and patterned metal wiring — met1 through met5 on this process — with vias (small holes filled with metal) connecting one metal level to the next.

The consequence for formalisation is happy: since every step is controlled by a 2D stencil, the entire design content of a chip is a finite stack of 2D polygon sets — one set per layer. That is literally what the design file contains: GDS, the format handed to the mask shop, is a list of polygons with integer coordinates (in database units of 1 nm here), tagged by layer number, organised in a hierarchy of reusable cells. The third dimension is not in the file, because it is not the designer's to choose — the vertical structure (layer thicknesses, what material ends up where when layers overlap) is fixed by the fabrication recipe, identical for every design on the process.

The formal picture this chapter builds is therefore: a drawn layout is a map from layers to polygon sets; a point of the plane has a "colour" — the set of layers covering it; and the process turns colours into materials via a fixed vertical profile, yielding the 3D material distribution that the physics layers below actually analyse. Two further wrinkles the definitions must carry. Some process layers are not drawn directly but derived from drawn ones by boolean combinations and small resizings (the rule deck — a program, supplied by the foundry, that this chapter must treat as part of the spec). And connectivity — which metal shapes form one electrical net — is genuinely three-dimensional, established through vias, so it can only be computed on the assembled stack, never per layer.

Statement

Fix the objects every other L1 theorem quantifies over: what a layout is, what the process turns it into, and which GDS files are admissible.

Nothing here is deep. It is written out because every subsequent statement — the sandwich theorem, LVS, the capacitance enclosures — is a claim about these objects, and they are currently defined only by the behaviour of tools.

Definitions

Layers. A finite set 𝓛, with a distinguished mask assignment col : 𝓛 → Masks (multiple patterning; singleton in the SKY130 case).

Drawn layout. D : 𝓛 → 𝒫(ℝ²), each D_ℓ a finite union of simple polygons with vertices in (δ·ℤ)² where δ is the database unit (exactly 1 nm in SKY130 — measured, Findings). Obtained from GDS by flattening the SREF/AREF hierarchy.

Colour. c_D : ℝ² → 2^𝓛, c_D(x) = {ℓ : x ∈ D_ℓ}. Finitely many values, and only a small subset of 2^𝓛 is realised — the "sparse colouring" of the coloured-image model.

Derived layers. d = F(D) where F is generated by boolean operations and morphology (⊕ B_s, ⊖ B_s). Morphology is not optional: self-alignment and diffusion mean a doped region is a boolean expression then sized. F is the rule deck; it is a program, and formalising L1 means formalising the fragment of it the design uses.

Material distribution. With a process z-profile Z : 2^𝓛 × ℝ → Material,

M(D) : ℝ³ → Material,     M(D)(x,y,z) = Z(c_{F(D)}(x,y), z)

This factorisation is the whole reason L1 is tractable: Z is a process constant, identical for every design on the node, so the extraction pattern library is finite and the design variable is purely the 2D colouring. If Z varied per design, no library could exist. (Second-order caveat: CMP makes thickness density-dependent, so Z carries a correction term depending on local pattern density — see 12.)

Conductive set. Cond(D) = M(D)^{-1}(conductor) ⊆ ℝ³. Nets are its connected components — note this is genuinely 3D connectivity, through vias; the per-layer 2D picture does not determine it.

Admissible GDS

The format permits objects with no agreed meaning. Restrict to a well-formed subset and say so, rather than inheriting tool-specific conventions:

Encouragingly the restriction is expected to cost nothing in practice: OpenROAD-era stream-out emits BOUNDARY polygons for routing, so production output lives in a much cleaner subset than the format allows — a claim the layer's checker pins per layout. The hand-drawn library cells do use PATH (2 in inv_1), so the polygonalisation question is confined to ~400 small files.

What is not determined by D

Worth listing, because these are the inputs to every later theorem and each is an axiom or a separate model:

• Z, the z-profile — process constant, empirical (part of E7's context).
• r_ℓ, the perturbation radii — bias + roughness, density-dependent (E7).
• d_m, the per-mask overlay — rigid displacement per mask (E7).
• ε, the permittivity field — a material property, measured (feeds 09).
• The process order — which matters for the antenna check, which quantifies over prefixes of the build sequence rather than over the finished layout.

Obligations

O1 (flattening). Hierarchy flattening is correct: c_D computed from the flattened polygon set equals the one computed compositionally. Mechanical, but note that abutted cells' wells and implants deliberately merge — inv_1's bbox is 1.760 × 3.100 µm against a 1.380 × 2.720 µm cell boundary — so the colouring of a row is not the disjoint union of its cells' colourings. Composition needs a merging lemma, not conjunction.

O2 (rule-deck fragment). F restricted to the operations the deck actually uses is well-defined and monotone where claimed.

O3 (finiteness). c_D takes finitely many values and each level set is a finite union of polygons — so all downstream quantification is over finite structures.

Effort

Small, and it is the prerequisite for everything else in the layer. Weeks for the definitions; the rule-deck fragment (O2) is the only part that could surprise.