Adding XAG resub and improving AIG resub (#658)

* Adding XAG resub and improving AIG resub

* Removing gcc11 from macOS checks

.github/workflows/macos.yml

@@ -9,24 +9,6 @@ on:
     - master
 
 jobs:
-  build-gcc11:
-    name: GNU GCC 11
-    runs-on: macOS-latest
-
-    steps:
-    - uses: actions/checkout@v1
-      with:
-        submodules: true
-    - name: Build mockturtle
-      run: |
-        mkdir build
-        cd build
-        cmake -DCMAKE_CXX_COMPILER=$(which g++-11) -DMOCKTURTLE_TEST=ON ..
-        make run_tests
-    - name: Run tests
-      run: |
-        cd build
-        ./test/run_tests "~[quality]"
   build-gcc12:
     name: GNU GCC 12
     runs-on: macOS-latest

docs/algorithms/resubstitution.rst

@@ -7,7 +7,7 @@ Several resubstitution algorithms are implemented and can be called directly, in
 
 - ``default_resubstitution`` does functional reduction within a window.
 
-- ``aig_resubstitution``, ``mig_resubstitution`` and ``xmg_resubstitution`` do window-based resubstitution in the corresponding network types.
+- ``aig_resubstitution``, ``aig_resubstitution2``, ``xag_resubstitution``, ``mig_resubstitution``, ``mig_resubstitution2``, and ``xmg_resubstitution`` do window-based resubstitution in the corresponding network types.
 
 - ``resubstitution_minmc_withDC`` minimizes multiplicative complexity in XAGs with window-based resubstitution.
 

docs/changelog.rst

@@ -19,6 +19,7 @@ v0.4 (not yet released)
     - Adding a new network type to represent multi-output gates (`block_network`) `#623 <https://github.com/lsils/mockturtle/pull/623>`_
 * Algorithms:
     - AIG balancing (`aig_balance`) `#580 <https://github.com/lsils/mockturtle/pull/580>`_
+    - AIG resubstitution (`xag_resubstitution2`) `#658 <https://github.com/lsils/mockturtle/pull/658>`_
     - Cost-generic resubstitution (`cost_generic_resub`) `#554 <https://github.com/lsils/mockturtle/pull/554>`_
     - Cost aware resynthesis solver (`cost_resyn`) `#554 <https://github.com/lsils/mockturtle/pull/554>`_
     - Resynthesis based on SOP factoring (`sop_factoring`) `#579 <https://github.com/lsils/mockturtle/pull/579>`_
@@ -38,6 +39,7 @@ v0.4 (not yet released)
     - Adding circuit extraction of half and full adders (`extract_adders`) `#623 <https://github.com/lsils/mockturtle/pull/623>`_
     - Adding don't care support in rewriting (`map`, `rewrite`) `#623 <https://github.com/lsils/mockturtle/pull/623>`_
     - XAG balancing (`xag_balance`) `#627 <https://github.com/lsils/mockturtle/pull/627>`_
+    - XAG resubstitution (`xag_resubstitution`) `#658 <https://github.com/lsils/mockturtle/pull/658>`_
 * I/O:
     - Write gates to GENLIB file (`write_genlib`) `#606 <https://github.com/lsils/mockturtle/pull/606>`_
 * Views:

experiments/aig_resubstitution.cpp

@@ -33,6 +33,8 @@
 #include <mockturtle/algorithms/resubstitution.hpp>
 #include <mockturtle/io/aiger_reader.hpp>
 #include <mockturtle/networks/aig.hpp>
+#include <mockturtle/views/depth_view.hpp>
+#include <mockturtle/views/fanout_view.hpp>
 
 #include <experiments.hpp>
 
@@ -56,11 +58,13 @@ int main()
     resubstitution_stats st;
 
     ps.max_pis = 8u;
-    ps.max_inserts = 1u;
+    ps.max_inserts = 2u;
     ps.progress = false;
 
     const uint32_t size_before = aig.num_gates();
-    aig_resubstitution( aig, ps, &st );
+    depth_view depth_aig{ aig };
+    fanout_view fanout_aig{ depth_aig };
+    aig_resubstitution2( fanout_aig, ps, &st );
 
     aig = cleanup_dangling( aig );
 

experiments/xag_resubstitution.cpp

@@ -0,0 +1,77 @@
+/* mockturtle: C++ logic network library
+ * Copyright (C) 2018-2024  EPFL
+ *
+ * Permission is hereby granted, free of charge, to any person
+ * obtaining a copy of this software and associated documentation
+ * files (the "Software"), to deal in the Software without
+ * restriction, including without limitation the rights to use,
+ * copy, modify, merge, publish, distribute, sublicense, and/or sell
+ * copies of the Software, and to permit persons to whom the
+ * Software is furnished to do so, subject to the following
+ * conditions:
+ *
+ * The above copyright notice and this permission notice shall be
+ * included in all copies or substantial portions of the Software.
+ *
+ * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
+ * EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES
+ * OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
+ * NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT
+ * HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY,
+ * WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
+ * FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR
+ * OTHER DEALINGS IN THE SOFTWARE.
+ */
+
+#include <lorina/aiger.hpp>
+#include <mockturtle/algorithms/cleanup.hpp>
+#include <mockturtle/algorithms/xag_resub.hpp>
+#include <mockturtle/io/aiger_reader.hpp>
+#include <mockturtle/networks/xag.hpp>
+#include <mockturtle/views/depth_view.hpp>
+#include <mockturtle/views/fanout_view.hpp>
+
+#include <experiments.hpp>
+#include <fmt/format.h>
+#include <string>
+
+int main()
+{
+  using namespace experiments;
+  using namespace mockturtle;
+
+  experiment<std::string, uint32_t, uint32_t, float, bool>
+      exp( "xag_resubstitution", "benchmark", "size_before", "size_after", "runtime", "equivalent" );
+
+  for ( auto const& benchmark : epfl_benchmarks() )
+  {
+    fmt::print( "[i] processing {}\n", benchmark );
+
+    xag_network xag;
+    if ( lorina::read_aiger( benchmark_path( benchmark ), aiger_reader( xag ) ) != lorina::return_code::success )
+    {
+      continue;
+    }
+
+    resubstitution_params ps;
+    resubstitution_stats st;
+    ps.max_pis = 8u;
+    ps.max_inserts = 1u;
+    ps.progress = false;
+
+    depth_view depth_xag{ xag };
+    fanout_view fanout_xag{ depth_xag };
+
+    uint32_t const size_before = fanout_xag.num_gates();
+    xag_resubstitution( fanout_xag, ps, &st );
+    xag = cleanup_dangling( xag );
+
+    bool const cec = benchmark == "hyp" ? true : abc_cec( fanout_xag, benchmark );
+    exp( benchmark, size_before, xag.num_gates(), to_seconds( st.time_total ), cec );
+  }
+
+  exp.save();
+  exp.table();
+
+  return 0;
+}

include/mockturtle/algorithms/aig_resub.hpp

@@ -27,6 +27,7 @@
   \file aig_resub.hpp
   \brief Resubstitution
 
+  \author Alessandro Tempia Calvino
   \author Eleonora Testa
   \author Heinz Riener
   \author Mathias Soeken
@@ -36,7 +37,10 @@
 #pragma once
 
 #include "../networks/aig.hpp"
+#include "../utils/index_list.hpp"
+#include "../utils/truth_table_utils.hpp"
 #include "resubstitution.hpp"
+#include "resyn_engines/xag_resyn.hpp"
 
 namespace mockturtle
 {
@@ -731,6 +735,90 @@ struct aig_resub_functor
   binate_divisors bdivs;
 }; /* aig_resub_functor */
 
+struct aig_resyn_resub_stats
+{
+  /*! \brief Time for finding dependency function. */
+  stopwatch<>::duration time_compute_function{ 0 };
+
+  /*! \brief Number of found solutions. */
+  uint32_t num_success{ 0 };
+
+  /*! \brief Number of times that no solution can be found. */
+  uint32_t num_fail{ 0 };
+
+  void report() const
+  {
+    fmt::print( "[i]     <ResubFn: mig_resyn_functor>\n" );
+    fmt::print( "[i]         #solution = {:6d}\n", num_success );
+    fmt::print( "[i]         #invoke   = {:6d}\n", num_success + num_fail );
+    fmt::print( "[i]         engine time: {:>5.2f} secs\n", to_seconds( time_compute_function ) );
+  }
+}; /* aig_resyn_resub_stats */
+
+/*! \brief Interfacing resubstitution functor with AIG resynthesis engines for `window_based_resub_engine`.
+ */
+template<typename Ntk, typename Simulator, typename TTcare, typename ResynEngine = xag_resyn_decompose<typename Simulator::truthtable_t, aig_resyn_static_params_for_win_resub<Ntk>>>
+struct aig_resyn_functor
+{
+public:
+  using node = aig_network::node;
+  using signal = aig_network::signal;
+  using stats = aig_resyn_resub_stats;
+  using TT = typename ResynEngine::truth_table_t;
+
+  static_assert( std::is_same_v<TT, typename Simulator::truthtable_t>, "truth table type of the simulator does not match" );
+
+public:
+  explicit aig_resyn_functor( Ntk& ntk, Simulator const& sim, std::vector<node> const& divs, uint32_t num_divs, stats& st )
+      : ntk( ntk ), sim( sim ), tts( ntk ), divs( divs ), st( st )
+  {
+    assert( divs.size() == num_divs );
+    (void)num_divs;
+    div_signals.reserve( divs.size() );
+  }
+
+  std::optional<signal> operator()( node const& root, TTcare care, uint32_t required, uint32_t max_inserts, uint32_t potential_gain, uint32_t& real_gain )
+  {
+    (void)required;
+    TT target = sim.get_tt( sim.get_phase( root ) ? !ntk.make_signal( root ) : ntk.make_signal( root ) );
+    TT care_transformed = target.construct();
+    care_transformed = care;
+
+    typename ResynEngine::stats st_eng;
+    ResynEngine engine( st_eng );
+    for ( auto const& d : divs )
+    {
+      div_signals.emplace_back( sim.get_phase( d ) ? !ntk.make_signal( d ) : ntk.make_signal( d ) );
+      tts[d] = sim.get_tt( ntk.make_signal( d ) );
+    }
+
+    auto const res = call_with_stopwatch( st.time_compute_function, [&]() {
+      return engine( target, care_transformed, std::begin( divs ), std::end( divs ), tts, std::min( potential_gain - 1, max_inserts ) );
+    } );
+    if ( res )
+    {
+      ++st.num_success;
+      signal ret;
+      real_gain = potential_gain - ( *res ).num_gates();
+      insert( ntk, div_signals.begin(), div_signals.end(), *res, [&]( signal const& s ) { ret = s; } );
+      return ret;
+    }
+    else
+    {
+      ++st.num_fail;
+      return std::nullopt;
+    }
+  }
+
+private:
+  Ntk& ntk;
+  Simulator const& sim;
+  unordered_node_map<TT, Ntk> tts;
+  std::vector<node> const& divs;
+  std::vector<signal> div_signals;
+  stats& st;
+}; /* aig_resyn_functor */
+
 template<class Ntk>
 void aig_resubstitution( Ntk& ntk, resubstitution_params const& ps = {}, resubstitution_stats* pst = nullptr )
 {
@@ -809,4 +897,90 @@ void aig_resubstitution( Ntk& ntk, resubstitution_params const& ps = {}, resubst
   }
 }
 
+/*! \brief AIG-specific resubstitution algorithm.
+ *
+ * This algorithms iterates over each node, creates a
+ * reconvergence-driven cut, and attempts to re-express the node's
+ * function using existing nodes from the cut.  Node which are no
+ * longer used (including nodes in their transitive fanins) can then
+ * be removed.  The objective is to reduce the size of the network as
+ * much as possible while maintaining the global input-output
+ * functionality.
+ *
+ * **Required network functions:**
+ *
+ * - `clear_values`
+ * - `fanout_size`
+ * - `foreach_fanin`
+ * - `foreach_fanout`
+ * - `foreach_gate`
+ * - `foreach_node`
+ * - `get_constant`
+ * - `get_node`
+ * - `is_complemented`
+ * - `is_pi`
+ * - `level`
+ * - `make_signal`
+ * - `set_value`
+ * - `set_visited`
+ * - `size`
+ * - `substitute_node`
+ * - `value`
+ * - `visited`
+ *
+ * \param ntk A network type derived from aig_network
+ * \param ps Resubstitution parameters
+ * \param pst Resubstitution statistics
+ */
+template<class Ntk>
+void aig_resubstitution2( Ntk& ntk, resubstitution_params const& ps = {}, resubstitution_stats* pst = nullptr )
+{
+  static_assert( is_network_type_v<Ntk>, "Ntk is not a network type" );
+  static_assert( std::is_same_v<typename Ntk::base_type, aig_network>, "Network type is not aig_network" );
+
+  static_assert( has_clear_values_v<Ntk>, "Ntk does not implement the clear_values method" );
+  static_assert( has_fanout_size_v<Ntk>, "Ntk does not implement the fanout_size method" );
+  static_assert( has_foreach_fanin_v<Ntk>, "Ntk does not implement the foreach_fanin method" );
+  static_assert( has_foreach_gate_v<Ntk>, "Ntk does not implement the foreach_gate method" );
+  static_assert( has_foreach_node_v<Ntk>, "Ntk does not implement the foreach_node method" );
+  static_assert( has_get_constant_v<Ntk>, "Ntk does not implement the get_constant method" );
+  static_assert( has_get_node_v<Ntk>, "Ntk does not implement the get_node method" );
+  static_assert( has_is_complemented_v<Ntk>, "Ntk does not implement the is_complemented method" );
+  static_assert( has_is_pi_v<Ntk>, "Ntk does not implement the is_pi method" );
+  static_assert( has_make_signal_v<Ntk>, "Ntk does not implement the make_signal method" );
+  static_assert( has_set_value_v<Ntk>, "Ntk does not implement the set_value method" );
+  static_assert( has_set_visited_v<Ntk>, "Ntk does not implement the set_visited method" );
+  static_assert( has_size_v<Ntk>, "Ntk does not implement the has_size method" );
+  static_assert( has_substitute_node_v<Ntk>, "Ntk does not implement the has substitute_node method" );
+  static_assert( has_value_v<Ntk>, "Ntk does not implement the has_value method" );
+  static_assert( has_visited_v<Ntk>, "Ntk does not implement the has_visited method" );
+  static_assert( has_level_v<Ntk>, "Ntk does not implement the level method" );
+  static_assert( has_foreach_fanout_v<Ntk>, "Ntk does not implement the foreach_fanout method" );
+
+  using truthtable_t = kitty::dynamic_truth_table;
+  using truthtable_dc_t = kitty::dynamic_truth_table;
+  using functor_t = aig_resyn_functor<Ntk, detail::window_simulator<Ntk, truthtable_t>, truthtable_dc_t>;
+
+  using resub_impl_t = detail::resubstitution_impl<Ntk, detail::window_based_resub_engine<Ntk, truthtable_t, truthtable_dc_t, functor_t>>;
+
+  resubstitution_stats st;
+  typename resub_impl_t::engine_st_t engine_st;
+  typename resub_impl_t::collector_st_t collector_st;
+
+  resub_impl_t p( ntk, ps, st, engine_st, collector_st );
+  p.run();
+
+  if ( ps.verbose )
+  {
+    st.report();
+    collector_st.report();
+    engine_st.report();
+  }
+
+  if ( pst )
+  {
+    *pst = st;
+  }
+}
+
 } /* namespace mockturtle */

include/mockturtle/algorithms/resyn_engines/xag_resyn.hpp

@@ -99,13 +99,28 @@ struct aig_resyn_static_params_default : public xag_resyn_static_params_default<
   static constexpr bool use_xor = false;
 };
 
+template<class Ntk>
+struct xag_resyn_static_params_for_win_resub : public xag_resyn_static_params
+{
+  using truth_table_storage_type = unordered_node_map<kitty::dynamic_truth_table, Ntk>;
+  using node_type = typename Ntk::node;
+};
+
 template<class Ntk>
 struct xag_resyn_static_params_for_sim_resub : public xag_resyn_static_params
 {
   using truth_table_storage_type = incomplete_node_map<kitty::partial_truth_table, Ntk>;
   using node_type = typename Ntk::node;
 };
 
+template<class Ntk>
+struct aig_resyn_static_params_for_win_resub : public xag_resyn_static_params
+{
+  using truth_table_storage_type = unordered_node_map<kitty::dynamic_truth_table, Ntk>;
+  using node_type = typename Ntk::node;
+  static constexpr bool use_xor = false;
+};
+
 template<class Ntk>
 struct aig_resyn_static_params_for_sim_resub : public xag_resyn_static_params_for_sim_resub<Ntk>
 {