diff --git a/PARTITIONING.md b/PARTITIONING.md deleted file mode 100644 index 419d6fa..0000000 --- a/PARTITIONING.md +++ /dev/null @@ -1,276 +0,0 @@ -# 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). 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` | 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`. diff --git a/README.md b/README.md index 8195dfe..1a55e63 100644 --- a/README.md +++ b/README.md @@ -1,62 +1,122 @@ # NEM Synthesis Tool Yosys-based synthesis tool with BBDD, BDD, and MUXIG resynthesis passes specialized for NEM technology, developed as part of the Master’s thesis ‘Pass-through logic optimization for NEM technology’. --- ## 📂 Project Structure Below is an overview of the main files and directories: - `synth.sh` - main synthesis bash script, open interactive shell, generates yosys scripts and executes them - `src/` - conversion algorithms and interfaces to yosys -- `yosys/` - yosys scipt templates and modules used for the techmap pass +- `yosys/` - yosys script templates and modules used for the techmap pass - `include/` - Public headers - `bbdd/` - bbdd manipulation package used for the optimization - `mockturtle/` - mockturtle library from the EPFL Logic Synthesis Libraries - `util/` - conversion helper function to convert from the mockturtle cover network type to one of the decision diagram - `lib/` - external libraries used by mockturtle - `benchmarks/` - benchmark circuits for testing and benchmarking purposes - `liberty/` - liberty files used in the techmap pass +- `temp/`, `out/` - scratch files and default output of the synthesis runs + - `CMakeLists.txt` - Build configuration (CMake project setup) - `README.md` - This file - `LICENSE` - License file --- ## Getting Started ### Installation requirements - CMAKE version >= 3.8 - C++ compiler (tested with g++ version 15.2.1 20250808) - support C++ 17 standard - Buddy BDD library installed in /usr/local/lib - Information on how to install it can be found here https://github.com/jgcoded/BuDDy - Path to the library can also be configured in src/CMakeLists.txt + - yosys (tested with 0.33 and 0.51) + - `timeout` and GNU `time` (`/usr/bin/time`) + - python3 with `pyyaml`, `matplotlib` and `numpy` for the run summary + (optional, the synthesis runs without it) ### Build with CMake -- Build examples - ```bash git clone https://phabricator.ict.tuwien.ac.at/source/SoC_NEM_Synthesis.git +cd SoC_NEM_Synthesis git submodule update --init --recursive mkdir build && cd build cmake .. -make +make # converters in build/src/ +make docs # optional, Doxygen documentation ``` - - Build the docs + +--- + +## Usage + +### Interactive synthesis + ```bash -git clone https://phabricator.ict.tuwien.ac.at/source/SoC_NEM_Synthesis.git -mkdir build && cd build -cmake .. -make docs +./synth.sh [-nosat] [-nocleanup] [-v] [-n MAX_INPUTS] +``` + +Pick the pass (1 = bbdd, 2 = bdd, 3 = muxig), then give a Verilog file or a +directory of `.v` files, an output directory and the top module. Results land in +`//`: netlists, `stat -json` reports before and after abc, +and longest-path reports. + +| Flag | Meaning | +|---|---| +| `-nosat` | skip the SAT equivalence proof against the golden netlist | +| `-nocleanup` | keep the rendered yosys script and intermediate blif files in `temp/` | +| `-v` | show the full yosys output | +| `-n MAX_INPUTS` | partition before conversion, see below (bbdd and bdd only) | + +### Partitioning + +A decision diagram grows exponentially with its number of variables in the worst +case, so beyond roughly 20 inputs the conversion stops finishing. Both DD +converters can therefore split the circuit into blocks whose input support is at +most `n`, build one diagram per block and stitch the results into a single +netlist. + +- `-n 0` (default): no partitioning, one diagram over all primary inputs. + `n >= |PI|` gives the same result. +- `-n N`: blocks with at most `N` inputs. Diagrams are not shared across blocks, + so this costs area; it is what makes the large circuits feasible at all. +- `-g CAP`: after `-n`, merge blocks up to support `CAP`, but only when the + merged diagram is measurably smaller. Recovers much of the area `-n` loses. + +`-n 0` gives the smallest netlist wherever it finishes; the best `n` otherwise +depends on the circuit. + +### Converters + +The converters read a flattened blif and are normally called by the yosys +templates, but they can be run on their own: + +```bash +build/src/convert_bbdd [-n N] [-g CAP] [-t TABLE] [-r REPS] [-h] [-o DIR] [-i DIR] [-v] +build/src/convert_bdd [-n N] [-g CAP] [-t TABLE] [-c CACHE] [-o DIR] ``` + +| Flag | Meaning | +|---|---| +| `-n`, `-g` | partitioning, see above | +| `-t` | unique-table size (bbdd: upper bound per block; bdd: initial BuDDy node table) | +| `-o` | output directory for `_bbdd.blif` / `_bdd.blif` and a `_stats.csv` (default `temp`) | +| `-r` | bbdd: sifting repetitions | +| `-h` | bbdd: sift for height instead of node count | +| `-i` | bbdd: append the variable ordering per block to a CSV in this directory | +| `-v` | bbdd: dump the diagram as `.dot`/`.png` (unpartitioned only) | +| `-c` | bdd: BuDDy cache size |