Repository navigation
Place latches with the exact placer by cutting their loops - #68
Merged
Merged
Conversation
The exact placer builds compact combinational cells but could not place a latch. Netlists rejected cycles. The model's stage order and the lazy feedback check forbade a torch reaching its own support. Verification was combinational and started from every torch lit, which races a latch. This sets up an environment for compact sequential cells, as was done for the full adder. - NorNetlist::state names state nets. Cases cover the inputs and the stored state, and readers of a state net read the stored bit. The text form gains state(...) and out(...). - The model cuts each loop at its state net. The torch carries the next value and the cells past the cut carry the stored value (fact cut). The cut alone is exempt from soundness and stage order, and acyclic.rs treats it the same way. - The first version used only settled cases. It let the solver build "latches" whose inputs never reached the loop (a NOT where NOR(s,q) belonged), and the simulator rejected thousands. Requiring the next value from every stored state removes that: the set-reset latch now has no rejection. - Sequential verification starts each settled case with its own torch states, then flips one input at a time and checks outputs and burnout. Exported worlds store a settled case. Results: - A set-reset latch in 2x3x3 with 8 blocks, proven fewest. - A D latch written as a 4-torch multiplexer in 2x3x4 with 16 blocks, proven fewest. The heuristic layouts were 12x9x5 and 14x10x10. - Master-slave flip-flops found nothing in one solve, like the full adder. They need construction that places a loop in one step. Both latches are kept as fixtures, checked by pasting their NBT and pulling the levers. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
The 10-torch flip-flop also found nothing in 2x8x5 (900 s), and the 6-torch one nothing in 2x6x5 (600 s), so the doc's conclusion stands: flip-flops need construction that places a latch's loop in one step. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Latches placed in seconds, but no flip-flop came out of one solve. The experiments separate the possible causes: - With the D latch fixture fixed as the master (new SEQ_FIX_RCELL hint), a six-torch falling-edge flip-flop is found in 0.7-2.7 s with no simulator rejection: 39 blocks in 2x6x4. So flip-flops do fit small boxes. - The same six torches with both loops opened, the stored values as levers, take 6-10 minutes in one solve. Six torches over 16 cases is slow already. - Closed loops make it much slower: nothing in 30 minutes with 10 workers. Forcing the cut onto the state torch's output did not help. So the route to flip-flops is construction that places each latch's loop as one step and the gating around it, as fixing the master by hand did once. The hinted flip-flop is kept as a fixture, tested by pasting its NBT and clocking it. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…blocks Faster solving should not cost optimality. Pinning outside signals and fixing slices both lose it. A symmetry rule keeps it: the model cannot tell east from west or north from south, so a mirrored layout is a layout too. box_symmetry adds the lex-leader constraint for the x, y, and xy mirrors over which cells are filled. It applies only to symmetric instances: default sites, nothing fixed or given, no carry. Every mirror family keeps a member, so optima and infeasibility proofs are unchanged. Measured in pairs, 4 workers each: optimum proofs got 1.5-2.2x faster (set-reset latch, 2:1 mux; one mux proof finished only with it). Infeasibility proofs got 15-30% slower (D latches, half adder). So it stays off by default. The flip-flop fixture is replaced by its compaction: 39 -> 29 blocks in 2x6x4. Recompaction now takes sequential cells (RECOMPACT_SEQ), and the latch it started from was not kept fixed. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…e removal Symmetry: the opt-in lex-leader constraint compared filled cells, which sped up optimum proofs but slowed infeasibility proofs, so it stayed off. BoxSymmetry now picks what is compared (filled cells or torch positions), the order (height or length first), and the mirrors (all or x only). Over five instances and three seeds each, comparing torch positions was 17% faster overall and never more than 4% slower, so it is the default. Core-guided removal: when a slice removal's window is infeasible, ask which fixed cells around it the proof needs, free only those, and retry; an empty core rules the removal out. Fixed cells near the window become soft (fact `soft`, one guard each), ExactLocalPlacer::fixed_core solves with them assumed and adds acyclicity lazily, and rsdsl's GroundOptions::guard_rules guards only the selected rules. It does not pay: a guarded require is not a unit, so the grounder cannot fold the fixed cells away, and the core solve takes over 20 s where the plain proof takes 1-3 s. The first version also missed lazy acyclicity and got cyclic models. CompactionConfig::core_guided stays off; the measurements are in docs/exact_local_placer.md. The rsdsl reference instance gains the Sym, Order, cut, mirror, and soft declarations; its test had failed since the model gained `cut`. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Why: the guarded-assumption core cost more than ten times the proof it explained, because a guarded require is not a unit and the grounder could no longer fold the fixed cells away. The proof itself says which clauses it used, so the units can stay units. How: SatSolver::trace_frat writes CaDiCaL's proof in FRAT with antecedents (original clauses with ids, including lazily added acyclicity clauses, and each derived clause with the ids it rests on). frat::refutation_originals walks back from the empty clause. Soft cells now sit in an rsdsl @NoFold rule: their units stay plain unit clauses that neither folding nor the final unit propagation touches, while every other fixed cell still folds. ExactLocalPlacer::proof_core returns the soft cells whose units the proof used; a test breaks a placed NOR's torch and checks that the core names it and that the core alone stays infeasible. The assumption path, the soft cell guards, and rsdsl's guard_rules are gone. Result: core queries take 0.03-10 s on one thread, but slice-removal cores cover most of the window's boundary, since every wire through the slice must be reconnected. Freeing more than 20 cells times out; with that cap 4 of 89 retries placed the removal, and on three full adders the core-guided runs ended at 189/98/117 blocks against 165/60/99 without. core_guided stays off; proof_core stays as a cheap explanation for local infeasibility. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
rollrat
force-pushed
the
claude/sequential-cells
branch
from
November 8, 2026 06:23
3e9a4cc to
2ba9f12
Compare
Make the current placement constraints readable as one predicate with factored power relations and Korean annotations, so subsequent pruning experiments can distinguish model assumptions from preservation claims.
Preserve candidate constraints, counterexamples, complete tiny-layout fixtures and benchmark evidence so future pruning work can distinguish safe reductions from representation loss. Include NBT examples for inspecting equivalent boundaries.
Avoid per-cell allocation during Kind decoding and run a lone solver worker inline. Preserve CNF and search behavior, and retain A/B benchmarks so frontend gains are not mistaken for SAT search improvements.
Preserve the cold six-gate DFF discovery and independently verified NBT fixtures. Add whole-layout keep-or-remove optimization to compaction and sequential export so redundant blocks are removed automatically instead of by manual coordinate edits. The original 45-block discovery reduces to 33 blocks while retaining I/O pins and sequential behavior.
Remove redundant auxiliary rank and stage assignments without excluding physical layouts. Keep the general model opt-in because paired multi-seed measurements improve XOR and the recorded DFF configuration but slow some smaller combinational circuits. Include per-worker profiling, reproducible benchmarks, 120 combinational runs, preservation checks over 1,442 layouts, disabled-model CNF parity, and independently verified DFF artifacts. Retain the historical DFF timing caveat after relocating the rule.
rollrat
marked this pull request as ready for review
November 8, 2026 12:21
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.
The exact placer now supports sequential cells by cutting declared state-net loops and verifying both settled states and single-input transitions. The follow-up work finds a falling-edge DFF without fixing an existing latch and automatically removes redundant blocks from verified layouts.
Sequential placement
NorNetlist::state,state(...)/out(...), and cases over inputs plus stored state bits. A state-net torch computes the next value; cells past the cut carry the stored value.Block counts exclude input switches. The latch minima are within their tested exact-model configurations; the 29-block DFF is a separate construction result.
Global search, minimization and optimization
Global DFF discovery and automatic minimization
Find all six gates and their wiring together in a 2×7×4 box, with no fixed blocks, fixed input sites, or initial latch layout. The original discovery took 163.5 seconds and produced 45 blocks.
The search specifies the original six-gate logical topology and fanins. It does not preserve every possible Boolean-equivalent DFF implementation, and its failure would not prove that all DFF layouts are impossible.
ExactLocalPlacer::minimize_existinglets every existing non-switch block either retain its kind or become Air, fixes empty cells and I/O pins, and minimizes block count using normal full verification. It is integrated into compaction and sequential export. The original discovery shrinks 45 → 33 blocks in about 0.08 seconds. Optimality applies to deletion subsets of that fixed geometry under the configured model, not arbitrary re-placement.Optional source-rank normalization
Add
canonical_source_ranks:These kinds have no incoming comparisons in the corresponding order, so lowering the auxiliary values preserves the physical layout. The rule sits beside the existing rank/stage symmetry rules, with a Korean rule name.
Same-seed DFF measurements improved from 144.5 seconds in the control (163.5 seconds historically) to 43.4 / 43.8 seconds. Seeds 12 and 13 still failed to finish within 120 seconds. Those DFF timings precede relocation of the rule within the DSL; they are not a timing claim for the reorganized file.
The general model keeps this option off by default. A 120-run combinational study using seeds 1, 2, 3, 11 and 23 found:
Timeouts are retained as failures, not treated as completed timings or infeasibility proofs. These results establish circuit/configuration-specific gains, not a universal speedup.
Supporting work
Preserve symbolic constraints, pruning candidates and counterexamples, tiny complete layout sets, boundary-equivalence experiments, NBT illustrations and benchmark records. Reduce Kind-decoding allocation and single-worker dispatch overhead separately from SAT-search improvements.
Validation
Recent release-mode checks passed:
Final local release checks on head 0a5af79: cargo test --release --lib -- --test-threads=1 passed 387 tests (56 ignored); cargo test --release -p rsdsl passed 9 tests. The library test build uses the existing local counter.v and d-flip-flop.v snapshot samples, which are not tracked by Git; that dependency also exists on the base branch. GitHub CI passed the NBT Viewer build; it does not run the Rust test suite.
Documentation:
docs/sequential_exact_cells.md,docs/global_dff_search.md,docs/dff_search_optimization.md, anddocs/combinational_source_rank_benchmark.md.