lsils / mockturtle

C++ logic network library
MIT License
202 stars 136 forks source link

NEQ bug in new LUT mapper #596

Closed lee30sonia closed 1 year ago

lee30sonia commented 1 year ago

Describe the bug Mapping an MIG into k-LUT (k=5) and converting back to MIG becomes non-equivalent.

To Reproduce (latest commit) code:

int main()
{
  std::string benchmark = "debug_minimized.v";
  mig_network _ntk;
  if ( lorina::read_verilog( benchmark, verilog_reader( _ntk ) ) != lorina::return_code::success )
  {
    std::cerr << "Cannot read " << benchmark << "\n";
    return -1;
  }

  using Ntk = mig_network;
  mig_network const copy = _ntk.clone();

  lut_map_params mps;
  mps.cut_enumeration_ps.cut_size = 5;
  mapping_view<Ntk> mapped{ _ntk };
  lut_map( mapped, mps );
  const auto klut = *collapse_mapped_network<klut_network>( mapped );
  write_blif( klut, "klut.blif" );

  _ntk = convert_klut_to_graph<Ntk>( klut );
  std::cout << *equivalence_checking( *miter<mig_network>( copy, _ntk ) ) << "\n";
  return 0;
}

minimized input MIG (debug_minimized.v):

module top( x0 , x1 , x2 , x3 , x4 , x5 , x6 , x7 , x8 , x9 , x10 , x11 , y0 );
  input x0 , x1 , x2 , x3 , x4 , x5 , x6 , x7 , x8 , x9 , x10 , x11 ;
  output y0 ;
  wire n13 , n14 , n15 , n16 , n17 , n18 , n19 , n20 , n21 , n22 , n23 , n24 , n25 , n26 , n27 ;
  assign n13 = ~x6 & x7 ;
  assign n14 = x11 & n13 ;
  assign n15 = x3 | x4 ;
  assign n16 = x0 & x9 ;
  assign n17 = x5 & ~n13 ;
  assign n18 = x10 & ~n17 ;
  assign n19 = x0 & n18 ;
  assign n20 = x8 & ~n19 ;
  assign n21 = ~n16 & n20 ;
  assign n22 = ~x1 & n21 ;
  assign n23 = n15 & ~n22 ;
  assign n24 = x0 & ~x9 ;
  assign n25 = n23 & ~n24 ;
  assign n26 = n14 | n25 ;
  assign n27 = ~x2 & n26 ;
  assign y0 = n27 ;
endmodule

The intermediate k-LUT write-out (klut.blif):

.model top
.inputs pi2 pi3 pi4 pi5 pi6 pi7 pi8 pi9 pi10 pi11 pi12 pi13 
.outputs po0 
.names new_n0
0
.names new_n1
1
.names new_n0 new_n14
1 1
.names new_n14 po0
1 1
.end

The eventual MIG output has PO connected to constant 0.

Environment

Check list

aletempiac commented 1 year ago

Bug fixed in #597