Incorrect level update in `rewrite` leads to depth violation and assertion failure when `preserve_depth = true`

[jfkey]

Summary

When running rewrite with preserve_depth = true, the logic for updating node levels is insufficient. This results in two issues:

1. Depth Violation: The final network depth increases, contradicting the preserve_depth constraint.
2. Assertion Failure: The process crashes with Assertion ntk.level( ntk.get_node( new_f ) ) <= required[n] failed.

Root Cause Analysis

The issue stems from how node levels are updated during the rewrite process. Currently, mockturtle only updates the level of the current node based on its immediate fanins after subgraph replacement. It does not perform a forward traversal to propagate level updates to the affected fanout cone.

Problematic Code in mockturtle/algorithms/rewrite.hpp:
Link to code

/* update level for node */
if constexpr ( has_level_v<Ntk> )
{
  if ( ps.preserve_depth )
  {
    uint32_t level = 0;
    ntk.foreach_fanin( n, [&]( auto const& f ) {
      level = std::max( level, ntk.level( ntk.get_node( f ) ) );
    } );
    ntk.set_level( n, level + 1 ); // Only updates the current node locally
    best_level = level + 1;
  }
}

Since subgraph replacement potentially affects the levels of the fanins or requires re-evaluating the path delays, a local update is often insufficient.

Comparison with ABC:
In ABC, the node levels are correctly updated by propagating the changes (or ensuring the topological order is respected/re-calculated).
Reference: abcAig.c#L1063

Symptoms & Reproduction

Case 1: Logic Depth Increases

Even with ps.preserve_depth = true, the depth of the resulting network increases.

• Benchmark: experiments/benchmarks/div.aig
• Script: aig_rw.cpp (provided below)
• Observed Output:

  [AIG]     PIs = 128  POs = 128  Gates = 57247  Depth = 4372
  [AIG opt] PIs = 128  POs = 128  Gates = 41258  Depth = 4373  <-- Depth increased
  

Case 2: Assertion Failure

The rewrite process crashes due to an assertion failure regarding required levels.

• Error Message:

  rw_mig: .../rewrite.hpp:327: ... Assertion `ntk.level( ntk.get_node( new_f ) ) <= required[n]' failed.
  

• Benchmarks triggering this:
  • AIG Rewrite (aig_rw.cpp): DSP.aig, leon3mp.aig, RISC.aig, wb_conmax.aig
  • MIG Rewrite (mig_rw.cpp): c432.aig, c499.aig, c880.aig, c1908.aig, c3540.aig, ethernet.aig, i2c.aig, multiplier.aig, simple_spi.aig, sin.aig, sqrt.aig, systemcdes.aig, voter.aig

Reproduction Scripts

1. aig_rw.cpp

#include <mockturtle/algorithms/cleanup.hpp>
#include <mockturtle/algorithms/node_resynthesis/xag_npn.hpp>
#include <mockturtle/algorithms/rewrite.hpp>
#include <mockturtle/io/aiger_reader.hpp>
#include <mockturtle/io/write_aiger.hpp>
#include <mockturtle/networks/aig.hpp>
#include <mockturtle/utils/tech_library.hpp>
#include <mockturtle/views/depth_view.hpp>
#include <lorina/aiger.hpp>
#include <chrono>
#include <iostream>

using namespace mockturtle;

int main( int argc, char* argv[] )
{
  if ( argc != 2 )
  {
    std::cout << "Usage: " << argv[0] << " <aiger_file>\n";
    return 1;
  }

  /* Read AIG */
  aig_network aig;
  if ( lorina::read_aiger( argv[1], aiger_reader( aig ) ) != lorina::return_code::success )
  {
    std::cout << "Error: Cannot read AIG file\n";
    return 1;
  }

  /* Print original AIG statistics */
  {
    depth_view aig_depth{ aig };
    std::cout << "[AIG]     PIs = " << aig.num_pis()
              << "  POs = " << aig.num_pos()
              << "  Gates = " << aig.num_gates()
              << "  Depth = " << aig_depth.depth() << "\n";
  }

  xag_npn_resynthesis<aig_network> resyn;
  exact_library<aig_network> lib( resyn );

  rewrite_params ps;
  ps.preserve_depth = true;
  ps.allow_zero_gain = true;
  ps.verbose = true;

  rewrite_stats st;

  auto start = std::chrono::high_resolution_clock::now();
  rewrite( aig, lib, ps, &st );
  auto end = std::chrono::high_resolution_clock::now();
  auto elapsed = std::chrono::duration_cast<std::chrono::milliseconds>( end - start ).count();

  /* Print optimized AIG statistics */
  {
    depth_view aig_depth{ aig };
    std::cout << "[AIG opt] PIs = " << aig.num_pis()
              << "  POs = " << aig.num_pos()
              << "  Gates = " << aig.num_gates()
              << "  Depth = " << aig_depth.depth()
              << "  (rewrite: " << elapsed << " ms)\n";
  }

  return 0;
}

2. mig_rw.cpp

#include <mockturtle/algorithms/cleanup.hpp>
#include <mockturtle/algorithms/node_resynthesis/mig_npn.hpp>
#include <mockturtle/algorithms/rewrite.hpp>
#include <mockturtle/io/aiger_reader.hpp>
#include <mockturtle/networks/aig.hpp>
#include <mockturtle/networks/mig.hpp>
#include <mockturtle/utils/tech_library.hpp>
#include <mockturtle/views/depth_view.hpp>
#include <lorina/aiger.hpp>
#include <chrono>
#include <iostream>

using namespace mockturtle;

int main( int argc, char* argv[] )
{
  if ( argc != 2 )
  {
    std::cout << "Usage: " << argv[0] << " <aiger_file>\n";
    return 1;
  }

  mig_network mig;
  if ( lorina::read_aiger( argv[1], aiger_reader( mig ) ) != lorina::return_code::success )
  {
    std::cout << "Error: Cannot read AIGER file to MIG\n";
    return 1;
  }

  /* Print MIG statistics */
  {
    depth_view mig_depth{ mig };
    std::cout << "[MIG]     PIs = " << mig.num_pis()
              << "  POs = " << mig.num_pos()
              << "  Gates = " << mig.num_gates()
              << "  Depth = " << mig_depth.depth() << "\n";
  }

  mig_npn_resynthesis resyn{ true };
  exact_library<mig_network> lib( resyn );

  rewrite_params ps;
  ps.preserve_depth = true;
  ps.allow_zero_gain = true;
  ps.verbose = true;

  rewrite_stats st;

  auto start = std::chrono::high_resolution_clock::now();
  rewrite( mig, lib, ps, &st );
  auto end = std::chrono::high_resolution_clock::now();
  auto elapsed = std::chrono::duration_cast<std::chrono::milliseconds>( end - start ).count();

  /* Print optimized MIG statistics */
  {
    depth_view mig_depth{ mig };
    std::cout << "[MIG opt] PIs = " << mig.num_pis()
              << "  POs = " << mig.num_pos()
              << "  Gates = " << mig.num_gates()
              << "  Depth = " << mig_depth.depth()
              << "  (rewrite: " << elapsed << " ms)\n";
  }

  return 0;
}