diff --git a/src/opt/eslim/eslimCirMan.cpp b/src/opt/eslim/eslimCirMan.cpp index 5b0fa6a785..dd9fa1068d 100644 --- a/src/opt/eslim/eslimCirMan.cpp +++ b/src/opt/eslim/eslimCirMan.cpp @@ -967,7 +967,8 @@ namespace eSLIM { for (int i = 1; i <= getNofPos(); i++) { insertSorted(nodes[nodes.size() - i].get(), nodes_aux, replacement, out_map, invec); } - assert (nodes_aux.size() <= nodes.size()); + // Account for replacement growth; primary outputs are not yet in nodes_aux. + assert (nodes_aux.size() <= nodes.size() - size_diff - getNofPos()); int current_depth = 0; for (int i = 0; i < getNofPos(); i++) { int po_id = getNofObjs() - getNofPos() + i; diff --git a/test/CMakeLists.txt b/test/CMakeLists.txt index 7fb1208539..db3263cbf1 100644 --- a/test/CMakeLists.txt +++ b/test/CMakeLists.txt @@ -1,5 +1,10 @@ add_subdirectory(gia) +add_executable(eslim_replace eslim_replace.cpp) +target_link_libraries(eslim_replace PRIVATE libabc) +add_test(NAME eslim_replace COMMAND eslim_replace) +set_tests_properties(eslim_replace PROPERTIES SKIP_RETURN_CODE 77) + # The eSLIM2 oracles are local, uncommitted test assets. A fresh checkout must # still configure and build when those files are absent. set(ESLIM2_LOCAL_TEST_NAMES small_exact small_timing small_order area_refinement windows instances) diff --git a/test/eslim_replace.cpp b/test/eslim_replace.cpp new file mode 100644 index 0000000000..4704196ff3 --- /dev/null +++ b/test/eslim_replace.cpp @@ -0,0 +1,112 @@ +// Regression for replacing an eSLIM window with a larger equivalent circuit. +// Build both libabc and the test with assertions enabled; NDEBUG builds skip it. +// Run from the repository root: +// cmake -S . -B build -DCMAKE_BUILD_TYPE=Debug +// cmake --build build --config Debug --target eslim_replace +// ctest --test-dir build -C Debug -R '^eslim_replace$' --output-on-failure +#include + +#ifdef NDEBUG +int main() { + std::puts("SKIP: eslim_replace requires assertions in libabc and the test; use a Debug build."); + return 77; +} +#else + +#include +#include +#include +#include + +#include "opt/eslim/eslimCirMan.hpp" +#include "opt/eslim/subcircuit.hpp" + +ABC_NAMESPACE_USING_NAMESPACE + +// Every gate is reachable, and the output is a & b for any positive size. +static eSLIM::eSLIMCirMan makeCircuit(int gates) { + eSLIM::eSLIMCirMan circuit(gates + 4); + int a = circuit.addPi(); + int b = circuit.addPi(); + int output = circuit.addNode({a, b}, 8); + for (int i = 1; i < gates; ++i) + output = circuit.addNode({output, i % 2 ? a : b}, 8); + circuit.addPo(output, false); + return circuit; +} + +static void checkCircuit(const eSLIM::eSLIMCirMan& circuit, int gates) { + assert(circuit.getNofPis() == 2); + assert(circuit.getNofPos() == 1); + assert(circuit.getNofGates() == gates); + assert(circuit.getNofObjs() == gates + 4); + assert(circuit.getDepth() == gates + 1); + + std::set objects; + std::set ids; + for (int i = 0; i < circuit.getNofObjs(); ++i) + objects.insert(&circuit.getObj(i)); + for (int i = 0; i < circuit.getNofObjs(); ++i) { + const auto& node = circuit.getObj(i); + assert(node.node_id == i); + if (i > 0) { + bool inserted = ids.insert(node.getId()).second; + assert(inserted); + } + int depth = 0; + for (auto fanin : node.fanins) { + assert(objects.count(fanin) == 1); + assert(fanin->node_id >= 0 && fanin->node_id < i); + assert(fanin->fanouts.count(const_cast(&node)) == 1); + depth = std::max(depth, fanin->depth + 1); + } + assert(node.depth == depth); + for (auto fanout : node.fanouts) { + assert(objects.count(fanout) == 1); + assert(std::find(fanout->fanins.begin(), fanout->fanins.end(), &node) != fanout->fanins.end()); + } + if (circuit.isGate(i)) + assert(!node.fanouts.empty()); + } + + // Exhaustively check equivalence to a & b, including the PO truth table. + for (unsigned input = 0; input < 4; ++input) { + std::vector values(circuit.getNofObjs(), 0); + values[1] = input & 1; + values[2] = (input >> 1) & 1; + for (int i = 3; i < circuit.getNofObjs(); ++i) { + const auto& node = circuit.getObj(i); + unsigned row = 0; + for (unsigned j = 0; j < node.fanins.size(); ++j) + row |= values[node.fanins[j]->node_id] << j; + values[i] = (node.tt >> row) & 1; + } + assert(values.back() == (input == 3)); + } +} + +int main() { + auto circuit = makeCircuit(1); + checkCircuit(circuit, 1); + // The first replacement grows by two gates: before appending the PO, + // nodes_aux contains six objects, while the original has only five. + // Also exercise equal size, growth by one, and shrinking on the same manager. + for (int gates : {3, 3, 4, 1}) { + { + auto replacement = makeCircuit(gates); + checkCircuit(replacement, gates); + std::vector nodes; + for (int i = 3; i < circuit.getNofObjs() - 1; ++i) + nodes.push_back(i); + circuit.incrementTraversalId(); + auto subcir = eSLIM::Subcircuit::getSubcircuitBare(circuit, nodes.begin(), nodes.end()); + assert((subcir.inputs == std::vector{1, 2})); + assert(subcir.outputs.size() == 1); + circuit.replace(replacement, subcir); + } + // Check ownership and links after the replacement manager is destroyed. + checkCircuit(circuit, gates); + } + std::puts("PASS: eSLIM replacement counts, graph consistency and exhaustive equivalence"); +} +#endif