lut_map creates non-equivalent network
Closed this issue · 1 comments
dl575 commented
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
Fixed by #593. Thank you for reporting.