Repository navigation
Verification hardening: exhaustive fixtures, oracle differentials, and the defects they found - #1
Merged
Merged
Conversation
OmarSiwy
added a commit
that referenced
this pull request
Oct 11, 2026
On PR #1 the job tested every mutant of the whole branch's diff in one 45-minute job and timed out. Eight shards of 300 minutes each finish a large pull request and cost nothing extra on a small one. Claude-Session: https://claude.ai/code/session_01BKvitR43fxnbTgyL5mQapn
OmarSiwy
force-pushed
the
verification-hardening
branch
from
October 12, 2026 04:21
6247b0b to
0792aff
Compare
PDNSim found it (finding for the coordinator, N-O1-1): on a mesh, a load whose marker sits on a 40 um met1 rail at x = 2.5 um was tapped onto a met2 strap crossing the rail at x = 5 um. The load attach took the supply shape whose box centre is nearest the marker's centre: the strap's centre (5.0, 5.2) um is nearer than the rail's (21, 3) um, though the marker never touches the strap. Every drop and current downstream was wrong (34.23 mV where PDNSim read 36.25 mV; vias at 0 A in PDNSim carried 3.6 mA). Now a device taps, among the supply shapes its marker box touches or overlaps, the one whose centre is nearest; with none touching, the nearest centre over all as before. The per-net networks of p2p_resistance attach the same way. Test: a_device_draws_from_a_shape_its_marker_touches (hand-derived boxes: the rail alone touches the marker, the strap's centre is nearer). It fails on the old nearest-centre rule. The PDNSim differential is the end-to-end check.
LVS_FINGERS_MATCH, LVS_FINGERS_MISMATCH and LVS_SERIES_MERGE: the p2p_resistance finding moves from 278.1 Ohm (layer 3, shapes 2 and 11) to 210 Ohm within shape 11 on layer 17 (diff_active), the intended effect of "a device draws supply current from a shape its marker touches". Hand derivation, from the drawn GDS (all three cells draw the same diffusion and gates): diff (0..1000, 0..200) nm, poly gates at x = 200..250 and 600..650, so diff_active = diff not poly is three pieces, the middle one (250..600, 0..200) nm, shape 11, on the net the two transistors share. Each gate_n marker (200..250 and 600..650, 0..200) touches only the middle piece among that net's shapes (the outer pieces are other nets), so both devices attach to it. A tap is the marker centre projected on the piece's chain axis (x) and clamped to it: x = 225 -> 250 and x = 625 -> 600. The chain between them is 350 nm long and 200 nm wide: 1.75 squares x 120 Ohm/sq (params.deck, pex diff_active) = 210 Ohm, with no contact or via between the two attach points. Before, each device attached to the net shape whose box centre was nearest the marker centre over the whole net (licon and li included), which is how the value carried the 152 Ohm licon cut and li: not the diffusion between the two channels.
…s no output (O1) Five X4 antenna_electrical fixtures carry only rows with a diode credit or bonus, which the differential does not mirror; their empty output file read as 'no output'. Only a missing file is now an error.
…s (O1) The base's harness now gives each row (id, outcome, examined); the differentials take the first two.
…no open-tool definition (O1) ERC-A1 drops TX:MAG (no test runs Magic's antenna check); ERC-G3 drops TX:YOSYS: Yosys check counts cell outputs, and a transistor channel has no direction until the design's rails orient it, so no open tool defines multiple drivers on a transistor netlist. The notes of G3 and G7 say so; both stay on X4's naive graph oracle (ledger P1).
…ere KLayout has no form (O1) H5 gave antenna_electrical LEF's diode terms, a cut factor, PWL tables, oxide rows and an exemption; the differentials read only the old rows. OpenROAD: the boards carry eleven antenna_electrical rows (each layer's own ratio, cumulative metal-only and cut-only rows, and three metal rows with a limit and a diode table). Two more OpenROAD runs state the same terms in the LEF, scaled by the factor 1000: ANTENNAAREAFACTOR (times cut_factor 2.5 on the cuts), ANTENNAAREAMINUSDIFF (area_minus_diode 0.1), ANTENNAGATEPLUSDIFF (gate_plus_diode 3), ANTENNAAREADIFFREDUCEPWL (diode_reduce), and on the metals ANTENNAAREARATIO 5 with ANTENNADIFFAREARATIO PWL (diode_max_ratio) for the verdicts. calculateWirePar/ViaPar then give a node with diffusion (factor * area * reduce - minus * diff) / (gate + plus * diff), H5's partial ratio. Not compared, and said in the module docs: ANTENNACUMROUTINGPLUSCUT (OpenROAD 26Q2 does not read it; it sums metals and cuts apart), truncation of a negative sum at zero (the parameters keep every partial ratio positive), sky130's credit, bonus and exemption (no LEF counterpart). KLayout: a single collector's sky130 credit is mirrored as antenna_check's [diode, credit] (the threshold rises by the credit per um2; the value compared is ratio - (max_ratio_eff - max_ratio)); rows with an exemption, a constant bonus, a diode area term, a PWL table, a cut factor or a cumulative credit are counted as not mirrored, each with its reason. A sidewall antenna_electrical row is mirrored with perimeter_only. A merge-tier test checks the board deck runs and that its H5 rows reduce to the plain ones where the diode terms vanish (h5.cont = 2.5 * par.cont on a diode-free gate, h5.met1 = par.met1 on a diode-free run). It fails if a cut factor or a diode term leaks onto a gate with no diode.
… TX:OR (O1) A1-A4 and A8 gain TX:KL,OR; A5 and A12 TX:KL (credit rows and oxide rows mirrored by antenna_check); A6 and A7 TX:OR (ANTENNAGATEPLUSDIFF, ANTENNADIFFAREARATIO PWL and ANTENNAAREADIFFREDUCEPWL through the LEF); A11 TX:KL; E1 and E2 TX:OR psm. A1 drops MAG (no test runs Magic's antenna check). G3 and G7 note that no open tool defines them on a transistor netlist.
Reviewed against CI run 38206610106's regenerated artifact: ERC-A2, A3, A4, A6, A7, A8, A11, A12, E1 and E2 leave the list of checks no open tool performs, now that a KLayout or OpenROAD differential checks each. The artifact predates H8's rebase, so only these rows were taken; the local catalog test agrees.
…ge-tier tests catch it first (O1) The heavy run stopped on two base changes: an X4 antenna fixture (H5) derives its protection diode with with_area, which the KLayout script did not translate, and em_current_density now takes a narrow band, which the PDNSim mesh deck did not state. with_area is translated as the mirror deck does (inclusive nm2 bounds, KLayout's upper bound exclusive); the mesh deck states narrow: none. So the nightly tier no longer finds a deck it cannot read, two merge-tier tests run the same inputs without the tools: every_antenna_fixture_translates_or_is_counted (every row of every X4 antenna fixture and a board is mirrored or counted; it fails on an untranslated derived layer), and the_mesh_deck_runs_and_the_pad_cut_carries_the_budget (Kirchhoff: the pad's one via2 cut carries the whole budget, every load reads a drop; it fails on a deck that does not parse or a lost load).
…y KLayout (O1)
H5's sky130 .ar.1 and IHP Ant.g fixtures name a diode layer that is no
conductor (a derived diff.with_area); antenna_check reads a diode only
on a layer of the extraction and stopped with 'Non-hierarchical layers
cannot be used in netlist extraction'. GPurify joins such a layer to
the conductor it lies on; KLayout would need a connect the deck does
not state, so the row is counted ('a diode layer that is no
conductor') rather than mirrored.
…KLayout antenna differential (O1) H5's IHP Ant.g fixtures run the antenna rows' deck with DRC alone (the /drc variants check the diode size), so GPurify reports no ERC row. Such rows were broken as 'GPurify has no such row'; they now count with the rows GPurify did not run.
… (O1) H6 added the NfetC and PfetC models to the ERC fixtures after O1's last rebase; the Yosys corpus draws neither, but the cell-name match must cover them.
…ed under (H14)
DRC-092's cell-name exemptions were missing: the layout is flattened at
ingest, so no rule could say "for cell names ..." or "except in cell
...", as sky130 m1.4/m1.4a, li.1a, poly.12 and x.25 do, and as the
sky130 KLayout precheck deck does with `select`.
The deck gains `L.in_cells("p", ...)` and `L.not_in_cells("p", ...)` on
a drawn layer. A shape is in when a cell on its placement path, root
included, matches a pattern: KLayout's `source.select("-", "+p")` and
`select("-p")` (DRC reference, Source#select: a filter enables or
disables a cell with its subtree). Patterns are whole-name globs, `*`
and `?`, case-sensitive; `[`, `]`, `{`, `}` and `\` are refused, since
KLayout reads them as classes, alternatives and escapes.
The flat engine is unchanged. Each selection is one bit; the flatten
walk or-s each cell's own bits down the placement path and tags every
pushed ring, permutes the tags with the layer sort, and the derived pass
copies the receiver's tagged rows. The tags are dropped once derived
layers exist; a deck with no selection allocates none. At most 64
selections per deck (MAX_CELL_SELECTIONS). A store built in memory has
no cells: in_cells is empty there, not_in_cells the whole layer.
Tests: a hand-built GDS (byte-level writer) with PAD_A placed under all
eight STRANS orientations and once magnified (the per-element path),
nesting INNER, beside core and a top-level INNER: construct-from-answer
boxes for each selection (a walk that read only the owning cell would
leave the nested INNER out and fail); the in-memory case from the
rustdoc; parser refusals. Also fixes a pedantic format_collect in
deck_text.rs.
The exhaustive harness wrote one flat cell, so no fixture could place a
cell. A harness Layout now carries placements (orientation and offset)
and the cells they name; such a layout is written with testgen's
write_library under TOP and read back by the real reader, a round trip
through the GDS writer. Transforming a fixture composes each top-level
placement with the symmetry and leaves cells in their own frames.
Fixtures (DRC-092, every placement): in_cells / not_in_cells on a
nested tree (nested INNER in, top-level INNER out, several patterns a
union, the root's name counts, case matters); a width exempted in PAD*
cells and its in-cell limit, swept; sky130 x.25 (DRC-097), where a
longer name does not match. Oracles: hand-derived areas and widths.
A wrong orientation mapping or a tag that ignored the path changes the
areas or the split and fails them.
a_placed_cell_lands_where_its_symmetry_maps_it holds the writer's
STRANS mapping to the harness's own Symmetry::apply (round trip).
renaming_a_cell_changes_only_what_its_name_selects is metamorphic:
renaming a non-matching cell changes no finding; renaming it into the
pattern moves only its finding from not_in_cells to in_cells.
The KLayout mirror translates in_cells to `src.select("-", "+p")` and
not_in_cells to `select("-p")`, so the heavy tier runs these fixtures
through KLayout. pex.rs: a struct literal gains the new fields, and a
format! push becomes write!.
…y cell name (H14) Rules the SKY130 periphery manual scopes by cell name were left out or applied everywhere for lack of cell names: - m1.4 0.030um "exempted for cell names documented in rule m1.4a"; m1.4a 0.005um for s8cell_ee_plus_sseln_a/b, s8cell_ee_plus_sselp_a/b, s8fpls_pl8, s8fs_cmux4_fm (the precheck deck sky130A_mr.drc scopes the same pair with select); - li.1 0.170um except li.1a 0.140um inside s8rf2_xcmvpp_hd5_*; - poly.12 exempted for cell s8fgvr_n_fg2; - x.25 pnp.dg only within s8rf_pnp, s8rf_pnp5x, s8tesd_iref_pnp, stk14ecx_*. li.3a is not split out: a pair straddling the cell boundary would be held to neither number, so li.3 keeps every pair at 0.170um. The left-out list names what stays out (x.12-x.24, x.26-x.29, li.3a, licon.11c/d, x.15b, difftap.2a, poly.2's core-rule exemption). Tests draw the geometry inside a named cell placed by TOP (GDS written with write_library and read back), at and past each limit, and in a cell whose name only nearly matches. Oracle: the manual's numbers and cell lists.
DRC-092 stays partial (deck rule flags are still missing) and now states the cell-name scoping. DRC-097 moves from missing to partial: sky130 x.25 is written with `forbidden` over not_in_cells and proved by symmetric fixtures (SY, MR); the frame, die and seal-ring rules and x.26 (per placement) remain out. The rule reference in check's crate docs lists DRC-097 under `forbidden`. The generated blocks of limitations.md and check-sources.md come from CI.
Nightly run 38186321535 compared the hierarchical fixtures with KLayout: every selected shape was the same figure as GPurify's but at half size, so widths and areas disagreed (160 rows). Source#select returns a source without the global_transform(magnify(2)) the mirror runs under (a1); the translation now applies it again. The selection itself agreed on every fixture, the tree, the width exemptions and x.25.
R2 added Calibre's DRC MAXIMUM CELL NAME LENGTH to DRC-097. With cell
names kept for the selections, a limit of n is forbidden(L.in_cells("?…?*"))
with n + 1 '?': it flags the shapes under any longer-named cell. It sees
only a cell that holds or places a shape on L; docs/deck.md says so and
the DRC-097 notes record it.
Fixture cell_exemption/name_length (every placement): TOP and ABCD pass,
ABCDE fails, and AB fails under LONGNAME. Oracle: hand-derived areas
from the glob's definition; a pattern read as a prefix or a tag that
ignored the path changes the flagged set.
…on (H14)
The base gained a public DeckSource with `lower`, a printer, and a Rust
DeckBuilder with a twin of each shipped deck. After the rebase they did
not know DerivedOp::InCells: a source built in code could carry a
derived receiver or a pattern range past the table, the printer could
not write sky130.deck, and the builder had no way to state it.
- lower refuses what the parser refuses: a receiver that is not one
drawn layer, a missing or empty pattern range, a pattern holding
`[`, `]`, `{`, `}` or `\`, more than MAX_CELL_SELECTIONS.
- print writes `.in_cells("p", ...)` / `.not_in_cells(...)`.
- LayerExpr::in_cells / not_in_cells; a node now holds its patterns as
a list, renumbered into the source's texts at finish as with_text's.
- The sky130 twin states li_vpp/li_not_vpp, mcon_m1_4a/mcon_m1_4,
li.1a, m1.4a, poly.12's exemption and x.25.
- README's sky130 rule count: 271 -> 274 (li.1a, m1.4a, x.25).
Tests: the twin test holds the builder to the parsed deck (a wrong
pattern list or op names the first difference); a lowering test built
in code (derived receiver, range past the table, no pattern, a class:
each refused; the plain one lowers). Oracle: the parser's rules, which
lower's contract says a hand-built source meets.
… its KLayout mirror (H14) H4 made DerivedOp::Sized per-axis after H14 branched; the cell-selection lowering test builds a sized layer and now states both axes. DRC-092's fixtures pass the KLayout mirror (heavy 38229697765), so its oracle claims TX:KL; the generated blocks and README counts follow.
…he diode wiring ESD clamps need (H7) The ESD and latch-up kinds that follow share this machinery, added here with no new kind of its own. - power.rs: extract_stress_into builds a resistor network over any set of nets (each modelled as the supply grid models a net: sheet * ds / w chains, vias per cut), forces a current in at one polygon and out at held pins (or each net's feed point when it has none), and adds each listed device's resistance between its attach points as EdgeKind::Device edges, last in the grid. solve_into solves it unchanged. feed_shape (highest layer, then widest) is shared with extract_into. allowed_current takes a device edge as unlimited. - voltage.rs: NetVoltage records which ground domains reach each net (ground_of), as power_of does for supplies. - supply.rs: the esd_topological clamp walk becomes clamp_reach_into, which lists the nets it reaches, and skips a diode between a supply and a non-supply net that the declared rails forward-bias (reverse_biased): such a diode is a leak, not a clamp (limitations.md, "Rules that can pass a layout signoff would flag"). A diode between two supplies is taken as wired, so IHP's nmoscl rail clamps still count. - domain.rs, reliability.rs: terminal, device_id, push_device, narrow_rings and encloses are pub(crate) for the new modules. Tests: erc/esd/wiring/* (ERC-C1; oracle: each diode's bias at the declared rail voltages, by hand) and the extracted-graph reference in erc_reference.rs (same bias test, 300 random circuits) come with the fixture commit; the stress network is proved by esd_path's dense nodal-solve oracle there and by the crate tests that kill its mutants. Breaks if a reversed up diode completes a pad path again, or if device edges stop coming last (each clamp share then reads a wire's current).
…sd_parasitic and esd_exposed (H7) Ledger H rows ERC-C2..C10, from public material only; each kind's rustdoc states its definition, its sources and its limits. - esd_path (C6; with its options C2, C7, C8 and D4): for each pad and each supply its clamps reach, forces the deck's current in at the pad and out at the supply over the stress network; measures the path resistance, each clamp's share against It2 times its width or perimeter (C2), each wire's and cut's current against its pulse rating (C7), the pin's rise (C8), and, with a source layer, a guard ring's injection path (D4). - esd_ground_coupling (C5): every two ground domains must share a group closed under anti-parallel diodes of the listed models. - esd_cross_domain (C4, C9): a transistor whose gate swings on another domain's supply needs its driver's and its own grounds coupled, and, when the row names local clamps, one from its gate to its own ground. - esd_parasitic (C10): a pad's diffusion closer than min_spacing to another net's. - esd_exposed (C3): a gate reachable from a pad through series resistors needs clamps to both rail kinds; a transistor driving a pad must be a rated or clamp model. Tests come with the fixture commit (tests/exhaustive/erc.rs, closed form below/at/above) and the second oracles (erc_reference.rs: dense nodal solve, ground-coupling closure, cross-domain reach fixpoint). Breaks if a clamp share, a coupling group or an exposed-net walk moves.
…d_diode, conditional_tie and latchup_victim (H7) Ledger H rows ERC-D1a..D8 (D4 is esd_path's injection option), from public material only; each kind's rustdoc states its definition, its sources and its limits. With them limitations.md's "esd_topological, esd_latchup only check that a clamp path exists" is answered: the rings, ties and victims are now measured. - guard_ring_bias (D3): an n-type ring sits on the highest supply, a p-type ring on a ground. - tie_area (D1b): a well's or ring's tap contact area against a share of the channel area it holds. - guard_ring (D2, D6, D7): a target no closed ring hole surrounds, or one too far from or too thin a ring, optionally only near a pad. - forward_diode (D8): a diode of the listed models the supplies can forward-bias that no marker covers. - conditional_tie (D1a): a tap distance that tightens in bands as a neighbouring well's diffusion closes in (GF180MCU LU.4). - latchup_victim (D5): a region near an injecting pad junction is held to a tighter tap distance. Tests come with the fixture commit (closed form below/at/above, every placement). Breaks if a ring's hole test, a tie's area share or a band edge moves.
Each new kind gets its row in every table the deck library is built from: the typed constructors (deck/rules.rs), the parser's kind table (ingest deck/kinds.rs, esd_path with and without a source layer), the printer (deck/decompile.rs), RuleSet's columns, parse arms, value checks and run calls (erc/ruleset.rs), and the rule reference in lib.rs. RunInputs carries the whole Process, not only its grid, since esd_path reads the stack and connectivity. Tests: - tests/deck/esd_kinds.rs: each kind built by its constructor equals the same rule parsed from text, and prints back to that text. Oracle: the deck text, written by hand from docs/deck.md. - tests/erc/dispatch.rs: every new row produces exactly one run row, and the intent-gated ones skip without intent. Oracle: the documented dispatch contract. Breaks if a kind is missing from any table, or its parameters drift between the parser and the printer.
power::extract_into, push_edges and the tap, chain and connection helpers behind them are called by no gpurify-check test: the hand-worked grid fixtures live in the root crate's tests/erc_closed_form.rs, which cargo-mutants does not run for this crate, so the extraction's mutants survived (sampled: extract_into's `!=` to `==`, a deleted `-`, `+` to `-`; push_edges' `+` to `*` and `*` to `/`). tests/erc/closed_form.rs ports those fixtures unchanged, behind a harness that runs the crate's own path (parse_deck, CompiledDeck, net, device and port extraction, erc::check at 85 C over the drawn extent) in place of the engine's. The oracles are the root file's: Ohm's law on a series ladder (drops 0.75, 1.25, 1.75 mV, strict at the limit, on a power and a ground rail), a ring with a hole, a via into a global layer, a conductor with no sheet resistance refusing only the rows that read one, a 4:1 current divider through two vias (1.0 mV, 4000 uA through via A), Black and Arrhenius derating (2.16225793), the Blech product exemption at exactly 8 mA, per-width and per-cut limits on one row, and the reliability model at and off its reference point (1728.4623 h). The root file stays: it also holds the engine's glue to the same answers. Breaks on any change to the grid's taps, chains, squares, link widths, via lengths, load shares, feed point or edge emission. Claude-Session: https://claude.ai/code/session_01BKvitR43fxnbTgyL5mQapn
… fold to hand values (M2) Three paths had no gpurify-check test that pinned their answers: power::extract_nets_into (the per-net networks p2p_resistance probes), the AC supply grids erc::check builds for em_rms and em_peak from IntentMap::with_budget, and classify_nets_into's scrap row for a terminal on no net (sampled survivors: extract_nets_into's `!=` to `==` and `+` to `-`, net_slice's `+` to `-`, check's `!` deleted, with_budget's budget field deleted, classify_nets_into's `+` to `*`). - p2p_resistance_is_the_worst_attach_pair_by_ohms_law: three loads on one met1 bar, worst pair the outer two, 16 squares x 0.125 = 2.0 ohm; two met1 bars joined through met2 by a via each, 0.25 + 0.0625 + 0.375 + 0.0625 + 0.25 = 1.0 ohm; limits 0.01 ohm either side (the probe is a dense solve, exact to rounding). - ac_current_rows_load_the_grid_with_their_own_current: the single 8 um edge carries the net's RMS (500 uA) for em_rms and its peak (2000 uA) for em_peak, not its budget, against density x 1 um, strictly: 999 uA/um fails only the peak row, 2000 passes both at the limit, 499 fails both. - a_terminal_on_no_net_or_past_the_extraction_is_dropped: a gate on net 0, a drain on NetId::NONE and a source past the extraction give net 0 the gate bit alone, one row per net. Oracle: Ohm's law and the AC table by hand; the documented contract. Claude-Session: https://claude.ai/code/session_01BKvitR43fxnbTgyL5mQapn
…on (M2) propagate_into and channel document that a terminal on no net, or on a net past the extraction, is ignored, but no test put such an id at the boundary, so `net.idx() < count` turned `<=` survived (sampled in channel and propagate_into). a_supply_or_terminal_past_the_extraction_is_ignored: a resistor from a 1.8 V supply to a second net, propagated, then again with a resistor between NetId(count) and NetId::NONE appended and NetId(count) declared a 5 V supply: every net's range is unchanged (metamorphic). With `<=` the first id past the end indexes past the adjacency and supply columns. Claude-Session: https://claude.ai/code/session_01BKvitR43fxnbTgyL5mQapn
…mined nodes (M2) check_em_thermal's usability conjunction was tested at one point (sigma 0), so its comparisons survived (sampled: limit_failure `> 0` to `>= 0`); check_ir_drop's count of examined nodes ORs three stated limits, and `|` to `^` survived because no net stated two. - em_thermal_runs_exactly_on_the_documented_domain_of_each_parameter: each bound one step either side: sigma 0, NaN, infinite; conductivity 0, infinite; spreading 0 runs, -0.01 and infinite refuse; limit_failure 0 and 1 refuse; max_failure 0 and 1.01 refuse, 1 runs; a 0 K reference, a zero or infinite exponent and a negative activation energy refuse, zero activation runs. - ir_drop_examines_every_node_whose_net_states_any_limit: the series ladder with an absolute limit, a fraction and an overvoltage all stated examines all four nodes; the 0.0009 fraction (1.62 mV of 1800) reports the far node alone at 1.75 mV. Oracle: the documented domains; Ohm's law on the ladder. Claude-Session: https://claude.ai/code/session_01BKvitR43fxnbTgyL5mQapn
… diodes (M2) Every crate test of esd_topological wires its pad diodes the right way round, so reverse_biased replaced by `true` survived, as did its cathode test `> 0` turned `>= 0`. a_pad_with_only_forward_wired_diodes_reaches_no_rail: a diode from VDD into the pad (anode at 1.8 V) and one from the pad into VSS (cathode at 0 V), with a rail clamp so the rails are clean: three pads, the pad alone flagged, reaching 0 rail kinds of 2. Oracle: construct-from-answer, per reverse_biased's documented rule. Claude-Session: https://claude.ai/code/session_01BKvitR43fxnbTgyL5mQapn
… net grouping (M2) No crate test drew a net whose hard part is two shapes of one piece, so soft_connection's `piece != first` guard forced true survived; and mixed_tag had no crate test at all (sampled: its group range's `<` turned `==`). - two_overlapping_shapes_left_by_the_soft_layer_are_one_piece: two overlapping layer-0 shapes with a resistive body cut to both stay one component without the body: examined 1, clean. - mixed_tag_flags_only_an_untagged_figure_sharing_a_net_with_a_tagged_one: W1 and W2 strapped into one net with W2 tagged, W4 tagged alone, W3 untagged alone: four figures examined, one violation at W1 counting 1 tagged figure against 0 and naming W2. Oracle: construct-from-answer, per each kind's documented contract. Claude-Session: https://claude.ai/code/session_01BKvitR43fxnbTgyL5mQapn
…nes (M2) check_floating_supply had no crate test that drew a supply in pieces, so its piece grouping survived (sampled: `group.len() < 2` turned `> 2`). floating_supply_flags_every_piece_but_the_fed_one, in the closed-form harness (labels, intent, erc::check): VDD drawn as a met2 bar and two met1 bars, none touching, is three pieces; the met2 bar (highest layer) is fed and the two met1 bars are flagged at their first vertices, 0 connections against 1; a VDD in one piece flags nothing. Oracle: the kind's documented rule (OpenROAD check_power_grid's unreached shapes), construct-from-answer. Claude-Session: https://claude.ai/code/session_01BKvitR43fxnbTgyL5mQapn
…heir limits (M2) esd_latchup's only crate test counts pads and one ring, so its ring measurements survived (sampled: narrow_rings' `band < limit` turned `==`; nearest_supply and separation reached only through it). esd_latchup_reports_narrow_rings_and_rings_far_from_a_supply: a supply bar and three rings: 50 wide at gap 500 (narrow), exactly 100 wide at gap exactly 1000 (clean at both strict limits), 200 wide at gap 4000 (far): violations R1 Length(50) against 100 and R2 Length(4000) against 1000, three rings examined. Oracle: construct-from-answer, widths and gaps by hand. Claude-Session: https://claude.ai/code/session_01BKvitR43fxnbTgyL5mQapn
…ts sees them (M2)
What was wrong: the round-2 ERC kinds (esd_path, esd_pin_pair,
esd_cross_domain, esd_exposed, the latch-up kinds, antenna and density,
gate_path, combinational_loop, matching, power_switch,
dielectric_field and more) are proved by the fixtures of the root
crate's tests/exhaustive/erc.rs, and cargo mutants runs only each
crate's own tests, so the nightly mutation gate scored gpurify-check at
60 % with whole functions surviving (series_resistance, turn_on,
check_gate_path, check_density_cmp, attach, ...).
The change: tests/erc/fixture.rs is the root harness's ERC half in this
crate: the deck parsed and compiled, the layout drawn in memory through
LayoutBuilder, labels placed and bound, derived layers computed, nets,
devices and ports extracted, erc::check run with the engine's die and
temperature, and every rule row compared with the fixture's claims
(outcome, exact findings by measurement and marker, examined count).
tests/erc/ported.rs carries the root fixture groups whose kinds live in
erc/rules/{esd,antenna,topology,latchup,domain,matching}.rs, with their
doc comments and so their oracles unchanged: LEF/DEF Appendix C antenna
ratios, the window clip for density, Board's naive judge of every
topology rule on the planted circuit, the series/parallel closed forms
of the ESD strips (Kirchhoff, White Paper 2's turn-on sum), the
GF180MCU latch-up constructions, LEF58_VOLTAGESPACING. Each group is
one test.
Kept in the root only: the keyhole-isolation hv case (it proves the GDS
reader's keyhole-to-hole conversion, which the in-memory path skips),
the DRC half of ihp_ant_g, and the nightly enumerations. To keep the
crate suite fast enough to run once per mutant, the sampled
enumerations draw the first fifth of the root's merge sample (same
seeded shuffle) and each placed fixture runs as drawn, transposed at
the far offset and turned half way instead of under all eight
symmetries at both offsets: the ERC binary runs in 1.4 s.
What breaks the tests: any change to a covered kind's measurement,
marker, outcome or examined count on these layouts. Measured with a
narrowed cargo mutants run on esd.rs (series_resistance, turn_on,
check_esd_path, check_esd_pin_pair, clamp_capacity, narrow_wires,
interconnect_capacity): 149 tested, 124 caught, 9 timeouts, 16 missed,
where the nightly shard missed every mutant it sampled in
series_resistance and turn_on. The next commit kills most of the 16.
Claude-Session: https://claude.ai/code/session_01BKvitR43fxnbTgyL5mQapn
…d esd_exposed's series network (M2) What survived the ported fixtures (narrowed cargo mutants on series_resistance, turn_on, check_esd_path, check_esd_pin_pair, clamp_capacity, narrow_wires, interconnect_capacity: 149 tested, 124 caught, 9 timeouts, 16 missed): every ported turn-on case uses a 1 ohm clamp, so dividing or multiplying the held voltage by it is the same; none drives a clamp backwards, so the refusal floor was never read; no source polygon lies off every net; no unlisted reverse-biased diode or resistor sits between path nets; no supply's pin differs from its feed point; no listed resistor leaves the exposed nets. New tests, each hand-derived on the strips of the ported ESD process (pad 0.0625, met1 0.125, met2 0.0625 ohm/sq, 1 um wide) or the secondary-stage circuit (rs 200 ohm): - esd_path_contract: a 2 ohm clamp holding 700 mV raises the pin 1.33 A x 3.5 ohm + 700 mV = 5355 mV and carries all 1.33 A (breaks on the turn-on source scaled the wrong way, the clamp share read with the source added or divided by its sign); a 5 V turn-on drives the up-rail path backwards (-304.5 mA to VSS, -425.8 mA to VDD by the two-path solve), so the row is refused (breaks on the backward floor or its comparison); a source on the diode markers, on no net, is never stressed (breaks on dropping the no-net skip); an unlisted reverse-biased diode stays out, 2.5 ohm (breaks on && -> ||); with the pad below met1 VSS is still held at its pin, 3.75 ohm, not its feed point's 2.5 ohm (breaks on the pin filter); a MOS clamp on the pad, VDD and VSS rated 1 A/m is flagged once per pin pair, twice, not once per pair of its nets (breaks on clamp_capacity's same-device guard). - esd_exposed_contract: an unlisted rs2 resistor in parallel leaves the gate at 200 ohm, clean against 150 (breaks on || -> && in the model filter); a listed pull-down to VSS1 is left out, 200 ohm flagged against 300 (breaks on && -> || in the end filter, which indexes a rail's missing node). Equivalent: esd.rs:195 `sign > 0.0` -> `>=` (sign is +1 or -1, never 0); series_resistance's `abs() < f64::MIN_POSITIVE` -> `<=` (no pivot is exactly the least normal). Left: the same comparison -> `==` (a singular series network, which only a non-resistor of a listed model can make). Claude-Session: https://claude.ai/code/session_01BKvitR43fxnbTgyL5mQapn
…t (M2) The cut-layer, overlay and one-layer spacing kinds (drc/rules/via.rs, overlay.rs, spacing.rs, facing.rs) and the rule-set tables and deck lowering (drc/ruleset.rs) were proved mostly by the root crate's exhaustive fixtures, which cargo-mutants does not run when it scores gpurify-check: the mutants-in-diff log of run 38286522387 lists 569 survivors in these five files (max_cut_spacing 43, from_deck 35, octilinear and keep-out readings, via_redundancy, cut_class_spacing, dfm_scored, wide_runs, the table validators, ...). A crate-level deck harness (tests/drc/deck_fixture.rs) parses deck text, computes the derived layers (ingest's derive_layers), extracts nets from the deck's connect statements, types the deck with CompiledDeck::from_deck and runs its DRC rules with those nets; each case is checked under the eight symmetries of the square at two translations, every pinned marker mapped with the layout, as the root harness does without GDS. Holed figures are drawn as abutting bands, since a ring through itself does not validate in memory. The cases are the root fixtures with their oracles restated on each test (LEF/DEF 5.8 examples, OpenROAD's readings, the sky130 and ASAP7 rule values, distances and areas by construction, each limit swept one unit either side): - via_deck: max_space, keep_out_zone, cut_class_space, cut spacing (edge, centre, adjacent cuts), redundant_via, min_cuts (wide wire and thin-to-wide distance), via_stack (plain and single-cut), via_map, stack_space (same net), via_redundancy, cut_area_change; - overlay_deck: opposite enclosure, enclosure by wire band, noncoincident enclosure, full_width, projection spacing, max_enclosure, extension, bend/covers_corner; - spacing_deck: eol, eol within (parallel edge, two edges, end to end), eol keep-out, prl, corner and convex-corner spacing, wide and attached-wide spacing, net spacing (one layer, two layers, a derived layer), space_table, two_width_table, tip_space_table, forbidden_space, exact pitch, span_length (with EXCEPTOTHERSPAN); - tables: each table validator broken one stated condition at a time from a valid table, CutAreaBands::limit and CoverBands::need at band starts (inclusive and not), Pattern::anchor at its don't-care edges, Rule::required_spacing at each threshold and on another layer; - ruleset_refusals: from_deck's refusals at their boundaries (wire band, via_map band, forbidden range, single-cut stack layer count, anchored patterning layer count, cut class and allowed width sides, off_grid reading drawn layers only). What breaks them: any change to a kind's measurement, its comparison at the limit, its marker, which pairs or shapes it holds, or a table's validation or band lookup. Claude-Session: https://claude.ai/code/session_01BKvitR43fxnbTgyL5mQapn
dfm_scored (drc/ruleset.rs) had every mutant surviving in the crate: no crate test ran a dfm_score rule. Pattern matching and the value ranges Rule::validate holds a hand-built rule to (via redundancy's space, a DFM score's required/recommended order, a keep-out zone's oblong class and zone reaches) were likewise untested in the crate. dfm_deck ports the root dfm_score and pattern fixtures (oracle: the score by hand, Π 1 - rate (1 - score) over each finding, and matches by construction in all eight orientations, don't-care boxes matching anything), and adds where the score is reported: two gaps of 150 and 120 score 0.5 and 0.2, a design of 0.75 x 0.6 = 0.45 at the 120 gap's middle, held to the sign-off 0.9. tables gains each validate range read at its line and one unit past it, each refusal with the value the rustdoc says it reports. What breaks them: a score off its formula, a finding kept for a design at or above the sign-off, the score reported elsewhere than the worst finding, a match missing an orientation or ignoring a don't-care box, and any range check moved by one unit or reporting another value. Equivalent mutants left: Rule::more_layers returning [None; 4], and deleting any of its arms, change only when a layer's validation is freed (forget after its last reader); every rule re-validates a forgotten layer to the same result, so no output can differ. Claude-Session: https://claude.ai/code/session_01BKvitR43fxnbTgyL5mQapn
…d max_space's rounding (M2) A narrowed cargo-mutants run over max_cut_spacing, isqrt_up, cut_class_spacing, keep_out_zone and of_class (drc/rules/via.rs, 137 mutants) with the deck ports killed 112 of 120 viable mutants (110 caught, 2 timeouts); eight survived, all at boundaries no case reached: - `wider`/`taller` read with `>=` makes a square cut face with its SIDE; the licon table's square END and SIDE cells are equal, so nothing saw it; - `apart_x`/`apart_y` read with `>=` makes a touching pair apart; it still measures 0 and fails, only its limit changes, which the harness did not compare; - max_space's half-unit rounding: no case put two centres a half-unit-odd distance apart, or a non-square distance whose floor and ceiling halve differently. The harness now also claims a finding's limit (`Finding::held`). New cases, with oracles from Rule::CutClassSpacing's and Rule::MaxCutSpacing's rustdocs: a square-and-slot table whose square END (200) differs from its SIDE (300): squares 250 apart are clean, 199 apart one finding held to 200; two slots touching end to end are held to their largest cell, 500, not the END-END 350; a cut whose centre is 1000 along and a half unit up is √(1000² + 0.25) away, lonely, measuring 1001; a 101-wide cut's centre 1101.5 away measures 1102. What breaks them: a square read as facing with its side, a touching pair read as apart along an axis, a distance rounded down or halved before rounding. Claude-Session: https://claude.ai/code/session_01BKvitR43fxnbTgyL5mQapn
…ceilings (M2) whole_at's 45-degree path (drc/rules/spacing.rs) had its marker arithmetic and its touch/nested guard surviving: no crate test pinned where a spacing finding on a 45-degree shape is reported. And RuleSet::from_deck's count ceilings (a count stored in a u16 or u8) and its pattern corner-pair check had no crate case past their edge. New cases: - space(a, b) >= 20nm on diamonds (oracle: whole_at's rustdoc, points by construction): tips 10 apart marked at their midpoint (15, 0); a tip 10 from a square's side, the same; tips touching, 0 at the touch (10, 0); a diamond nested in another, 0 at the boxes' common centre; under all eight symmetries; - a via stack's height 65535 builds, 65536 is the wrong kind of value; a patterning's 255 colours build, 256 do not; an odd count of pattern corners is a bad table. What breaks them: a 45-degree marker computed off the nearest points, a touch read as nested or the reverse, a count past its integer accepted (from_deck then panics converting it), an odd corner list accepted. Claude-Session: https://claude.ai/code/session_01BKvitR43fxnbTgyL5mQapn
…(M2) strip_ends (drc/rules/overlay.rs) reads a side straight out from just inside each end; an edge that ends exactly at the side's end covers none of it. Its `covers_low`/`covers_high` comparisons survived in the crate (mutants-in-diff run 38286522387): no crate case put a host step exactly at an inner corner. Oracle: adjacent enclosure's rustdoc, readings by construction: a [0, 100]² via in [-50, 200] x [0, 200] over [-10, 200] x [-20, 0], the host's left side stepping from 50 to 10 exactly at the via's bottom. At (0, 0) the left edge reads 50 and the bottom 20, better 50; every other corner's better edge reads 100: `>= 51nm` finds 50, `>= 50nm` nothing, under all eight symmetries. What breaks it: an edge ending at a side's end counted as covering it (the left side would read 10 and the corner 20). Claude-Session: https://claude.ai/code/session_01BKvitR43fxnbTgyL5mQapn
…ion (M2) The nightly mutation gate scores gpurify-check against its own tests, and system.rs's check_alignment, gap2, gap_middle and bumps_into were reached only from the root crate's system fixtures: every mutant of the offset row, the space row and the face reader survived. Four unit tests, each value hand-derived from the rustdoc: - a bond offset over its limit is one row at the middle of the centres: bumps 3-4-5 apart, a row at a 4 offset measured 5 at the floored middle (6, 7), none at 5, a bond with no offset not examined, no row at all with no limit. Breaks on a wrong centre, distance, floor, comparison or examined count. - a facing bump closer than the space is a row at the middle of the gap: gaps 3-4 (5) and 2-with-overlap, rows under 6, one under 5, at (11, 12) and (-1, 5); the bonded bump skipped; four examined; gap2 symmetric. Breaks on a wrong gap, middle, skip or count. - a face is its rectangles on nets: a placed rectangle is a bump; a four-vertex diamond and a six-vertex L are not rectangles; a layer past the store holds none. - a face on no conductor is refused as on no net. Measured (cargo mutants --file system.rs --file lvs/gates.rs, 144 mutants): every check_alignment, gap2 and bumps_into mutant caught. Equivalent, not killed: gap_middle's `ohi < lo` and `hi < olo` to `==` or `<=` (440:33, 442:22). The third branch, (max(lo, olo) + min(hi, ohi)) / 2, is the same point as either gap branch for disjoint boxes and for touching ones, so every branch choice gives the same middle. Claude-Session: https://claude.ai/code/session_01BKvitR43fxnbTgyL5mQapn
`lvs recognize_gates` (catalog LVS-047, gates.rs) was exercised only by the root crate's LVS fixtures, so cargo-mutants, which runs the check crate's own tests, saw every mutant of gates::pass, plain, sound and emit survive, and compare_traced's folding of the deck's recognize_gates and relaxed controls into the options as well. New tests/lvs/gates.rs, each expected graph written out by hand from Silvaco Guardian's definition the module cites and compared whole: - NAND2's pull-down stack is one device with both gates, its ends as source and drain, the internal net dropped and the nets above it renumbered, one Series merge; nothing merges with the control off; - a NAND3 stack drawn out of order is one device, ends in member order; - NAND2's pull-up and NAND3's are one parallel device each; a pair on one gate is left alone; - every precondition refused on its own: model, size, diffusion or stress stated, bulk, port, a third terminal, the same gate, a fifth role, two gates on one device, a resistor, a gate on no net; - a ring, a stack repeating a gate, and a shorted pair stay as drawn; - a whole NAND2 merges parallel first, then series, devices ordered by lowest row; - through compare_traced, a stack whose inputs swap matches its schematic only under the deck's recognize_gates (a resistor on one input breaks the net symmetry), and the reduced reference rows trace back to [0, 1] and [2]. Each breaks when a precondition, the ordering, the renumbering, the end selection, or the controls' fold into the options is changed. Measured (cargo mutants --file lvs/gates.rs, before the last three cases were added): 125 of 136 viable mutants caught or timed out; the last three cases target 275:36, 282:12 and 266:35. Equivalent, not killed: - 199:48, `a == b ||` to `&&`: a == b is one device, whose gate equals its own, so the `pa.gate != pb.gate` test refuses the join anyway. - 199:69, the two `!channel(role)` tests joined by `&&`: a net of one channel and one gate or bulk terminal then joins, but the group has three unconsumed ends and is never sound, so it falls apart. - 235:24, `group.len() < 2` to `==` or `<=`: a singleton is always sound, and a series pair that is not sound has its two ends on one net, which makes it a parallel pair the parallel pass takes first. Claude-Session: https://claude.ai/code/session_01BKvitR43fxnbTgyL5mQapn
…yout's measures (M2) lvs/lde.rs (catalog LVS-074) and the measured side of graph::from_layout and checks::check_param_ranges / check_device_counts were reached only from the root crate's LVS fixtures: in the nightly shard every sampled mutant of Gate::spans, stress, line_intervals, strips, rectangle, channel, well_distance and add_lde_params survived, and from_layout's metre scale, area scale and r = sheet * l / w did too. tests/lvs/lde.rs: one transistor drawn by hand under a minimal deck, extracted and recognised, then add_lde_params. Oracles: - SA/SB by BSIM4's effective-distance law, hand-evaluated: a source- side OD strip makes 800 nm over half the width, so sb = 1/(0.5/875 + 0.5/575) - 75 = 619.0 nm and sa = 500 nm, after the device's own w and l; the same under the transpose, a mirror and a quarter turn; - the `max` cap at 700 and 400 nm; - SCA/SCB/SCC by Silvaco's closed forms, written out again in the test apart from lvs::lde::wpe, over distances read off the drawing: an enclosing well, a stepped well edge (the width-weighted median, both sides of half and exactly half), a well edge on the gate edge (not outward); - only interned names written, nothing for a gate off its OD, an OD running both ways, or another model. Breaks on a wrong axis, strip, weight, cap, side, median, sign, merge of abutting OD spans, or metre scale. tests/lvs/measures.rs: two nmos sharing a diffusion, a resistor, a capacitor, a bipolar and an inductor drawn by hand. Oracles, hand- derived: w, l, nf, area, perim, the shared diffusion halved, r = 100 ohm/sq x 800/400 = 200 ohm, c = 1 fF/um2 x 0.32 um2 + 0.1 fF/um x 2.4 um = 0.56 fF, ae/pe of the emitter pad, ind 2 nH; with no grid only counts and the inductance; with no name interned, nothing. Ranges: a length at its bound passes and one unit past fails both ways, at each gate's first vertex; a shared diffusion held by its share (ratio 500000 and 250000 against 250000 and 249999); an area and a count compared exactly; a bound of the wrong kind or an unmeasured parameter refuses the run, keeping the other rows. Counts: over a maximum on the max+1-th device, under a minimum on the first, a model with no device at no place. Measured (narrowed cargo mutants on lvs/lde.rs, Sorted, line_intervals and Gate::spans, stopped at 23 of 133 when the round was wrapped up): 19 caught, 4 missed, all in Sorted::meeting. Equivalent, not killed: Sorted::meeting's `x < xlo - widest` to `==` or `<=` and its `&&` filters to `||` (110:42, 117:37, 117:60). The window is the gate's box grown by `max` and every distance is capped at `max`, so a polygon outside the window, kept or dropped, gives a crossing more than `max` away (read as `max`) or a strip cut at the same distance, and no result changes; the candidate scan is pruning. Claude-Session: https://claude.ai/code/session_01BKvitR43fxnbTgyL5mQapn
…omparison and the tables (M2) The nightly shard's remaining in-scope survivors, one test each, all construct-from-answer or law: - gates: NAND3's pull-up is one parallel device (275:36, `2 *` to `2 +`), and a stack repeating a gate and a shorted pair stay as drawn (266:35, 282:12); - reduce: a stack of two models stays two devices (join_series' kind/model test, 810:13); - compare: a layout measure sorting before the card's parameter is passed over and the card's parameter still compared (compare_params' `at_mine += 1`); ten interchangeable dummies of ten widths in opposite orders pair by parameters, beyond the tie-break's eight tries (aimed at Sides::distance and the ranking; not yet measured); - checks: a split label is an error, a warning under a matching connect_implicit pattern or connect_explicit group, an error under a non-matching one (must_connect); the substrate alone does not float and the table says which net is global-only (is_global_only); - topology: every cut of a stack is its own via_cuts_into row, where via_edges_into merges them; - report: rows differing only in a ratio sort by its numeric value, negatives first (f64_key). Each breaks on the mutant named. Equivalent, not killed: - reduce.rs group_is_sound and passive_group_is_sound's kind/model tests (959:34, 989:13): a group is joined only pairwise through join_series / passive_pair, which already require one kind and model, so every member shares the head's. - refine.rs refine_into's `cursor < split` to `>` (834:22): the cursor only skips settled nodes before the stalled-node search, which scans from it to the end either way. - controls.rs Classes::reported's `self.asymmetric` guards: FIXED_SOURCE and FIXED_DRAIN are assigned only to asymmetric models. - compare.rs compare_terminals' `at_mine += 1` (720:25): a terminal mismatch needs a pairing refinement could not tell apart, and role codes are what refinement splits on; no graph reaches the branch. - topology/device.rs recognise_into's `measured && pieced.is_none()` to `||` (402:25): it only computes the touching set earlier or again, and it is read for measured terminals only. Claude-Session: https://claude.ai/code/session_01BKvitR43fxnbTgyL5mQapn
…als and the rule listing (M2) The nightly shard's deck survivors: CompiledDeck::enclosure's pair guards, via_array_spacing's `>` threshold, density's layer guard, rules() replaced by an empty iterator, source()'s rule order with no provenance, RuleRow::kind, DeckBuilder::area's scale, remove_layer's "nothing removed" test, remove() of a custom rule, and CustomRule's equality. Tests, each answer read off a deck written for it or the rustdoc: - the queries keep to the layers asked about: every enclosure kind on a via in two metals with different limits (largest minimum per kind, smallest maximum, full_width on one pair), an array spacing for more cuts than its threshold (2 none, 3 the first, 4 both), each density row on its own layer; - a deck lists its rules by id and kind, DRC in deck order, then ERC, then custom; a builder row names its constructor's kind; - a rule missing from the provenance is still written by source(), after the listed ones; - an area in nm² is whole square grid units (250000 nm² is 250000 on 1 nm and 10000 on 5 nm; 30 nm² on 5 nm is refused); - removing an absent layer is refused with derived layers present; removing the second custom rule keeps the first; - custom rules are equal field by field. Each breaks on the mutant named. Claude-Session: https://claude.ai/code/session_01BKvitR43fxnbTgyL5mQapn
…er M2 moved the base-layer cases into the crate M2 moved drc_octilinear's base-layer cases into crates/check and removed found_under and holds_under_symmetries with them; N1's any-angle tests, which stay in the root, still call both. Claude-Session: https://claude.ai/code/session_01BKvitR43fxnbTgyL5mQapn
…nts are checked, and paths stop at ports (N5) R4 (docs/research/blocked-rows.md) found public definitions for five ERC rows the catalog called undefinable or partial. Each is now a kind or a report field, with its definition and citation on the table type, deck-library parity (kind table, builder, printer/decompiler, twins) and fixtures. - ERC-D9 well_sharing(; models, resistors): US 5,638,286's latch-up check. A transistor's bulk net is its well (the patent groups by back gate terminal); it passes with a channel end on it, a resistor to it (resistors: true), or a chain of same-bulk channels to it. - ERC-F4 hot_carrier(; models, max_length), a warning row: GF180MCU 14.1.4.1 (e), a minimum-length device used bi-directionally, read as each channel end reaching both a power and a ground supply without it or a parallel partner. No static stress condition is public. - ERC-H3 net_type(; net, path, break, exclude) over net types and type sets the intent declares (net_types, type_sets): US20100306720A1's net types by name (? wildcard, lvsPower/lvsGround/lvsOutline) and by device pins, paths broken at nets meeting -break, path types with -exclude, and the -netType/-pathType net check. gate_path's count is HP US 6,367,062's one per series device. erc::Inputs carries the run's strings for the name match. - ERC-G9 supply_path gains labels_are_ports: a labelled net is a top-cell port where a path stops (P12 [0262]). - ERC-A15: a violation can carry a fix hint (Violations::fix, JSON "fix", text "fix"). antenna_electrical solves its own credit, bonus and diode_max_ratio PWL for the least added diode area (SKY130 EGAR, US 9,142,556, the LEF PWL read backwards); antenna gains diode_area and diode_min, IHP Ant.g Note 4, written on the IHP deck's Ant.d rows. Waivers and staging carry the hint (push_row). Every antenna row in the decks, twins and tests states the two new parameters; every supply_path row states labels_are_ports. Tests and oracles: - erc/well_sharing/*: the patent's own cases (Q5 fed from another supply, a resistor with and without condition 2, a chain through another well); breaks if a chain may cross wells or a resistor counts when the deck says not. - erc/hot_carrier/pass_gates: two transmission gates, a NAND, at the length limit and one under; breaks if a partner carries the walk or a stack's inner node counts as driven both ways. - erc/net_type/perc_examples: P12's init_5/init_6/check_1, [0239]'s device-typed resistor nets, a pin-typed gate, lvsPower; breaks if an AND break splits paths or break nets lend excluded types. - erc/supply_path/stops_at_port: a pass gate beyond a labelled output; breaks if a port stops nothing or stops its own rails. - Board oracles (NV) over every enumerated topology board: ws (the patent's conditions by a naive walk), hc, and sp3 (ports). - antenna fix hints (closed form and spec examples): DRM linear, LEF PWL (22 007 and 125 000 nm2, none past the table), the patent's 58.196 um2, IHP Note 4 with its 0.16 um2 floor. - intent: net types read back; four malformed forms refused by name. Claude-Session: https://claude.ai/code/session_01BKvitR43fxnbTgyL5mQapn
…olour cycles, track widths and line ends are checked (N5) DRC-127 and DRC-128 were "not definable from public sources"; R4 found the definitions. - DRC-127 def.cell_edge_spacing, an integration check on a DEF design. The LEF reader keeps the library's LEF58_CELLEDGESPACINGTABLE (from PROPERTYDEFINITIONS or a library PROPERTY) and each macro's LEF58_EDGETYPE, and marks CLASS CORE SPACER. Two parallel typed edges of different placed cells sharing a stretch are held to the table's spacing for their types: the ISPD 2014 contest's Suite A slides 16 and 27 (any parallel pair, left against left) and the ICCAD 2017 Problem C FAQ (symmetric pairs). CELLROW, HALFROW and RANGE spans, mirrored cells and fillers as OpenROAD dpl reads them; EXCEPTABUTTED exempts a zero gap by its name. Entries with EXCEPTNONFILLERINBETWEEN, OPTIONAL, SOFT or EXACT, and DEFAULT types, are undefined publicly and skipped. - DRC-128 sadp(L; different, same, track_width, track_space): US 2015/0286764 A1's colour bands by union-find with parity (an odd number of different-colour edges in a cycle is not decomposable), a self-conflict notch, and the odd-track width rule; Xiao's ISPD 2012 slides state the two-colouring as necessary. sadp_line_end(L; adjacent, tip, overlap, corner, offset): Xu et al. TCAD 2015 Table II rules 1-4 on gridded rectangle lines. SAQP stays undefined. Neither is mirrored in KLayout. Tests and oracles: - integration (hand-derived from OpenROAD's dpl tests mirror_edge_spacing and edge_spacing): a mirrored cell's typed edge lands on its neighbour's (0 against 1000), EXCEPTABUTTED and SOFT exempt it, a filler has no edges; CELLROW types one row (760 against 1000 at the second row only), a point contact is no run. Breaks if mirroring does not move the edge or CELLROW is the whole side. - sadp/* (the patent's figures, every placement): triangles whose different-colour count is odd (1 or 3) flag one cycle, even (2) or colour-free do not; a U with a 50 nm notch self-conflicts; FIG. 1R's 72 nm line flags (two tracks), 120 nm does not. - sadp_line_end/* (Xu's p. 703 example: tip 32, overlap 58, corner 21.2 -> 22, offset 44 nm): one finding a unit under each limit, none at it, nothing three tracks apart. OpenROAD 26Q2 (the oracles shell) does report the table (DPL-0009); a dpl differential is not written yet. Claude-Session: https://claude.ai/code/session_01BKvitR43fxnbTgyL5mQapn
…cked and what stays undefined (N5) The catalog rows carry R4's definitions and citations as implemented: DRC-127 partial (EXCEPTNONFILLERINBETWEEN, OPTIONAL, SOFT, EXACT and DEFAULT types undefined publicly), DRC-128 partial (SAQP, trim-mask rules and overlay not public), ERC-A15 partial (no hint where the ratio moves with the diode), ERC-D9 implemented (Calibre PERC's own rule is not public; the patent's is checked), ERC-F4 partial (no public static stress condition), ERC-H3 partial (device checks, per-cell types and other path definitions not modelled), ERC-G9's note names labels_are_ports. G3 and G7 are unchanged: no source states either check; Zwerger's 2017 TUM thesis defines definite and potential short-circuit paths and floating nodes in power-down mode, which is ERC-H1's ground, not a driver or tie rule. deck.md, the rule reference, README's kind counts (82 DRC, 57 ERC) and the proof table (DRC-127 and ERC-A15 are proved by named tests) follow; limitations.md and check-sources.md are tests/catalog.rs's rewrite, run twice. Claude-Session: https://claude.ai/code/session_01BKvitR43fxnbTgyL5mQapn
Formatting only; no behaviour changes. Claude-Session: https://claude.ai/code/session_01BKvitR43fxnbTgyL5mQapn
…tement must declare (N5) N5's net_type wrote its net, path, break and exclude lists as Dim::Models, so the deck lowering's check that every model a rule names is declared by a device statement (D4) refused the type names `"!"`, `"power"`, `"ground"`: every erc/net_type/perc_examples fixture failed with `rule init5: model "!" is not declared by any device statement`. A new Dim::Names reads and prints as Dim::Models does (one quoted name per engine param, the same ParamSource::Model), and the model check skips params of that dim. net_type's four lists take it; every other model list keeps the check. Tests: tests/exhaustive erc/net_type/perc_examples (16 placements, hand-derived from the PERC patent's examples) now load and hold; they break again if net_type's lists are checked as models. Claude-Session: https://claude.ai/code/session_01BKvitR43fxnbTgyL5mQapn
…egration branch - README's status table is recomputed from docs/check-catalog.tsv: DRC 56/6/44/0, ERC 64/4/13/0 (both rows were stale). - tests/engine/def.rs (N3) and crates/check/tests/erc/ported.rs (M2): antenna rows state `diode_area: none, diode_min: none` and supply_path rows `labels_are_ports: false`, the old behaviour, now that N5 made those parameters required (docs/deck.md's forms). - ERC-A15's oracle column names MR, which its fixtures give; the generated docs/check-sources.md block is rewritten by tests/catalog.rs. - DRC-038's PROVED_BY_TEST points at crates/check/tests/drc/octilinear.rs, where M2 moved the test; its doc still names the row. - Oracle lines for net_space_across_two_layers_reads_their_nets (nets and gaps by construction) and the two DRC-127 cell-edge tests (their hand derivation from OpenROAD's dpl tests now starts its own line). - seg_dist2 floors any-angle distances, as its doc and N1's exact comparison say; M2's test expected the older round-up. Slope-1/2 lines `y = x/2` and `y = x/2 + 3` are 9 - 9/5 = 7.2 apart squared, floored to 7 (a round-up would read 8); the test is renamed to the contract and its equality with seg_seg_dist2 dropped. Claude-Session: https://claude.ai/code/session_01BKvitR43fxnbTgyL5mQapn
OmarSiwy
marked this pull request as ready for review
October 15, 2026 15:14
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Work in progress, opened as a draft so GitHub Actions runs the heavy test tiers (label
heavy) instead of a developer machine.What this branch does, tracked in
docs/testing-plan.md(§8 ledger, findings table):tests/exhaustive/): bitmap reference DRC over every small pattern, brute-force LVS over every small circuit, closed-form ERC and PEX, metamorphic relations on the corpus.tests/klayout/), with Netgen/FastCap and the foundry decks in progress.Remaining work is listed in the ledger.
https://claude.ai/code/session_01BKvitR43fxnbTgyL5mQapn
Merge note
Merged on the maintainer's instruction with the combined branch's full local
workspace suite green (
cargo test --workspace --no-fail-fast). The nightlytier (run 38758359381) and this PR's CI were still running at merge; their
results are followed up on
main. The PR-onlymutants-in-diffgate iswaived for this merge: it mutates the whole branch diff (about 8000 mutants)
and cannot finish within its job limit. The nightly mutation gate, which
samples a tenth of geom and check each day against a 65 % floor, stays in
force. Work not yet done is tracked in issues #37-#65.
https://claude.ai/code/session_01BKvitR43fxnbTgyL5mQapn