diff --git a/PARTITIONING.md b/PARTITIONING.md index 0554a35..1452837 100644 --- a/PARTITIONING.md +++ b/PARTITIONING.md @@ -1,165 +1,206 @@ # 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//.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 run in progress; table lands here._ +### 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`. ## 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 | | +| 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 | | | 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/include/util/cover_to_bbdd.hpp b/include/util/cover_to_bbdd.hpp index 8bc8252..7506652 100644 --- a/include/util/cover_to_bbdd.hpp +++ b/include/util/cover_to_bbdd.hpp @@ -1,164 +1,288 @@ // Copyright 2025 Oliver Theimer #pragma once #include #include +#include +#include #include "../bbdd/include/bbdd.hpp" #include "../bbdd/include/bbdd_node.hpp" #include "../bbdd/include/unique_table.hpp" #include "mockturtle/traits.hpp" +#include "partition.hpp" #include "util.hpp" #define LEFT_CHILD(node) node.children[0].index #define RIGHT_CHILD(node) node.children[1].index #define CUBE(node) ntk._storage->data.covers[node.data[1].h1] int nodes_visited; using namespace mockturtle; +/** + * @brief maps network nodes to the bbdd variables of a single block + * + * The bbdd chain variable ordering addresses its variables through + * `POS(in, cvo)`, which is a plain `in % cvo->size()`, so the variable ids of + * a block have to be the contiguous range `2 .. k+1` for that modulo to be a + * bijection. Network node indices of a block are arbitrary, hence this + * indirection: `local[n]` is the variable id of node `n`, or 0 when `n` is not + * a leaf of the block. + */ +struct leaf_map_t { + /// node index -> bbdd variable id in 2..k+1, 0 when not a leaf + std::vector local; + /// bbdd variable id - 2 -> node index + std::vector nodes; + + uint32_t operator[](uint64_t n) const { return local[n]; } + size_t size() const { return nodes.size(); } +}; + +/** + * @brief builds the leaf map of a block + * + * @param network_size number of nodes in the network the block came from + * @param leaves leaves of the block, at most one bbdd variable each + * @return leaf map assigning the contiguous ids 2..k+1 to the leaves + */ +inline leaf_map_t make_leaf_map(size_t network_size, + std::vector const &leaves) { + leaf_map_t map; + map.local.assign(network_size, 0); + map.nodes.reserve(leaves.size()); + for (uint64_t const &l : leaves) { + map.local[l] = static_cast(map.nodes.size()) + 2; + map.nodes.push_back(l); + } + return map; +} + /** * @brief recursively creates a bbdd based on the given network * + * The recursion stops at the leaves of the block, which are the primary inputs + * for an unpartitioned run and additionally the boundary nets of the block + * otherwise. Leaves become bbdd variables, everything above them is built as + * bbdd nodes. + * * @tparam Ntk template for which network type is used * @param table unique table in which the bbdd should be stored in * @param ntk input network data structure that should be converted + * @param leaf_map maps the leaves of the block to their bbdd variable ids * @param node_i starting node from which onwards the bbdd should be created, * will be used for the recursion * @param output_completed statistics that are used in the recursion to properly * show the progress bar + * @param show_progress whether the progress bar should be drawn * @return root node of the created bbdd */ template static bbdd_node_t *create_bbdd(Unique_table *table, Ntk &ntk, - const auto &node_i, int output_completed) { + leaf_map_t const &leaf_map, const auto &node_i, + int output_completed, bool show_progress) { static_assert(has_is_ci_v, "Ntk does not implement the is_ci method"); const auto &node = ntk._storage->nodes[node_i]; bbdd_node_t *f, *g, *result; + + // constants are shared between every block and are always in the table + if (node_i == 1 || node_i == 0) { + return table->get_node_p(node_i); + } + + // a leaf of the block: a primary input, or a boundary net that another + // block drives. Either way it terminates the recursion and becomes a + // variable of this block's bbdd. + if (leaf_map[node_i]) { + assert(node_i < pow(2, 31)); + return table->insert_node({{leaf_map[node_i], INT_MAX}, 0, 1}); + } + bbdd_op_t op = Util::cube_to_bbdd_op(CUBE(node)); if (ntk.visited(node_i)) { return table->get_node_p(ntk.visited(node_i)); } #ifdef DEBUG_COVER printf("[INFO] CREATE: node %d with op %s\n", node_i, bbdd_op_s[op].c_str()); #endif - if (node.children.size() != 2 && node.children.size() != 1) { - if (node_i == 1 || node_i == 0) { - return table->get_node_p(node_i); - } -#ifdef DEBUG_COVER - std::cout << node_i << ": " << node.children.size() << " with " - << bbdd_op_s[op].c_str() << "\n"; -#endif - assert(ntk.is_ci(node_i)); - assert(node_i < pow(2, 31)); - assert(node_i - 2 < ntk._storage->inputs.size()); - return table->insert_node({{(node_index_t)node_i, INT_MAX}, 0, 1}); - } - assert(node.children.size() == 2 || node.children.size() == 1); + // a node that is neither a constant nor a leaf has to be a gate of the block + assert((node.children.size() == 2 || node.children.size() == 1) && + "node is not a leaf of the block but has no usable fanin"); + // all the logic gates except buf and inv if (node.children.size() == 2) { node_index_t f_i = LEFT_CHILD(node), g_i = RIGHT_CHILD(node); - if (ntk.is_ci(LEFT_CHILD(node)) && ntk.is_ci(RIGHT_CHILD(node))) { - result = base_case_two_inputs(table, f_i, g_i, op); + if (leaf_map[f_i] && leaf_map[g_i]) { + result = base_case_two_inputs(table, leaf_map[f_i], leaf_map[g_i], op); #ifdef DEBUG_COVER printf("[INFO] CREATE: two input case %d: %d %s %d\n", result->index, f_i, bbdd_op_s[op].c_str(), g_i); #endif return result; } - f = create_bbdd(table, ntk, LEFT_CHILD(node), output_completed); - g = create_bbdd(table, ntk, RIGHT_CHILD(node), output_completed); + f = create_bbdd(table, ntk, leaf_map, LEFT_CHILD(node), output_completed, + show_progress); + g = create_bbdd(table, ntk, leaf_map, RIGHT_CHILD(node), output_completed, + show_progress); result = merge_bbdds(table, f, g, op); #ifdef DEBUG_COVER std::cout << "[INFO] CREATE: merging " << result->index << ": " << f->index << " " << bbdd_op_s[op] << " " << g->index << "\n"; dump_node(g); #endif ntk.set_visited(node_i, result->index); - Util::show_progress_bar( - {{"Output", {output_completed, ntk._storage->outputs.size()}}, - {"Nodes", {++nodes_visited, ntk._storage->nodes.size()}}}, - 50); + if (show_progress) { + Util::show_progress_bar( + {{"Output", {output_completed, ntk._storage->outputs.size()}}, + {"Nodes", {++nodes_visited, ntk._storage->nodes.size()}}}, + 50); + } return result; } else { // buf and inverter nodes - f = create_bbdd(table, ntk, LEFT_CHILD(node), output_completed); + f = create_bbdd(table, ntk, leaf_map, LEFT_CHILD(node), output_completed, + show_progress); if (op == bbdd_inv) { result = negate_recursive(table, f); ntk.set_visited(node_i, result->index); + if (show_progress) { + Util::show_progress_bar( + {{"Output", {output_completed, ntk._storage->outputs.size()}}, + {"Nodes", {++nodes_visited, ntk._storage->nodes.size()}}}, + 50); + } + return result; + } + ntk.set_visited(node_i, f->index); + if (show_progress) { Util::show_progress_bar( {{"Output", {output_completed, ntk._storage->outputs.size()}}, {"Nodes", {++nodes_visited, ntk._storage->nodes.size()}}}, 50); - return result; } - ntk.set_visited(node_i, f->index); - Util::show_progress_bar( - {{"Output", {output_completed, ntk._storage->outputs.size()}}, - {"Nodes", {++nodes_visited, ntk._storage->nodes.size()}}}, - 50); return f; } } +/** + * @brief converts one block of a partition into a bbdd forest + * + * Builds one bbdd per root of the block over the block's leaves and registers + * it in the table under the matching name. The caller owns the table: it has + * to be initialised with a chain variable ordering over the leaf ids of this + * block, and it has to be freed and reinitialised between blocks. + * + * The visited flags of the network are used to memoize nodes to table indices. + * They therefore have to be cleared by the caller between two blocks, because + * indices of a previous table do not mean anything in the current one. + * + * @tparam Ntk template of network type that should be used + * @param table unique table in which the data structure should be stored + * @param ntk network that holds the block + * @param block block that should be converted + * @param leaf_map maps the leaves of the block to their bbdd variable ids + * @param root_names name of each root of the block, in the same order + * @param use_height if true the height of the bbdd is used as the target + * function for the sifting algorithm, otherwise the number of nodes is used + * @param sifting_repetitions how often sifting should be repeated at the end + * @param sift_height_limit skip sifting when the forest is taller than this, + * 0 disables the limit + * @param show_progress whether the per-node progress bar should be drawn + */ +template +void block_to_bbdd(Unique_table *table, Ntk &ntk, block_t const &block, + leaf_map_t const &leaf_map, + std::vector const &root_names, bool use_height, + int sifting_repetitions, uint32_t sift_height_limit = 30, + bool show_progress = false) { + assert(block.roots.size() == root_names.size()); + + for (size_t i = 0; i < block.roots.size(); i++) { + bbdd_node_t *output = add_ref(create_bbdd(table, ntk, leaf_map, + block.roots[i], static_cast(i), + show_progress)); + table->add_output(root_names[i], output); + } + + for (int i = 0; i < sifting_repetitions; i++) { + if (sift_height_limit == 0 || table->get_total_height() < sift_height_limit) { + if (use_height) { + sift(table, &Unique_table::get_total_height, table); + } else { + sift(table, &Unique_table::get_total_number_nodes, table); + } + } + } +} + /** * @brief main conversion function that should be used as an interface, it * interact with the recursive function, instantiates the progress bar and * registers output in the unique table * + * Converts the whole network as a single block, which is the unpartitioned + * behaviour: every primary input is a bbdd variable and every primary output + * gets its own bbdd. + * * @tparam Ntk template of network type that should be used * @param table unique table in which the data structure should be stores * @param ntk data strucutre that stores the input network type which should be * converted * @param use_height if true the height of the bbdd is used as the target * function for the sifting algorithm, otherwise the number of nodes i used * @param sifting_repetitions indicates how often the sifting algorithm should be repeated at the end of the conversion */ template void cover_to_bbdd(Unique_table *table, Ntk &ntk, bool use_height, int sifting_repetitions) { static_assert(has_foreach_co_v, "Ntk does not implement the foreach_pi method"); static_assert(has_get_node_v, "Ntk does not implement the get_node method"); static_assert(has_set_visited_v, "Ntk does not implement the set_visited method"); static_assert(has_visited_v, "Ntk does not implement the set_visited method"); int index = ntk._storage->inputs.size() + 2; int output_completed = 0; nodes_visited = 0; + + leaf_map_t leaf_map = make_leaf_map( + ntk._storage->nodes.size(), + std::vector(std::begin(ntk._storage->inputs), + std::end(ntk._storage->inputs))); + Util::show_progress_bar( {{"Output", {output_completed, ntk._storage->outputs.size()}}, {"Nodes", {++nodes_visited, ntk._storage->nodes.size()}}}, 50); - ntk.foreach_co([ntk, &table, &index, &output_completed, - sifting_repetitions](const auto &node_i) { + ntk.foreach_co([&ntk, &table, &index, &output_completed, &leaf_map]( + const auto &node_i) { const auto &node = ntk.get_node(node_i); - auto &n = ntk._storage->nodes[node_i]; #ifdef DEBUG_COVER + auto &n = ntk._storage->nodes[node_i]; std::cout << "output with node_i: " << node_i << " and n->index: " << " : " << n.children.size() << "\n"; #endif bbdd_node_t *output = - add_ref(create_bbdd(table, ntk, node, output_completed)); + add_ref(create_bbdd(table, ntk, leaf_map, node, output_completed, true)); Util::show_progress_bar( {{"Output", {++output_completed, ntk._storage->outputs.size()}}, {"Nodes", {++nodes_visited, ntk._storage->nodes.size()}}}, 50); table->add_output(ntk.get_signal_name(index), output); index++; }); for (int i = 0; i < sifting_repetitions; i++) { if (table->get_total_height() < 30) { if (use_height) { sift(table, &Unique_table::get_total_height, table); } else { sift(table, &Unique_table::get_total_number_nodes, table); } } } } diff --git a/test/run_iscas85.sh b/test/run_iscas85.sh index 1bf8e68..0ebf0a2 100755 --- a/test/run_iscas85.sh +++ b/test/run_iscas85.sh @@ -1,180 +1,191 @@ #!/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 + # yosys -l only captures what yosys itself prints; the converter is spawned + # through `exec` and writes to the inherited stderr, so its diagnostics + # (e.g. "Unique Table is full") only show up in the combined stdio stream. + stdio="$OUT_DIR/$name/stdio.log" + printf '%-8s ' "$name" start=$(date +%s.%N) - timeout "$YOSYS_TIMEOUT" yosys -ql "$log" "$rendered" + timeout "$YOSYS_TIMEOUT" yosys -ql "$log" "$rendered" > "$stdio" 2>&1 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 + elif grep -qE "Induction step failed|model found: FAIL|Assert failed|induction length [0-9]+ failed" "$log" "$stdio" 2>/dev/null; then verdict="FAIL" - elif grep -qE "Induction step proven: SUCCESS|no model found: SUCCESS" "$log" 2>/dev/null; then + elif grep -qE "Induction step proven: SUCCESS|no model found: SUCCESS" "$log" "$stdio" 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 + elif grep -q "Unique Table is full" "$log" "$stdio" 2>/dev/null; then + # the converter exhausted its hash table: a capacity problem, not a + # timeout, and it aborts within seconds rather than running long + verdict="TABLE-FULL" + elif grep -qE "Assertion .* failed|Segmentation fault" "$log" "$stdio" 2>/dev/null; then + verdict="ASSERT" + elif grep -qE "did not finish in time|Command failed: timeout|ERROR: Can't open input file" "$log" "$stdio" 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