diff --git a/.gitignore b/.gitignore index 861889c..a6305dc 100644 --- a/.gitignore +++ b/.gitignore @@ -1,8 +1,9 @@ docs/ benchmarks/ temp/ build/ compile_commands.json out/ include/bbdd/ *.csv +trace.vcd diff --git a/PARTITIONING.md b/PARTITIONING.md index 1452837..419d6fa 100644 --- a/PARTITIONING.md +++ b/PARTITIONING.md @@ -1,206 +1,276 @@ # Support-bounded partitioning for the DD conversion passes Living design + progress document for the partitioning preprocessing step. Updated as implementation proceeds — see [Progress log](#progress-log) and [ISCAS85 results](#iscas85-results). ## Motivation `convert_bbdd` and `convert_bdd` read a flattened `.blif` into a `mockturtle::cover_network` and build **one decision diagram per primary output over all primary inputs** (`include/util/cover_to_bbdd.hpp:34-104`; the recursion bottoms out at `ntk.is_ci(node_i)`). Decision diagram size is worst-case exponential in the number of variables, so beyond roughly 20-25 primary inputs the construction stops being feasible and the `timeout` guard in the yosys scripts kills the run. Of the 11 ISCAS85 circuits only **c17** (5 PIs) is comfortably inside that limit. Everything else sits at or well past it — c6288/c432 ≈ 32-36 PIs, c499/c1355 ≈ 41, c3540 ≈ 50, c880 ≈ 60, c5315 ≈ 178, c7552 ≈ 207, c2670 ≈ 233. **Goal:** a preprocessing step that splits the circuit into subcircuits ("blocks") whose input support is at most a parameter `n`, builds a decision diagram per block, and stitches the per-block netlists back into a single `.blif`. With `n >= |PI|` the flow must reduce exactly to the current behaviour. ## Approach - **Partitioning — maximal support-bounded cones.** Grow a cone backwards from each output while its input support stays `<= n`. A fanin that would push the support over budget becomes a *boundary net*: it is cut there, and it seeds a new block. This keeps blocks as large as the budget allows, which maximises node sharing inside each diagram. - **DD storage — one unique table per block.** Each block gets its own `Unique_table`, its own chain variable ordering and its own sifting run. Sifting over `<= n` variables is cheap and effective; that is the main quality win. There is no node sharing across blocks. ``` n = 4 PI: a b c d e f g | | | | | | | +---+--+--+--+ | | | | BLOCK 1 | | | | support {a,b,c,d} -> DD over 4 vars +------+-----+ | | | | w1 | | | +---+----+--+--+ | BLOCK 2 | support {w1,e,f,g} -> DD over 4 vars +------+-------+ | PO 2 blocks, 2 DDs; boundary net w1 becomes a named internal wire in the output .blif ``` ## Constraints that shape the implementation These were found while reading the existing code and are the reason this is not a small patch. 1. **`cvo` is indexed by a bare modulo, not a hash.** `POS(in, cvo)` is `(*cvo)[in % cvo->size()].pos` (`include/bbdd/include/chain_variable_ordering.hpp:14`), and `init_ordering` under `cvo_none` writes `(*cvo)[inputs[i] % inputs.size()].pos = i` (`:99-107`). This is collision-free today only because the inputs are the *contiguous* cover node indices `2 .. |PI|+1`. A block's leaves are arbitrary cover node indices (say `{2, 57, 130}`) and `57 % 3 == 130 % 3` — the ordering silently corrupts. → **Every block renumbers its leaves to a contiguous `2 .. k+1`** before `init_cvo`, and keeps a local-id → cover-node map for name lookup. This also satisfies `write_blif_recursive_muxxor`, which reads `signal_map[node->cvo_lvl.pv - 2]` (`include/bbdd/include/unique_table.hpp:337-341`). 2. **The in-place `color_view` would destroy the cover network.** It stores colors in `_storage->nodes[n].data[1].h1` (`include/mockturtle/views/color_view.hpp:82-110`) — the exact slot `cover_network` uses for the node's cover index (`include/mockturtle/networks/cover.hpp:84`, and the `CUBE(node)` macro at `include/util/cover_to_bbdd.hpp:15`). → Use **`out_of_place_color_view`** (`color_view.hpp:159-247`): separate storage, identical API. 3. **`ntk.visited()` is the DD memoization slot.** `cover_network::visited` is `data[1].h2` (`cover.hpp:669-678`) and `create_bbdd` stores unique-table indices there (`cover_to_bbdd.hpp:41, 79, 97`). With a fresh table per block those go stale. → **`ntk.clear_visited()` between blocks**, and keep `depth_view` off the cover network during conversion for the same reason. 4. **`mockturtle::expand_towards_tfi` is not sufficient on its own.** It stops only on a *trivial* cut — all leaves `is_ci`/`is_constant` (`include/mockturtle/utils/window_utils.hpp:298-311, 502-546`) — and has no notion of "already belongs to another block", so it would expand through and duplicate other blocks' logic. The growth loop is written locally with a terminal predicate; `cover()` (`window_utils.hpp:832`) and `collect_outputs()` (`:232`) are reused verbatim. The LUT-mapping alternative was considered and rejected: it produces one tiny diagram per node, losing the sharing that motivates the whole pass, and it would cap `n` at 16 (`max_cut_size`, `include/mockturtle/algorithms/cut_enumeration.hpp:102`). The cone partitioner has no such cap. ## Environment notes - **BuDDy** is installed in `/usr/local/{lib,include}` and registered with `ldconfig`. Verified: headers compile, `-lbdd` links, binaries run without `LD_LIBRARY_PATH`. -- **Yosys 0.33** is installed, which predates `flatten -noscopeinfo` (added in 0.40). The - committed `.ys` templates use that flag, so `test/run_iscas85.sh` detects the yosys version - and strips the flag when unsupported. On 0.33 plain `flatten` is equivalent, because no - `$scopeinfo` cells are produced in the first place. +- **Yosys 0.33** is installed, which predates `flatten -noscopeinfo` (added in 0.40). On 0.33 + the flag is a hard error (`Command syntax error: Unknown option`), so both `synth.sh` and + `test/run_iscas85.sh` detect the yosys version and strip it from the rendered script. Plain + `flatten` is equivalent there, because no `$scopeinfo` cells are produced in the first + place — this yosys is sufficient, no upgrade needed. +- **Converter options are injected through `{{CONV_FLAGS}}`**, substituted by both `synth.sh` + (`-n MAX_INPUTS`) and the runner (`-n`). Only `yosys/bbdd_synth_muxxor.ys` carries the + placeholder; `convert_bdd` parses no options at all (`src/convert_bdd.cpp:118` reads + `argv[optind]` directly), so its template deliberately has none and the runner refuses `-n` + against it rather than dropping the flag silently. Lifting that is step 8. +- **`print_summary.py` needs `matplotlib`, which is not installed**; `yaml` is. `synth.sh` + resolves `python3` before `python` (this box has no `python`) and treats a failed summary as + a warning, since it runs *after* a finished synthesis and must not look like a flow failure. - `src/CMakeLists.txt:15` links `bdd` into *every* target via the `*.cpp` glob, though only `src/convert_bdd.cpp` includes `bdd.h`. Harmless, but worth narrowing. ## Testbench `test/run_iscas85.sh` — non-interactive regression runner over the ISCAS85 suite. `synth.sh` cannot be reused for this: it prompts via `read -e -p`, and its directory mode globs `"$file_path"*.v` (`synth.sh:100`), which misses the nested `benchmarks/ISCAS85//.v` layout. ``` test/run_iscas85.sh [-n MAX_INPUTS] [-t TIMEOUT] [-T YOSYS_TIMEOUT] [-o OUT_DIR] [-s SCRIPT] [-k] [circuit ...] ``` It renders the yosys template with the same substitutions `synth.sh` uses, runs it **with the SAT equivalence check enabled**, classifies the outcome, and prints a markdown table. Verdicts: | Verdict | Meaning | |---|---| | `PASS` | the miter was proven unsatisfiable — optimised netlist is equivalent to golden | | `FAIL` | a counterexample was found — a real miscompile | | `TABLE-FULL` | the converter exhausted its unique table (`resize not implemented yet`) | | `ASSERT` | the converter hit an assertion or segfaulted | | `TIMEOUT(conv)` | the converter hit its `-t` timeout | | `TIMEOUT(yosys)` | the whole yosys run hit `-T` | | `ERROR(rc)` | yosys aborted | | `NO-PROOF` | ran to completion but no SAT verdict in the log | `TABLE-FULL` and `ASSERT` have to be detected in the *combined* stdio stream rather than the yosys logfile: the converter is spawned through yosys's `exec`, so it writes to the inherited stderr and its diagnostics never reach `yosys -l`. Note the proof string depends on the SAT flags: with `-tempinduct` (what the templates use) yosys reports `Induction step proven: SUCCESS!`, not the more familiar `SAT proof finished - no model found: SUCCESS!`. The classifier accepts both. ## ISCAS85 results ### Baseline — no partitioning `test/run_iscas85.sh -t 2m -T 10m -o out/baseline`, yosys 0.33, converter table size `-t 300000`, 2 minute converter timeout. | Circuit | PIs | POs | Gates (golden) | Gates (bbdd) | Runtime | SAT equivalence | |---|---|---|---|---|---|---| | c17 | 5 | 2 | 12 | 13 | 0.2s | **PASS** | | c432 | 36 | 7 | – | – | 120.1s | TIMEOUT(conv) | | c499 | 41 | 32 | – | – | 120.1s | TIMEOUT(conv) | | c880 | 60 | 26 | – | – | 19.7s | TABLE-FULL | | c1355 | 41 | 32 | – | – | 120.3s | TIMEOUT(conv) | | c1908 | 33 | 25 | – | – | 120.3s | TIMEOUT(conv) | | c2670 | 233 | 140 | – | – | 2.8s | TABLE-FULL | | c3540 | 50 | 22 | – | – | 2.4s | TABLE-FULL | | c5315 | 178 | 123 | – | – | 9.0s | TABLE-FULL | | c6288 | 32 | 32 | – | – | 3.6s | TABLE-FULL | | c7552 | 207 | 108 | – | – | 6.2s | TABLE-FULL | **1 of 11 circuits passes.** Only c17, the 5-input circuit, is small enough to convert. There are two distinct failure modes, and they matter for how the fix is judged: - **`TIMEOUT(conv)`** (c432, c499, c1355, c1908 — 33 to 41 PIs): the diagram construction is simply too slow. These circuits are near the feasibility boundary and burn the full two minutes. - **`TABLE-FULL`** (c880 and everything above 50 PIs): the converter aborts *within seconds* with `[ERROR] Unique Table is full resize not implemented yet` followed by an assertion failure at `include/bbdd/include/unique_table.hpp:535`. This is a capacity wall, not a time wall — the diagrams outgrow the 300000-entry hash table long before the timeout. The second mode is the more encouraging one for this work: per-block tables hold diagrams over at most `n` variables, so they should stay far below the capacity that is being blown here. Note that the runtimes above are the *wall clock of the whole yosys run*; the converter's own time is in `out/baseline//_bbdd_time.txt`. +### n = 8 — support-bounded partitioning + +`test/run_iscas85.sh -n 8 -t 2m -T 10m -o out/n8`, same environment as the baseline. Every +`PASS` is a yosys `sat -tempinduct -verify` proof against the golden netlist, run on the +final techmapped design. + +| Circuit | PIs | POs | Gates (golden) | Gates (bbdd) | Runtime | Baseline | n = 8 | +|---|---|---|---|---|---|---|---| +| c17 | 5 | 2 | 12 | 18 | 0.3s | PASS | **PASS** | +| c432 | 36 | 7 | 282 | 504 | 1.5s | TIMEOUT(conv) | **PASS** | +| c499 | 41 | 32 | 200 | 455 | 1.3s | TIMEOUT(conv) | **PASS** | +| c880 | 60 | 26 | 481 | 733 | 4.0s | TABLE-FULL | **PASS** | +| c1355 | 41 | 32 | 888 | 436 | 2.1s | TIMEOUT(conv) | **PASS** | +| c1908 | 33 | 25 | 739 | 1128 | 4.7s | TIMEOUT(conv) | **PASS** | +| c2670 | 233 | 140 | 1040 | 1631 | 6.7s | TABLE-FULL | **PASS** | +| c3540 | 50 | 22 | 1403 | 2567 | 25.6s | TABLE-FULL | **PASS** | +| c5315 | 178 | 123 | 2413 | 3946 | 21.5s | TABLE-FULL | **PASS** | +| c6288 | 32 | 32 | – | – | 600.0s | TABLE-FULL | TIMEOUT(yosys) | +| c7552 | 207 | 108 | 3294 | 5519 | 30.9s | TABLE-FULL | **PASS** | + +**10 of 11 circuits pass, against 1 of 11 at baseline.** Both baseline failure modes are gone: +no circuit exhausts its unique table, and no conversion times out. + +Partition shape and diagram cost, from `temp/_bbdd_stats.csv`: + +| Circuit | Blocks | Support max / avg | Largest block | BBDD nodes | Max height | Peak table | +|---|---|---|---|---|---|---| +| c17 | 2 | 4 / 3.5 | 8 | 13 | 9 | 157 | +| c432 | 38 | 8 / 5.3 | 16 | 391 | 24 | 2590 | +| c499 | 53 | 8 / 4.5 | 9 | 367 | 20 | 1698 | +| c880 | 72 | 8 / 4.6 | 34 | 578 | 41 | 2281 | +| c1355 | 53 | 8 / 4.5 | 55 | 352 | 19 | 2264 | +| c1908 | 71 | 8 / 5.4 | 31 | 938 | 33 | 2991 | +| c2670 | 216 | 8 / 3.2 | 51 | 1345 | 27 | 4425 | +| c3540 | 192 | 8 / 5.6 | 49 | 2162 | 43 | 3321 | +| c5315 | 316 | 8 / 5.1 | 52 | 3380 | 29 | 4332 | +| c6288 | 236 | 8 / 5.0 | 39 | 5181 | 26 | 4506 | +| c7552 | 393 | 8 / 4.9 | 51 | 4569 | 33 | 3652 | + +**Peak table occupancy never exceeds 4506 entries**, against the 300000-entry table that six +circuits were blowing at baseline — a factor of ~65 of headroom. The capacity wall is gone +rather than pushed back, which is what per-block tables were supposed to buy. + +Two results are worth reading carefully: + +- **c6288 now fails at a different stage.** The converter handles it fine (236 blocks, 5181 + nodes, 4.5k peak table); it is the *equivalence proof* that runs out of time, grinding on + the base case of a 56373-variable miter for the full 600s. The 16x16 multiplier remains + hard, but the failure has moved from "cannot build the diagram" to "cannot verify it in ten + minutes", which are different problems. +- **c1355 comes out smaller than golden** (888 -> 436) while everything else grows 1.4-1.8x. + This is not a partitioning effect. c1355 is c499 with its XOR trees expanded into NAND + gates, so the two are the same function; after resynthesis they converge to 436 and 455 + gates respectively. The pass re-derives the function from its diagrams and so normalises + the padded encoding away. The area *growth* on the other circuits is the real cost of hard + cut points at block boundaries, as predicted. + +The unpartitioned path is unchanged: `n = 0` still gives 13 gates on c17 and passes, matching +the baseline exactly, so the `write_blif_body` buffering is fully absorbed by the following +`opt` pass. + ## Progress log | # | Step | Status | Notes | |---|------|--------|-------| | 0 | Branch + this document | done | branch `feat/support-bounded-partitioning` | | 0b | First `cmake .. && make` | done | all 4 binaries build and run | | 1a | `src/CMakeLists.txt` — narrow the `bdd` link | not started | tidy-up, not blocking | | 1b | `test/run_iscas85.sh` + baseline run | done | baseline: 1/11 pass, 4 timeout, 6 table-full | | 2 | `include/util/partition.hpp` — cone partitioner | done | validated on c17/c432/c880, n in {4,6,8,10,16} | | 3 | `cover_to_bbdd.hpp` — leaf-map generalisation | done | A/B byte-identical on add8/mul4/par12/c17 | -| 4 | bbdd submodule — `write_blif_body` | not started | separate submodule commit | -| 5 | `src/convert_bbdd.cpp` — `-n`, per-block loop, stats | not started | | -| 6 | `synth.sh` + `.ys` plumbing | not started | | -| 7 | `n` sweep + report | not started | | +| 4 | bbdd submodule — `write_blif_body` | done | emits gates without a header so blocks can share one file | +| 5 | `src/convert_bbdd.cpp` — `-n`, per-block loop, stats | done | per-block table sized from the support, stats to `temp/_bbdd_stats.csv` | +| 6 | `synth.sh` + `.ys` plumbing | done | `{{CONV_FLAGS}}` placeholder, `-n` on `synth.sh` and the runner | +| 7 | `n` sweep + report | in progress | n = 8 measured, 10/11 pass; sweep over other n still open | | 8 | `convert_bdd` / BuDDy path | not started | | ## Known risks - **c6288 is a 16×16 multiplier**, the classic worst case for BDD-based methods: its diagrams are exponential regardless of variable ordering. Expect it to stay `TIMEOUT` even partitioned — a known result, not a partitioner bug. - **Small `n` produces many tiny blocks**, and boundary nets become hard cut points that block optimisation across them. Area is expected to get worse before runtime gets better; finding the useful `n` range is itself a result. - **Cone growth is greedy and PO-order-dependent.** The worklist is seeded deterministically (POs in `foreach_co` order) so runs are reproducible. - **`Unique_table` has no resize** (`unique_table.hpp:519-521`, "resize not implemented yet"). Per-block tables can be far smaller than the current `-t 300000`; consider sizing from `n`.