Simulation-guided Boolean resubstitution & unified resub framework

docs/algorithms/resubstitution.rst

@@ -3,6 +3,17 @@ Resubstitution
 
 **Header:** ``mockturtle/algorithms/resubstitution.hpp``
 
+Several resubstitution algorithms are implemented and can be called directly, including:
+
+- ``default_resubstitution`` does functional reduction within a window.
+
+- ``aig_resubstitution``, ``mig_resubstitution`` and ``xmg_resubstitution`` do window-based resubstitution in the corresponding network types.
+
+- ``resubstitution_minmc_withDC`` minimizes multiplicative complexity in XAGs with window-based resubstitution.
+
+- ``sim_resubstitution`` does simulation-guided resubstitution in AIGs or XAGs.
+
+
 The following example shows how to resubstitute nodes in an MIG.
 
 .. code-block:: c++
@@ -11,9 +22,10 @@ The following example shows how to resubstitute nodes in an MIG.
    mig_network mig = ...;
 
    /* resubstitute nodes */
-   resubstitution( mig );
+   mig_resubstitution( mig );
    mig = cleanup_dangling( mig );
 
+
 Parameters and statistics
 ~~~~~~~~~~~~~~~~~~~~~~~~~
 
@@ -23,7 +35,73 @@ Parameters and statistics
 .. doxygenstruct:: mockturtle::resubstitution_stats
    :members:
 
-Algorithm
+Structure
 ~~~~~~~~~
 
-.. doxygenfunction:: mockturtle::resubstitution
+In addition to the example algorithms listed above, custom resubstitution algorithms can also be composed.
+
+**Top level**
+
+First, the top-level framework ``detail::resubstitution_impl`` is built-up with a resubstitution engine and a divisor collector.
+
+.. doxygenclass:: mockturtle::detail::resubstitution_impl
+
+.. doxygenfunction:: mockturtle::detail::resubstitution_impl::resubstitution_impl
+
+**ResubEngine**
+
+There are two resubstitution engines implemented: `window_based_resub_engine` and `simulation_based_resub_engine`.
+
+.. doxygenclass:: mockturtle::detail::window_based_resub_engine
+
+.. doxygenclass:: mockturtle::detail::simulation_based_resub_engine
+
+**DivCollector**
+
+Currently, there is only one implementation:
+
+.. doxygenclass:: mockturtle::detail::default_divisor_collector
+
+**Example**
+
+The following example shows how to compose a customized resubstitution algorithm.
+
+.. code-block:: c++
+
+   /* derive some AIG */
+   aig_network aig = ...;
+
+   /* prepare the needed views */
+   using resub_view_t = fanout_view<depth_view<aig_network>>;
+   depth_view<aig_network> depth_view{aig};
+   resub_view_t resub_view{depth_view};
+
+   /* compose the resubstitution framework */
+   using validator_t = circuit_validator<Ntk, bill::solvers::bsat2, false, true, false>;
+   using functor_t = typename detail::sim_aig_resub_functor<resub_view_t, validator_t>;
+   using engine_t = typename detail::simulation_based_resub_engine<resub_view_t, validator_t, functor_t>;
+   using resub_impl_t = typename detail::resubstitution_impl<resub_view_t, engine_t>;
+
+   /* statistics objects */
+   resubstitution_stats st;
+   typename resub_impl_t::engine_st_t engine_st;
+   typename resub_impl_t::collector_st_t collector_st;
+
+   /* instantiate the framework and run it */
+   resubstitution_params ps;
+   resub_impl_t p( resub_view, ps, st, engine_st, collector_st );
+   p.run();
+
+   /* report statistics */
+   st.report();
+   collector_st.report();
+   engine_st.report();
+
+Detailed statistics
+~~~~~~~~~~~~~~~~~~~
+
+.. doxygenstruct:: mockturtle::detail::window_resub_stats
+   :members:
+
+.. doxygenstruct:: mockturtle::detail::sim_resub_stats
+   :members:

docs/changelog.rst

@@ -30,6 +30,7 @@ v0.2 (not yet released)
     - Collapse network into single node per output network `#309 <https://github.com/lsils/mockturtle/pull/309>`_
     - Generic balancing algorithm `#340 <https://github.com/lsils/mockturtle/pull/340>`_
     - Check functional equivalence (`circuit_validator`) `#346 <https://github.com/lsils/mockturtle/pull/346>`_
+    - Restructured resubstitution framework (`resubstitution`), simulation-guided resubstitution (`sim_resub`) `#373 <https://github.com/lsils/mockturtle/pull/373>`_
 * Views:
     - Assign names to signals and outputs (`names_view`) `#181 <https://github.com/lsils/mockturtle/pull/181>`_ `#184 <https://github.com/lsils/mockturtle/pull/184>`_
     - Creates a CNF while creating a network (`cnf_view`) `#274 <https://github.com/lsils/mockturtle/pull/274>`_

experiments/aig_resubstitution.json

@@ -723,5 +723,150 @@
       }
     ],
     "version": "fc251b3"
+  },
+  {
+    "entries": [
+      {
+        "benchmark": "adder",
+        "equivalent": true,
+        "runtime": 0.006387114059180021,
+        "size_after": 893,
+        "size_before": 1020
+      },
+      {
+        "benchmark": "bar",
+        "equivalent": true,
+        "runtime": 0.021806901320815086,
+        "size_after": 3336,
+        "size_before": 3336
+      },
+      {
+        "benchmark": "div",
+        "equivalent": true,
+        "runtime": 0.5128353238105774,
+        "size_after": 52305,
+        "size_before": 57247
+      },
+      {
+        "benchmark": "hyp",
+        "equivalent": true,
+        "runtime": 1.575783133506775,
+        "size_after": 208375,
+        "size_before": 214335
+      },
+      {
+        "benchmark": "log2",
+        "equivalent": true,
+        "runtime": 0.307009220123291,
+        "size_after": 32012,
+        "size_before": 32060
+      },
+      {
+        "benchmark": "max",
+        "equivalent": true,
+        "runtime": 0.01488445233553648,
+        "size_after": 2865,
+        "size_before": 2865
+      },
+      {
+        "benchmark": "multiplier",
+        "equivalent": true,
+        "runtime": 0.25727105140686035,
+        "size_after": 26971,
+        "size_before": 27062
+      },
+      {
+        "benchmark": "sin",
+        "equivalent": true,
+        "runtime": 0.06176622956991196,
+        "size_after": 5375,
+        "size_before": 5416
+      },
+      {
+        "benchmark": "sqrt",
+        "equivalent": true,
+        "runtime": 0.2681542932987213,
+        "size_after": 20526,
+        "size_before": 24618
+      },
+      {
+        "benchmark": "square",
+        "equivalent": true,
+        "runtime": 0.16956447064876556,
+        "size_after": 18160,
+        "size_before": 18484
+      },
+      {
+        "benchmark": "arbiter",
+        "equivalent": true,
+        "runtime": 0.08660183846950531,
+        "size_after": 11839,
+        "size_before": 11839
+      },
+      {
+        "benchmark": "cavlc",
+        "equivalent": true,
+        "runtime": 0.014331983402371407,
+        "size_after": 674,
+        "size_before": 693
+      },
+      {
+        "benchmark": "ctrl",
+        "equivalent": true,
+        "runtime": 0.00372308399528265,
+        "size_after": 108,
+        "size_before": 174
+      },
+      {
+        "benchmark": "dec",
+        "equivalent": true,
+        "runtime": 0.01071423664689064,
+        "size_after": 304,
+        "size_before": 304
+      },
+      {
+        "benchmark": "i2c",
+        "equivalent": true,
+        "runtime": 0.011223589070141315,
+        "size_after": 1241,
+        "size_before": 1342
+      },
+      {
+        "benchmark": "int2float",
+        "equivalent": true,
+        "runtime": 0.0027788400184363127,
+        "size_after": 236,
+        "size_before": 260
+      },
+      {
+        "benchmark": "mem_ctrl",
+        "equivalent": true,
+        "runtime": 0.4201244115829468,
+        "size_after": 46446,
+        "size_before": 46836
+      },
+      {
+        "benchmark": "priority",
+        "equivalent": true,
+        "runtime": 0.009349452331662178,
+        "size_after": 852,
+        "size_before": 978
+      },
+      {
+        "benchmark": "router",
+        "equivalent": true,
+        "runtime": 0.0017743620555847883,
+        "size_after": 257,
+        "size_before": 257
+      },
+      {
+        "benchmark": "voter",
+        "equivalent": true,
+        "runtime": 0.12908892333507538,
+        "size_after": 10498,
+        "size_before": 13758
+      }
+    ],
+    "version": "88afeb8"
   }
 ]

experiments/mig_resubstitution.cpp

@@ -30,7 +30,6 @@
 #include <lorina/aiger.hpp>
 #include <mockturtle/algorithms/mig_resub.hpp>
 #include <mockturtle/algorithms/cleanup.hpp>
-#include <mockturtle/algorithms/resubstitution.hpp>
 #include <mockturtle/io/aiger_reader.hpp>
 #include <mockturtle/networks/mig.hpp>