feat: convert one bbdd per partition block and size the table from the support
Adds -n to convert_bbdd: the cover network is split into support-bounded
blocks, each block gets its own unique table, chain variable ordering and
sifting run, and the per-block netlists are written into a single .blif.
-n 0 keeps the previous behaviour of one diagram per primary output over all
primary inputs.
Naming is done up front, before any block is written, because a block may
use the root of a later block as one of its leaves. A root that drives a
primary output is named after it so the common case needs no buffer; the
remaining outputs (a primary input or constant wired straight through, or a
second output on the same driver) get an explicit one at the end.
Each block allocates 8 * 2^k entries with a 16k floor rather than the full
-t size, because init_table zeroes everything it allocates and clearing a
300000-entry table a few thousand times costs far more than building the
diagrams. The factor is empirical: peak occupancy is driven by the
intermediate nodes that merging and sifting create, not by the size of the
reduced diagram, and measured peaks on c432/c880 run to 86.5k at k = 16.
Blocks are freed between iterations, and ntk.clear_visited() drops the
memoized indices of the table that was just freed.
Also writes temp/<circuit>_bbdd_stats.csv with the partition shape and the
peak table occupancy, so a run that comes close to the capacity is visible
instead of only showing up as an abort.
Measured on ISCAS85 at n = 8, each verified with yosys sat -tempinduct
-verify against the golden netlist: 10 of 11 circuits prove equivalent,
against 1 of 11 unpartitioned. Peak table occupancy never exceeds 4506
entries where six circuits previously exhausted a 300000-entry table, so the
capacity wall is removed rather than deferred. c6288 still fails, but now on
the equivalence proof rather than the conversion.
Requires the bbdd submodule fix that names every node after its own wire;
without it a node shared by two outputs is emitted as an undriven net.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_014JTKS4uaDDZejKn7pE8vjc