L1/02 — Extraction and LVS

Background

A layout is polygons; a netlist is transistors and wires. Extraction is the map between them — the recognition procedure that reads a circuit back out of geometry — and its key fact is a beautiful economy of the CMOS process: a transistor is not drawn; it happens. Wherever a polysilicon shape crosses an active (diffusion) region, the crossing is a MOSFET: the poly strip over the crossing is the gate, insulated from the silicon by the thin oxide grown between them; the two pieces of active region on either side are the source and drain; and the surrounding well determines whether it is the N-type or P-type flavour. Even the transistor's electrical parameters are geometric readings — channel length L is the width of the poly strip, channel width W the extent of the active region it crosses. Wires, likewise, are just the connected clumps of metal-and-via material. So extraction is: intersect two layers to find the devices, compute 3D connected components to find the nets, record which touches which.

LVS — "layout versus schematic" — is the industrial check built on extraction: extract the circuit from the drawn polygons and compare it, as a graph, against the intended netlist. The comparison is graph isomorphism, which is notoriously hard in general and easy here for a concrete reason the chapter explains: the graph's nodes are richly labelled (device types, W/L values, port names), and the labels shatter the graph into tiny equivalence classes before any search begins. A clean LVS run is the flow's certificate that what was drawn is the circuit that was meant — which, chained with 01's sandwich theorem ("what is printed is topologically what was drawn"), yields the layer's full conclusion: what is printed is the circuit that was meant.

This chapter also owns a piece of honesty about 01: writing the composition revealed that the sandwich theorem as stated covers nets but not devices — a printed distortion could in principle sever a transistor or detach a terminal without violating any net-level hypothesis — so the device-level analogues (D1)–(D3) are added here, and the enclosure/extension design rules find their formal role as exactly those hypotheses.

Statement

The layout implements the intended netlist: Ext(M(A)) ≅ N_intended, an isomorphism of labelled graphs.

Place and route, and the certificate that replaces monolithic LVS

The statement above is LVS as an independent oracle: throw away how the layout was made, read the circuit back out of the polygons, and compare. That is the right picture when the layout is an inherited artifact of unknown provenance. Here it is not — the layout is generated from the netlist by a program this repository runs — and that changes the cheapest sound architecture. For the stages of the generator that are deterministic we validate the program once; for the stages that search we extract a certificate from the check the search already performs on the configuration it accepts. Re-deriving the whole circuit from silicon to compare against the netlist is redundant work when the netlist is the generator's own input.

What place and route are. The netlist is a graph — cells, and which pins share a net — with no geometry. Two stages give it geometry.

Placement assigns every cell instance a location and orientation in the standard-cell rows: the netlist's 203,027 instances become 203,027 COMPONENTS in the DEF, each stamped with (x, y, orient). It changes nothing logical — same instances, same nets, same incidence — placement only decorates the graph with coordinates. It is a search (minimise wirelength and congestion, meet timing) but a connectivity-preserving one.

Routing assigns every net a set of metal wires and vias that physically join its pins: the netlist's nets become 67,449 NETS in the DEF, each carrying geometry. This is where connectivity is genuinely decided — the router chooses which metal, on which layer, through which vias, realises the net — and its acceptance criterion is exactly two properties: every net's pins connected (no opens), no two nets' metal touching (no shorts).

A single net makes it concrete. In the routed DEF:

- _000000_ ( _111026_ D ) ( _053306_ X ) + USE SIGNAL
  + ROUTED met1 ( 2169590 1965370 ) ( 2174190 * )
  NEW li1 ( 2174190 1965370 ) L1M1_PR_MR
  NEW li1 ( 2169590 1965370 ) L1M1_PR_MR ;

The netlist says only "net _000000_ joins the output pin X of cell _053306_ to the input pin D of cell _111026_" — an edge, no geometry. Placement put _053306_ near (2.1696, 1.9654) mm and _111026_ about 4.6 µm to its right. Routing then chose the physical wire: a li1→met1 via at each pin (L1M1_PR_MR), and a met1 segment from x = 2.16959 to x = 2.17419 mm at y = 1.96537 mm joining them. That three-shape path is the connection. The NETS section is 67,449 such witnesses (coordinates are integer nanometres).

The decomposition. Read this way, RTL → GDS is a pipeline of stages, each with its own certificate:

Monolithic LVS — re-extract the whole 362 MB GDS and isomorphism-check it — is then unnecessary, and the extraction machinery of this chapter narrows to where it is still load-bearing: the finite cell library (each master's polygons ⊨ its CDL, amortised once — the extraction theory below), and the validation of the streamout program (which assembles the GDS deterministically from the DEF and the placed masters). The only genuinely decided connectivity in the whole flow is the routing, and the router already computed its witness and checked it — the flow runs checker-disconnectedpins (no opens) and checker-trdrc (no shorts; ChipTop.drc is empty). Passing those is the connectivity certificate; the L1 obligation becomes to re-verify that witness with a small independent checker rather than to re-derive the circuit from silicon.

This is the same search-vs-certificate split L2/04 makes for SAT — the tool stays an untrusted heuristic search; trust lives in a small checker of the witness it emits — pushed down to place and route. The extraction map that follows is now scoped to the two places it is genuinely needed, not to the chip.

Measured: the routing witness re-verified

tools/routecheck.py reads the routed DEF (ChipTop.def: COMPONENTS 203,027 placed, NETS 67,449 routed) and re-derives both acceptance properties from the routing geometry alone; check-l1 carries it as routing-witness.

No-shorts. Over all 559,285 wire segments, zero pairs of distinct nets have intersecting centerlines — a sound short-detector (crossing centerlines are a guaranteed short, independent of wire width), run by a sweep-line across each layer. This re-verifies trdrc independently of the router.

No-opens. Each net's segments and vias are unioned into connected components (endpoints, via layer-crossings, T-junctions where a via lands mid-segment, and segment crossings). All 41,287 two-pin nets self-connect — and for a two-pin net the routing is the entire connection, so this is the complete no-opens check for the 61% of nets that are two-pin. The 11 unrouted nets are exactly the 11 one-pin nets (nothing to route). The residual 3,762 multi-piece nets are all large-fanout nets whose routing additionally connects through the pin metal shapes — visible only with the cell pin geometry (LEF + placement), which is the extraction half of this chapter, not an open: the router's own disconnectedpins already certified none. Closing them is the cell-master obligation below, not a defect.

So the connectivity content of LVS is obtained here as a witness-check of the router's output — no re-extraction of silicon — with the residual precisely delimiting where the cell-library extraction is still needed.

The extraction map

Given a material distribution M (00):

Devices. Connected components of poly ∩ active. Each is one MOSFET: the component is the gate, the two active regions it separates are source and drain, the surrounding well fixes the type. This is the sense in which a transistor is the intersection of two rectangles — visible directly in inv_1, where poly (0.430 µm wide) crosses diff (0.670 × 2.250 µm).

Parameters. L = the poly dimension across the channel, W = the active dimension along it. Both are read off the geometry, which is why the geometry family propagates into device parameters and hence into E1's enclosure. (On FinFET these quantise to fin counts — a strictly easier map, since the parameter is an integer.)

Nets. Connected components of Cond(M) — 3D, through vias.

Incidence. Which device terminals meet which nets.

Ext(M) is the resulting labelled bipartite graph.

Theorem

Under 01's hypotheses (H1)–(H3), plus a device-level analogue (D1)–(D3) below:

Ext(M(A)) ≅ Ext(M(D))    for every A in the sandwich

so checking Ext(M(D)) ≅ N_intended on the drawn layout settles the fabricated one.

That composition is the soundness of LVS as actually practised, and it is the point of having 01 at all.

A gap in 01, found by writing this

01's stated conclusion includes "ν preserves incidence with device terminals", but the proof as given does not deliver it. The proof handles nets — components of Cond — and says nothing about devices, which are components of poly ∩ active and perturb under their own sandwich.

What is needed is a device-level analogue:

• (D1) (poly ∩ active) ⊖ B_r has the same number of components as poly ∩ active, each nonempty and connected — i.e. no device is severed or split.
• (D2) distinct devices stay separated: dist between components exceeds the summed radii plus overlay. Note this is a different rule from net spacing — it is poly-over-active spacing, and it is why gate-to-gate and poly-extension rules exist.
• (D3) incidence is stable: a terminal that meets net N in D meets ν(N) in A. This does not follow from (D1)+(D2); it needs the source/drain active region to remain attached to its net under perturbation, which is what enclosure and extension rules supply.

(D3) is the interesting one: it is precisely where line-end pullback bites, since a poly line end that retracts can expose channel, and a contact that pulls back can detach a terminal. So the enclosure rules flagged in 01 as "systematic and directional" are the hypotheses of (D3), not of the net-level theorem.

Action: 01's theorem statement should be weakened to nets only, with (D1)–(D3) added here. Left as-is in 01 with a pointer, so the gap is visible rather than silently patched.

Why the isomorphism check is easy

Graph isomorphism is hard in general and trivial here, for a specific reason: label diversity. Devices carry (type, W, L); nets carry names when they survive synthesis, and port nets carry them always. Refinement by labels partitions the graph into tiny cells before any search begins. Production LVS tools exploit exactly this and scale to hundreds of millions of devices.

So the difficulty is not the isomorphism. It is that Ext must be well-defined.

The real obligations

E1 (well-definedness). Ext(M) picks out finitely many devices and nets, with unambiguous terminal assignment. Non-obvious cases that must be decided rather than inherited from tool behaviour:

• a poly shape crossing active twice ⟹ two devices sharing a gate net;
• poly over field oxide (no active beneath) ⟹ no device — this is why npc and field-poly layers exist;
• abutted diffusion: two devices sharing a source/drain region with no contact between, which is a normal and space-saving idiom, not an error;
• a device whose "two sides" are actually one connected active region (a poly ring) — must be excluded or given a convention.

E2 (parameter tolerance). Real LVS compares W/L up to a tolerance, so the statement is isomorphism up to parameter windows — and the windows must contain the whole geometry family, linking directly to 01's r.

E3 (computability). All predicates are polygon boolean operations plus connected components: near-linear with a scanline.

First experiments

The generator decomposition reorders these. The chip-level connectivity certificate is the routing witness, not a re-extraction, so the first build is a checker over the routed DEF's NETS: per net, build the segment+via adjacency graph, confirm it is one connected component touching exactly the net's pins (re-verifying checker-disconnectedpins), and confirm no two nets' geometry abut (re-verifying checker-trdrc), cross-checked against the netlist's net membership. Then the two lighter obligations: the placement connectivity-preservation invariant (the DEF's instances and nets are identical to the synthesis netlist — a diff; note COMPONENTS 203027 already equals the post-route netlist's cell count), and the streamout validation (GDS = f(DEF, masters)).

The extraction theory then applies only to the library, where it is cheap and finite:

• Extract inv_1 from its shipped GDS against its CDL. Two devices expected; check W, L against the measured geometry (poly 0.430 wide over diff 0.670 × 2.250). This is the cell-master half of the decomposition, and it composes with L0/06's switch-level certificate on the same 437 cells.
• Enumerate which of E1's edge cases occur in the SKY130 HD library. If none do, well-definedness shrinks to a short list of excluded patterns.
• Attempt (D1)–(D3) on the same cell to size the device-level sandwich.

Effort

Small relative to the rest of L1, and smaller than the monolithic framing suggested: the chip-level check is a witness-verifier over 67,449 routed nets (near-linear, no isomorphism search), and the extraction algorithms run only on the finite library. The cost is in E1's conventions and the (D1)–(D3) gap above, neither deep, both of which must be decided rather than discovered.