diff --git a/PARTITIONING.md b/PARTITIONING.md
new file mode 100644
index 0000000..0554a35
--- /dev/null
+++ b/PARTITIONING.md
@@ -0,0 +1,165 @@
+# 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.
+- `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/<name>/<name>.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 |
+| `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 |
+
+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-TABLE -->
+_Baseline run in progress; table lands here._
+
+## 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 | in progress | harness done and verified on c17 (PASS) |
+| 2 | `include/util/partition.hpp` — cone partitioner | not started | |
+| 3 | `cover_to_bbdd.hpp` — leaf-map generalisation | not started | |
+| 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 | |
+| 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/test/run_iscas85.sh b/test/run_iscas85.sh
new file mode 100755
index 0000000..1bf8e68
--- /dev/null
+++ b/test/run_iscas85.sh
@@ -0,0 +1,180 @@
+#!/bin/bash
+# Non-interactive ISCAS85 regression runner for the DD synthesis passes.
+#
+# Renders one of the yosys script templates for every ISCAS85 circuit, runs it
+# with the SAT equivalence check enabled, and reports for each circuit whether
+# the optimised netlist was proven equivalent to the golden one.
+#
+# Usage: test/run_iscas85.sh [-n MAX_INPUTS] [-t TIMEOUT] [-o OUT_DIR]
+#                           [-s SCRIPT] [-k] [circuit ...]
+#
+#   -n  max inputs per partition block, forwarded to the converter as -n
+#       (0 or unset = no partitioning, i.e. the original behaviour)
+#   -t  timeout for the converter call itself       (default 2m)
+#   -T  timeout for the whole yosys run             (default 10m)
+#   -o  output directory                            (default out/iscas85)
+#   -s  yosys script template   (default yosys/bbdd_synth_muxxor.ys)
+#   -k  keep the rendered .ys and intermediate blif files
+#
+# With no circuit names all 11 ISCAS85 benchmarks are run.
+
+set -u
+
+BENCH_DIR="benchmarks/ISCAS85"
+SCRIPT="yosys/bbdd_synth_muxxor.ys"
+OUT_DIR="out/iscas85"
+TEMP_DIR="temp"
+LIBERTY_FILE="liberty/nem_thesis.lib"
+TECHMAP_BBDD="yosys/techmap_bbdd.v"
+TIMEOUT="2m"
+YOSYS_TIMEOUT="10m"
+MAX_INPUTS=0
+KEEP=false
+
+while getopts "n:t:T:o:s:k" opt; do
+  case "$opt" in
+    n) MAX_INPUTS="$OPTARG" ;;
+    t) TIMEOUT="$OPTARG" ;;
+    T) YOSYS_TIMEOUT="$OPTARG" ;;
+    o) OUT_DIR="$OPTARG" ;;
+    s) SCRIPT="$OPTARG" ;;
+    k) KEEP=true ;;
+    *) sed -n '2,20p' "$0"; exit 1 ;;
+  esac
+done
+shift $((OPTIND - 1))
+
+if [ ! -f "$SCRIPT" ]; then
+  echo "[ERROR] script template not found: $SCRIPT" >&2
+  exit 1
+fi
+if [ ! -x ./build/src/convert_bbdd ]; then
+  echo "[ERROR] ./build/src/convert_bbdd missing - build first:" >&2
+  echo "        mkdir -p build && cd build && cmake .. && make" >&2
+  exit 1
+fi
+
+# Circuits: either those named on the command line, or all of ISCAS85.
+if [ $# -gt 0 ]; then
+  CIRCUITS=("$@")
+else
+  CIRCUITS=()
+  for d in "$BENCH_DIR"/*/; do
+    CIRCUITS+=("$(basename "${d%/}")")
+  done
+fi
+
+# yosys 0.40 added `flatten -noscopeinfo`; on older yosys the flag is a hard
+# error, and plain `flatten` is equivalent there because no $scopeinfo cells
+# are ever produced. Detect once and patch the rendered script if needed.
+STRIP_NOSCOPEINFO=false
+if ! yosys -qp "help flatten" 2>/dev/null | grep -q -- "-noscopeinfo"; then
+  STRIP_NOSCOPEINFO=true
+  echo "[INFO] yosys $(yosys -V 2>/dev/null | awk '{print $2}') has no 'flatten -noscopeinfo'; stripping the flag"
+fi
+
+safe_path() { printf '%s\n' "$1" | sed 's/[&/\]/\\&/g'; }
+
+mkdir -p "$TEMP_DIR" "$OUT_DIR"
+
+RESULTS=()
+
+for name in "${CIRCUITS[@]}"; do
+  src="$BENCH_DIR/$name/$name.v"
+  if [ ! -f "$src" ]; then
+    echo "[WARN] no such benchmark: $src" >&2
+    continue
+  fi
+
+  mkdir -p "$OUT_DIR/$name"
+  rendered="$TEMP_DIR/${name}_synth.ys"
+  log="$OUT_DIR/$name/yosys.log"
+
+  conv_flags="-t 300000"
+  if [ "$MAX_INPUTS" -gt 0 ] 2>/dev/null; then
+    conv_flags="$conv_flags -n $MAX_INPUTS"
+  fi
+
+  sed -e "s/{{VERILOG_FILE}}/$(safe_path "$src")/g" \
+      -e "s/{{TEMP_DIR}}/$(safe_path "$TEMP_DIR")/g" \
+      -e "s/{{TOP_MODULE}}/$name/g" \
+      -e "s/{{BASE_NAME}}/$name/g" \
+      -e "s/{{TECHMAP_BBDD}}/$(safe_path "$TECHMAP_BBDD")/g" \
+      -e "s/{{LIBERTY_FILE}}/$(safe_path "$LIBERTY_FILE")/g" \
+      -e "s/{{OUT_DIR}}/$(safe_path "$OUT_DIR")/g" \
+      -e "s/{{TIMEOUT}}/$TIMEOUT/g" \
+      -e "s/{{SAT}}//g" \
+      "$SCRIPT" > "$rendered"
+
+  # forward -n to the converter invocation inside the rendered script
+  sed -i "s#\(convert_bbdd\|convert_bdd\) -t 300000#\1 $conv_flags#" "$rendered"
+  if $STRIP_NOSCOPEINFO; then
+    sed -i 's/flatten -noscopeinfo/flatten/' "$rendered"
+  fi
+
+  printf '%-8s ' "$name"
+  start=$(date +%s.%N)
+  timeout "$YOSYS_TIMEOUT" yosys -ql "$log" "$rendered"
+  rc=$?
+  end=$(date +%s.%N)
+  elapsed=$(awk -v a="$start" -v b="$end" 'BEGIN{printf "%.1f", b-a}')
+
+  # Classify. The SAT step is `sat -prove-asserts -tempinduct ... equal`.
+  # With -tempinduct yosys reports "Induction step proven: SUCCESS!"; without
+  # it, "SAT proof finished - no model found: SUCCESS!". Accept either.
+  if [ $rc -eq 124 ]; then
+    verdict="TIMEOUT(yosys)"
+  elif grep -qE "Induction step failed|model found: FAIL|Assert failed|induction length [0-9]+ failed" "$log" 2>/dev/null; then
+    verdict="FAIL"
+  elif grep -qE "Induction step proven: SUCCESS|no model found: SUCCESS" "$log" 2>/dev/null; then
+    verdict="PASS"
+  elif grep -qE "did not finish in time|Command failed: timeout|ERROR: Can't open input file" "$log" 2>/dev/null; then
+    verdict="TIMEOUT(conv)"
+  elif [ $rc -ne 0 ]; then
+    verdict="ERROR($rc)"
+  else
+    verdict="NO-PROOF"
+  fi
+
+  # Stats straight out of the blif the flow already writes.
+  blif="$TEMP_DIR/$name.blif"
+  pi=$(awk '/^\.inputs/{print NF-1; exit}' "$blif" 2>/dev/null)
+  po=$(awk '/^\.outputs/{print NF-1; exit}' "$blif" 2>/dev/null)
+  gold=$(python3 -c "
+import json,sys
+try:
+  d=json.load(open('$OUT_DIR/$name/${name}_golden.json'))
+  m=list(d['modules'].values())[0]
+  print(sum(m['num_cells_by_type'].values()))
+except Exception: print('-')" 2>/dev/null)
+  opt=$(python3 -c "
+import json,sys
+try:
+  d=json.load(open('$OUT_DIR/$name/${name}_bbdd.json'))
+  m=list(d['modules'].values())[0]
+  print(sum(m['num_cells_by_type'].values()))
+except Exception: print('-')" 2>/dev/null)
+
+  echo "PI=${pi:--} PO=${po:--} gates:${gold:--}->${opt:--} ${elapsed}s  $verdict"
+  RESULTS+=("$name|${pi:--}|${po:--}|${gold:--}|${opt:--}|${elapsed}|$verdict")
+
+  if ! $KEEP; then
+    rm -f "$rendered" "$TEMP_DIR/${name}_bbdd.blif" "$TEMP_DIR/${name}_bdd.blif"
+  fi
+done
+
+n_label=$([ "$MAX_INPUTS" -gt 0 ] 2>/dev/null && echo "$MAX_INPUTS" || echo "off")
+
+echo
+echo "| Circuit | PIs | POs | n | Gates (golden) | Gates (bbdd) | Runtime | SAT equivalence |"
+echo "|---|---|---|---|---|---|---|---|"
+for r in "${RESULTS[@]}"; do
+  IFS='|' read -r c pi po g o t v <<< "$r"
+  echo "| $c | $pi | $po | $n_label | $g | $o | ${t}s | $v |"
+done
+
+# exit non-zero if anything actually miscompiled (timeouts are not failures here)
+for r in "${RESULTS[@]}"; do
+  case "$r" in *"|FAIL") exit 1 ;; esac
+done
+exit 0