Repository navigation
Search equivalent NOR netlists with an e-graph - #61
Merged
Merged
Conversation
Exact placer on an rsdsl v2 model: optimization, carry tiles, timing, dust physics
Construction steps that place a new input sometimes failed as infeasible within 0.1 s for every window, then restarted with a new seed (three of five seeds of one full-adder netlist, and earlier the carry tile's carry entry). The step diagnosis (EXACT_DIAGNOSE_INFEASIBLE) showed the culprit: freeing an earlier input's kept switch made the step solvable. The new input's candidate sites covered the whole window, including the overlap slice where a switch placed in an earlier step is kept as a fixed cell. dsl.rs gave a fixed switch to the first input with a site there, so the kept switch became the new input's: the earlier input lost its only site and the frozen gates it drove contradicted their given signals. New inputs no longer get sites where a switch is already placed, and a fixed switch belongs to the input whose only site it is when several inputs could claim it (an error if that is still ambiguous). The same seed now places that step in 9 s. The diagnosis hook stays: with EXACT_DIAGNOSE_INFEASIBLE, an infeasible step is re-solved with given signals, each observation, each single-site input, and frozen air dropped in turn, and the placed inputs' surroundings are logged. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
The exact placer builds whatever NOR netlist it is handed, so a hand-written netlist such as the full adder's nor9 fixes its torch count and logic depth before placement starts. egraph.rs explores the equivalent netlists with egg and extracts ones worth placing. Saturation runs De Morgan, double negation, commutativity and associativity, distribution and factoring both ways, absorption, and XOR and XNOR expansions. Each e-class carries its truth table, and classes with equal tables are unioned in modify, so different forms of one function always meet. The full adder reaches 230 of the 256 three-input functions in 73 ms. Greedy extraction decides class by class and missed the shared NORs (13 gates against nor9's 9), so extraction is exact: egraph_extract.rsdsl, grounded with rsdsl and solved with the placer's CaDiCaL binding, picks one node per needed class (outputs are torches, a NOT adds a tick, an OR none) and minimizes gates, plus or_cost per OR node since every NOR input is a signal to route, within an optional depth bound. Each extraction is proven optimal for its e-graph in 0.1-10 s. On the full adder: - fewest gates: 8 (nor9 has 9), depth 3/4, but NORs of up to 4 inputs; - depth 3: 9 gates, depth 2/3; - or_cost 1: 9 gates, depth 4/5 against nor9's 5/6, fan-in 3, and the same 4 nets alive at once as nor9. The circuit harness places them (CIRCUIT=egraph-full-adder with EGRAPH_DEPTH and EGRAPH_OR_COST); explore_egraph_netlists sweeps depth bounds and OR costs. ExactLocalPlacer::from_netlist takes a netlist built elsewhere. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
The e-graph finds full adders with fewer gates (8) or less depth than nor9, so the question was whether placement gains from them. Placed with the same settings, the wide NORs they rely on are what construction cannot handle: steps with a 3- or 4-input NOR ran out of their 60 s repeatedly. The 8-gate and depth-3 netlists found no layout in 3 and 5 restarts; the or_cost 1 netlist (9 gates, depths 4/5, fan-in 3) took 15-16 minutes to construct against nor9's 1-1.5, and then compacted to the best cell of the runs on one seed (88 blocks, 11 ticks) and a poor one on the other. A `binary` extraction option allows only two-input NORs (an OR may not join classes built as ORs). Under it the minimum is nor9 itself, 9 gates at depth 5/6, proven optimal for the e-graph, so every gain over nor9 needs wider NORs and therefore a construction that can build them. docs/egraph_netlists.md records the method, the extractions, the placements, and that as the next step. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
The e-graph's smaller and shallower full adders rely on NORs of 3 and 4 signals, and construction kept running out of time on those steps: every input has to reach the torch's block within one window two cells wide. Splitting such a NOR lets construction merge its inputs first and place the torch on a two-signal OR later. Netlists gain NetDriver::Or: a net that is the OR of its inputs, built from dust and blocks without a torch. Netlists from a logic graph never contain one (their ORs fold into gates as before, and the CNF hashes are unchanged). Construction orders OR nets as steps like gates, step timing gives them their latest input's arrival, RCELL expressions write them as (a|b), and netlist depths count them free. ExtractOptions::split_wide builds every NOR of more than two signals from the two halves of its OR, each an OR net when wider than one signal, with OR nets shared between gates through their e-class. The 8-gate full adder becomes 8 two-input NORs and 5 OR nets. Splitting does not cut the nets alive at once (6 against nor9's 4, the OR nets being signals too), so placement will tell whether the narrower steps pay for it. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Every live net crosses a construction step's last slice, and the e-graph's netlists keep more nets alive than nor9 (6 against 4), so the order construction places gates in might narrow them. GateOrder::MinLive picks, among the ready gates, the one after which the fewest nets are still needed, ties going to the smaller cone (CIRCUIT_ORDER=min-live). It does not help these netlists: nor9 and the OR-cost netlist stay at 4, and the 8-gate netlist split into two-input NORs stays at 6, which is a property of the netlist and not of the order. The order is kept as an option and as part of the topological-order test. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Splitting was meant to let construction build the e-graph's wide NORs in narrow steps. Placed, it made the 8-gate full adder placeable once (2x23x10, 327 blocks, 14/25 ticks after compaction, against nor9's ~147 blocks and 13-17/17-18) and the OR-cost netlist about equal to nor9 (138 blocks, 13/18), still with several restarts. The doc records why: the cross-section stays as wide (OR nets are signals too, and no gate order narrows it), and an OR is only free on the block a torch reads. Carried on as a net, dust would power both merged lines back, so it needs a block and a repeater. The next step it names is building a wide NOR around a reserved support block instead. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
rollrat
changed the title
This was referenced Oct 5, 2026
rollrat
changed the title
Splitting a wide NOR into OR nets did not help, because an OR carried to later steps is not free: merged dust powers both of its lines back, so it needs a block and a repeater. The OR is only free on the block the torch reads. This builds a wide NOR around that block instead, one more signal per step, so the OR never has to travel. NorNetlist::chain_wide_gates turns every NOR of more than max_fan_in signals into a left-leaning chain of OR nets, inputs first and the rest in topological order: NOR(x1, x2, x3, x4) becomes s1 = OR(x1, x2), s2 = OR(s1, x3), NOR(s2, x4). Construction treats an OR net read by exactly one net that reads no other OR net (chained_ors) as a stage of a support block: - its first OR is observed on a block of the last slice (ExactPlacerConfig::solid_observations, the mechanism the carry out uses), and the block's position is kept in the step state; - every later stage, and the NOR that ends the chain, fixes that block, keeps its slice open (the frozen boundary stops there), and observes the next OR on the same block, so the new signal has to reach it; - gate orders move each chain to just before the NOR it ends in, so its stages are consecutive steps. Nothing changes for netlists without OR nets (the CNF hashes are the same). The circuit harness takes EGRAPH_CHAIN=<max fan-in>; a test checks that chaining keeps every function and that orders keep chains together. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
The support-block construction does what it was built for: a chain's OR lands on a block and the next stage reaches the same block, each such step in 9-28 s. It did not make the e-graph's netlists constructible. With two seeds of the 8-gate netlist and one of the depth-3 netlist, 35-50% of the step attempts ran out of their 60 s, at a different step each attempt, and none was proven infeasible. A 3-wide box made every step slower, nor9 included. The doc records the result and what it points to: these netlists keep 6-7 nets alive where nor9 keeps 4, and windowed construction pays for every crossing net in every step. Next steps: longer steps to see whether they place at all, and crossing width as an extraction cost. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Every failed step of the e-graph netlists ran out of its 60 s, none was proven infeasible, so the next question is whether they place at all with more time. Longer steps alone would not show it: an attempt still restarted after the default 600 s. CIRCUIT_RESTART_SECONDS sets that limit (default 600, as before). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
The last open question was whether the e-graph's wide-NOR full adders place at all with more time. With 240 s per step and an hour per attempt they do not: the flat 8-gate netlist stuck at its first 4-input NOR after three 240 s windows, and the chained 8-gate and depth-3 netlists stuck at cout, with chaining getting further than flat. The doc's conclusion: under two-input NORs nor9 is the proven minimum, and every better netlist needs wider NORs and more nets alive at once, which windowed construction cannot place however the NORs are split or staged. The search and exact extraction remain useful to prove netlists optimal and to look for better two-input netlists of other circuits, which is the next step it names. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
The 8-gate and depth-3 full-adder netlists from the e-graph never constructed in a 2x10 box. Their steps only ever timed out, so it was open whether the box was simply too small. This raises the height to 12 and 14 and lets windows grow to 6 slices (new CIRCUIT_MAX_WINDOW knob) to answer that. They still stall at the same steps on every seed, while nor9 builds in the same settings in 1.5-2.5 minutes. The same g4 that fails as one 3-input NOR builds in two short steps when chained, with the same nets alive afterwards. So the obstacle is merging a new input and three signals in one step, not the cross-section. Whether a layout exists at all is still open and needs a solve without windows. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
The e-graph's full-adder netlists with wide NORs never constructed, even in taller boxes, and no step was ever proven infeasible. To see what makes a step hard, EXACT_DIAGNOSE_UNKNOWN re-solves the first timed-out step with one requirement dropped at a time. Dropping the new gate's own output from the window's last slice solves the step in 1-5 s. Dropping any other net mostly does not. The gate is easy; getting its output out past inputs that branch to later gates is not. The steps are hard rather than impossible: the same flat g4 step was placed in 54 s in one run and stayed undecided for 30 min in another. The harness now prints, per step, how many of the gate's inputs are used again later. With the peak live-net count, it separates the netlists that build from those that do not: nor9 has 4 and 2. The or_cost 1 netlist chained on a support block has the same numbers. It was predicted to build easily and did, first try on both seeds, and compacted to 115-116 blocks against nor9's 146-148 in the same box. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Explaining why a step such as g5 fails needed the netlist in the order construction places it: which gate each step builds, what it computes, which of its inputs later steps need again, and what stays alive. The harness only printed the gates by net index and the counts. It now prints one entry per step with all four. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Construction only places netlists that keep few nets alive between steps and few continuing inputs per gate. The e-graph's cheaper full adders break both, and listing its netlists one by one to screen them was impractical: ORs nest and pad with redundant inputs, so a minute found 8. nor_synthesis.rsdsl builds the netlist and its construction order together, with those counts as constraints. Each step is a NOR or an OR stage of a support-block chain, reads at most two nets, and wastes nothing. The model minimizes torches per step count. Findings for the full adder, each proven per step count: - No buildable full adder of up to 14 steps has fewer than 9 torches, even with 6 nets alive. - At 9 torches the best depth is 4/5 (cout/s). It needs 11 steps, and the netlist is the e-graph's or_cost 1 one chained, found again from scratch. - Depth 4 for s is impossible within 14 steps, and 3 live nets within 13. Every synthesized netlist built, all steps in window 2. Placement runs also showed that 600 s compaction varies more by seed (nor9 at height 12: 90-237 blocks) than by netlist, so blocks need the full pipeline and more seeds to rank netlists. Also: NorNetlist::to_text/from_text with a CIRCUIT=netlist harness mode, and a refactor of e-graph extraction into GroundedExtraction. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Synthesis proved what a buildable full adder needs. This applies it to
the harness's other circuits, settles the full adder's block comparison
with longer compaction, and checks the proofs' reach.
- Other circuits (synthesize_buildable_circuits, SYNTH_CIRCUIT):
- half adder 5 torches and 2:1 mux 4, both proven, against 7 gates
each from expressions;
- 4:1 mux 8 torches, against 20 gates and 6 live nets. That netlist
never built. The synthesized one built in all three runs and
compacted to 142-168 blocks, RCELL-verified;
- 2-bit adder 14 torches, against the hand-written 15, and shallower
(not proven).
- The full adder's 9-torch floor holds to 16 steps at 4 live nets. With
7 live nets the model finds 8 torches, so the bound excludes them, not
a modeling error.
- With 1800 s of compaction (3 seeds each), nor9 averages 84 blocks and
the chained or_cost 1 netlist 80, best 72. The 30-block gap at 600 s
was mostly unfinished compaction.
- The doc no longer says the harness ran without step and repair
minimization; both are on by default.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Synthesis should give smaller cells than hand-written or decomposed netlists, not only fewer torches on paper. The synthesized 14-torch 2-bit adder was placed against the hand-written 15-gate adder2-nor with the same settings (7 workers, 1800 s of compaction, two seeds). It came out about a fifth smaller and faster on both seeds: - 122 and 134 blocks, against 160 and 163; - s1 in 12-15 ticks, against 16-22. The 4:1 mux's 20-gate netlist never built. The 8-torch synthesized one compacted to 142 blocks. Both cells are now fixtures with tests that check the arithmetic or the selection in every case and every settled input transition. They are also viewer examples. The manifest refresh picks up sizes of NBTs regenerated earlier, and full-adder.nbt's stale copy. export_rcell_cell writes any RCELL's .nbt and .outputs.json. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
rollrat
marked this pull request as ready for review
October 9, 2026 23:26
3 tasks done
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
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.
Stacked on #59.
Why
The exact placer builds whatever NOR netlist it is given. A hand-written netlist (the full adder's
nor9) therefore fixes the torch count and the logic depth before placement starts. This PR searches the equivalent netlists with an e-graph and measures whether placement gains from them.What
dsl.rsthen read that fixed switch as the new input's. New inputs now skip placed switches, and a fixed switch belongs to the input whose only site it is.EXACT_DIAGNOSE_INFEASIBLEre-solves an infeasible step with one requirement dropped at a time; that is how this was found.exact/egraph.rs, egg 0.9):exact/egraph_extract.rsdsl):NetDriver::OrandExtractOptions::split_widebuild a wide NOR from OR nets placed as steps of their own. Netlists from a logic graph never contain OR nets, and the CNF hashes are unchanged.chain_wide_gates,solid_observations): a wide NOR is built in stages: its first OR sits on a block on the step's last slice, and later stages feed that block.exact/synthesis.rs,exact/nor_synthesis.rsdsl): builds a NOR netlist and its construction order together. Each step is a NOR or an OR stage of a support-block chain. The live nets between steps are a constraint, so everything it returns can be placed.SynthesisOutcomeseparates a proven infeasible result from a time-out.NorNetlist::to_text/from_textand aCIRCUIT=netlistharness mode, which places any netlist given as text.GateOrder::MinLive: places the ready gate after which the fewest nets stay alive.Findings (full adder,
docs/egraph_netlists.md)nor9or_cost1nor9, proven optimalnor9uses NORs of 3-4 signals. Construction cannot place those in a window two cells wide: the steps time out, and the layouts take many restarts or none.nor9's 4, whatever the order). And an OR carried on to later steps needs a block and a repeater, since merged dust powers both of its lines back.nor9placed at about 147 blocks and 13-17/17-18 ticks.EGRAPH_CHAIN) gets further, but steps with 6-7 nets alive still time out, with 60 s or 240 s per step.nor9builds in the same settings in 1.5-2.5 minutes. The sameg4that fails as one 3-input NOR builds in two short steps when chained, so the obstacle is merging a new input and three signals in one step.EXACT_DIAGNOSE_UNKNOWNre-solves a timed-out step with one requirement dropped at a time. Dropping the new gate's own output solves it in 1-5 s, and dropping any other net mostly does not. The hard part is getting the new torch's output out past inputs that branch on to later gates.nor9's 5/6. That netlist is the chainedor_cost1 one, found again from scratch. Placement runs showed that 600 s compaction varies more by seed (nor9at height 12: 90-237 blocks) than by netlist (docs/nor_synthesis.md).test/adder2-synth-exact-2x16x8.rcell,test/mux4-synth-exact-2x16x10.rcell). Their tests check every case and every settled transition.nor9and the chainedor_cost1 full adder end up close (84 against 80 blocks on average over three seeds).nor9has 4 and 2). Theor_cost1 netlist chained on a support block meets it. As predicted, it built on the first try on both seeds (110-119 s) and compacted to 115-116 blocks, againstnor9's 146-148 in the same 2x10 box.Test plan
cargo test --release --lib: 372 passed; the one failure (world_to_logic_extracts_d_latch_nbt_as_sequential_node) fails on master too.print_cnf_hashes: unchanged for netlists from logic graphs.diagnose_construct_circuit(CIRCUIT=egraph-full-adder,EGRAPH_*knobs): every cell that was placed passes its RCELL check.🤖 Generated with Claude Code