lsils / mockturtle

C++ logic network library
MIT License
212 stars 140 forks source link

lut_map creates non-equivalent network #592

Closed dl575 closed 1 year ago

dl575 commented 1 year ago

I'm seeing cases where the result of running lut_map creates a network that is not equivalent with the original. Does anyone know why this is happening? Is there an issue with my original network that makes it incompatible with lut_map?

Here's is a program that reproduces this:

#include <mockturtle/networks/klut.hpp>
#include <mockturtle/io/bench_reader.hpp>

#include <mockturtle/algorithms/lut_mapper.hpp>
#include <mockturtle/algorithms/collapse_mapped.hpp>
#include <mockturtle/views/mapping_view.hpp>

#include <mockturtle/algorithms/miter.hpp>
#include <mockturtle/algorithms/equivalence_checking.hpp>

using namespace mockturtle;

int main(int argc, char* argv[])
{
    assert(argc == 2);
    const std::string filename = argv[1];

    // Read bench file
    klut_network origNetwork;
    auto const result = lorina::read_bench(filename, bench_reader(origNetwork));
    assert(result == lorina::return_code::success);

    // Create mapping view
    mapping_view<klut_network, true> preLutNetwork{origNetwork};

    // LUT mapping parameters
    lut_map_params ps = {};
    ps.cut_enumeration_ps.cut_size = 8;

    // Run LUT mapping algorithm
    lut_map<decltype(preLutNetwork), true>(preLutNetwork, ps);

    // Collapse mapped network into a k-LUT network.
    const auto lutNetworkOptional = collapse_mapped_network<klut_network>(preLutNetwork);
    // Check that optional is valid
    assert(lutNetworkOptional);
    const auto lutNetwork = *lutNetworkOptional;

    // Check network equivalence
    const auto miterNetwork = *miter<klut_network>(preLutNetwork, lutNetwork);
    const auto equivResult = equivalence_checking(miterNetwork);
    std::cout << "success = " << (equivResult && *equivResult) << "\n";

    return 0;
}

And a .bench to feed the above program:

INPUT(n2)
INPUT(n3)
OUTPUT(po0)
n0 = gnd
n1 = vdd
n4 = LUT 0xe8 (n2, n0, n1)
n5 = LUT 0x3 (n3, n4)
po0 = LUT 0x2 (n5)
aletempiac commented 1 year ago

Fixed by #593. Thank you for reporting.