Network fails equivalence check after applying the refactoring operation with direct_resynthesis twice

[KamilDre]

Hi,

I was experimenting with the refactoring operation and noticed that if I apply it twice with the direct_resynthesis resynthesis engine to the "adder" network from the EPFL Arithmetic benchmark (https://github.com/lsils/benchmarks/tree/master/arithmetic), then the resultant network is no longer equivalent to the original network. However, this is not the case if I apply the refactoring operation only once or change the resynthesis engine to exact_aig_resynthesis. Do you maybe know why this is the case?

The code below illustrates how this reproduce this issue.

#include <iostream>
#include <mockturtle/mockturtle.hpp>

using namespace std;
using namespace mockturtle;

int main() {

    string epfl_arithmetic_benchmark_dir = "/path/to/epfl/arithmetic/benchmark/";
    string ntk_name = "adder.aig";

    // load network
    aig_network ntk;
    auto const loading_res = lorina::read_aiger(epfl_arithmetic_benchmark_dir + ntk_name, aiger_reader(ntk));
    assert(loading_res == lorina::return_code::success);
    cout << "Network " << ntk_name << " has been loaded successfully" << "\n";

    // make a copy of the ntk for equivalence checking
    aig_network original_ntk = ntk;

    // refactoring parameters
    refactoring_params refactor_ps;
    refactor_ps.max_pis = 3u;
    direct_resynthesis<aig_network> refactor_resyn;

    // Apply refactoring twice
    refactoring(ntk, refactor_resyn, refactor_ps);
    ntk = cleanup_dangling(ntk);

    refactoring(ntk, refactor_resyn, refactor_ps);
    ntk = cleanup_dangling(ntk);

    // equivalence checking
    const auto miter_ntk = *miter<aig_network>(original_ntk, ntk);
    const auto equivalence_res = equivalence_checking(miter_ntk);

    /* result is an optional, which is nullopt if no solution was found */
    if (equivalence_res && *equivalence_res) {
        cout << "networks are equivalent after applying sequence\n";
    }
    else{
        cout << "networks are NOT equivalent after applying sequence\n";
    }
}

adder.zip

[hriener]

I can not reproduce your error, but multiple things do not look right:

• This line aig_network original_ntk = ntk; does not make a copy. However, you could read the benchmark twice, misuse cleanup_dangling to copy, or wait for PR #522.
• The method direct_resynthesis does only support some 3-input functions, but not all. Other resynthesis methods support more or all functions. That's likely why the problem disappears if you change the resynthesis method. Have a look at the documentation: https://mockturtle.readthedocs.io/en/latest/algorithms/node_resynthesis.html
• If you compile your example in DEBUG mode and run it, you will likely see lots of warnings informing you about logic functions that cannot be synthesized.
• I believe refactoring is mostly outdated. Use one of the resubstitution algorithms instead.

[lee30sonia]

Have you merged #521 which fixed the issue last time?

[hriener]

I tested, of course, on the latest version with the fix.

[lee30sonia]

I am closing this issue as we could not reproduce the error. Please feel free to reopen it with more information.