L0/06 — The cut discipline

Background

Lumping (08) cuts the die into components and composes their contracts — but where may one legally cut? The answer lives in the transistor-level structure of a CMOS cell, and turns on the MOSFET's fundamental asymmetry: the gate terminal is (almost) purely an input — it controls the channel through a capacitor, drawing no steady current and pushing (almost) nothing back — while the source and drain are the channel's two ends, through which current flows bidirectionally, with no inherent notion of which side drives which. A signal path through gates is one-way; a path through source/drain terminals is a two-way electrical continuum.

This asymmetry induces a canonical decomposition of any transistor network, due to Bryant: partition the circuit's nodes by connectivity through source/drain terminals only, and call each part a channel-connected component (CCC). Within a CCC, everything is bidirectionally coupled — charge can slosh both ways, nodes can fight, and analysis must treat the component as one analog lump (this is where charge sharing lives: a driven node connected through a pass transistor to an undriven one redistributes its charge, possibly corrupting both). Between CCCs, all influence flows through gate terminals — unidirectional and restoring. So CCC boundaries are exactly the places where cutting is sound: a contract stated at a gate input composes forward without any fixed-point argument about mutual feedback, because there is none.

The chapter's other two obligations are also best previewed in circuit terms. PUN/PDN duality: a static CMOS gate is built as two complementary switch networks — a pull-up network of PMOS transistors to the high rail and a pull-down network of NMOS to ground — designed as logical duals (series in one ↔ parallel in the other), so that for every input exactly one network conducts: output always driven, rails never shorted. That "exactly one" is a checkable graph property of the cell's transistor network, and it is the within-cell half of the no-contention condition V1. And the bistable containment condition: a storage element is electrically a feedback loop (two inverters tail-to-head), and the discipline requires every such loop to live inside one declared sequential cell — a feedback loop straddling a cut boundary would be a latch the composition never modelled, exactly the kind of surprise the cut discipline exists to exclude.

Statement

The per-cell transistor-level combinatorics that license 08's composition: where may the network be cut, and why is every bistable inside a component rather than spanning components?

This is a narrow document. An earlier draft collected all the combinatorial obligations here, which was a scoping error — most of them are about artifacts L0 does not own. See the dispatch table for where they went.

The object: channel-connected components

Bryant's decomposition (Bibliography). Partition nodes by connectivity through source/drain terminals; transistor gates are unidirectional inputs and therefore the boundaries.

inside a CCC   : bidirectional; needs full switch-level analysis; charge sharing possible
between CCCs   : unidirectional (through gates); restoring

This is exactly why cuts are legitimate only at CCC boundaries: only there is signal flow unidirectional, so a component's terminal contract composes without a fixed-point argument. It is the transistor-level counterpart of 06's restoration property — the same fact about where information flows one way.

The three obligations, per cell (×~400)

C1 — CCC structure. Compute the partition: each cell's CCCs, and the graph they form under gate-terminal edges.

C2 — PUN/PDN duality. For static CMOS the pull-up and pull-down networks are series/parallel duals, so for every input assignment exactly one conducts. This is V1(a) — the within-cell half of "no conducting path from Vdd to GND" — and it is the half genuinely about transistors rather than about netlist topology. Checking it is a graph-duality test on the transistor network, not a simulation.

C3 — bistables are CCC-internal. Every cycle in the cell's CCC graph must lie inside one declared sequential element. A cycle spanning CCCs is an unintended latch or oscillator. This is what makes 08's claim — "every bistable loop is internal to a component" — a checked fact rather than a hope.

All three need transistor netlists for the library. The chapter long assumed this meant extraction (recover the netlist from each cell's GDS) and treated that as the gating cost. It does not: the PDK ships the transistor netlists directly — sky130_fd_sc_hd.cdl, one .SUBCKT per cell, the same schematic LVS checks the layout against. C1–C3 read that file; no extraction stands between the obligation and the data.

Measured: C1–C3 over the whole library

tools/celltopo.py runs the three checks over all 437 cells, and check-l0 carries the result as ccc and v1a-tristate.

C1 (CCC structure) is computed by union-find over source/drain edges with the power rails excluded as connectors — each channel-connected component is one switching island, and the islands form a DAG under gate-terminal edges (for combinational cells) or contain a cycle (for storage).

C2 (PUN/PDN duality) is checked not as an abstract graph-duality test but against the Liberty function the digital tools actually trust. For each input assignment the checker evaluates the switch network at the level of individual transistors (nMOS closed when its gate is 1, pMOS when 0), asks whether the output node is pulled to exactly one rail, and compares the resulting truth table to the cell's function attribute. "Exactly one rail for every input" is duality made operational; agreement with Liberty ties it to what synthesis assumed. 311 of the 437 cells are CERTIFIED this way, with zero function mismatches — the transistor topology provably computes the Boolean function named in the library.

C3 (bistables are CCC-internal) falls out of C1's island graph: a cycle in the CCC-dependency graph is feedback, hence storage. 98 cells are so classified — every flop and latch family (dfxtp, dlclkp, sdfrtp, …) plus the physical fillers that carry transistors but no logic — and in each the feedback lives inside the one cell, never spanning a cut. This is exactly what 08 needs made a checked fact.

The remaining 28 cells FLOAT — for some input no rail drives the output — and this is not a failure but the detection of Open Problem 3 below: they are precisely the non-static families (einvn/einvp/ebufn tri-states, the *kapwr always-on power-gated clock cells with a second rail, and conb/probe/spare specials). The partition is clean and exhaustive: 311 certified + 98 bistable + 28 non-static = 437, with no cell mis-sorted into the certified set (no certified cell carries a sequential or tri-state name). Classification is topological — from the CCC graph — not from the cell's name, so it is a check rather than a restatement of the library's own labelling.

Where the other conditions are discharged

04's envelope is L0's, but most of its conditions are discharged against artifacts other layers own. The envelope states them; the owning layer checks them.

Two things this makes visible. The envelope is a genuinely cross-cutting concern: L0 owns the statement of every safety condition but the check for only one of them. And the checks cluster in L1 and L2 — where the geometry and the netlist actually live — which is what one would want, and is the argument that the layer split is by artifact rather than by topic.

Open problems

1. Formalise the cut licence: signal flow between CCCs is unidirectional, therefore composition at CCC boundaries is sound. This is the theorem 08 needs and currently assumes — and the only remaining L0/06 obligation of substance, since C1–C3 now run. The switch-level checker establishes the premise (the islands and their gate-edge DAG) that this theorem quantifies over.
2. Extract transistor netlists and run C1–C3. Done — over all 437 cells, from the shipped CDL (see Measured). The assumed extraction dependency was illusory.
3. Non-static-CMOS cells break C2. Resolved into a closed, checked list. The 28 FLOAT cells are exactly the non-static families, and v1a-tristate asserts that set is closed — every logic cell is covered by the static-CMOS certificate and every exception is named, not assumed away. Each still wants its own terminal contract (a tri-state has a high-Z output state the digital model must carry), which is the remaining bounded work here.

What is left

The switch-level function certificate does not touch the analog side: it establishes that the transistor topology computes the right Boolean function, not that the physics stays in the digital regime (that the pulled rail actually wins, with margin, under the operating envelope). That is E1 / 07's job, and the two compose — 07's enclosure gives the voltages, this chapter gives the switching function they realise.

Effort

The per-cell problems are tiny and near-linear, and they now run in seconds over the whole library, because the transistor netlists were shipped rather than extracted. What remains is the cut-licence theorem (open problem 1) and the per-cell tri-state contracts (open problem 3) — both bounded.

Reading

Bryant on switch-level simulation and the channel-connected-component decomposition — the source of the cut discipline. Melham for transistor-level CMOS in HOL.