diff --git a/docs/algorithms/resubstitution.rst b/docs/algorithms/resubstitution.rst index 9c8babf5d..22bcd5011 100644 --- a/docs/algorithms/resubstitution.rst +++ b/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 depth_view{aig}; + resub_view_t resub_view{depth_view}; + + /* compose the resubstitution framework */ + using validator_t = circuit_validator; + using functor_t = typename detail::sim_aig_resub_functor; + using engine_t = typename detail::simulation_based_resub_engine; + using resub_impl_t = typename detail::resubstitution_impl; + + /* 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: diff --git a/docs/changelog.rst b/docs/changelog.rst index bc7bc0ffb..701ee68af 100644 --- a/docs/changelog.rst +++ b/docs/changelog.rst @@ -30,6 +30,7 @@ v0.2 (not yet released) - Collapse network into single node per output network `#309 `_ - Generic balancing algorithm `#340 `_ - Check functional equivalence (`circuit_validator`) `#346 `_ + - Restructured resubstitution framework (`resubstitution`), simulation-guided resubstitution (`sim_resub`) `#373 `_ * Views: - Assign names to signals and outputs (`names_view`) `#181 `_ `#184 `_ - Creates a CNF while creating a network (`cnf_view`) `#274 `_ diff --git a/experiments/aig_resubstitution.json b/experiments/aig_resubstitution.json index dfd9a592d..da010ed9d 100644 --- a/experiments/aig_resubstitution.json +++ b/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" } ] diff --git a/experiments/mig_resubstitution.cpp b/experiments/mig_resubstitution.cpp index 7eba95026..7e5f0039d 100644 --- a/experiments/mig_resubstitution.cpp +++ b/experiments/mig_resubstitution.cpp @@ -30,7 +30,6 @@ #include #include #include -#include #include #include diff --git a/experiments/mig_resubstitution.json b/experiments/mig_resubstitution.json index ee989bee9..bde0ec390 100644 --- a/experiments/mig_resubstitution.json +++ b/experiments/mig_resubstitution.json @@ -143,5 +143,150 @@ } ], "version": "bbd1506" + }, + { + "entries": [ + { + "benchmark": "adder", + "equivalent": true, + "runtime": 0.010076023638248444, + "size_after": 893, + "size_before": 1020 + }, + { + "benchmark": "bar", + "equivalent": true, + "runtime": 0.03214477375149727, + "size_after": 3072, + "size_before": 3336 + }, + { + "benchmark": "div", + "equivalent": true, + "runtime": 0.67690509557724, + "size_after": 56714, + "size_before": 57247 + }, + { + "benchmark": "hyp", + "equivalent": true, + "runtime": 5.334950923919678, + "size_after": 206473, + "size_before": 214335 + }, + { + "benchmark": "log2", + "equivalent": true, + "runtime": 0.4067056477069855, + "size_after": 32008, + "size_before": 32060 + }, + { + "benchmark": "max", + "equivalent": true, + "runtime": 0.021115295588970184, + "size_after": 2840, + "size_before": 2865 + }, + { + "benchmark": "multiplier", + "equivalent": true, + "runtime": 0.4099847078323364, + "size_after": 26819, + "size_before": 27062 + }, + { + "benchmark": "sin", + "equivalent": true, + "runtime": 0.09224862605333328, + "size_after": 5339, + "size_before": 5416 + }, + { + "benchmark": "sqrt", + "equivalent": true, + "runtime": 0.45702600479125977, + "size_after": 21902, + "size_before": 24618 + }, + { + "benchmark": "square", + "equivalent": true, + "runtime": 0.27489277720451355, + "size_after": 18276, + "size_before": 18484 + }, + { + "benchmark": "arbiter", + "equivalent": true, + "runtime": 0.10679267346858978, + "size_after": 11839, + "size_before": 11839 + }, + { + "benchmark": "cavlc", + "equivalent": true, + "runtime": 0.06770826876163483, + "size_after": 636, + "size_before": 693 + }, + { + "benchmark": "ctrl", + "equivalent": true, + "runtime": 0.025390056893229485, + "size_after": 103, + "size_before": 174 + }, + { + "benchmark": "dec", + "equivalent": true, + "runtime": 0.01241659838706255, + "size_after": 304, + "size_before": 304 + }, + { + "benchmark": "i2c", + "equivalent": true, + "runtime": 0.01579423062503338, + "size_after": 1280, + "size_before": 1342 + }, + { + "benchmark": "int2float", + "equivalent": true, + "runtime": 0.005563724786043167, + "size_after": 237, + "size_before": 260 + }, + { + "benchmark": "mem_ctrl", + "equivalent": true, + "runtime": 0.7887808084487915, + "size_after": 44613, + "size_before": 46836 + }, + { + "benchmark": "priority", + "equivalent": true, + "runtime": 0.014381092973053455, + "size_after": 781, + "size_before": 978 + }, + { + "benchmark": "router", + "equivalent": true, + "runtime": 0.0028713271021842957, + "size_after": 257, + "size_before": 257 + }, + { + "benchmark": "voter", + "equivalent": true, + "runtime": 0.23080433905124664, + "size_after": 11874, + "size_before": 13758 + } + ], + "version": "88afeb8" } ] diff --git a/experiments/sim_resubstitution.cpp b/experiments/sim_resubstitution.cpp new file mode 100644 index 000000000..50911f7c4 --- /dev/null +++ b/experiments/sim_resubstitution.cpp @@ -0,0 +1,70 @@ +/* mockturtle: C++ logic network library + * Copyright (C) 2018-2020 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 +#include + +#include +#include +#include +#include +#include +#include + +#include + +int main() +{ + using namespace experiments; + using namespace mockturtle; + + experiment exp( "sim_resubstitution", "benchmark", "size", "gain", "runtime", "equivalent" ); + + for ( auto const& benchmark : epfl_benchmarks() ) + { + fmt::print( "[i] processing {}\n", benchmark ); + aig_network aig; + lorina::read_aiger( benchmark_path( benchmark ), aiger_reader( aig ) ); + + resubstitution_params ps; + resubstitution_stats st; + + //ps.pattern_filename = "1024sa1/" + benchmark + ".pat"; + ps.max_inserts = 1; + + const uint32_t size_before = aig.num_gates(); + sim_resubstitution( aig, ps, &st ); + aig = cleanup_dangling( aig ); + + const auto cec = benchmark == "hyp" ? true : abc_cec( aig, benchmark ); + + exp( benchmark, size_before, size_before - aig.num_gates(), to_seconds( st.time_total ), cec ); + } + + exp.save(); + exp.table(); + + return 0; +} diff --git a/experiments/sim_resubstitution.json b/experiments/sim_resubstitution.json new file mode 100644 index 000000000..f45bf3b10 --- /dev/null +++ b/experiments/sim_resubstitution.json @@ -0,0 +1,147 @@ +[ + { + "entries": [ + { + "benchmark": "adder", + "equivalent": true, + "gain": 127, + "runtime": 0.06293122470378876, + "size": 1020 + }, + { + "benchmark": "bar", + "equivalent": true, + "gain": 0, + "runtime": 0.055317867547273636, + "size": 3336 + }, + { + "benchmark": "div", + "equivalent": true, + "gain": 5218, + "runtime": 76.69324493408203, + "size": 57247 + }, + { + "benchmark": "hyp", + "equivalent": true, + "gain": 6305, + "runtime": 147.6929931640625, + "size": 214335 + }, + { + "benchmark": "log2", + "equivalent": true, + "gain": 522, + "runtime": 19.900320053100586, + "size": 32060 + }, + { + "benchmark": "max", + "equivalent": true, + "gain": 3, + "runtime": 0.05850469321012497, + "size": 2865 + }, + { + "benchmark": "multiplier", + "equivalent": true, + "gain": 91, + "runtime": 1.3532203435897827, + "size": 27062 + }, + { + "benchmark": "sin", + "equivalent": true, + "gain": 92, + "runtime": 2.563305377960205, + "size": 5416 + }, + { + "benchmark": "sqrt", + "equivalent": true, + "gain": 4195, + "runtime": 42.06993865966797, + "size": 24618 + }, + { + "benchmark": "square", + "equivalent": true, + "gain": 346, + "runtime": 1.428206205368042, + "size": 18484 + }, + { + "benchmark": "arbiter", + "equivalent": true, + "gain": 0, + "runtime": 0.24237634241580963, + "size": 11839 + }, + { + "benchmark": "cavlc", + "equivalent": true, + "gain": 19, + "runtime": 0.02373042143881321, + "size": 693 + }, + { + "benchmark": "ctrl", + "equivalent": true, + "gain": 67, + "runtime": 0.00992374774068594, + "size": 174 + }, + { + "benchmark": "dec", + "equivalent": true, + "gain": 0, + "runtime": 0.011482873931527138, + "size": 304 + }, + { + "benchmark": "i2c", + "equivalent": true, + "gain": 77, + "runtime": 0.04038527235388756, + "size": 1342 + }, + { + "benchmark": "int2float", + "equivalent": true, + "gain": 24, + "runtime": 0.008397926576435566, + "size": 260 + }, + { + "benchmark": "mem_ctrl", + "equivalent": true, + "gain": 1403, + "runtime": 4.762147426605225, + "size": 46836 + }, + { + "benchmark": "priority", + "equivalent": true, + "gain": 126, + "runtime": 0.06392306834459305, + "size": 978 + }, + { + "benchmark": "router", + "equivalent": true, + "gain": 0, + "runtime": 0.009761467576026917, + "size": 257 + }, + { + "benchmark": "voter", + "equivalent": true, + "gain": 3204, + "runtime": 5.274948596954346, + "size": 13758 + } + ], + "version": "df695e1" + } +] diff --git a/include/CMakeLists.txt b/include/CMakeLists.txt index c01cfe4ca..18964fcf5 100644 --- a/include/CMakeLists.txt +++ b/include/CMakeLists.txt @@ -1,6 +1,6 @@ add_library(mockturtle INTERFACE) target_include_directories(mockturtle INTERFACE ${PROJECT_SOURCE_DIR}/include) -target_link_libraries(mockturtle INTERFACE kitty lorina sparsepp percy json bill libabcesop) +target_link_libraries(mockturtle INTERFACE kitty lorina sparsepp percy json bill libabcesop abcresub) if(CMAKE_CXX_COMPILER_ID STREQUAL "GNU" AND CMAKE_CXX_COMPILER_VERSION VERSION_LESS 9) target_link_libraries(mockturtle INTERFACE stdc++fs) diff --git a/include/mockturtle/algorithms/aig_resub.hpp b/include/mockturtle/algorithms/aig_resub.hpp index 5de2ab091..8eb965656 100644 --- a/include/mockturtle/algorithms/aig_resub.hpp +++ b/include/mockturtle/algorithms/aig_resub.hpp @@ -758,42 +758,55 @@ void aig_resubstitution( Ntk& ntk, resubstitution_params const& ps = {}, resubst depth_view depth_view{ntk}; resub_view_t resub_view{depth_view}; - resubstitution_stats st; if ( ps.max_pis == 8 ) { using truthtable_t = kitty::static_truth_table<8u>; using truthtable_dc_t = kitty::dynamic_truth_table; - using simulator_t = detail::simulator; - using node_mffc_t = detail::node_mffc_inside; - using resubstitution_functor_t = aig_resub_functor; - typename resubstitution_functor_t::stats resub_st; - detail::resubstitution_impl p( resub_view, ps, st, resub_st ); + using resub_impl_t = detail::resubstitution_impl, truthtable_dc_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( resub_view, ps, st, engine_st, collector_st ); p.run(); + if ( ps.verbose ) { st.report(); - resub_st.report(); + collector_st.report(); + engine_st.report(); + } + + if ( pst ) + { + *pst = st; } } else { using truthtable_t = kitty::dynamic_truth_table; - using simulator_t = detail::simulator; - using node_mffc_t = detail::node_mffc_inside; - using resubstitution_functor_t = aig_resub_functor; - typename resubstitution_functor_t::stats resub_st; - detail::resubstitution_impl p( resub_view, ps, st, resub_st ); + using truthtable_dc_t = kitty::dynamic_truth_table; + using resub_impl_t = detail::resubstitution_impl, truthtable_dc_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( resub_view, ps, st, engine_st, collector_st ); p.run(); + if ( ps.verbose ) { st.report(); - resub_st.report(); + collector_st.report(); + engine_st.report(); } - } - if ( pst ) - { - *pst = st; + if ( pst ) + { + *pst = st; + } } } diff --git a/include/mockturtle/algorithms/circuit_validator.hpp b/include/mockturtle/algorithms/circuit_validator.hpp index 5205c2e52..42f24aada 100644 --- a/include/mockturtle/algorithms/circuit_validator.hpp +++ b/include/mockturtle/algorithms/circuit_validator.hpp @@ -61,6 +61,7 @@ template const& )>; @@ -286,7 +287,9 @@ class circuit_validator /*! \brief Generate pattern(s) for signal `f` to be `value`, optionally blocking several known patterns. * - * Requires `use_pushpop = true`. + * Requires `use_pushpop = true`, which is only supported for `bsat2` and `z3`. If `bsat2` is used, + * and if the network has more than 2048 PIs, the `BUFFER_SIZE` in `lib/bill/sat/interface/abc_bsat2.hpp` + * has to be increased to at least `ntk.num_pis()`. * * If `block_patterns` and the returned vector are both empty, `f` is validated to be a constant of `!value`. * diff --git a/include/mockturtle/algorithms/detail/resub_utils.hpp b/include/mockturtle/algorithms/detail/resub_utils.hpp new file mode 100644 index 000000000..510cc28f5 --- /dev/null +++ b/include/mockturtle/algorithms/detail/resub_utils.hpp @@ -0,0 +1,366 @@ +/* mockturtle: C++ logic network library + * Copyright (C) 2018-2020 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. + */ + +/*! + \file resub_utils.hpp + \brief Utility classes for the resubstitution framework + + class `node_mffc_inside`, class `window_simulator` (originally `simulator`), + and class `default_resub_functor` moved from resubstitution.hpp + + \author Heinz Riener +*/ + +#pragma once + +#include +#include +#include + +#include + +namespace mockturtle::detail +{ + +/* based on abcRefs.c */ +template +class node_mffc_inside +{ +public: + using node = typename Ntk::node; + +public: + explicit node_mffc_inside( Ntk const& ntk ) + : ntk( ntk ) + { + } + + int32_t run( node const& n, std::vector const& leaves, std::vector& inside ) + { + /* increment the fanout counters for the leaves */ + for ( const auto& l : leaves ) + ntk.incr_fanout_size( l ); + + /* dereference the node */ + auto count1 = node_deref_rec( n ); + + /* collect the nodes inside the MFFC */ + node_mffc_cone( n, inside ); + + /* reference it back */ + auto count2 = node_ref_rec( n ); + (void)count2; + assert( count1 == count2 ); + + for ( const auto& l : leaves ) + ntk.decr_fanout_size( l ); + + return count1; + } + +private: + /* ! \brief Dereference the node's MFFC */ + int32_t node_deref_rec( node const& n ) + { + if ( ntk.is_pi( n ) ) + return 0; + + int32_t counter = 1; + ntk.foreach_fanin( n, [&]( const auto& f ) { + auto const& p = ntk.get_node( f ); + + ntk.decr_fanout_size( p ); + if ( ntk.fanout_size( p ) == 0 ) + { + counter += node_deref_rec( p ); + } + } ); + + return counter; + } + + /* ! \brief Reference the node's MFFC */ + int32_t node_ref_rec( node const& n ) + { + if ( ntk.is_pi( n ) ) + return 0; + + int32_t counter = 1; + ntk.foreach_fanin( n, [&]( const auto& f ) { + auto const& p = ntk.get_node( f ); + + auto v = ntk.fanout_size( p ); + ntk.incr_fanout_size( p ); + if ( v == 0 ) + { + counter += node_ref_rec( p ); + } + } ); + + return counter; + } + + void node_mffc_cone_rec( node const& n, std::vector& cone, bool top_most ) + { + /* skip visited nodes */ + if ( ntk.visited( n ) == ntk.trav_id() ) + { + return; + } + ntk.set_visited( n, ntk.trav_id() ); + + if ( !top_most && ( ntk.is_pi( n ) || ntk.fanout_size( n ) > 0 ) ) + { + return; + } + + /* recurse on children */ + ntk.foreach_fanin( n, [&]( const auto& f ) { + node_mffc_cone_rec( ntk.get_node( f ), cone, false ); + } ); + + /* collect the internal nodes */ + cone.emplace_back( n ); + } + + void node_mffc_cone( node const& n, std::vector& cone ) + { + cone.clear(); + ntk.incr_trav_id(); + node_mffc_cone_rec( n, cone, true ); + } + +private: + Ntk const& ntk; +}; /* node_mffc_inside */ + +template +class window_simulator +{ +public: + using node = typename Ntk::node; + using signal = typename Ntk::signal; + using truthtable_t = TT; + + explicit window_simulator( Ntk const& ntk, uint32_t num_divisors, uint32_t max_pis ) + : ntk( ntk ), num_divisors( num_divisors ), tts( num_divisors + 1 ), node_to_index( ntk.size(), 0u ), phase( ntk.size(), false ) + { + auto tt = kitty::create( max_pis ); + tts[0] = tt; + + for ( auto i = 0u; i < tt.num_vars(); ++i ) + { + kitty::create_nth_var( tt, i ); + tts[i + 1] = tt; + } + } + + void resize() + { + if ( ntk.size() > node_to_index.size() ) + { + node_to_index.resize( ntk.size(), 0u ); + } + if ( ntk.size() > phase.size() ) + { + phase.resize( ntk.size(), false ); + } + } + + void assign( node const& n, uint32_t index ) + { + assert( n < node_to_index.size() ); + assert( index < num_divisors + 1 ); + node_to_index[n] = index; + } + + truthtable_t get_tt( signal const& s ) const + { + auto const tt = tts.at( node_to_index.at( ntk.get_node( s ) ) ); + return ntk.is_complemented( s ) ? ~tt : tt; + } + + void set_tt( uint32_t index, truthtable_t const& tt ) + { + tts[index] = tt; + } + + void normalize( std::vector const& nodes ) + { + for ( const auto& n : nodes ) + { + assert( n < phase.size() ); + assert( n < node_to_index.size() ); + + if ( n == 0 ) + { + return; + } + + auto& tt = tts[node_to_index.at( n )]; + if ( kitty::get_bit( tt, 0 ) ) + { + tt = ~tt; + phase[n] = true; + } + else + { + phase[n] = false; + } + } + } + + bool get_phase( node const& n ) const + { + assert( n < phase.size() ); + return phase.at( n ); + } + +private: + Ntk const& ntk; + uint32_t num_divisors; + + std::vector tts; + std::vector node_to_index; + std::vector phase; +}; /* window_simulator */ + +struct default_resub_functor_stats +{ + /*! \brief Accumulated runtime for const-resub */ + stopwatch<>::duration time_resubC{0}; + + /*! \brief Accumulated runtime for zero-resub */ + stopwatch<>::duration time_resub0{0}; + + /*! \brief Number of accepted constant resubsitutions */ + uint32_t num_const_accepts{0}; + + /*! \brief Number of accepted zero resubsitutions */ + uint32_t num_div0_accepts{0}; + + void report() const + { + std::cout << "[i] kernel: default_resub_functor\n"; + std::cout << fmt::format( "[i] constant-resub {:6d} ({:>5.2f} secs)\n", + num_const_accepts, to_seconds( time_resubC ) ); + std::cout << fmt::format( "[i] 0-resub {:6d} ({:>5.2f} secs)\n", + num_div0_accepts, to_seconds( time_resub0 ) ); + std::cout << fmt::format( "[i] total {:6d}\n", + ( num_const_accepts + num_div0_accepts ) ); + } +}; + +/*! \brief A window-based resub functor which is basically doing functional reduction (fraig). */ +template +class default_resub_functor +{ +public: + using node = typename Ntk::node; + using signal = typename Ntk::signal; + using stats = default_resub_functor_stats; + + explicit default_resub_functor( Ntk const& ntk, Simulator const& sim, std::vector const& divs, uint32_t num_divs, default_resub_functor_stats& st ) + : ntk( ntk ), sim( sim ), divs( divs ), num_divs( num_divs ), st( st ) + { + } + + std::optional operator()( node const& root, TT care, uint32_t required, uint32_t max_inserts, uint32_t num_mffc, uint32_t& last_gain ) const + { + /* The default resubstitution functor does not insert any gates + and consequently does not use the argument `max_inserts`. Other + functors, however, make use of this argument. */ + (void)care; + (void)max_inserts; + assert( kitty::is_const0( ~care ) ); + + /* consider constants */ + auto g = call_with_stopwatch( st.time_resubC, [&]() { + return resub_const( root, required ); + } ); + if ( g ) + { + ++st.num_const_accepts; + last_gain = num_mffc; + return g; /* accepted resub */ + } + + /* consider equal nodes */ + g = call_with_stopwatch( st.time_resub0, [&]() { + return resub_div0( root, required ); + } ); + if ( g ) + { + ++st.num_div0_accepts; + last_gain = num_mffc; + return g; /* accepted resub */ + } + + return std::nullopt; + } + +private: + std::optional resub_const( node const& root, uint32_t required ) const + { + (void)required; + auto const tt = sim.get_tt( ntk.make_signal( root ) ); + if ( tt == sim.get_tt( ntk.get_constant( false ) ) ) + { + return sim.get_phase( root ) ? ntk.get_constant( true ) : ntk.get_constant( false ); + } + return std::nullopt; + } + + std::optional resub_div0( node const& root, uint32_t required ) const + { + (void)required; + auto const tt = sim.get_tt( ntk.make_signal( root ) ); + for ( const auto& d : divs ) + { + if ( root == d ) + { + break; + } + + if ( tt != sim.get_tt( ntk.make_signal( d ) ) ) + { + continue; /* next */ + } + + return ( sim.get_phase( d ) ^ sim.get_phase( root ) ) ? !ntk.make_signal( d ) : ntk.make_signal( d ); + } + + return std::nullopt; + } + +private: + Ntk const& ntk; + Simulator const& sim; + std::vector const& divs; + uint32_t num_divs; + stats& st; +}; /* default_resub_functor */ + +} /* namespace mockturtle::detail */ diff --git a/include/mockturtle/algorithms/mig_resub.hpp b/include/mockturtle/algorithms/mig_resub.hpp index 915a6ada0..8962908d0 100644 --- a/include/mockturtle/algorithms/mig_resub.hpp +++ b/include/mockturtle/algorithms/mig_resub.hpp @@ -669,42 +669,55 @@ void mig_resubstitution( Ntk& ntk, resubstitution_params const& ps = {}, resubst depth_view depth_view{ntk}; resub_view_t resub_view{depth_view}; - resubstitution_stats st; if ( ps.max_pis == 8 ) { - using truthtable_t = kitty::static_truth_table<8>; + using truthtable_t = kitty::static_truth_table<8u>; using truthtable_dc_t = kitty::dynamic_truth_table; - using simulator_t = detail::simulator; - using node_mffc_t = detail::node_mffc_inside; - using resubstitution_functor_t = mig_resub_functor; - typename resubstitution_functor_t::stats resub_st; - detail::resubstitution_impl p( resub_view, ps, st, resub_st ); + using resub_impl_t = detail::resubstitution_impl, truthtable_dc_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( resub_view, ps, st, engine_st, collector_st ); p.run(); + if ( ps.verbose ) { st.report(); - resub_st.report(); + collector_st.report(); + engine_st.report(); + } + + if ( pst ) + { + *pst = st; } } else { using truthtable_t = kitty::dynamic_truth_table; - using simulator_t = detail::simulator; - using node_mffc_t = detail::node_mffc_inside; - using resubstitution_functor_t = mig_resub_functor; - typename resubstitution_functor_t::stats resub_st; - detail::resubstitution_impl p( resub_view, ps, st, resub_st ); + using truthtable_dc_t = kitty::dynamic_truth_table; + using resub_impl_t = detail::resubstitution_impl, truthtable_dc_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( resub_view, ps, st, engine_st, collector_st ); p.run(); + if ( ps.verbose ) { st.report(); - resub_st.report(); + collector_st.report(); + engine_st.report(); } - } - if ( pst ) - { - *pst = st; + if ( pst ) + { + *pst = st; + } } } diff --git a/include/mockturtle/algorithms/pattern_generation.hpp b/include/mockturtle/algorithms/pattern_generation.hpp index df19f5968..d0da63c68 100644 --- a/include/mockturtle/algorithms/pattern_generation.hpp +++ b/include/mockturtle/algorithms/pattern_generation.hpp @@ -51,7 +51,12 @@ struct pattern_generation_params /*! \brief Whether to remove constant nodes. Requires `substitute_node`. */ bool substitute_const{false}; - /*! \brief Number of patterns each node should have for both values. */ + /*! \brief Number of patterns each node should have for both values. + * + * When this parameter is set to greater than 1, and if the network has more + * than 2048 PIs, the `BUFFER_SIZE` in `lib/bill/sat/interface/abc_bsat2.hpp` + * has to be increased to at least `ntk.num_pis()`. + */ uint32_t num_stuck_at{1}; /*! \brief Whether to consider observability, and how many levels. 0 = no. -1 = Consider TFO until PO. */ @@ -434,7 +439,7 @@ class patgen_impl * stuck-at value checking and observability checking. Please refer to * [1] for details of the algorithm and its purpose. * - * [1] Simulation-Guided Boolean Resubstitution. IWLS 2020 / ICCAD 2020. + * [1] Simulation-Guided Boolean Resubstitution. IWLS 2020 (arXiv:2007.02579). * * \param sim Reference of a `partial_simulator` object where the generated * patterns will be stored. It can be empty (`partial_simulator( ntk.num_pis(), 0 )`) diff --git a/include/mockturtle/algorithms/resubstitution.hpp b/include/mockturtle/algorithms/resubstitution.hpp index 02b4c576e..a168d567a 100644 --- a/include/mockturtle/algorithms/resubstitution.hpp +++ b/include/mockturtle/algorithms/resubstitution.hpp @@ -1,5 +1,5 @@ /* mockturtle: C++ logic network library - * Copyright (C) 2018-2019 EPFL + * Copyright (C) 2018-2020 EPFL * * Permission is hereby granted, free of charge, to any person * obtaining a copy of this software and associated documentation @@ -25,26 +25,26 @@ /*! \file resubstitution.hpp - \brief Resubstitution + \brief Generalized resubstitution framework + \author Heinz Riener + \author Siang-Yun Lee */ #pragma once +#include + #include "../traits.hpp" #include "../utils/progress_bar.hpp" #include "../utils/stopwatch.hpp" #include "../views/depth_view.hpp" #include "../views/fanout_view.hpp" +#include "detail/resub_utils.hpp" #include "dont_cares.hpp" #include "reconv_cut2.hpp" -#include -#include -#include -#include - namespace mockturtle { @@ -76,11 +76,39 @@ struct resubstitution_params /*! \brief Be verbose. */ bool verbose{false}; - /*! \brief Use don't cares for optimization. */ + /****** window-based resub engine ******/ + + /*! \brief Use don't cares for optimization. Only used by window-based resub engine. */ bool use_dont_cares{false}; - /* \brief Window size for don't cares calculation */ + /* \brief Window size for don't cares calculation. Only used by window-based resub engine. */ uint32_t window_size{12u}; + + /****** simulation-based resub engine ******/ + + /*! \brief Whether to use pre-generated patterns stored in a file. + * If not, by default, 1024 random pattern + 1x stuck-at patterns will be generated. Only used by simulation-based resub engine. + */ + std::optional pattern_filename{}; + + /*! \brief Whether to save the appended patterns (with CEXs) into file. Only used by simulation-based resub engine. */ + std::optional save_patterns{}; + + /*! \brief Conflict limit for the SAT solver. Only used by simulation-based resub engine. */ + uint32_t conflict_limit{1000}; + + /*! \brief Random seed for the SAT solver (influences the randomness of counter-examples). Only used by simulation-based resub engine. */ + uint32_t random_seed{0}; + + /*! \brief Whether to utilize ODC, and how many levels. 0 = no. -1 = Consider TFO until PO. Only used by simulation-based resub engine. */ + int odc_levels{0}; + + /*! \brief Maximum number of trials to call the resub functor. Only used by simulation-based resub engine. */ + uint32_t max_trials{100}; + + /* k-resub engine specific */ + /*! \brief Maximum number of divisors to consider in k-resub engine. Only used by `abc_resub_functor` with simulation-based resub engine. */ + uint32_t max_divisors_k{50}; }; /*! \brief Statistics for resubstitution. @@ -93,370 +121,487 @@ struct resubstitution_stats /*! \brief Total runtime. */ stopwatch<>::duration time_total{0}; - /*! \brief Accumulated runtime for cut computation. */ - stopwatch<>::duration time_cuts{0}; - - /*! \brief Accumulated runtime for cut evaluation/computing a resubsitution. */ - stopwatch<>::duration time_eval{0}; - - /*! \brief Accumulated runtime for mffc computation. */ - stopwatch<>::duration time_mffc{0}; - - /*! \brief Accumulated runtime for divisor computation. */ + /*! \brief Accumulated runtime of the divisor collector. */ stopwatch<>::duration time_divs{0}; - /*! \brief Accumulated runtime for updating the network. */ - stopwatch<>::duration time_substitute{0}; - - /*! \brief Accumulated runtime for simulation. */ - stopwatch<>::duration time_simulation{0}; + /*! \brief Accumulated runtime of the resub engine. */ + stopwatch<>::duration time_resub{0}; - /*! \brief Initial network size (before resubstitution) */ - uint64_t initial_size{0}; + /*! \brief Accumulated runtime of the callback function. */ + stopwatch<>::duration time_callback{0}; - /*! \brief Total number of divisors */ + /*! \brief Total number of divisors. */ uint64_t num_total_divisors{0}; - /*! \brief Total number of leaves */ - uint64_t num_total_leaves{0}; - - /*! \brief Total number of gain */ + /*! \brief Total number of gain. */ uint64_t estimated_gain{0}; + /*! \brief Initial network size (before resubstitution). */ + uint64_t initial_size{0}; + void report() const { - std::cout << fmt::format( "[i] total time ({:>5.2f} secs)\n", to_seconds( time_total ) ); - std::cout << fmt::format( "[i] cut time ({:>5.2f} secs)\n", to_seconds( time_cuts ) ); - std::cout << fmt::format( "[i] mffc time ({:>5.2f} secs)\n", to_seconds( time_mffc ) ); - std::cout << fmt::format( "[i] divs time ({:>5.2f} secs)\n", to_seconds( time_divs ) ); - std::cout << fmt::format( "[i] simulation time ({:>5.2f} secs)\n", to_seconds( time_simulation ) ); - std::cout << fmt::format( "[i] evaluation time ({:>5.2f} secs)\n", to_seconds( time_eval ) ); - std::cout << fmt::format( "[i] substitute ({:>5.2f} secs)\n", to_seconds( time_substitute ) ); - std::cout << fmt::format( "[i] total divisors = {:8d}\n", ( num_total_divisors ) ); - std::cout << fmt::format( "[i] total leaves = {:8d}\n", ( num_total_leaves ) ); - std::cout << fmt::format( "[i] estimated gain = {:8d} ({:>5.2f}%)\n", - estimated_gain, ( ( 100.0 * estimated_gain ) / initial_size ) ); + // clang-format off + std::cout << "[i] \n"; + std::cout << "[i] ======== Stats ========\n"; + std::cout << fmt::format( "[i] #divisors = {:8d}\n", num_total_divisors ); + std::cout << fmt::format( "[i] est. gain = {:8d} ({:>5.2f}%)\n", estimated_gain, ( 100.0 * estimated_gain ) / initial_size ); + std::cout << "[i] ======== Runtime ========\n"; + std::cout << fmt::format( "[i] total : {:>5.2f} secs\n", to_seconds( time_total ) ); + std::cout << fmt::format( "[i] DivCollector: {:>5.2f} secs\n", to_seconds( time_divs ) ); + std::cout << fmt::format( "[i] ResubEngine : {:>5.2f} secs\n", to_seconds( time_resub ) ); + std::cout << fmt::format( "[i] callback : {:>5.2f} secs\n", to_seconds( time_callback ) ); + std::cout << "[i] =========================\n\n"; + // clang-format on } }; namespace detail { -/* based on abcRefs.c */ template -class node_mffc_inside +bool substitute_fn( Ntk& ntk, typename Ntk::node const& n, typename Ntk::signal const& g ) { -public: - using node = typename Ntk::node; - -public: - explicit node_mffc_inside( Ntk const& ntk ) - : ntk( ntk ) - { - } - - int32_t run( node const& n, std::vector const& leaves, std::vector& inside ) - { - /* increment the fanout counters for the leaves */ - for ( const auto& l : leaves ) - ntk.incr_fanout_size( l ); + ntk.substitute_node( n, g ); + return true; +}; - /* dereference the node */ - auto count1 = node_deref_rec( n ); +template +bool report_fn( Ntk& ntk, typename Ntk::node const& n, typename Ntk::signal const& g ) +{ + (void)ntk; + std::cout << "substitute node " << unsigned( n ) << " with node " << unsigned( ntk.get_node( g ) ) << std::endl; + return false; +}; - /* collect the nodes inside the MFFC */ - node_mffc_cone( n, inside ); +struct default_collector_stats +{ + /*! \brief Total number of leaves */ + uint64_t num_total_leaves{0}; - /* reference it back */ - auto count2 = node_ref_rec( n ); - (void)count2; - assert( count1 == count2 ); + /*! \brief Accumulated runtime for cut computation. */ + stopwatch<>::duration time_cuts{0}; - for ( const auto& l : leaves ) - ntk.decr_fanout_size( l ); + /*! \brief Accumulated runtime for mffc computation. */ + stopwatch<>::duration time_mffc{0}; - return count1; - } + /*! \brief Accumulated runtime for divisor computation. */ + stopwatch<>::duration time_divs{0}; -private: - /* ! \brief Dereference the node's MFFC */ - int32_t node_deref_rec( node const& n ) + void report() const { - if ( ntk.is_pi( n ) ) - return 0; - - int32_t counter = 1; - ntk.foreach_fanin( n, [&]( const auto& f ) { - auto const& p = ntk.get_node( f ); + // clang-format off + std::cout << "[i] \n"; + std::cout << fmt::format( "[i] #leaves = {:6d}\n", num_total_leaves ); + std::cout << "[i] ======== Runtime ========\n"; + std::cout << fmt::format( "[i] reconv. cut : {:>5.2f} secs\n", to_seconds( time_cuts ) ); + std::cout << fmt::format( "[i] MFFC : {:>5.2f} secs\n", to_seconds( time_mffc ) ); + std::cout << fmt::format( "[i] divs collect: {:>5.2f} secs\n", to_seconds( time_divs ) ); + std::cout << "[i] =========================\n\n"; + // clang-format on + } +}; - ntk.decr_fanout_size( p ); - if ( ntk.fanout_size( p ) == 0 ) - { - counter += node_deref_rec( p ); - } - } ); +/*! \brief Prepare the three public data members `leaves`, `divs` and `MFFC` + * to be ready for usage. + * + * `leaves`: sufficient support for all divisors + * `divs`: divisor nodes that can be used for resubstitution + * `MFFC`: MFFC nodes which are needed to do simulation from + * `leaves`, through `divs` and `MFFC` until the root node, + * but should be excluded from resubstitution. + * The last element of `MFFC` is always the root node. + * + * `divs` and `MFFC` are in topological order. + * + * \param MffcMgr Manager class to compute the potential gain if a + * resubstitution exists (number of MFFC nodes when the cost function is circuit size). + * \param MffcRes Typename of the return value of `MffcMgr`. + * \param CutMgr Manager class to compute the cut to construct the window. + */ +template, typename MffcRes = uint32_t, class CutMgr = cut_manager> +class default_divisor_collector +{ +public: + using stats = default_collector_stats; + using mffc_result_t = MffcRes; + using node = typename Ntk::node; - return counter; +public: + explicit default_divisor_collector( Ntk const& ntk, resubstitution_params const& ps, stats& st ) + : ntk( ntk ), ps( ps ), st( st ), cut_mgr( ps.max_pis ) + { } - /* ! \brief Reference the node's MFFC */ - int32_t node_ref_rec( node const& n ) + bool run( node const& n, mffc_result_t& potential_gain ) { - if ( ntk.is_pi( n ) ) - return 0; + /* skip nodes with many fanouts */ + if ( ntk.fanout_size( n ) > ps.skip_fanout_limit_for_roots ) + { + return false; + } - int32_t counter = 1; - ntk.foreach_fanin( n, [&]( const auto& f ) { - auto const& p = ntk.get_node( f ); + /* compute a reconvergence-driven cut */ + leaves = call_with_stopwatch( st.time_cuts, [&]() { + return reconv_driven_cut( cut_mgr, ntk, n ); + }); + st.num_total_leaves += leaves.size(); - auto v = ntk.fanout_size( p ); - ntk.incr_fanout_size( p ); - if ( v == 0 ) - { - counter += node_ref_rec( p ); - } - } ); + /* collect the MFFC */ + MffcMgr mffc_mgr( ntk ); + potential_gain = call_with_stopwatch( st.time_mffc, [&]() { + return mffc_mgr.run( n, leaves, MFFC ); + }); + + /* collect the divisor nodes in the cut */ + bool div_comp_success = call_with_stopwatch( st.time_divs, [&]() { + return collect_divisors( n ); + }); - return counter; + if ( !div_comp_success ) + { + return false; + } + + return true; } - void node_mffc_cone_rec( node const& n, std::vector& cone, bool top_most ) +private: + void collect_divisors_rec( node const& n ) { /* skip visited nodes */ if ( ntk.visited( n ) == ntk.trav_id() ) + { return; + } ntk.set_visited( n, ntk.trav_id() ); - if ( !top_most && ( ntk.is_pi( n ) || ntk.fanout_size( n ) > 0 ) ) - return; - - /* recurse on children */ ntk.foreach_fanin( n, [&]( const auto& f ) { - node_mffc_cone_rec( ntk.get_node( f ), cone, false ); + collect_divisors_rec( ntk.get_node( f ) ); } ); /* collect the internal nodes */ - cone.emplace_back( n ); + if ( ntk.value( n ) == 0 && n != 0 ) /* ntk.fanout_size( n ) */ + { + divs.emplace_back( n ); + } } - void node_mffc_cone( node const& n, std::vector& cone ) + bool collect_divisors( node const& root ) { - cone.clear(); - ntk.incr_trav_id(); - node_mffc_cone_rec( n, cone, true ); - } + /* add the leaves of the cuts to the divisors */ + divs.clear(); -private: - Ntk const& ntk; -}; + ntk.incr_trav_id(); + for ( const auto& l : leaves ) + { + divs.emplace_back( l ); + ntk.set_visited( l, ntk.trav_id() ); + } -template -class simulator -{ -public: - using node = typename Ntk::node; - using signal = typename Ntk::signal; - using truthtable_t = TT; + /* mark nodes in the MFFC */ + for ( const auto& t : MFFC ) + { + ntk.set_value( t, 1 ); + } - explicit simulator( Ntk const& ntk, uint32_t num_divisors, uint32_t max_pis ) - : ntk( ntk ), num_divisors( num_divisors ), tts( num_divisors + 1 ), node_to_index( ntk.size(), 0u ), phase( ntk.size(), false ) - { - auto tt = kitty::create( max_pis ); - tts[0] = tt; + /* collect the cone (without MFFC) */ + collect_divisors_rec( root ); - for ( auto i = 0u; i < tt.num_vars(); ++i ) + /* unmark the current MFFC */ + for ( const auto& t : MFFC ) { - kitty::create_nth_var( tt, i ); - tts[i + 1] = tt; + ntk.set_value( t, 0 ); } - } - void resize() - { - if ( ntk.size() > node_to_index.size() ) - node_to_index.resize( ntk.size(), 0u ); - if ( ntk.size() > phase.size() ) - phase.resize( ntk.size(), false ); - } - - void assign( node const& n, uint32_t index ) - { - assert( n < node_to_index.size() ); - assert( index < num_divisors + 1 ); - node_to_index[n] = index; - } + /* check if the number of divisors is not exceeded */ + if ( divs.size() - leaves.size() + MFFC.size() >= ps.max_divisors - ps.max_pis ) + { + return false; + } - truthtable_t get_tt( signal const& s ) const - { - auto const tt = tts.at( node_to_index.at( ntk.get_node( s ) ) ); - return ntk.is_complemented( s ) ? ~tt : tt; - } + /* get the number of divisors to collect */ + int32_t limit = ps.max_divisors - ps.max_pis - ( uint32_t( divs.size() ) + 1 - uint32_t( leaves.size() ) + uint32_t( MFFC.size() ) ); - void set_tt( uint32_t index, truthtable_t const& tt ) - { - tts[index] = tt; - } + /* explore the fanouts, which are not in the MFFC */ + int32_t counter = 0; + bool quit = false; - void normalize( std::vector const& nodes ) - { - for ( const auto& n : nodes ) + /* NOTE: this is tricky and cannot be converted to a range-based loop */ + auto size = divs.size(); + for ( auto i = 0u; i < size; ++i ) { - assert( n < phase.size() ); - assert( n < node_to_index.size() ); - - if ( n == 0 ) - return; + auto const d = divs.at( i ); - auto& tt = tts[node_to_index.at( n )]; - if ( kitty::get_bit( tt, 0 ) ) + if ( ntk.fanout_size( d ) > ps.skip_fanout_limit_for_divisors ) { - tt = ~tt; - phase[n] = true; + continue; } - else + + /* if the fanout has all fanins in the set, add it */ + ntk.foreach_fanout( d, [&]( node const& p ) { + if ( ntk.visited( p ) == ntk.trav_id() ) + { + return true; /* next fanout */ + } + + bool all_fanins_visited = true; + ntk.foreach_fanin( p, [&]( const auto& g ) { + if ( ntk.visited( ntk.get_node( g ) ) != ntk.trav_id() ) + { + all_fanins_visited = false; + return false; /* terminate fanin-loop */ + } + return true; /* next fanin */ + } ); + + if ( !all_fanins_visited ) + return true; /* next fanout */ + + bool has_root_as_child = false; + ntk.foreach_fanin( p, [&]( const auto& g ) { + if ( ntk.get_node( g ) == root ) + { + has_root_as_child = true; + return false; /* terminate fanin-loop */ + } + return true; /* next fanin */ + } ); + + if ( has_root_as_child ) + { + return true; /* next fanout */ + } + + divs.emplace_back( p ); + ++size; + ntk.set_visited( p, ntk.trav_id() ); + + /* quit computing divisors if there are too many of them */ + if ( ++counter == limit ) + { + quit = true; + return false; /* terminate fanout-loop */ + } + + return true; /* next fanout */ + } ); + + if ( quit ) { - phase[n] = false; + break; } } - } - bool get_phase( node const& n ) const - { - assert( n < phase.size() ); - return phase.at( n ); + /* Note: different from the previous version, now we do not add MFFC nodes into divs */ + assert( root == MFFC.at( MFFC.size() - 1u ) ); + assert( divs.size() + MFFC.size() - leaves.size() <= ps.max_divisors - ps.max_pis ); + + return true; } private: Ntk const& ntk; - uint32_t num_divisors; + resubstitution_params const& ps; + stats& st; - std::vector tts; - std::vector node_to_index; - std::vector phase; -}; /* simulator */ + CutMgr cut_mgr; -struct default_resub_functor_stats +public: + std::vector leaves; + std::vector divs; + std::vector MFFC; +}; + +template +struct window_resub_stats { - /*! \brief Accumulated runtime for const-resub */ - stopwatch<>::duration time_resubC{0}; + /*! \brief Number of successful resubstitutions. */ + uint32_t num_resub{0}; + + /*! \brief Time for simulation. */ + stopwatch<>::duration time_sim{0}; - /*! \brief Accumulated runtime for zero-resub */ - stopwatch<>::duration time_resub0{0}; + /*! \brief Time for don't-care computation. */ + stopwatch<>::duration time_dont_care{0}; - /*! \brief Number of accepted constant resubsitutions */ - uint32_t num_const_accepts{0}; + /*! \brief Time of the resub functor. */ + stopwatch<>::duration time_compute_function{0}; - /*! \brief Number of accepted zero resubsitutions */ - uint32_t num_div0_accepts{0}; + ResubFnSt functor_st; void report() const { - std::cout << "[i] kernel: default_resub_functor\n"; - std::cout << fmt::format( "[i] constant-resub {:6d} ({:>5.2f} secs)\n", - num_const_accepts, to_seconds( time_resubC ) ); - std::cout << fmt::format( "[i] 0-resub {:6d} ({:>5.2f} secs)\n", - num_div0_accepts, to_seconds( time_resub0 ) ); - std::cout << fmt::format( "[i] total {:6d}\n", - ( num_const_accepts + num_div0_accepts ) ); + // clang-format off + std::cout << "[i] \n"; + std::cout << fmt::format( "[i] #resub = {:6d}\n", num_resub ); + std::cout << "[i] ======== Runtime ========\n"; + std::cout << fmt::format( "[i] simulation: {:>5.2f} secs\n", to_seconds( time_sim ) ); + std::cout << fmt::format( "[i] don't care: {:>5.2f} secs\n", to_seconds( time_dont_care ) ); + std::cout << fmt::format( "[i] functor : {:>5.2f} secs\n", to_seconds( time_compute_function ) ); + std::cout << "[i] ======== Details ========\n"; + functor_st.report(); + std::cout << "[i] =========================\n\n"; + // clang-format on } }; -template -class default_resub_functor +/*! \brief Window-based resubstitution engine. + * + * This engine computes the complete truth tables of nodes within a window + * with the leaves as inputs. It does not verify the resubstitution candidates + * given by the resubstitution functor. This engine requires the divisor + * collector to prepare three data members: `leaves`, `divs` and `MFFC`. + * + * Required interfaces of the resubstitution functor: + * - Constructor: `resub_fn( Ntk const& ntk, Simulator const& sim,` + * `std::vector const& divs, uint32_t num_divs, default_resub_functor_stats& st )` + * - A public `operator()`: `std::optional operator()` + * `( node const& root, TTdc care, uint32_t required, uint32_t max_inserts,` + * `uint32_t potential_gain, uint32_t& last_gain ) const` + * + * Compatible resubstitution functors implemented: + * - `default_resub_functor` + * - `aig_resub_functor` + * - `mig_resub_functor` + * - `xmg_resub_functor` + * - `xag_resub_functor` + * + * \param TTsim Truth table type for simulation. + * \param TTdc Truth table type for don't-care computation. + * \param ResubFn Resubstitution functor to compute the resubstitution. + * \param MffcRes Typename of `potential_gain` needed by the resubstitution functor. + */ +template, TTdc>, typename MffcRes = uint32_t> +class window_based_resub_engine { public: + static constexpr bool require_leaves_and_MFFC = true; + using stats = window_resub_stats; + using mffc_result_t = MffcRes; + using node = typename Ntk::node; using signal = typename Ntk::signal; - using stats = default_resub_functor_stats; - explicit default_resub_functor( Ntk const& ntk, Simulator const& sim, std::vector const& divs, uint32_t num_divs, default_resub_functor_stats& st ) - : ntk( ntk ), sim( sim ), divs( divs ), num_divs( num_divs ), st( st ) + explicit window_based_resub_engine( Ntk& ntk, resubstitution_params const& ps, stats& st ) + : ntk( ntk ), ps( ps ), st( st ), sim( ntk, ps.max_divisors, ps.max_pis ) { } - std::optional operator()( node const& root, TT care, uint32_t required, uint32_t max_inserts, uint32_t num_mffc, uint32_t& last_gain ) const + std::optional run( node const& n, std::vector const& leaves, std::vector const& divs, std::vector const& MFFC, mffc_result_t potential_gain, uint32_t& last_gain ) { - /* The default resubstitution functor does not insert any gates - and consequently does not use the argument `max_inserts`. Other - functors, however, make use of this argument. */ - (void)care; - (void)max_inserts; - assert( kitty::is_const0( ~care ) ); - - /* consider constants */ - auto g = call_with_stopwatch( st.time_resubC, [&]() { - return resub_const( root, required ); - } ); - if ( g ) - { - ++st.num_const_accepts; - last_gain = num_mffc; - return g; /* accepted resub */ - } + /* simulate the collected divisors */ + call_with_stopwatch( st.time_sim, [&]() { + simulate( leaves, divs, MFFC ); + }); - /* consider equal nodes */ - g = call_with_stopwatch( st.time_resub0, [&]() { - return resub_div0( root, required ); - } ); - if ( g ) + auto care = kitty::create( static_cast( leaves.size() ) ); + call_with_stopwatch( st.time_dont_care, [&]() { + if ( ps.use_dont_cares ) + { + care = ~satisfiability_dont_cares( ntk, leaves, ps.window_size ); + } + else + { + care = ~care; + } + }); + + ResubFn resub_fn( ntk, sim, divs, divs.size(), st.functor_st ); + auto res = call_with_stopwatch( st.time_compute_function, [&]() { + return resub_fn( n, care, std::numeric_limits::max(), ps.max_inserts, potential_gain, last_gain ); + }); + if ( res ) { - ++st.num_div0_accepts; - last_gain = num_mffc; - ; - return g; /* accepted resub */ + ++st.num_resub; } - - return std::nullopt; + return res; } private: - std::optional resub_const( node const& root, uint32_t required ) const + void simulate( std::vector const& leaves, std::vector const& divs, std::vector const& MFFC ) { - (void)required; - auto const tt = sim.get_tt( ntk.make_signal( root ) ); - if ( tt == sim.get_tt( ntk.get_constant( false ) ) ) + sim.resize(); + for ( auto i = 0u; i < divs.size() + MFFC.size(); ++i ) { - return sim.get_phase( root ) ? ntk.get_constant( true ) : ntk.get_constant( false ); - } - return std::nullopt; - } + const auto d = i < divs.size() ? divs.at( i ) : MFFC.at( i - divs.size() ); - std::optional resub_div0( node const& root, uint32_t required ) const - { - (void)required; - auto const tt = sim.get_tt( ntk.make_signal( root ) ); - for ( const auto& d : divs ) - { - if ( root == d ) - break; + /* skip constant 0 */ + if ( d == 0 ) + continue; + + /* assign leaves to variables */ + if ( i < leaves.size() ) + { + sim.assign( d, i + 1 ); + continue; + } - if ( tt != sim.get_tt( ntk.make_signal( d ) ) ) - continue; /* next */ + /* compute truth tables of inner nodes */ + sim.assign( d, i - uint32_t( leaves.size() ) + ps.max_pis + 1 ); + std::vector tts; + ntk.foreach_fanin( d, [&]( const auto& s ) { + tts.emplace_back( sim.get_tt( ntk.make_signal( ntk.get_node( s ) ) ) ); /* ignore sign */ + } ); - return ( sim.get_phase( d ) ^ sim.get_phase( root ) ) ? !ntk.make_signal( d ) : ntk.make_signal( d ); + auto const tt = ntk.compute( d, tts.begin(), tts.end() ); + sim.set_tt( i - uint32_t( leaves.size() ) + ps.max_pis + 1, tt ); } - return std::nullopt; + /* normalize truth tables */ + sim.normalize( divs ); + sim.normalize( MFFC ); } private: - Ntk const& ntk; - Simulator const& sim; - std::vector const& divs; - uint32_t num_divs; + Ntk& ntk; + resubstitution_params const& ps; stats& st; -}; /* default_resub_functor */ -template + window_simulator sim; +}; /* window_based_resub_engine */ + +/*! \brief The top-level resubstitution framework. + * + * \param ResubEngine The engine that computes the resubtitution for a given root + * node and divisors. One can choose from `window_based_resub_engine` which + * does complete simulation within small windows, or `simulation_based_resub_engine` + * which does partial simulation on the whole circuit. + * + * \param DivCollector Collects divisors near a given root node, and compute + * the potential gain (MFFC size or its variants). + * Currently only `default_divisor_collector` is implemented, but + * a frontier-based approach may be integrated in the future. + * When using `window_based_resub_engine`, the `DivCollector` should prepare + * three public data members: `leaves`, `divs`, and `MFFC` (see documentation + * of `default_divisor_collector` for details). When using `simulation_based_resub_engine`, + * only `divs` is needed. + */ +template, class DivCollector = default_divisor_collector> class resubstitution_impl { public: + using engine_st_t = typename ResubEngine::stats; + using collector_st_t = typename DivCollector::stats; using node = typename Ntk::node; using signal = typename Ntk::signal; - - explicit resubstitution_impl( Ntk& ntk, resubstitution_params const& ps, resubstitution_stats& st, typename ResubFn::stats& resub_st ) - : ntk( ntk ), sim( ntk, ps.max_divisors, ps.max_pis ), ps( ps ), st( st ), resub_st( resub_st ) + using resub_callback_t = std::function; + using mffc_result_t = typename ResubEngine::mffc_result_t; + + /*! \brief Constructor of the top-level resubstitution framework. + * + * \param ntk The network to be optimized. + * \param ps Resubstitution parameters. + * \param st Top-level resubstitution statistics. + * \param engine_st Statistics of the resubstitution engine. + * \param collector_st Statistics of the divisor collector. + * \param callback Callback function when a resubstitution is found. + */ + explicit resubstitution_impl( Ntk& ntk, resubstitution_params const& ps, resubstitution_stats& st, engine_st_t& engine_st, collector_st_t& collector_st ) + : ntk( ntk ), ps( ps ), st( st ), engine_st( engine_st ), collector_st( collector_st ) { + static_assert( std::is_same_v, "MFFC result type of the engine and the collector are different" ); + st.initial_size = ntk.num_gates(); auto const update_level_of_new_node = [&]( const auto& n ) { @@ -481,38 +626,55 @@ class resubstitution_impl ntk._events->on_delete.emplace_back( update_level_of_deleted_node ); } - void run() + void run( resub_callback_t const& callback = substitute_fn ) { stopwatch t( st.time_total ); /* start the managers */ - cut_manager mgr( ps.max_pis ); + DivCollector collector( ntk, ps, collector_st ); + ResubEngine resub_engine( ntk, ps, engine_st ); progress_bar pbar{ntk.size(), "resub |{0}| node = {1:>4} cand = {2:>4} est. gain = {3:>5}", ps.progress}; auto const size = ntk.num_gates(); ntk.foreach_gate( [&]( auto const& n, auto i ) { if ( i >= size ) + { return false; /* terminate */ + } pbar( i, i, candidates, st.estimated_gain ); if ( ntk.is_dead( n ) ) + { return true; /* next */ + } - /* skip nodes with many fanouts */ - if ( ntk.fanout_size( n ) > ps.skip_fanout_limit_for_roots ) + /* compute cut, collect divisors, compute MFFC */ + mffc_result_t potential_gain; + const auto collector_success = call_with_stopwatch( st.time_divs, [&]() { + return collector.run( n, potential_gain ); + }); + if ( !collector_success ) + { return true; /* next */ + } - /* compute a reconvergence-driven cut */ - auto const leaves = call_with_stopwatch( st.time_cuts, [&]() { - return reconv_driven_cut( mgr, ntk, n ); - } ); + /* update statistics */ + last_gain = 0; + st.num_total_divisors += collector.divs.size(); - /* evaluate this cut */ - auto const g = call_with_stopwatch( st.time_eval, [&]() { - return evaluate( n, leaves ); - } ); + /* try to find a resubstitution with the divisors */ + auto g = call_with_stopwatch( st.time_resub, [&]() { + if constexpr ( ResubEngine::require_leaves_and_MFFC ) /* window-based */ + { + return resub_engine.run( n, collector.leaves, collector.divs, collector.MFFC, potential_gain, last_gain ); + } + else /* simulation-based */ + { + return resub_engine.run( n, collector.divs, potential_gain, last_gain ); + } + }); if ( !g ) { return true; /* next */ @@ -523,8 +685,8 @@ class resubstitution_impl st.estimated_gain += last_gain; /* update network */ - call_with_stopwatch( st.time_substitute, [&]() { - ntk.substitute_node( n, *g ); + call_with_stopwatch( st.time_callback, [&]() { + return callback( ntk, n, *g ); } ); return true; /* next */ @@ -532,6 +694,7 @@ class resubstitution_impl } private: + /* maybe should move to depth_view */ void update_node_level( node const& n, bool top_most = true ) { uint32_t curr_level = ntk.level( n ); @@ -561,249 +724,24 @@ class resubstitution_impl } } - void simulate( std::vector const& leaves ) - { - sim.resize(); - for ( auto i = 0u; i < divs.size(); ++i ) - { - const auto d = divs.at( i ); - - /* skip constant 0 */ - if ( d == 0 ) - continue; - - /* assign leaves to variables */ - if ( i < leaves.size() ) - { - sim.assign( d, i + 1 ); - continue; - } - - /* compute truth tables of inner nodes */ - sim.assign( d, i - uint32_t( leaves.size() ) + ps.max_pis + 1 ); - std::vector tts; - ntk.foreach_fanin( d, [&]( const auto& s, auto i ) { - (void)i; - tts.emplace_back( sim.get_tt( ntk.make_signal( ntk.get_node( s ) ) ) ); /* ignore sign */ - } ); - - auto const tt = ntk.compute( d, tts.begin(), tts.end() ); - sim.set_tt( i - uint32_t( leaves.size() ) + ps.max_pis + 1, tt ); - } - - /* normalize truth tables */ - sim.normalize( divs ); - } - - std::optional evaluate( node const& root, std::vector const& leaves ) - { - uint32_t const required = std::numeric_limits::max(); - - last_gain = 0; - - /* collect the MFFC */ - auto num_mffc = call_with_stopwatch( st.time_mffc, [&]() { - Node_mffc collector( ntk ); - auto num_mffc = collector.run( root, leaves, temp ); - return num_mffc; - } ); - - /* collect the divisor nodes in the cut */ - bool div_comp_success = call_with_stopwatch( st.time_divs, [&]() { - return collect_divisors( root, leaves, required ); - } ); - - if ( !div_comp_success ) - { - return std::nullopt; - } - - /* update statistics */ - st.num_total_divisors += num_divs; - st.num_total_leaves += leaves.size(); - - /* simulate the collected divisors */ - call_with_stopwatch( st.time_simulation, [&]() { simulate( leaves ); } ); - - auto care = kitty::create( static_cast( leaves.size() ) ); - if ( ps.use_dont_cares ) - care = ~satisfiability_dont_cares( ntk, leaves, ps.window_size ); - else - care = ~care; - - ResubFn resub_fn( ntk, sim, divs, num_divs, resub_st ); - return resub_fn( root, care, required, ps.max_inserts, num_mffc, last_gain ); - } - - void collect_divisors_rec( node const& n, std::vector& internal ) - { - /* skip visited nodes */ - if ( ntk.visited( n ) == ntk.trav_id() ) - return; - ntk.set_visited( n, ntk.trav_id() ); - - ntk.foreach_fanin( n, [&]( const auto& f ) { - collect_divisors_rec( ntk.get_node( f ), internal ); - } ); - - /* collect the internal nodes */ - if ( ntk.value( n ) == 0 && n != 0 ) /* ntk.fanout_size( n ) */ - internal.emplace_back( n ); - } - - bool collect_divisors( node const& root, std::vector const& leaves, uint32_t required ) - { - /* add the leaves of the cuts to the divisors */ - divs.clear(); - - ntk.incr_trav_id(); - for ( const auto& l : leaves ) - { - divs.emplace_back( l ); - ntk.set_visited( l, ntk.trav_id() ); - } - - /* mark nodes in the MFFC */ - for ( const auto& t : temp ) - ntk.set_value( t, 1 ); - - /* collect the cone (without MFFC) */ - collect_divisors_rec( root, divs ); - - /* unmark the current MFFC */ - for ( const auto& t : temp ) - ntk.set_value( t, 0 ); - - /* check if the number of divisors is not exceeded */ - if ( divs.size() - leaves.size() + temp.size() >= ps.max_divisors - ps.max_pis ) - return false; - - /* get the number of divisors to collect */ - int32_t limit = ps.max_divisors - ps.max_pis - ( uint32_t( divs.size() ) + 1 - uint32_t( leaves.size() ) + uint32_t( temp.size() ) ); - - /* explore the fanouts, which are not in the MFFC */ - int32_t counter = 0; - bool quit = false; - - /* NOTE: this is tricky and cannot be converted to a range-based loop */ - auto size = divs.size(); - for ( auto i = 0u; i < size; ++i ) - { - auto const d = divs.at( i ); - - if ( ntk.fanout_size( d ) > ps.skip_fanout_limit_for_divisors ) - continue; - - /* if the fanout has all fanins in the set, add it */ - ntk.foreach_fanout( d, [&]( node const& p ) { - if ( ntk.visited( p ) == ntk.trav_id() || ntk.level( p ) > required ) - return true; /* next fanout */ - - bool all_fanins_visited = true; - ntk.foreach_fanin( p, [&]( const auto& g ) { - if ( ntk.visited( ntk.get_node( g ) ) != ntk.trav_id() ) - { - all_fanins_visited = false; - return false; /* terminate fanin-loop */ - } - return true; /* next fanin */ - } ); - - if ( !all_fanins_visited ) - return true; /* next fanout */ - - bool has_root_as_child = false; - ntk.foreach_fanin( p, [&]( const auto& g ) { - if ( ntk.get_node( g ) == root ) - { - has_root_as_child = true; - return false; /* terminate fanin-loop */ - } - return true; /* next fanin */ - } ); - - if ( has_root_as_child ) - return true; /* next fanout */ - - divs.emplace_back( p ); - ++size; - ntk.set_visited( p, ntk.trav_id() ); - - /* quit computing divisors if there are too many of them */ - if ( ++counter == limit ) - { - quit = true; - return false; /* terminate fanout-loop */ - } - - return true; /* next fanout */ - } ); - - if ( quit ) - break; - } - - /* get the number of divisors */ - num_divs = uint32_t( divs.size() ); - - /* add the nodes in the MFFC */ - for ( const auto& t : temp ) - { - divs.emplace_back( t ); - } - - assert( root == divs.at( divs.size() - 1u ) ); - assert( divs.size() - leaves.size() <= ps.max_divisors - ps.max_pis ); - - return true; - } - private: Ntk& ntk; - Simulator sim; resubstitution_params const& ps; resubstitution_stats& st; - typename ResubFn::stats& resub_st; + engine_st_t& engine_st; + collector_st_t& collector_st; /* temporary statistics for progress bar */ uint32_t candidates{0}; uint32_t last_gain{0}; - - std::vector temp; - std::vector divs; - uint32_t num_divs{0}; }; } /* namespace detail */ -/*! \brief Boolean resubstitution. - * - * **Required network functions:** - * - `clear_values` - * - `fanout_size` - * - `foreach_fanin` - * - `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 Input network (will be changed in-place) - * \param ps Resubstitution params - * \param pst Resubstitution statistics - */ +/*! \brief Window-based Boolean resubstitution with default resub functor (only div0). */ template -void resubstitution( Ntk& ntk, resubstitution_params const& ps = {}, resubstitution_stats* pst = nullptr ) +void default_resubstitution( Ntk& ntk, resubstitution_params const& ps = {}, resubstitution_stats* pst = nullptr ) { static_assert( is_network_type_v, "Ntk is not a network type" ); static_assert( has_clear_values_v, "Ntk does not implement the clear_values method" ); @@ -818,51 +756,62 @@ void resubstitution( Ntk& ntk, resubstitution_params const& ps = {}, resubstitut static_assert( has_make_signal_v, "Ntk does not implement the make_signal method" ); static_assert( has_set_value_v, "Ntk does not implement the set_value method" ); static_assert( has_set_visited_v, "Ntk does not implement the set_visited method" ); - static_assert( has_size_v, "Ntk does not implement the has_size method" ); - static_assert( has_substitute_node_v, "Ntk does not implement the has substitute_node method" ); - static_assert( has_value_v, "Ntk does not implement the has_value method" ); - static_assert( has_visited_v, "Ntk does not implement the has_visited method" ); + static_assert( has_size_v, "Ntk does not implement the size method" ); + static_assert( has_substitute_node_v, "Ntk does not implement the substitute_node method" ); + static_assert( has_value_v, "Ntk does not implement the value method" ); + static_assert( has_visited_v, "Ntk does not implement the visited method" ); using resub_view_t = fanout_view>; depth_view depth_view{ntk}; resub_view_t resub_view{depth_view}; - resubstitution_stats st; if ( ps.max_pis == 8 ) { using truthtable_t = kitty::static_truth_table<8>; using truthtable_dc_t = kitty::dynamic_truth_table; - using simulator_t = detail::simulator; - using node_mffc_t = detail::node_mffc_inside; - using resubstitution_functor_t = detail::default_resub_functor; - typename resubstitution_functor_t::stats resub_st; - detail::resubstitution_impl p( resub_view, ps, st, resub_st ); + using resub_impl_t = detail::resubstitution_impl>; + + 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( resub_view, ps, st, engine_st, collector_st ); p.run(); + if ( ps.verbose ) { st.report(); - resub_st.report(); + collector_st.report(); + engine_st.report(); + } + + if ( pst ) + { + *pst = st; } } else { - using truthtable_t = kitty::dynamic_truth_table; - using simulator_t = detail::simulator; - using node_mffc_t = detail::node_mffc_inside; - using resubstitution_functor_t = detail::default_resub_functor; - typename resubstitution_functor_t::stats resub_st; - detail::resubstitution_impl p( resub_view, ps, st, resub_st ); + using resub_impl_t = detail::resubstitution_impl; + + 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( resub_view, ps, st, engine_st, collector_st ); p.run(); + if ( ps.verbose ) { st.report(); - resub_st.report(); + collector_st.report(); + engine_st.report(); } - } - if ( pst ) - { - *pst = st; + if ( pst ) + { + *pst = st; + } } } diff --git a/include/mockturtle/algorithms/sim_resub.hpp b/include/mockturtle/algorithms/sim_resub.hpp new file mode 100644 index 000000000..082413544 --- /dev/null +++ b/include/mockturtle/algorithms/sim_resub.hpp @@ -0,0 +1,1020 @@ +/* mockturtle: C++ logic network library + * Copyright (C) 2018-2020 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. + */ + +/*! + \file sim_resub.hpp + \brief Simulation-Guided Resubstitution + + \author Siang-Yun Lee +*/ + +#pragma once + +#include +#include + +#include "../utils/abc_resub.hpp" +#include "../utils/progress_bar.hpp" +#include "../utils/stopwatch.hpp" +#include "../utils/abc_resub.hpp" + +#include +#include +#include + +#include +#include +#include +#include +#include +#include +#include + +namespace mockturtle +{ + +namespace detail +{ + +/*! \brief Wrapper class of an imaginary circuit to be verified by `circuit_validator` */ +template +struct imaginary_circuit +{ + using node = typename Ntk::node; + using vgate = typename validator_t::gate; + + std::vector const& divs; + std::vector const ckt; + bool const out_neg; +}; + +struct sim_aig_resub_functor_stats +{ + /*! \brief Accumulated runtime for const-resub */ + stopwatch<>::duration time_resubC{0}; + + /*! \brief Accumulated runtime for zero-resub */ + stopwatch<>::duration time_resub0{0}; + + /*! \brief Accumulated runtime for collecting unate divisors. */ + stopwatch<>::duration time_collect_unate_divisors{0}; + + /*! \brief Accumulated runtime for one-resub */ + stopwatch<>::duration time_resub1{0}; + + /*! \brief Number of accepted constant resubsitutions */ + uint32_t num_const_accepts{0}; + + /*! \brief Number of accepted zero resubsitutions */ + uint32_t num_div0_accepts{0}; + + /*! \brief Total number of unate divisors */ + uint64_t num_unate_divisors{0}; + + /*! \brief Number of accepted one resubsitutions */ + uint64_t num_div1_accepts{0}; + + /*! \brief Number of accepted single AND-resubsitutions */ + uint64_t num_div1_and_accepts{0}; + + /*! \brief Number of accepted single OR-resubsitutions */ + uint64_t num_div1_or_accepts{0}; + + void report() const + { + // clang-format off + std::cout << "[i] \n"; + std::cout << fmt::format( "[i] #const = {:6d} ({:>5.2f} secs)\n", num_const_accepts, to_seconds( time_resubC ) ); + std::cout << fmt::format( "[i] #div0 = {:6d} ({:>5.2f} secs)\n", num_div0_accepts, to_seconds( time_resub0 ) ); + std::cout << fmt::format( "[i] >#udivs = {:6d} ({:>5.2f} secs)\n", num_unate_divisors, to_seconds( time_collect_unate_divisors ) ); + std::cout << fmt::format( "[i] #div1 = {:6d} ({:>5.2f} secs)\n", num_div1_accepts, to_seconds( time_resub1 ) ); + std::cout << fmt::format( "[i] #div1-AND = {:6d}\n", num_div1_and_accepts ); + std::cout << fmt::format( "[i] #div1-OR = {:6d}\n", num_div1_or_accepts ); + // clang-format on + } +}; + +template +class sim_aig_resub_functor +{ +public: + using stats = sim_aig_resub_functor_stats; + using node = typename Ntk::node; + using signal = typename Ntk::signal; + using vgate = typename validator_t::gate; + using fanin = typename vgate::fanin; + using gtype = typename validator_t::gate_type; + using circuit = imaginary_circuit; + using result_t = typename std::variant; + + struct unate_divisors + { + using signal = typename Ntk::signal; + + std::vector> positive_divisors; + std::vector> negative_divisors; + + void clear() + { + positive_divisors.clear(); + negative_divisors.clear(); + } + + void sort() + { + std::sort(positive_divisors.begin(), positive_divisors.end(), [](std::pair a, std::pair b) { + return a.second > b.second; + }); + std::sort(negative_divisors.begin(), negative_divisors.end(), [](std::pair a, std::pair b) { + return a.second > b.second; + }); + } + }; + + explicit sim_aig_resub_functor( Ntk const& ntk, resubstitution_params const& ps, stats& st, unordered_node_map const& tts, node const& root, std::vector const& divs, uint32_t const num_inserts ) + : ntk( ntk ), ps( ps ), st( st ), tts( tts ), root( root ), divs( divs ), num_inserts( num_inserts ), step( 0 ), i( 0 ), j( 0 ) + { + } + + std::optional operator()( uint32_t& size ) + { + tt = tts[root]; + ntt = ~tt; + + while ( true ) + { + switch ( step ) + { + case 0u: + { + auto const& res = call_with_stopwatch( st.time_resubC, [&]() { + return resub_const(); + }); + if ( res ) + { + ++st.num_const_accepts; + size = 0; + return res; + } + else + { + ++step; + continue; + } + } + case 1u: + { + if ( i == divs.size() ) + { + if ( num_inserts == 0 ) + { + return std::nullopt; + } + call_with_stopwatch( st.time_collect_unate_divisors, [&]() { + collect_unate_divisors(); + }); + st.num_unate_divisors += udivs.positive_divisors.size() + udivs.negative_divisors.size(); + w = kitty::count_ones( tt ); + nw = tt.num_bits() - w; + i = 0; j = 1; + ++step; + if ( udivs.positive_divisors.size() < 2 ) + { + ++step; + if ( udivs.negative_divisors.size() < 2 ) + { + ++step; + } + } + continue; + } + + auto const& res = call_with_stopwatch( st.time_resub0, [&]() { + return resub_div0(); + }); + ++i; + if ( res ) + { + ++st.num_div0_accepts; + size = 0; + return res; + } + else + { + continue; + } + } + case 2u: + { + if ( j == udivs.positive_divisors.size() ) + { + break_div1_pos_inner(); + continue; + } + + auto const& res = call_with_stopwatch( st.time_resub1, [&]() { + return resub_div1_pos(); + }); + ++j; + if ( res ) + { + ++st.num_div1_accepts; + ++st.num_div1_or_accepts; + size = 1; + return res; + } + else + { + continue; + } + } + case 3u: + { + if ( j == udivs.negative_divisors.size() ) + { + break_div1_neg_inner(); + continue; + } + + auto const& res = call_with_stopwatch( st.time_resub1, [&]() { + return resub_div1_neg(); + }); + ++j; + if ( res ) + { + ++st.num_div1_accepts; + ++st.num_div1_and_accepts; + size = 1; + return res; + } + else + { + continue; + } + } + default: + { + return std::nullopt; + } + } + } + } + +private: + void collect_unate_divisors() + { + udivs.clear(); + + for ( auto const& d : divs ) + { + auto const& tt_d = tts[d]; + auto const ntt_d = ~tt_d; + + /* check positive containment */ + if ( kitty::implies( tt_d, tt ) ) + { + udivs.positive_divisors.emplace_back( std::make_pair( ntk.make_signal( d ), kitty::count_ones( tt_d & tt ) ) ); + continue; + } + if ( kitty::implies( ntt_d, tt ) ) + { + udivs.positive_divisors.emplace_back( std::make_pair( !ntk.make_signal( d ), kitty::count_ones( ntt_d & tt ) ) ); + continue; + } + + /* check negative containment */ + if ( kitty::implies( tt, tt_d ) ) + { + udivs.negative_divisors.emplace_back( std::make_pair( ntk.make_signal( d ), kitty::count_zeros( tt_d & tt ) ) ); + continue; + } + if ( kitty::implies( tt, ntt_d ) ) + { + udivs.negative_divisors.emplace_back( std::make_pair( !ntk.make_signal( d ), kitty::count_zeros( ntt_d & tt ) ) ); + continue; + } + } + + udivs.sort(); + } + + std::optional resub_const() + { + auto const& zero = tts[ntk.get_constant( false )]; + + if ( tt == zero ) + { + return result_t( ntk.get_constant( false ) ); + } + else if ( ntt == zero ) + { + return result_t( ntk.get_constant( true ) ); + } + + return std::nullopt; + } + + std::optional resub_div0() + { + auto const& d = divs.at( i ); + auto const& ttd = tts[d]; + + if ( tt == ttd ) + { + return result_t( ntk.make_signal( d ) ); + } + else if ( ntt == ttd ) + { + return result_t( !ntk.make_signal( d ) ); + } + + return std::nullopt; + } + + std::optional resub_div1_pos() + { + auto const& s0 = udivs.positive_divisors.at( i ).first; + auto const& tt_s0 = ntk.is_complemented( s0 ) ? ~tts[ntk.get_node( s0 )] : tts[ntk.get_node( s0 )]; + auto const& w_s0 = udivs.positive_divisors.at( i ).second; + if ( w_s0 < uint32_t( w / 2 ) ) /* break div1_pos */ + { + break_div1_pos(); + return std::nullopt; + } + + if ( w_s0 + udivs.positive_divisors.at( j ).second < w ) /* break inner loop */ + { + break_div1_pos_inner(); + return std::nullopt; + } + + auto const& s1 = udivs.positive_divisors.at( j ).first; + auto const& tt_s1 = ntk.is_complemented( s1 ) ? ~tts[ntk.get_node( s1 )] : tts[ntk.get_node( s1 )]; + + for ( auto b = 0u; b < tt.num_blocks(); ++b ) + { + if ( ( tt_s0._bits[b] | tt_s1._bits[b] ) != tt._bits[b] ) + { + return std::nullopt; + } + } + assert( tt == ( tt_s0 | tt_s1 ) ); + fanin fi1{0, !ntk.is_complemented( s0 )}; + fanin fi2{1, !ntk.is_complemented( s1 )}; + vgate gate{{fi1, fi2}, gtype::AND}; + tmp.resize( 2 ); tmp[0] = ntk.get_node( s0 ); tmp[1] = ntk.get_node( s1 ); + + return result_t( circuit{tmp, {gate}, true} ); + } + + std::optional resub_div1_neg() + { + auto const& s0 = udivs.negative_divisors.at( i ).first; + auto const& tt_s0 = ntk.is_complemented( s0 ) ? ~tts[ntk.get_node( s0 )] : tts[ntk.get_node( s0 )]; + auto const& w_s0 = udivs.negative_divisors.at( i ).second; + if ( w_s0 < uint32_t( nw / 2 ) ) /* break div1_neg */ + { + break_div1_neg(); + return std::nullopt; + } + + if ( w_s0 + udivs.negative_divisors.at( j ).second < nw ) /* break inner loop */ + { + break_div1_neg_inner(); + return std::nullopt; + } + + auto const& s1 = udivs.negative_divisors.at( j ).first; + auto const& tt_s1 = ntk.is_complemented( s1 ) ? ~tts[ntk.get_node( s1 )] : tts[ntk.get_node( s1 )]; + + for ( auto b = 0u; b < tt.num_blocks(); ++b ) + { + if ( ( tt_s0._bits[b] & tt_s1._bits[b] ) != tt._bits[b] ) + { + return std::nullopt; + } + } + assert( tt == ( tt_s0 & tt_s1 ) ); + fanin fi1{0, ntk.is_complemented( s0 )}; + fanin fi2{1, ntk.is_complemented( s1 )}; + vgate gate{{fi1, fi2}, gtype::AND}; + tmp.resize( 2 ); tmp[0] = ntk.get_node( s0 ); tmp[1] = ntk.get_node( s1 ); + + return result_t( circuit{tmp, {gate}, false} ); + } + +#if 0 + std::optional resub_xor() + { + auto tt = get_tt( root ); + auto ntt = get_tt( root, true ); + + for ( auto i = 0u; i < num_divs - 1; ++i ) + { + auto const& s0 = divs.at( i ); + auto tt_s0 = get_tt( s0 ); + + for ( auto j = i + 1; j < num_divs; ++j ) + { + auto const& s1 = divs.at( j ); + auto const& tt_s1 = get_tt( s1 ); + + const auto isxor = call_with_stopwatch( st.time_div1_compare, [&]() { + return is_xor( tt_s0, tt_s1, tt); + }); + const auto isxnor = call_with_stopwatch( st.time_div1_compare, [&]() { + return is_xor( tt_s0, tt_s1, ntt); + }); + + if ( isxor || isxnor ) + { + fanin fi1{0, false}; + fanin fi2{1, false}; + vgate gate{{fi1, fi2}, gtype::XOR}; + + const auto valid = call_with_stopwatch( st.time_sat, [&]() { + return validator.validate( root, {s0, s1}, {gate}, isxnor ); + }); + + if ( !valid ) /* timeout */ + { + continue; + } + else if ( *valid ) + { + return isxor ? ntk.create_xor( ntk.make_signal( s0 ), ntk.make_signal( s1 ) ) : !ntk.create_xor( ntk.make_signal( s0 ), ntk.make_signal( s1 ) ); + } + else + { + ++st.num_cex_xor; + found_cex(); + tt = get_tt( root ); + ntt = get_tt( root, true ); + tt_s0 = get_tt( s0 ); + } + } + } + } + + return std::nullopt; + } +#endif + +private: + void break_div1_pos() + { + i = 0; j = 1; + ++step; + if ( udivs.negative_divisors.size() < 2 ) + { + ++step; + } + } + + void break_div1_pos_inner() + { + if ( ++i == udivs.positive_divisors.size() - 1 ) + { + break_div1_pos(); + } + else + { + j = i + 1; + } + } + + void break_div1_neg() + { + i = 0; j = 1; + ++step; + } + + void break_div1_neg_inner() + { + if ( ++i == udivs.negative_divisors.size() - 1 ) + { + break_div1_neg(); + } + else + { + j = i + 1; + } + } + +private: + Ntk const& ntk; + resubstitution_params const& ps; + stats& st; + + unordered_node_map const& tts; + kitty::partial_truth_table tt; + kitty::partial_truth_table ntt; + node const& root; + std::vector const& divs; + unate_divisors udivs; + std::vector tmp; + + uint32_t const num_inserts; + uint32_t step; + uint32_t i; + uint32_t j; + + uint32_t w; + uint32_t nw; +}; + +struct abc_resub_functor_stats +{ + /*! \brief Time for finding dependency function. */ + stopwatch<>::duration time_compute_function{0}; + + /*! \brief Time for interfacing with ABC. */ + stopwatch<>::duration time_interface{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 + { + // clang-format off + std::cout << "[i] \n"; + std::cout << fmt::format( "[i] #solution = {:6d}\n", num_success ); + std::cout << fmt::format( "[i] #invoke = {:6d}\n", num_success + num_fail ); + std::cout << fmt::format( "[i] ABC time: {:>5.2f} secs\n", to_seconds( time_compute_function ) ); + std::cout << fmt::format( "[i] interface: {:>5.2f} secs\n", to_seconds( time_compute_function ) ); + // clang-format on + } +}; + +template +class abc_resub_functor +{ +public: + using stats = abc_resub_functor_stats; + using node = typename Ntk::node; + using signal = typename Ntk::signal; + using TT = unordered_node_map; + using vgate = typename validator_t::gate; + using fanin = typename vgate::fanin; + using gtype = typename validator_t::gate_type; + using circuit = imaginary_circuit; + using result_t = typename std::variant; + + explicit abc_resub_functor( Ntk const& ntk, resubstitution_params const& ps, stats& st, TT const& tts, node const& root, std::vector const& divs, uint32_t const num_inserts ) + : ntk( ntk ), ps( ps ), st( st ), tts( tts ), root( root ), divs( divs ), num_inserts( num_inserts ), num_blocks( 0 ) + { + } + + ~abc_resub_functor() + { + call_with_stopwatch( st.time_interface, [&]() { + abcresub::Abc_ResubPrepareManager( 0 ); + } ); + } + + void check_num_blocks() + { + if ( tts[ntk.get_constant( false )].num_blocks() != num_blocks ) + { + num_blocks = tts[ntk.get_constant( false )].num_blocks(); + call_with_stopwatch( st.time_interface, [&]() { + abcresub::Abc_ResubPrepareManager( num_blocks ); + }); + } + } + + std::optional operator()( uint32_t& size ) + { + check_num_blocks(); + abc_resub rs( 2ul + divs.size(), num_blocks, ps.max_divisors_k ); + call_with_stopwatch( st.time_interface, [&]() { + rs.add_root( root, tts ); + rs.add_divisors( std::begin( divs ), std::end( divs ), tts ); + }); + + auto const res = call_with_stopwatch( st.time_compute_function, [&]() { + if constexpr ( std::is_same::value ) + { + return rs.compute_function( num_inserts, true ); + } + else + { + return rs.compute_function( num_inserts, false ); + } + } ); + + if ( res ) + { + ++st.num_success; + auto const& index_list = *res; + if ( index_list.size() == 1u ) /* div0 or constant */ + { + if ( index_list[0] < 2 ) + { + return result_t( ntk.get_constant( bool( index_list[0] ) ) ); + } + assert( index_list[0] >= 4 ); + return result_t( bool( index_list[0] % 2 ) ? !ntk.make_signal( divs[( index_list[0] >> 1u ) - 2u] ) : ntk.make_signal( divs[( index_list[0] >> 1u ) - 2u] ) ); + } + + uint64_t const num_gates = ( index_list.size() - 1u ) / 2u; + std::vector gates; + gates.reserve( num_gates ); + size = 0u; + + call_with_stopwatch( st.time_interface, [&]() { + for ( auto i = 0u; i < num_gates; ++i ) + { + fanin f0{uint32_t( ( index_list[2 * i] >> 1u ) - 2u ), bool( index_list[2 * i] % 2 )}; + fanin f1{uint32_t( ( index_list[2 * i + 1u] >> 1u ) - 2u ), bool( index_list[2 * i + 1u] % 2 )}; + gates.emplace_back( vgate{{f0, f1}, f0.index < f1.index ? gtype::AND : gtype::XOR} ); + + if constexpr ( std::is_same::value ) + { + ++size; + } + else + { + size += ( gates[i].type == gtype::AND ) ? 1u : 3u; + } + } + }); + bool const out_neg = bool( index_list.back() % 2 ); + assert( size <= num_inserts ); + return result_t( circuit{divs, gates, out_neg} ); + } + else /* loop until no result can be found by the engine */ + { + ++st.num_fail; + return std::nullopt; + } + } + +private: + Ntk const& ntk; + resubstitution_params const& ps; + stats& st; + + TT const& tts; + node const& root; + std::vector const& divs; + + uint32_t const num_inserts; + uint32_t num_blocks; +}; + +template +struct sim_resub_stats +{ + /*! \brief Time for pattern generation. */ + stopwatch<>::duration time_patgen{0}; + + /*! \brief Time for simulation. */ + stopwatch<>::duration time_sim{0}; + + /*! \brief Time for SAT solving. */ + stopwatch<>::duration time_sat{0}; + + /*! \brief Time for finding dependency function. */ + stopwatch<>::duration time_functor{0}; + + /*! \brief Time for interfacing with circuit_validator. */ + stopwatch<>::duration time_interface{0}; + + /*! \brief Number of patterns used. */ + uint32_t num_pats{0}; + + /*! \brief Number of counter-examples. */ + uint32_t num_cex{0}; + + /*! \brief Number of successful resubstitutions. */ + uint32_t num_resub{0}; + + /*! \brief Number of SAT solver timeout. */ + uint32_t num_timeout{0}; + + ResubFnSt functor_st; + + void report() const + { + // clang-format off + std::cout << "[i] \n"; + std::cout << "[i] ======== Stats ========\n"; + std::cout << fmt::format( "[i] #pat = {:6d}\n", num_pats ); + std::cout << fmt::format( "[i] #resub = {:6d}\n", num_resub ); + std::cout << fmt::format( "[i] #CEX = {:6d}\n", num_cex ); + std::cout << fmt::format( "[i] #timeout = {:6d}\n", num_timeout ); + std::cout << "[i] ======== Runtime ========\n"; + std::cout << fmt::format( "[i] generate pattern: {:>5.2f} secs\n", to_seconds( time_patgen ) ); + std::cout << fmt::format( "[i] simulation: {:>5.2f} secs\n", to_seconds( time_sim ) ); + std::cout << fmt::format( "[i] SAT: {:>5.2f} secs\n", to_seconds( time_sat ) ); + std::cout << fmt::format( "[i] compute function: {:>5.2f} secs\n", to_seconds( time_functor ) ); + std::cout << fmt::format( "[i] interfacing: {:>5.2f} secs\n", to_seconds( time_interface ) ); + std::cout << "[i] ======== Details ========\n"; + functor_st.report(); + std::cout << "[i] =========================\n\n"; + // clang-format on + } +}; + +/*! \brief Simulation-based resubstitution engine. + * + * This engine simulates in the whole network and uses partial truth tables + * to find potential resubstitutions. It then formally verifies the resubstitution + * candidates given by the resubstitution functor. If the validation fails, + * a counter-example will be added to the simulation patterns, and the functor + * will be invoked again with updated truth tables, looping until it returns + * `std::nullopt`. This engine only requires the divisor collector to prepare `divs`. + * + * Please refer to the following paper for further details. + * + * [1] Simulation-Guided Boolean Resubstitution. IWLS 2020 (arXiv:2007.02579). + * + * Interfaces of the resubstitution functor: + * - Constructor: `resub_fn( Ntk const& ntk, resubstitution_params const& ps, stats& st,` + * `TT const& tts, node const& root, std::vector const& divs, uint32_t const num_inserts )` + * - A public `operator()`: `std::optional operator()( uint32_t& size )` + * + * Compatible resubstitution functors implemented: + * - `sim_aig_resub_functor`: compute div0 and div1 resub by truth table comparison + * - `abc_resub_functor`: dependency function computation engine ported from ABC + * + * \param validator_t Specialization of `circuit_validator`. + * \param ResubFn Resubstitution functor to compute the resubstitution. + * \param MffcRes Typename of `potential_gain` needed by the resubstitution functor. + */ +template, class ResubFn = abc_resub_functor, typename MffcRes = uint32_t> +class simulation_based_resub_engine +{ +public: + static constexpr bool require_leaves_and_MFFC = false; + using stats = sim_resub_stats; + using mffc_result_t = MffcRes; + + using node = typename Ntk::node; + using signal = typename Ntk::signal; + using TT = unordered_node_map; + using gtype = typename validator_t::gate_type; + using circuit = imaginary_circuit; + + explicit simulation_based_resub_engine( Ntk& ntk, resubstitution_params const& ps, stats& st ) + : ntk( ntk ), ps( ps ), st( st ), tts( ntk ), validator( ntk, vps ) + { + if constexpr ( !validator_t::use_odc_ ) + { + assert( ps.odc_levels == 0 && "to consider ODCs, circuit_validator::use_odc has to be turned on" ); + } + + vps.conflict_limit = ps.conflict_limit; + vps.random_seed = ps.random_seed; + + ntk._events->on_add.emplace_back( [&]( const auto& n ) { + call_with_stopwatch( st.time_sim, [&]() { + simulate_node( ntk, n, tts, sim ); + }); + } ); + + /* prepare simulation patterns */ + call_with_stopwatch( st.time_patgen, [&]() { + if ( ps.pattern_filename ) + { + sim = partial_simulator( *ps.pattern_filename ); + } + else + { + sim = partial_simulator( ntk.num_pis(), 1024 ); + pattern_generation( ntk, sim ); + } + }); + st.num_pats = sim.num_bits(); + + /* first simulation: the whole circuit; from 0 bits. */ + call_with_stopwatch( st.time_sim, [&]() { + simulate_nodes( ntk, tts, sim ); + }); + } + + ~simulation_based_resub_engine() + { + if ( ps.save_patterns ) + { + write_patterns( sim, *ps.save_patterns ); + } + } + + std::optional run( node const& n, std::vector const& divs, uint32_t potential_gain, uint32_t& last_gain ) + { + if ( potential_gain == 0 ) + { + return std::nullopt; + } + + ResubFn resub_fn( ntk, ps, st.functor_st, tts, n, divs, std::min( potential_gain - 1, ps.max_inserts ) ); + for ( auto j = 0u; j < ps.max_trials; ++j ) + { + check_tts( n ); + for ( auto const& d : divs ) + { + check_tts( d ); + } + + uint32_t size = 0; + const auto res = call_with_stopwatch( st.time_functor, [&]() { + return resub_fn( size ); + }); + if ( res ) + { + if ( std::get_if( &(*res) ) ) + { + signal const& g = std::get( *res ); + auto valid = call_with_stopwatch( st.time_sat, [&]() { + return validator.validate( n, g ); + }); + if ( valid ) + { + if ( *valid ) + { + ++st.num_resub; + last_gain = potential_gain; + return g; + } + else + { + found_cex(); + continue; + } + } + else /* timeout */ + { + return std::nullopt; + } + } + else + { + circuit const& c = std::get( *res ); + auto valid = call_with_stopwatch( st.time_sat, [&]() { + return validator.validate( n, c.divs, c.ckt, c.out_neg ); + }); + if ( valid ) + { + if ( *valid ) + { + ++st.num_resub; + last_gain = potential_gain - size; + return translate( c, c.divs ); + } + else + { + found_cex(); + continue; + } + } + else /* timeout */ + { + return std::nullopt; + } + } + } + else /* functor can not find any potential resubstitution */ + { + return std::nullopt; + } + } + return std::nullopt; + } + + void found_cex() + { + ++st.num_cex; + sim.add_pattern( validator.cex ); + + /* re-simulate the whole circuit (for the last block) when a block is full */ + if ( sim.num_bits() % 64 == 0 ) + { + call_with_stopwatch( st.time_sim, [&]() { + simulate_nodes( ntk, tts, sim, false ); + } ); + } + } + + void check_tts( node const& n ) + { + if ( tts[n].num_bits() != sim.num_bits() ) + { + call_with_stopwatch( st.time_sim, [&]() { + simulate_node( ntk, n, tts, sim ); + } ); + } + } + + kitty::partial_truth_table get_tt( node const& n, bool inverse = false ) + { + check_tts( n ); + + if ( ps.odc_levels == 0 ) + { + return inverse? ~tts[n]: tts[n]; + } + + return ( inverse? ~tts[n]: tts[n] ) | observability_dont_cares( ntk, n, sim, tts, ps.odc_levels ); + } + + signal translate( circuit const& c, std::vector const& divs ) + { + std::vector ckt; + + call_with_stopwatch( st.time_interface, [&]() { + for ( auto i = 0u; i < divs.size(); ++i ) + { + ckt.emplace_back( ntk.make_signal( divs[i] ) ); + } + + for ( auto g : c.ckt ) + { + auto const f0 = g.fanins[0].inverted ? !ckt[g.fanins[0].index] : ckt[g.fanins[0].index]; + auto const f1 = g.fanins[1].inverted ? !ckt[g.fanins[1].index] : ckt[g.fanins[1].index]; + if ( g.type == gtype::AND ) + { + ckt.emplace_back( ntk.create_and( f0, f1 ) ); + } + else if ( g.type == gtype::XOR ) + { + ckt.emplace_back( ntk.create_xor( f0, f1 ) ); + } + } + }); + + return c.out_neg ? !ckt.back() : ckt.back(); + } + +private: + Ntk& ntk; + resubstitution_params const& ps; + stats& st; + + TT tts; + partial_simulator sim; + + validator_params vps; + validator_t validator; +}; /* simulation_based_resub_engine */ + +} /* namespace detail */ + +template +void sim_resubstitution( Ntk& ntk, resubstitution_params const& ps = {}, resubstitution_stats* pst = nullptr ) +{ + static_assert( std::is_same::value || std::is_same::value, "Currently only supports AIG and XAG" ); + + using resub_view_t = fanout_view>; + depth_view depth_view{ntk}; + resub_view_t resub_view{depth_view}; + + using resub_impl_t = typename detail::resubstitution_impl>; + + 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( resub_view, 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 */ \ No newline at end of file diff --git a/include/mockturtle/algorithms/simulation.hpp b/include/mockturtle/algorithms/simulation.hpp index f42867b78..404ba7d7b 100644 --- a/include/mockturtle/algorithms/simulation.hpp +++ b/include/mockturtle/algorithms/simulation.hpp @@ -168,7 +168,7 @@ class default_simulator> class partial_simulator { public: - partial_simulator() = delete; + partial_simulator() {} /*! \brief Create a `partial_simulator` with random simulation patterns. * diff --git a/include/mockturtle/algorithms/xag_resub_withDC.hpp b/include/mockturtle/algorithms/xag_resub_withDC.hpp index 3988989fb..4562d1798 100644 --- a/include/mockturtle/algorithms/xag_resub_withDC.hpp +++ b/include/mockturtle/algorithms/xag_resub_withDC.hpp @@ -960,19 +960,22 @@ void resubstitution_minmc_withDC( Ntk& ntk, resubstitution_params const& ps = {} depth_view depth_view{ntk}; resub_view_t resub_view{depth_view}; + using truthtable_t = kitty::dynamic_truth_table; + using mffc_result_t = std::pair; + using resub_impl_t = detail::resubstitution_impl, truthtable_t>, mffc_result_t>, typename detail::default_divisor_collector, mffc_result_t>>; + resubstitution_stats st; + typename resub_impl_t::engine_st_t engine_st; + typename resub_impl_t::collector_st_t collector_st; - using truthtable_t = kitty::dynamic_truth_table; - using simulator_t = detail::simulator; - using node_mffc_t = detail::node_mffc_inside_xag; - using resubstitution_functor_t = xag_resub_functor; - typename resubstitution_functor_t::stats resub_st; - detail::resubstitution_impl p( resub_view, ps, st, resub_st ); + resub_impl_t p( resub_view, ps, st, engine_st, collector_st ); p.run(); + if ( ps.verbose ) { st.report(); - resub_st.report(); + collector_st.report(); + engine_st.report(); } if ( pst ) diff --git a/include/mockturtle/algorithms/xmg_resub.hpp b/include/mockturtle/algorithms/xmg_resub.hpp index 0bef2b77f..488d3af70 100644 --- a/include/mockturtle/algorithms/xmg_resub.hpp +++ b/include/mockturtle/algorithms/xmg_resub.hpp @@ -316,36 +316,22 @@ void xmg_resubstitution( Ntk& ntk, resubstitution_params const& ps = {}, resubst depth_view depth_view{ntk}; resub_view_t resub_view{depth_view}; - using node_mffc_t = detail::node_mffc_inside; + using truthtable_t = kitty::dynamic_truth_table; + using truthtable_dc_t = kitty::dynamic_truth_table; + using resub_impl_t = detail::resubstitution_impl, truthtable_dc_t>>>; + resubstitution_stats st; - if ( ps.max_pis == 8 ) - { - using truthtable_t = kitty::dynamic_truth_table; - using truthtable_dc_t = kitty::dynamic_truth_table; - using simulator_t = detail::simulator; - using resubstitution_functor_t = xmg_resub_functor; - typename resubstitution_functor_t::stats resub_st; - detail::resubstitution_impl p( resub_view, ps, st, resub_st ); - p.run(); - if ( ps.verbose ) - { - st.report(); - resub_st.report(); - } - } - else + typename resub_impl_t::engine_st_t engine_st; + typename resub_impl_t::collector_st_t collector_st; + + resub_impl_t p( resub_view, ps, st, engine_st, collector_st ); + p.run(); + + if ( ps.verbose ) { - using truthtable_t = kitty::dynamic_truth_table; - using simulator_t = detail::simulator; - using resubstitution_functor_t = xmg_resub_functor; - typename resubstitution_functor_t::stats resub_st; - detail::resubstitution_impl p( resub_view, ps, st, resub_st ); - p.run(); - if ( ps.verbose ) - { - st.report(); - resub_st.report(); - } + st.report(); + collector_st.report(); + engine_st.report(); } if ( pst ) diff --git a/include/mockturtle/io/write_patterns.hpp b/include/mockturtle/io/write_patterns.hpp index 4f3cd772f..83774b566 100644 --- a/include/mockturtle/io/write_patterns.hpp +++ b/include/mockturtle/io/write_patterns.hpp @@ -53,7 +53,7 @@ namespace mockturtle * \param sim The `partial_simulator` object containing simulation patterns * \param out Output stream */ -void write_patterns( partial_simulator const& sim, std::ostream& out = std::cout ) +inline void write_patterns( partial_simulator const& sim, std::ostream& out = std::cout ) { auto const& patterns = sim.get_patterns(); for ( auto i = 0u; i < patterns.size(); ++i ) @@ -70,7 +70,7 @@ void write_patterns( partial_simulator const& sim, std::ostream& out = std::cout * \param sim The `partial_simulator` object containing simulation patterns * \param filename Filename */ -void write_patterns( partial_simulator const& sim, std::string const& filename ) +inline void write_patterns( partial_simulator const& sim, std::string const& filename ) { std::ofstream os( filename.c_str(), std::ofstream::out ); write_patterns( sim, os ); diff --git a/include/mockturtle/utils/abc_resub.hpp b/include/mockturtle/utils/abc_resub.hpp new file mode 100644 index 000000000..47c348a7a --- /dev/null +++ b/include/mockturtle/utils/abc_resub.hpp @@ -0,0 +1,193 @@ +/* mockturtle: C++ logic network library + * Copyright (C) 2018-2020 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. + */ + +/*! + \file abc_resub.hpp + \brief Interface to `abc_resub`. + + \author Heinz Riener +*/ + +#pragma once + +#include +#include + +namespace mockturtle +{ +#if 0 +enum gate_type +{ + AND, + XOR, +}; + +struct gate +{ + struct fanin + { + uint32_t idx; + bool inv{false}; + }; + + std::vector fanins; + gate_type type{AND}; +}; +#endif + +class abc_resub +{ +public: + explicit abc_resub( uint64_t num_divisors, uint64_t num_blocks_per_truth_table, uint64_t max_num_divisors = 50ul ) + : num_divisors( num_divisors ) + , num_blocks_per_truth_table( num_blocks_per_truth_table ) + , max_num_divisors( max_num_divisors ) + , counter(0) + { + alloc(); + } + + virtual ~abc_resub() + { + release(); + } + + template + void add_root( node_type const& node, truth_table_storage_type const& tts ) + { + add_divisor( node, tts, true ); /* off-set */ + add_divisor( node, tts, false ); /* on-set */ + } + + template + void add_divisor( node_type const& node, truth_table_storage_type const& tts, bool complement = false ) + { + assert( abc_tts != nullptr && "assume that memory for truth tables has been allocated" ); + assert( abc_divs != nullptr && "assume that memory for divisors has been allocated" ); + + assert( tts[node].num_blocks() == num_blocks_per_truth_table ); + auto const tt = complement ? ~tts[node] : tts[node]; + for ( uint64_t i = 0ul; i < num_blocks_per_truth_table; ++i ) + { + Vec_WrdPush( abc_tts, tt._bits[i] ); + } + Vec_PtrPush( abc_divs, Vec_WrdEntryP( abc_tts, counter * num_blocks_per_truth_table ) ); + ++counter; + } + + template + void add_divisors( iterator_type begin, iterator_type end, truth_table_storage_type const& tts ) + { + assert( abc_tts != nullptr && "assume that memory for truth tables has been allocated" ); + assert( abc_divs != nullptr && "assume that memory for divisors has been allocated" ); + + while ( begin != end ) + { + add_divisor( *begin, tts ); + ++begin; + } + } + + std::optional> compute_function( uint32_t num_inserts, bool useXOR = false ) + { + int index_list_size; + int * index_list; + index_list_size = abcresub::Abc_ResubComputeFunction( (void **)Vec_PtrArray( abc_divs ), Vec_PtrSize( abc_divs ), num_blocks_per_truth_table, num_inserts, /* nDivsMax */max_num_divisors, /* nChoice = */0, int(useXOR), /* debug = */0, /* verbose = */0, &index_list ); + + if ( index_list_size ) + { + std::vector vec( index_list_size ); + for ( auto i = 0; i < index_list_size; ++i ) // probably could be smarter + { + vec[i] = index_list[i]; + } + return vec; + } + + return std::nullopt; + } + +#if 0 /* not used */ + std::optional> compute_function( bool& output_negation, uint32_t num_inserts, bool useXOR = false ) + { + int index_list_size; + int * index_list; + index_list_size = abcresub::Abc_ResubComputeFunction( (void **)Vec_PtrArray( abc_divs ), Vec_PtrSize( abc_divs ), num_blocks_per_truth_table, num_inserts, /* nDivsMax */max_num_divisors, /* nChoice = */0, int(useXOR), /* debug = */0, /* verbose = */0, &index_list ); + + if ( index_list_size ) + { + uint64_t const num_gates = ( index_list_size - 1u ) / 2u; + std::vector gates( num_gates ); + for ( auto i = 0u; i < num_gates; ++i ) + { + gate::fanin f0{uint32_t( ( index_list[2*i] >> 1u ) - 2u ), bool( index_list[2*i] % 2 )}; + gate::fanin f1{uint32_t( ( index_list[2*i + 1u] >> 1u ) - 2u ), bool( index_list[2*i + 1u] % 2 )}; + gates[i].fanins = { f0, f1 }; + + gates[i].type = f0.idx < f1.idx ? gate_type::AND : gate_type::XOR; + } + output_negation = index_list[index_list_size - 1u] % 2; + return gates; + } + + return std::nullopt; + } +#endif + + void dump( std::string const file = "dump.txt" ) const + { + abcresub::Abc_ResubDumpProblem( file.c_str(), (void **)Vec_PtrArray( abc_divs ), Vec_PtrSize( abc_divs ), num_blocks_per_truth_table ); + } + +protected: + void alloc() + { + assert( abc_tts == nullptr ); + assert( abc_divs == nullptr ); + abc_tts = abcresub::Vec_WrdAlloc( num_divisors * num_blocks_per_truth_table ); + abc_divs = abcresub::Vec_PtrAlloc( num_divisors ); + } + + void release() + { + assert( abc_divs != nullptr ); + assert( abc_tts != nullptr ); + Vec_PtrFree( abc_divs ); + Vec_WrdFree( abc_tts ); + abc_divs = nullptr; + abc_tts = nullptr; + } + +protected: + uint64_t num_divisors; + uint64_t num_blocks_per_truth_table; + uint64_t max_num_divisors; + uint64_t counter; + + abcresub::Vec_Wrd_t * abc_tts{nullptr}; + abcresub::Vec_Ptr_t * abc_divs{nullptr}; +}; /* abc_resub */ + +} /* namespace mockturtle */ diff --git a/lib/CMakeLists.txt b/lib/CMakeLists.txt index bcbfae6f4..006447723 100644 --- a/lib/CMakeLists.txt +++ b/lib/CMakeLists.txt @@ -75,6 +75,11 @@ if (NOT TARGET bill) endif() endif() +if (NOT TARGET abcresub) + add_library(abcresub INTERFACE) + target_include_directories(abcresub INTERFACE ${CMAKE_CURRENT_SOURCE_DIR}/abcresub) +endif() + if (NOT TARGET libabcesop) set(STATIC_LIBABC true) add_subdirectory(abcesop) diff --git a/lib/abcresub/abcresub/abc_global.hpp b/lib/abcresub/abcresub/abc_global.hpp new file mode 100644 index 000000000..508021f0a --- /dev/null +++ b/lib/abcresub/abcresub/abc_global.hpp @@ -0,0 +1,199 @@ +/*! + \file abc_global.hpp + \brief Extracted from ABC + https://github.com/berkeley-abc/abc + + \author Alan Mishchenko (UC Berkeley) +*/ + +#pragma once + +namespace abcresub +{ + +typedef uint64_t word; +inline int Abc_MaxInt( int a, int b ) { return a > b ? a : b; } +inline int Abc_MinInt( int a, int b ) { return a < b ? a : b; } +inline int Abc_LitIsCompl( int Lit ) { assert(Lit >= 0); return Lit & 1; } +inline int Abc_Lit2Var( int Lit ) { assert(Lit >= 0); return Lit >> 1; } +inline int Abc_Var2Lit( int Var, int c ) { assert(Var >= 0 && !(c >> 1)); return Var + Var + c; } +inline int Abc_LitNot( int Lit ) { assert(Lit >= 0); return Lit ^ 1; } +inline int Abc_LitNotCond( int Lit, int c ) { assert(Lit >= 0); return Lit ^ (int)(c > 0); } + +#ifndef ABC_CONST +#define ABC_CONST(number) number ## ULL +#endif /* ABC_CONST */ + +#ifndef ABC_ALLOC +#define ABC_ALLOC(type, num) ((type *) malloc(sizeof(type) * (size_t)(num))) +#endif /* ABC_ALLOC */ + +#ifndef ABC_CALLOC +#define ABC_CALLOC(type, num) ((type *) calloc((size_t)(num), sizeof(type))) +#endif /* ABC_CALLOC */ + +#ifndef ABC_FREE +#define ABC_FREE(obj) ((obj) ? (free((char *) (obj)), (obj) = 0) : 0) +#endif /* ABC_FREE */ + +#ifndef ABC_REALLOC +#define ABC_REALLOC(type, obj, num) \ + ((obj) ? ((type *) realloc((char *)(obj), sizeof(type) * (size_t)(num))) : \ + ((type *) malloc(sizeof(type) * (size_t)(num)))) +#endif /* ABC_REALLOC */ + +void Abc_SortMerge( int * p1Beg, int * p1End, int * p2Beg, int * p2End, int * pOut ) +{ + int nEntries = (p1End - p1Beg) + (p2End - p2Beg); + int * pOutBeg = pOut; + (void)nEntries; + (void)pOutBeg; + while ( p1Beg < p1End && p2Beg < p2End ) + { + if ( *p1Beg == *p2Beg ) + *pOut++ = *p1Beg++, *pOut++ = *p2Beg++; + else if ( *p1Beg < *p2Beg ) + *pOut++ = *p1Beg++; + else // if ( *p1Beg > *p2Beg ) + *pOut++ = *p2Beg++; + } + while ( p1Beg < p1End ) + *pOut++ = *p1Beg++; + while ( p2Beg < p2End ) + *pOut++ = *p2Beg++; + assert( pOut - pOutBeg == nEntries ); +} + +void Abc_Sort_rec( int * pInBeg, int * pInEnd, int * pOutBeg ) +{ + int nSize = pInEnd - pInBeg; + assert( nSize > 0 ); + if ( nSize == 1 ) + return; + if ( nSize == 2 ) + { + if ( pInBeg[0] > pInBeg[1] ) + { + pInBeg[0] ^= pInBeg[1]; + pInBeg[1] ^= pInBeg[0]; + pInBeg[0] ^= pInBeg[1]; + } + } + else if ( nSize < 8 ) + { + int temp, i, j, best_i; + for ( i = 0; i < nSize-1; i++ ) + { + best_i = i; + for ( j = i+1; j < nSize; j++ ) + if ( pInBeg[j] < pInBeg[best_i] ) + best_i = j; + temp = pInBeg[i]; + pInBeg[i] = pInBeg[best_i]; + pInBeg[best_i] = temp; + } + } + else + { + Abc_Sort_rec( pInBeg, pInBeg + nSize/2, pOutBeg ); + Abc_Sort_rec( pInBeg + nSize/2, pInEnd, pOutBeg + nSize/2 ); + Abc_SortMerge( pInBeg, pInBeg + nSize/2, pInBeg + nSize/2, pInEnd, pOutBeg ); + memcpy( pInBeg, pOutBeg, sizeof(int) * nSize ); + } +} + +void Abc_MergeSort( int * pInput, int nSize ) +{ + int * pOutput; + if ( nSize < 2 ) + return; + pOutput = (int *) malloc( sizeof(int) * nSize ); + Abc_Sort_rec( pInput, pInput + nSize, pOutput ); + free( pOutput ); +} + +void Abc_MergeSortCostMerge( int * p1Beg, int * p1End, int * p2Beg, int * p2End, int * pOut ) +{ + int nEntries = (p1End - p1Beg) + (p2End - p2Beg); + int * pOutBeg = pOut; + (void)nEntries; + (void)pOutBeg; + while ( p1Beg < p1End && p2Beg < p2End ) + { + if ( p1Beg[1] == p2Beg[1] ) + *pOut++ = *p1Beg++, *pOut++ = *p1Beg++, *pOut++ = *p2Beg++, *pOut++ = *p2Beg++; + else if ( p1Beg[1] < p2Beg[1] ) + *pOut++ = *p1Beg++, *pOut++ = *p1Beg++; + else // if ( p1Beg[1] > p2Beg[1] ) + *pOut++ = *p2Beg++, *pOut++ = *p2Beg++; + } + while ( p1Beg < p1End ) + *pOut++ = *p1Beg++, *pOut++ = *p1Beg++; + while ( p2Beg < p2End ) + *pOut++ = *p2Beg++, *pOut++ = *p2Beg++; + assert( pOut - pOutBeg == nEntries ); +} + +void Abc_MergeSortCost_rec( int * pInBeg, int * pInEnd, int * pOutBeg ) +{ + int nSize = (pInEnd - pInBeg)/2; + assert( nSize > 0 ); + if ( nSize == 1 ) + return; + if ( nSize == 2 ) + { + if ( pInBeg[1] > pInBeg[3] ) + { + pInBeg[1] ^= pInBeg[3]; + pInBeg[3] ^= pInBeg[1]; + pInBeg[1] ^= pInBeg[3]; + pInBeg[0] ^= pInBeg[2]; + pInBeg[2] ^= pInBeg[0]; + pInBeg[0] ^= pInBeg[2]; + } + } + else if ( nSize < 8 ) + { + int temp, i, j, best_i; + for ( i = 0; i < nSize-1; i++ ) + { + best_i = i; + for ( j = i+1; j < nSize; j++ ) + if ( pInBeg[2*j+1] < pInBeg[2*best_i+1] ) + best_i = j; + temp = pInBeg[2*i]; + pInBeg[2*i] = pInBeg[2*best_i]; + pInBeg[2*best_i] = temp; + temp = pInBeg[2*i+1]; + pInBeg[2*i+1] = pInBeg[2*best_i+1]; + pInBeg[2*best_i+1] = temp; + } + } + else + { + Abc_MergeSortCost_rec( pInBeg, pInBeg + 2*(nSize/2), pOutBeg ); + Abc_MergeSortCost_rec( pInBeg + 2*(nSize/2), pInEnd, pOutBeg + 2*(nSize/2) ); + Abc_MergeSortCostMerge( pInBeg, pInBeg + 2*(nSize/2), pInBeg + 2*(nSize/2), pInEnd, pOutBeg ); + memcpy( pInBeg, pOutBeg, sizeof(int) * 2 * nSize ); + } +} + +int * Abc_MergeSortCost( int * pCosts, int nSize ) +{ + int i, * pResult, * pInput, * pOutput; + pResult = (int *) calloc( sizeof(int), nSize ); + if ( nSize < 2 ) + return pResult; + pInput = (int *) malloc( sizeof(int) * 2 * nSize ); + pOutput = (int *) malloc( sizeof(int) * 2 * nSize ); + for ( i = 0; i < nSize; i++ ) + pInput[2*i] = i, pInput[2*i+1] = pCosts[i]; + Abc_MergeSortCost_rec( pInput, pInput + 2*nSize, pOutput ); + for ( i = 0; i < nSize; i++ ) + pResult[i] = pInput[2*i]; + free( pOutput ); + free( pInput ); + return pResult; +} + +} /* namespace abcresub */ diff --git a/lib/abcresub/abcresub/abcresub.hpp b/lib/abcresub/abcresub/abcresub.hpp new file mode 100644 index 000000000..e30ee91ed --- /dev/null +++ b/lib/abcresub/abcresub/abcresub.hpp @@ -0,0 +1,1711 @@ +/*! + \file abcresub.hpp + \brief Extracted from ABC + https://github.com/berkeley-abc/abc + + \author Alan Mishchenko (UC Berkeley) +*/ + +#pragma once + +#include "abc_global.hpp" +#include "vec_ptr.hpp" +#include "vec_int.hpp" +#include "vec_wec.hpp" +#include "vec_wrd.hpp" +#include "tt.hpp" + +namespace abcresub +{ + +#if 0 +/**Function************************************************************* + + Synopsis [Computes MFFCs of all qualifying nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_ObjCheckMffc_rec( Gia_Man_t * p,Gia_Obj_t * pObj, int Limit, Vec_Int_t * vNodes ) +{ + int iFanin; + if ( Gia_ObjIsCi(pObj) ) + return 1; + assert( Gia_ObjIsAnd(pObj) ); + iFanin = Gia_ObjFaninId0p(p, pObj); + Vec_IntPush( vNodes, iFanin ); + if ( !Gia_ObjRefDecId(p, iFanin) && (Vec_IntSize(vNodes) > Limit || !Gia_ObjCheckMffc_rec(p, Gia_ObjFanin0(pObj), Limit, vNodes)) ) + return 0; + iFanin = Gia_ObjFaninId1p(p, pObj); + Vec_IntPush( vNodes, iFanin ); + if ( !Gia_ObjRefDecId(p, iFanin) && (Vec_IntSize(vNodes) > Limit || !Gia_ObjCheckMffc_rec(p, Gia_ObjFanin1(pObj), Limit, vNodes)) ) + return 0; + if ( !Gia_ObjIsMux(p, pObj) ) + return 1; + iFanin = Gia_ObjFaninId2p(p, pObj); + Vec_IntPush( vNodes, iFanin ); + if ( !Gia_ObjRefDecId(p, iFanin) && (Vec_IntSize(vNodes) > Limit || !Gia_ObjCheckMffc_rec(p, Gia_ObjFanin2(p, pObj), Limit, vNodes)) ) + return 0; + return 1; +} +static inline int Gia_ObjCheckMffc( Gia_Man_t * p, Gia_Obj_t * pRoot, int Limit, Vec_Int_t * vNodes, Vec_Int_t * vLeaves, Vec_Int_t * vInners ) +{ + int RetValue, iObj, i; + Vec_IntClear( vNodes ); + RetValue = Gia_ObjCheckMffc_rec( p, pRoot, Limit, vNodes ); + if ( RetValue ) + { + Vec_IntClear( vLeaves ); + Vec_IntClear( vInners ); + Vec_IntSort( vNodes, 0 ); + Vec_IntForEachEntry( vNodes, iObj, i ) + if ( Gia_ObjRefNumId(p, iObj) > 0 || Gia_ObjIsCi(Gia_ManObj(p, iObj)) ) + { + if ( !Vec_IntSize(vLeaves) || Vec_IntEntryLast(vLeaves) != iObj ) + Vec_IntPush( vLeaves, iObj ); + } + else + { + if ( !Vec_IntSize(vInners) || Vec_IntEntryLast(vInners) != iObj ) + Vec_IntPush( vInners, iObj ); + } + Vec_IntPush( vInners, Gia_ObjId(p, pRoot) ); + } + Vec_IntForEachEntry( vNodes, iObj, i ) + Gia_ObjRefIncId( p, iObj ); + return RetValue; +} +Vec_Wec_t * Gia_ManComputeMffcs( Gia_Man_t * p, int LimitMin, int LimitMax, int SuppMax, int RatioBest ) +{ + Gia_Obj_t * pObj; + Vec_Wec_t * vMffcs; + Vec_Int_t * vNodes, * vLeaves, * vInners, * vMffc; + int i, iPivot; + assert( p->pMuxes ); + vNodes = Vec_IntAlloc( 2 * LimitMax ); + vLeaves = Vec_IntAlloc( 2 * LimitMax ); + vInners = Vec_IntAlloc( 2 * LimitMax ); + vMffcs = Vec_WecAlloc( 1000 ); + Gia_ManCreateRefs( p ); + Gia_ManForEachAnd( p, pObj, i ) + { + if ( !Gia_ObjRefNum(p, pObj) ) + continue; + if ( !Gia_ObjCheckMffc(p, pObj, LimitMax, vNodes, vLeaves, vInners) ) + continue; + if ( Vec_IntSize(vInners) < LimitMin ) + continue; + if ( Vec_IntSize(vLeaves) > SuppMax ) + continue; + // improve cut + // collect cut + vMffc = Vec_WecPushLevel( vMffcs ); + Vec_IntGrow( vMffc, Vec_IntSize(vLeaves) + Vec_IntSize(vInners) + 20 ); + Vec_IntPush( vMffc, i ); + Vec_IntPush( vMffc, Vec_IntSize(vLeaves) ); + Vec_IntPush( vMffc, Vec_IntSize(vInners) ); + Vec_IntAppend( vMffc, vLeaves ); +// Vec_IntAppend( vMffc, vInners ); + // add last entry equal to the ratio + Vec_IntPush( vMffc, 1000 * Vec_IntSize(vInners) / Vec_IntSize(vLeaves) ); + } + Vec_IntFree( vNodes ); + Vec_IntFree( vLeaves ); + Vec_IntFree( vInners ); + // sort MFFCs by their inner/leaf ratio + Vec_WecSortByLastInt( vMffcs, 1 ); + Vec_WecForEachLevel( vMffcs, vMffc, i ) + Vec_IntPop( vMffc ); + // remove those whose ratio is not good + iPivot = RatioBest * Vec_WecSize(vMffcs) / 100; + Vec_WecForEachLevelStart( vMffcs, vMffc, i, iPivot ) + Vec_IntErase( vMffc ); + assert( iPivot <= Vec_WecSize(vMffcs) ); + Vec_WecShrink( vMffcs, iPivot ); + return vMffcs; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManPrintDivStats( Gia_Man_t * p, Vec_Wec_t * vMffcs, Vec_Wec_t * vPivots ) +{ + int fVerbose = 0; + Vec_Int_t * vMffc; + int i, nDivs, nDivsAll = 0, nDivs0 = 0; + Vec_WecForEachLevel( vMffcs, vMffc, i ) + { + nDivs = Vec_IntSize(vMffc) - 3 - Vec_IntEntry(vMffc, 1) - Vec_IntEntry(vMffc, 2); + nDivs0 += (nDivs == 0); + nDivsAll += nDivs; + if ( !fVerbose ) + continue; + printf( "%6d : ", Vec_IntEntry(vMffc, 0) ); + printf( "Leaf =%3d ", Vec_IntEntry(vMffc, 1) ); + printf( "Mffc =%4d ", Vec_IntEntry(vMffc, 2) ); + printf( "Divs =%4d ", nDivs ); + printf( "\n" ); + } + printf( "Collected %d (%.1f %%) MFFCs and %d (%.1f %%) have no divisors (div ave for others is %.2f).\n", + Vec_WecSize(vMffcs), 100.0 * Vec_WecSize(vMffcs) / Gia_ManAndNum(p), + nDivs0, 100.0 * nDivs0 / Gia_ManAndNum(p), + 1.0*nDivsAll/Abc_MaxInt(1, Vec_WecSize(vMffcs) - nDivs0) ); + printf( "Using %.2f MB for MFFCs and %.2f MB for pivots. ", + Vec_WecMemory(vMffcs)/(1<<20), Vec_WecMemory(vPivots)/(1<<20) ); +} + +/**Function************************************************************* + + Synopsis [Compute divisors and Boolean functions for the nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManAddDivisors( Gia_Man_t * p, Vec_Wec_t * vMffcs ) +{ + Vec_Wec_t * vPivots; + Vec_Int_t * vMffc, * vPivot, * vPivot0, * vPivot1; + Vec_Int_t * vCommon, * vCommon2, * vMap; + Gia_Obj_t * pObj; + int i, k, iObj, iPivot, iMffc; +//abctime clkStart = Abc_Clock(); + // initialize pivots (mapping of nodes into MFFCs whose leaves they are) + vMap = Vec_IntStartFull( Gia_ManObjNum(p) ); + vPivots = Vec_WecStart( Gia_ManObjNum(p) ); + Vec_WecForEachLevel( vMffcs, vMffc, i ) + { + assert( Vec_IntSize(vMffc) == 3 + Vec_IntEntry(vMffc, 1) ); + iPivot = Vec_IntEntry( vMffc, 0 ); + Vec_IntWriteEntry( vMap, iPivot, i ); + // iterate through the MFFC leaves + Vec_IntForEachEntryStart( vMffc, iObj, k, 3 ) + { + vPivot = Vec_WecEntry( vPivots, iObj ); + if ( Vec_IntSize(vPivot) == 0 ) + Vec_IntGrow(vPivot, 4); + Vec_IntPush( vPivot, iPivot ); + } + } + Vec_WecForEachLevel( vPivots, vPivot, i ) + Vec_IntSort( vPivot, 0 ); + // create pivots for internal nodes while growing MFFCs + vCommon = Vec_IntAlloc( 100 ); + vCommon2 = Vec_IntAlloc( 100 ); + Gia_ManForEachAnd( p, pObj, i ) + { + // find commont pivots + // the slow down happens because some PIs have very large sets of pivots + vPivot0 = Vec_WecEntry( vPivots, Gia_ObjFaninId0(pObj, i) ); + vPivot1 = Vec_WecEntry( vPivots, Gia_ObjFaninId1(pObj, i) ); + Vec_IntTwoFindCommon( vPivot0, vPivot1, vCommon ); + if ( Gia_ObjIsMuxId(p, i) ) + { + vPivot = Vec_WecEntry( vPivots, Gia_ObjFaninId2(p, i) ); + Vec_IntTwoFindCommon( vPivot, vCommon, vCommon2 ); + ABC_SWAP( Vec_Int_t *, vCommon, vCommon2 ); + } + if ( Vec_IntSize(vCommon) == 0 ) + continue; + // add new pivots (this trick increased memory used in vPivots) + vPivot = Vec_WecEntry( vPivots, i ); + Vec_IntTwoMerge2( vPivot, vCommon, vCommon2 ); + ABC_SWAP( Vec_Int_t, *vPivot, *vCommon2 ); + // grow MFFCs + Vec_IntForEachEntry( vCommon, iObj, k ) + { + iMffc = Vec_IntEntry( vMap, iObj ); + assert( iMffc != -1 ); + vMffc = Vec_WecEntry( vMffcs, iMffc ); + Vec_IntPush( vMffc, i ); + } + } +//Abc_PrintTime( 1, "Time", Abc_Clock() - clkStart ); + Vec_IntFree( vCommon ); + Vec_IntFree( vCommon2 ); + Vec_IntFree( vMap ); + Gia_ManPrintDivStats( p, vMffcs, vPivots ); + Vec_WecFree( vPivots ); + // returns the modified array of MFFCs +} +void Gia_ManResubTest( Gia_Man_t * p ) +{ + Vec_Wec_t * vMffcs; + Gia_Man_t * pNew = Gia_ManDupMuxes( p, 2 ); +abctime clkStart = Abc_Clock(); + vMffcs = Gia_ManComputeMffcs( pNew, 4, 100, 8, 100 ); + Gia_ManAddDivisors( pNew, vMffcs ); + Vec_WecFree( vMffcs ); +Abc_PrintTime( 1, "Time", Abc_Clock() - clkStart ); + Gia_ManStop( pNew ); +} +#endif + + + + +/**Function************************************************************* + + Synopsis [Resubstitution data-structure.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +typedef struct Gia_ResbMan_t_ Gia_ResbMan_t; +struct Gia_ResbMan_t_ +{ + int nWords; + int nLimit; + int nDivsMax; + int iChoice; + int fUseXor; + int fDebug; + int fVerbose; + int fVeryVerbose; + Vec_Ptr_t * vDivs; + Vec_Int_t * vGates; + Vec_Int_t * vUnateLits[2]; + Vec_Int_t * vNotUnateVars[2]; + Vec_Int_t * vUnatePairs[2]; + Vec_Int_t * vBinateVars; + Vec_Int_t * vUnateLitsW[2]; + Vec_Int_t * vUnatePairsW[2]; + Vec_Wec_t * vSorter; + word * pSets[2]; + word * pDivA; + word * pDivB; + Vec_Wrd_t * vSims; +}; +inline Gia_ResbMan_t * Gia_ResbAlloc( int nWords ) +{ + Gia_ResbMan_t * p = ABC_CALLOC( Gia_ResbMan_t, 1 ); + p->nWords = nWords; + p->vUnateLits[0] = Vec_IntAlloc( 100 ); + p->vUnateLits[1] = Vec_IntAlloc( 100 ); + p->vNotUnateVars[0] = Vec_IntAlloc( 100 ); + p->vNotUnateVars[1] = Vec_IntAlloc( 100 ); + p->vUnatePairs[0] = Vec_IntAlloc( 100 ); + p->vUnatePairs[1] = Vec_IntAlloc( 100 ); + p->vUnateLitsW[0] = Vec_IntAlloc( 100 ); + p->vUnateLitsW[1] = Vec_IntAlloc( 100 ); + p->vUnatePairsW[0] = Vec_IntAlloc( 100 ); + p->vUnatePairsW[1] = Vec_IntAlloc( 100 ); + p->vSorter = Vec_WecAlloc( nWords*64 ); + p->vBinateVars = Vec_IntAlloc( 100 ); + p->vGates = Vec_IntAlloc( 100 ); + p->vDivs = Vec_PtrAlloc( 100 ); + p->pSets[0] = ABC_CALLOC( word, nWords ); + p->pSets[1] = ABC_CALLOC( word, nWords ); + p->pDivA = ABC_CALLOC( word, nWords ); + p->pDivB = ABC_CALLOC( word, nWords ); + p->vSims = Vec_WrdAlloc( 100 ); + return p; +} +inline void Gia_ResbInit( Gia_ResbMan_t * p, Vec_Ptr_t * vDivs, int nWords, int nLimit, int nDivsMax, int iChoice, int fUseXor, int fDebug, int fVerbose, int fVeryVerbose ) +{ + assert( p->nWords == nWords ); + p->nLimit = nLimit; + p->nDivsMax = nDivsMax; + p->iChoice = iChoice; + p->fUseXor = fUseXor; + p->fDebug = fDebug; + p->fVerbose = fVerbose; + p->fVeryVerbose = fVeryVerbose; + Abc_TtCopy( p->pSets[0], (word *)Vec_PtrEntry(vDivs, 0), nWords, 0 ); + Abc_TtCopy( p->pSets[1], (word *)Vec_PtrEntry(vDivs, 1), nWords, 0 ); + Vec_PtrClear( p->vDivs ); + Vec_PtrAppend( p->vDivs, vDivs ); + Vec_IntClear( p->vGates ); + Vec_IntClear( p->vUnateLits[0] ); + Vec_IntClear( p->vUnateLits[1] ); + Vec_IntClear( p->vNotUnateVars[0] ); + Vec_IntClear( p->vNotUnateVars[1] ); + Vec_IntClear( p->vUnatePairs[0] ); + Vec_IntClear( p->vUnatePairs[1] ); + Vec_IntClear( p->vUnateLitsW[0] ); + Vec_IntClear( p->vUnateLitsW[1] ); + Vec_IntClear( p->vUnatePairsW[0] ); + Vec_IntClear( p->vUnatePairsW[1] ); + Vec_IntClear( p->vBinateVars ); +} +inline void Gia_ResbFree( Gia_ResbMan_t * p ) +{ + Vec_IntFree( p->vUnateLits[0] ); + Vec_IntFree( p->vUnateLits[1] ); + Vec_IntFree( p->vNotUnateVars[0] ); + Vec_IntFree( p->vNotUnateVars[1] ); + Vec_IntFree( p->vUnatePairs[0] ); + Vec_IntFree( p->vUnatePairs[1] ); + Vec_IntFree( p->vUnateLitsW[0] ); + Vec_IntFree( p->vUnateLitsW[1] ); + Vec_IntFree( p->vUnatePairsW[0] ); + Vec_IntFree( p->vUnatePairsW[1] ); + Vec_IntFree( p->vBinateVars ); + Vec_IntFree( p->vGates ); + Vec_WrdFree( p->vSims ); + Vec_PtrFree( p->vDivs ); + Vec_WecFree( p->vSorter ); + ABC_FREE( p->pSets[0] ); + ABC_FREE( p->pSets[1] ); + ABC_FREE( p->pDivA ); + ABC_FREE( p->pDivB ); + ABC_FREE( p ); +} + +/**Function************************************************************* + + Synopsis [Print resubstitution.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +inline void Gia_ManResubPrintNode( Vec_Int_t * vRes, int nVars, int Node, int fCompl ) +{ + extern void Gia_ManResubPrintLit( Vec_Int_t * vRes, int nVars, int iLit ); + int iLit0 = Vec_IntEntry( vRes, 2*Node + 0 ); + int iLit1 = Vec_IntEntry( vRes, 2*Node + 1 ); + assert( iLit0 != iLit1 ); + if ( iLit0 > iLit1 && Abc_LitIsCompl(fCompl) ) // xor + { + printf( "~" ); + fCompl = 0; + } + printf( "(" ); + Gia_ManResubPrintLit( vRes, nVars, Abc_LitNotCond(iLit0, fCompl) ); + printf( " %c ", iLit0 > iLit1 ? '^' : (fCompl ? '|' : '&') ); + Gia_ManResubPrintLit( vRes, nVars, Abc_LitNotCond(iLit1, fCompl) ); + printf( ")" ); +} +inline void Gia_ManResubPrintLit( Vec_Int_t * vRes, int nVars, int iLit ) +{ + if ( Abc_Lit2Var(iLit) < nVars ) + { + if ( nVars < 26 ) + printf( "%s%c", Abc_LitIsCompl(iLit) ? "~":"", 'a' + Abc_Lit2Var(iLit)-2 ); + else + printf( "%si%d", Abc_LitIsCompl(iLit) ? "~":"", Abc_Lit2Var(iLit)-2 ); + } + else + Gia_ManResubPrintNode( vRes, nVars, Abc_Lit2Var(iLit) - nVars, Abc_LitIsCompl(iLit) ); +} +inline int Gia_ManResubPrint( Vec_Int_t * vRes, int nVars ) +{ + int iTopLit; + if ( Vec_IntSize(vRes) == 0 ) + return printf( "none" ); + assert( Vec_IntSize(vRes) % 2 == 1 ); + iTopLit = Vec_IntEntryLast(vRes); + if ( iTopLit == 0 ) + return printf( "const0" ); + if ( iTopLit == 1 ) + return printf( "const1" ); + Gia_ManResubPrintLit( vRes, nVars, iTopLit ); + return 0; +} + +/**Function************************************************************* + + Synopsis [Verify resubstitution.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +inline int Gia_ManResubVerify( Gia_ResbMan_t * p, word * pFunc ) +{ + int nVars = Vec_PtrSize(p->vDivs); + int iTopLit, RetValue; + word * pDivRes; + if ( Vec_IntSize(p->vGates) == 0 ) + return -1; + iTopLit = Vec_IntEntryLast(p->vGates); + assert( iTopLit >= 0 ); + if ( iTopLit == 0 ) + { + if ( pFunc ) Abc_TtClear( pFunc, p->nWords ); + return Abc_TtIsConst0( p->pSets[1], p->nWords ); + } + if ( iTopLit == 1 ) + { + if ( pFunc ) Abc_TtFill( pFunc, p->nWords ); + return Abc_TtIsConst0( p->pSets[0], p->nWords ); + } + if ( Abc_Lit2Var(iTopLit) < nVars ) + { + assert( Vec_IntSize(p->vGates) == 1 ); + pDivRes = (word *)Vec_PtrEntry( p->vDivs, Abc_Lit2Var(iTopLit) ); + } + else + { + int i, iLit0, iLit1; + assert( Vec_IntSize(p->vGates) > 1 ); + assert( Vec_IntSize(p->vGates) % 2 == 1 ); + assert( Abc_Lit2Var(iTopLit)-nVars == Vec_IntSize(p->vGates)/2-1 ); + Vec_WrdFill( p->vSims, p->nWords * Vec_IntSize(p->vGates)/2, 0 ); + Vec_IntForEachEntryDouble( p->vGates, iLit0, iLit1, i ) + { + int iVar0 = Abc_Lit2Var(iLit0); + int iVar1 = Abc_Lit2Var(iLit1); + word * pDiv0 = iVar0 < nVars ? (word *)Vec_PtrEntry(p->vDivs, iVar0) : Vec_WrdEntryP(p->vSims, p->nWords*(iVar0 - nVars)); + word * pDiv1 = iVar1 < nVars ? (word *)Vec_PtrEntry(p->vDivs, iVar1) : Vec_WrdEntryP(p->vSims, p->nWords*(iVar1 - nVars)); + word * pDiv = Vec_WrdEntryP(p->vSims, p->nWords*i/2); + if ( iVar0 < iVar1 ) + Abc_TtAndCompl( pDiv, pDiv0, Abc_LitIsCompl(iLit0), pDiv1, Abc_LitIsCompl(iLit1), p->nWords ); + else if ( iVar0 > iVar1 ) + { + assert( !Abc_LitIsCompl(iLit0) ); + assert( !Abc_LitIsCompl(iLit1) ); + Abc_TtXor( pDiv, pDiv0, pDiv1, p->nWords, 0 ); + } + else assert( 0 ); + } + pDivRes = Vec_WrdEntryP( p->vSims, p->nWords*(Vec_IntSize(p->vGates)/2-1) ); + } + if ( Abc_LitIsCompl(iTopLit) ) + RetValue = !Abc_TtIntersectOne(p->pSets[1], 0, pDivRes, 0, p->nWords) && !Abc_TtIntersectOne(p->pSets[0], 0, pDivRes, 1, p->nWords); + else + RetValue = !Abc_TtIntersectOne(p->pSets[0], 0, pDivRes, 0, p->nWords) && !Abc_TtIntersectOne(p->pSets[1], 0, pDivRes, 1, p->nWords); + if ( pFunc ) Abc_TtCopy( pFunc, pDivRes, p->nWords, Abc_LitIsCompl(iTopLit) ); + return RetValue; +} + +#if 0 +/**Function************************************************************* + + Synopsis [Construct AIG manager from gates.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_ManConstructFromMap( Gia_Man_t * pNew, Vec_Int_t * vGates, int nVars, Vec_Int_t * vUsed, Vec_Int_t * vCopy, int fHash ) +{ + int i, iLit0, iLit1, iLitRes, iTopLit = Vec_IntEntryLast( vGates ); + assert( Vec_IntSize(vUsed) == nVars ); + assert( Vec_IntSize(vGates) > 1 ); + assert( Vec_IntSize(vGates) % 2 == 1 ); + assert( Abc_Lit2Var(iTopLit)-nVars == Vec_IntSize(vGates)/2-1 ); + Vec_IntClear( vCopy ); + Vec_IntForEachEntryDouble( vGates, iLit0, iLit1, i ) + { + int iVar0 = Abc_Lit2Var(iLit0); + int iVar1 = Abc_Lit2Var(iLit1); + int iRes0 = iVar0 < nVars ? Vec_IntEntry(vUsed, iVar0) : Vec_IntEntry(vCopy, iVar0 - nVars); + int iRes1 = iVar1 < nVars ? Vec_IntEntry(vUsed, iVar1) : Vec_IntEntry(vCopy, iVar1 - nVars); + if ( iVar0 < iVar1 ) + { + if ( fHash ) + iLitRes = Gia_ManHashAnd( pNew, Abc_LitNotCond(iRes0, Abc_LitIsCompl(iLit0)), Abc_LitNotCond(iRes1, Abc_LitIsCompl(iLit1)) ); + else + iLitRes = Gia_ManAppendAnd( pNew, Abc_LitNotCond(iRes0, Abc_LitIsCompl(iLit0)), Abc_LitNotCond(iRes1, Abc_LitIsCompl(iLit1)) ); + } + else if ( iVar0 > iVar1 ) + { + assert( !Abc_LitIsCompl(iLit0) ); + assert( !Abc_LitIsCompl(iLit1) ); + if ( fHash ) + iLitRes = Gia_ManHashXor( pNew, Abc_LitNotCond(iRes0, Abc_LitIsCompl(iLit0)), Abc_LitNotCond(iRes1, Abc_LitIsCompl(iLit1)) ); + else + iLitRes = Gia_ManAppendXor( pNew, Abc_LitNotCond(iRes0, Abc_LitIsCompl(iLit0)), Abc_LitNotCond(iRes1, Abc_LitIsCompl(iLit1)) ); + } + else assert( 0 ); + Vec_IntPush( vCopy, iLitRes ); + } + assert( Vec_IntSize(vCopy) == Vec_IntSize(vGates)/2 ); + iLitRes = Vec_IntEntry( vCopy, Vec_IntSize(vGates)/2-1 ); + return iLitRes; +} +Gia_Man_t * Gia_ManConstructFromGates( Vec_Wec_t * vFuncs, int nVars ) +{ + Vec_Int_t * vGates; int i, k, iLit; + Vec_Int_t * vCopy = Vec_IntAlloc( 100 ); + Vec_Int_t * vUsed = Vec_IntStartFull( nVars ); + Gia_Man_t * pNew = Gia_ManStart( 100 ); + pNew->pName = Abc_UtilStrsav( "resub" ); + Vec_WecForEachLevel( vFuncs, vGates, i ) + { + assert( Vec_IntSize(vGates) % 2 == 1 ); + Vec_IntForEachEntry( vGates, iLit, k ) + { + int iVar = Abc_Lit2Var(iLit); + if ( iVar > 0 && iVar < nVars && Vec_IntEntry(vUsed, iVar) == -1 ) + Vec_IntWriteEntry( vUsed, iVar, Gia_ManAppendCi(pNew) ); + } + } + Vec_WecForEachLevel( vFuncs, vGates, i ) + { + int iLitRes, iTopLit = Vec_IntEntryLast( vGates ); + if ( Abc_Lit2Var(iTopLit) == 0 ) + iLitRes = 0; + else if ( Abc_Lit2Var(iTopLit) < nVars ) + iLitRes = Gia_ManAppendCi(pNew); + else + iLitRes = Gia_ManConstructFromMap( pNew, vGates, nVars, vUsed, vCopy, 0 ); + Gia_ManAppendCo( pNew, Abc_LitNotCond( iLitRes, Abc_LitIsCompl(iTopLit) ) ); + } + Vec_IntFree( vCopy ); + Vec_IntFree( vUsed ); + return pNew; +} +#endif + +#if 0 +/**Function************************************************************* + + Synopsis [Construct AIG manager from gates.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManInsertOrder_rec( Gia_Man_t * p, int iObj, Vec_Int_t * vObjs, Vec_Wec_t * vFuncs, Vec_Int_t * vNodes ) +{ + Gia_Obj_t * pObj = Gia_ManObj( p, iObj ); + if ( iObj == 0 ) + return; + if ( pObj->fPhase ) + { + int nVars = Gia_ManObjNum(p); + int k, iLit, Index = Vec_IntFind( vObjs, iObj ); + Vec_Int_t * vGates = Vec_WecEntry( vFuncs, Index ); + assert( Gia_ObjIsCo(pObj) || Gia_ObjIsAnd(pObj) ); + Vec_IntForEachEntry( vGates, iLit, k ) + if ( Abc_Lit2Var(iLit) < nVars ) + Gia_ManInsertOrder_rec( p, Abc_Lit2Var(iLit), vObjs, vFuncs, vNodes ); + } + else if ( Gia_ObjIsCo(pObj) ) + Gia_ManInsertOrder_rec( p, Gia_ObjFaninId0p(p, pObj), vObjs, vFuncs, vNodes ); + else if ( Gia_ObjIsAnd(pObj) ) + { + Gia_ManInsertOrder_rec( p, Gia_ObjFaninId0p(p, pObj), vObjs, vFuncs, vNodes ); + Gia_ManInsertOrder_rec( p, Gia_ObjFaninId1p(p, pObj), vObjs, vFuncs, vNodes ); + } + else assert( Gia_ObjIsCi(pObj) ); + if ( !Gia_ObjIsCi(pObj) ) + Vec_IntPush( vNodes, iObj ); +} +Vec_Int_t * Gia_ManInsertOrder( Gia_Man_t * p, Vec_Int_t * vObjs, Vec_Wec_t * vFuncs ) +{ + int i, Id; + Vec_Int_t * vNodes = Vec_IntAlloc( Gia_ManObjNum(p) ); + Gia_ManForEachCoId( p, Id, i ) + Gia_ManInsertOrder_rec( p, Id, vObjs, vFuncs, vNodes ); + return vNodes; +} +Gia_Man_t * Gia_ManInsertFromGates( Gia_Man_t * p, Vec_Int_t * vObjs, Vec_Wec_t * vFuncs ) +{ + Gia_Man_t * pNew, * pTemp; + Gia_Obj_t * pObj; + int i, nVars = Gia_ManObjNum(p); + Vec_Int_t * vUsed = Vec_IntStartFull( nVars ); + Vec_Int_t * vNodes, * vCopy = Vec_IntAlloc(100); + Gia_ManForEachObjVec( vObjs, p, pObj, i ) + pObj->fPhase = 1; + vNodes = Gia_ManInsertOrder( p, vObjs, vFuncs ); + pNew = Gia_ManStart( Gia_ManObjNum(p) + 1000 ); + Gia_ManHashStart( pNew ); + Gia_ManConst0(p)->Value = 0; + Gia_ManForEachCi( p, pObj, i ) + pObj->Value = Gia_ManAppendCi( pNew ); + Gia_ManForEachObjVec( vNodes, p, pObj, i ) + if ( !pObj->fPhase ) + { + if ( Gia_ObjIsCo(pObj) ) + pObj->Value = Gia_ObjFanin0Copy(pObj); + else if ( Gia_ObjIsAnd(pObj) ) + pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + else assert( 0 ); + } + else + { + int k, iLit, Index = Vec_IntFind( vObjs, Gia_ObjId(p, pObj) ); + Vec_Int_t * vGates = Vec_WecEntry( vFuncs, Index ); + int iLitRes, iTopLit = Vec_IntEntryLast( vGates ); + if ( Abc_Lit2Var(iTopLit) == 0 ) + iLitRes = 0; + else if ( Abc_Lit2Var(iTopLit) < nVars ) + iLitRes = Gia_ManObj(p, Abc_Lit2Var(iTopLit))->Value; + else + { + Vec_IntForEachEntry( vGates, iLit, k ) + Vec_IntWriteEntry( vUsed, Abc_Lit2Var(iLit), Gia_ManObj(p, Abc_Lit2Var(iLit))->Value ); + iLitRes = Gia_ManConstructFromMap( pNew, vGates, nVars, vUsed, vCopy, 1 ); + Vec_IntForEachEntry( vGates, iLit, k ) + Vec_IntWriteEntry( vUsed, Abc_Lit2Var(iLit), -1 ); + } + pObj->Value = Abc_LitNotCond( iLitRes, Abc_LitIsCompl(iTopLit) ); + } + Gia_ManForEachCo( p, pObj, i ) + Gia_ManAppendCo( pNew, pObj->Value ); + Gia_ManForEachObjVec( vObjs, p, pObj, i ) + pObj->fPhase = 0; + Gia_ManHashStop( pNew ); + pNew = Gia_ManCleanup( pTemp = pNew ); + Gia_ManStop( pTemp ); + Vec_IntFree( vNodes ); + Vec_IntFree( vUsed ); + Vec_IntFree( vCopy ); + Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) ); + return pNew; +} +#endif + +/**Function************************************************************* + + Synopsis [Perform resubstitution.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Gia_ManFindFirstCommonLit( Vec_Int_t * vArr1, Vec_Int_t * vArr2, int fVerbose ) +{ + (void)fVerbose; + + int * pBeg1 = vArr1->pArray; + int * pBeg2 = vArr2->pArray; + int * pEnd1 = vArr1->pArray + vArr1->nSize; + int * pEnd2 = vArr2->pArray + vArr2->nSize; + int * pStart1 = vArr1->pArray; + int * pStart2 = vArr2->pArray; + int nRemoved = 0; + while ( pBeg1 < pEnd1 && pBeg2 < pEnd2 ) + { + if ( Abc_Lit2Var(*pBeg1) == Abc_Lit2Var(*pBeg2) ) + { + if ( *pBeg1 != *pBeg2 ) + return *pBeg1; + else + pBeg1++, pBeg2++; + nRemoved++; + } + else if ( *pBeg1 < *pBeg2 ) + *pStart1++ = *pBeg1++; + else + *pStart2++ = *pBeg2++; + } + while ( pBeg1 < pEnd1 ) + *pStart1++ = *pBeg1++; + while ( pBeg2 < pEnd2 ) + *pStart2++ = *pBeg2++; + Vec_IntShrink( vArr1, pStart1 - vArr1->pArray ); + Vec_IntShrink( vArr2, pStart2 - vArr2->pArray ); + //if ( fVerbose ) printf( "Removed %d duplicated entries. Array1 = %d. Array2 = %d.\n", nRemoved, Vec_IntSize(vArr1), Vec_IntSize(vArr2) ); + return -1; +} + +inline void Gia_ManFindOneUnateInt( word * pOff, word * pOn, Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnateLits, Vec_Int_t * vNotUnateVars ) +{ + (void)pOn; + + word * pDiv; int i; + Vec_IntClear( vUnateLits ); + Vec_IntClear( vNotUnateVars ); + Vec_PtrForEachEntryStart( word *, vDivs, pDiv, i, 2 ) + if ( !Abc_TtIntersectOne( pOff, 0, pDiv, 0, nWords ) ) + Vec_IntPush( vUnateLits, Abc_Var2Lit(i, 0) ); + else if ( !Abc_TtIntersectOne( pOff, 0, pDiv, 1, nWords ) ) + Vec_IntPush( vUnateLits, Abc_Var2Lit(i, 1) ); + else + Vec_IntPush( vNotUnateVars, i ); +} +inline int Gia_ManFindOneUnate( word * pSets[2], Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnateLits[2], Vec_Int_t * vNotUnateVars[2], int fVerbose ) +{ + int n; + if ( fVerbose ) printf( " " ); + for ( n = 0; n < 2; n++ ) + { + Gia_ManFindOneUnateInt( pSets[n], pSets[!n], vDivs, nWords, vUnateLits[n], vNotUnateVars[n] ); + if ( fVerbose ) printf( "U%d =%4d ", n, Vec_IntSize(vUnateLits[n]) ); + } + return Gia_ManFindFirstCommonLit( vUnateLits[0], vUnateLits[1], fVerbose ); +} + +static inline int Gia_ManDivCover( word * pOff, word * pOn, word * pDivA, int ComplA, word * pDivB, int ComplB, int nWords ) +{ + (void)pOff; + + //assert( !Abc_TtIntersectOne(pOff, 0, pDivA, ComplA, nWords) ); + //assert( !Abc_TtIntersectOne(pOff, 0, pDivB, ComplB, nWords) ); + return !Abc_TtIntersectTwo( pOn, 0, pDivA, !ComplA, pDivB, !ComplB, nWords ); +} +inline int Gia_ManFindTwoUnateInt( word * pOff, word * pOn, Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnateLits, Vec_Int_t * vUnateLitsW, int * pnPairs ) +{ + int i, k, iDiv0_, iDiv1_, Cover0, Cover1; + int nTotal = Abc_TtCountOnesVec( pOn, nWords ); + (*pnPairs) = 0; + Vec_IntForEachEntryTwo( vUnateLits, vUnateLitsW, iDiv0_, Cover0, i ) + { + if ( 2*Cover0 < nTotal ) + break; + Vec_IntForEachEntryTwoStart( vUnateLits, vUnateLitsW, iDiv1_, Cover1, k, i+1 ) + { + int iDiv0 = Abc_MinInt( iDiv0_, iDiv1_ ); + int iDiv1 = Abc_MaxInt( iDiv0_, iDiv1_ ); + word * pDiv0 = (word *)Vec_PtrEntry(vDivs, Abc_Lit2Var(iDiv0)); + word * pDiv1 = (word *)Vec_PtrEntry(vDivs, Abc_Lit2Var(iDiv1)); + if ( Cover0 + Cover1 < nTotal ) + break; + (*pnPairs)++; + if ( Gia_ManDivCover(pOff, pOn, pDiv1, Abc_LitIsCompl(iDiv1), pDiv0, Abc_LitIsCompl(iDiv0), nWords) ) + return Abc_Var2Lit((Abc_LitNot(iDiv1) << 15) | Abc_LitNot(iDiv0), 1); + } + } + return -1; +} +inline int Gia_ManFindTwoUnate( word * pSets[2], Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnateLits[2], Vec_Int_t * vUnateLitsW[2], int fVerbose ) +{ + int n, iLit, nPairs; + if ( fVerbose ) printf( " " ); + for ( n = 0; n < 2; n++ ) + { + //int nPairsAll = Vec_IntSize(vUnateLits[n])*(Vec_IntSize(vUnateLits[n])-1)/2; + iLit = Gia_ManFindTwoUnateInt( pSets[n], pSets[!n], vDivs, nWords, vUnateLits[n], vUnateLitsW[n], &nPairs ); + if ( fVerbose ) printf( "UU%d =%5d ", n, nPairs ); + if ( iLit >= 0 ) + return Abc_LitNotCond(iLit, n); + } + return -1; +} + +inline void Gia_ManFindXorInt( word * pOff, word * pOn, Vec_Int_t * vBinate, Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnatePairs ) +{ + (void)pOn; + + int i, k, iDiv0_, iDiv1_; + int Limit2 = Vec_IntSize(vBinate);//Abc_MinInt( Vec_IntSize(vBinate), 100 ); + Vec_IntForEachEntryStop( vBinate, iDiv1_, i, Limit2 ) + Vec_IntForEachEntryStop( vBinate, iDiv0_, k, i ) + { + int iDiv0 = Abc_MinInt( iDiv0_, iDiv1_ ); + int iDiv1 = Abc_MaxInt( iDiv0_, iDiv1_ ); + word * pDiv0 = (word *)Vec_PtrEntry(vDivs, iDiv0); + word * pDiv1 = (word *)Vec_PtrEntry(vDivs, iDiv1); + if ( !Abc_TtIntersectXor( pOff, 0, pDiv0, pDiv1, 0, nWords ) ) + Vec_IntPush( vUnatePairs, Abc_Var2Lit((Abc_Var2Lit(iDiv0, 0) << 15) | Abc_Var2Lit(iDiv1, 0), 0) ); + else if ( !Abc_TtIntersectXor( pOff, 0, pDiv0, pDiv1, 1, nWords ) ) + Vec_IntPush( vUnatePairs, Abc_Var2Lit((Abc_Var2Lit(iDiv0, 0) << 15) | Abc_Var2Lit(iDiv1, 0), 1) ); + } +} +inline int Gia_ManFindXor( word * pSets[2], Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vBinateVars, Vec_Int_t * vUnatePairs[2], int fVerbose ) +{ + int n; + if ( fVerbose ) printf( " " ); + for ( n = 0; n < 2; n++ ) + { + Vec_IntClear( vUnatePairs[n] ); + Gia_ManFindXorInt( pSets[n], pSets[!n], vBinateVars, vDivs, nWords, vUnatePairs[n] ); + if ( fVerbose ) printf( "UX%d =%5d ", n, Vec_IntSize(vUnatePairs[n]) ); + } + return Gia_ManFindFirstCommonLit( vUnatePairs[0], vUnatePairs[1], fVerbose ); +} + +inline void Gia_ManFindUnatePairsInt( word * pOff, word * pOn, Vec_Int_t * vBinate, Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnatePairs ) +{ + int n, i, k, iDiv0_, iDiv1_; + int Limit2 = Vec_IntSize(vBinate);//Abc_MinInt( Vec_IntSize(vBinate), 100 ); + Vec_IntForEachEntryStop( vBinate, iDiv1_, i, Limit2 ) + Vec_IntForEachEntryStop( vBinate, iDiv0_, k, i ) + { + int iDiv0 = Abc_MinInt( iDiv0_, iDiv1_ ); + int iDiv1 = Abc_MaxInt( iDiv0_, iDiv1_ ); + word * pDiv0 = (word *)Vec_PtrEntry(vDivs, iDiv0); + word * pDiv1 = (word *)Vec_PtrEntry(vDivs, iDiv1); + for ( n = 0; n < 4; n++ ) + { + int iLit0 = Abc_Var2Lit( iDiv0, n&1 ); + int iLit1 = Abc_Var2Lit( iDiv1, n>>1 ); + //if ( !Abc_TtIntersectTwo( pOff, 0, pDiv1, n>>1, pDiv0, n&1, nWords ) ) + if ( !Abc_TtIntersectTwo( pOff, 0, pDiv1, n>>1, pDiv0, n&1, nWords ) && Abc_TtIntersectTwo( pOn, 0, pDiv1, n>>1, pDiv0, n&1, nWords ) ) + Vec_IntPush( vUnatePairs, Abc_Var2Lit((iLit1 << 15) | iLit0, 0) ); + } + } +} +inline void Gia_ManFindUnatePairs( word * pSets[2], Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vBinateVars, Vec_Int_t * vUnatePairs[2], int fVerbose ) +{ + int n, RetValue; + if ( fVerbose ) printf( " " ); + for ( n = 0; n < 2; n++ ) + { + int nBefore = Vec_IntSize(vUnatePairs[n]); + Gia_ManFindUnatePairsInt( pSets[n], pSets[!n], vBinateVars, vDivs, nWords, vUnatePairs[n] ); + if ( fVerbose ) printf( "UP%d =%5d ", n, Vec_IntSize(vUnatePairs[n])-nBefore ); + } + RetValue = Gia_ManFindFirstCommonLit( vUnatePairs[0], vUnatePairs[1], fVerbose ); + assert( RetValue == -1 ); (void)RetValue; +} + +inline void Gia_ManDeriveDivPair( int iDiv, Vec_Ptr_t * vDivs, int nWords, word * pRes ) +{ + int fComp = Abc_LitIsCompl(iDiv); + int iDiv0 = Abc_Lit2Var(iDiv) & 0x7FFF; + int iDiv1 = Abc_Lit2Var(iDiv) >> 15; + word * pDiv0 = (word *)Vec_PtrEntry(vDivs, Abc_Lit2Var(iDiv0)); + word * pDiv1 = (word *)Vec_PtrEntry(vDivs, Abc_Lit2Var(iDiv1)); + if ( iDiv0 < iDiv1 ) + { + assert( !fComp ); (void)fComp; + Abc_TtAndCompl( pRes, pDiv0, Abc_LitIsCompl(iDiv0), pDiv1, Abc_LitIsCompl(iDiv1), nWords ); + } + else + { + assert( !Abc_LitIsCompl(iDiv0) ); + assert( !Abc_LitIsCompl(iDiv1) ); + Abc_TtXor( pRes, pDiv0, pDiv1, nWords, 0 ); + } +} +inline int Gia_ManFindDivGateInt( word * pOff, word * pOn, Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnateLits, Vec_Int_t * vUnatePairs, Vec_Int_t * vUnateLitsW, Vec_Int_t * vUnatePairsW, word * pDivTemp ) +{ + int i, k, iDiv0, iDiv1, Cover0, Cover1; + int nTotal = Abc_TtCountOnesVec( pOn, nWords ); + Vec_IntForEachEntryTwo( vUnateLits, vUnateLitsW, iDiv0, Cover0, i ) + { + word * pDiv0 = (word *)Vec_PtrEntry(vDivs, Abc_Lit2Var(iDiv0)); + if ( 2*Cover0 < nTotal ) + break; + Vec_IntForEachEntryTwo( vUnatePairs, vUnatePairsW, iDiv1, Cover1, k ) + { + int fComp1 = Abc_LitIsCompl(iDiv1); + if ( Cover0 + Cover1 < nTotal ) + break; + Gia_ManDeriveDivPair( iDiv1, vDivs, nWords, pDivTemp ); + if ( Gia_ManDivCover(pOff, pOn, pDiv0, Abc_LitIsCompl(iDiv0), pDivTemp, fComp1, nWords) ) + return Abc_Var2Lit((Abc_Var2Lit(k, 1) << 15) | Abc_LitNot(iDiv0), 1); + } + } + return -1; +} +inline int Gia_ManFindDivGate( word * pSets[2], Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnateLits[2], Vec_Int_t * vUnatePairs[2], Vec_Int_t * vUnateLitsW[2], Vec_Int_t * vUnatePairsW[2], word * pDivTemp ) +{ + int n, iLit; + for ( n = 0; n < 2; n++ ) + { + iLit = Gia_ManFindDivGateInt( pSets[n], pSets[!n], vDivs, nWords, vUnateLits[n], vUnatePairs[n], vUnateLitsW[n], vUnatePairsW[n], pDivTemp ); + if ( iLit >= 0 ) + return Abc_LitNotCond( iLit, n ); + } + return -1; +} + +inline int Gia_ManFindGateGateInt( word * pOff, word * pOn, Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnatePairs, Vec_Int_t * vUnatePairsW, word * pDivTempA, word * pDivTempB ) +{ + int i, k, iDiv0, iDiv1, Cover0, Cover1; + int nTotal = Abc_TtCountOnesVec( pOn, nWords ); + Vec_IntForEachEntryTwo( vUnatePairs, vUnatePairsW, iDiv0, Cover0, k ) + { + int fCompA = Abc_LitIsCompl(iDiv0); + if ( 2*Cover0 < nTotal ) + break; + Gia_ManDeriveDivPair( iDiv0, vDivs, nWords, pDivTempA ); + Vec_IntForEachEntryTwoStart( vUnatePairs, vUnatePairsW, iDiv1, Cover1, i, k+1 ) + { + int fCompB = Abc_LitIsCompl(iDiv1); + if ( Cover0 + Cover1 < nTotal ) + break; + Gia_ManDeriveDivPair( iDiv1, vDivs, nWords, pDivTempB ); + if ( Gia_ManDivCover(pOff, pOn, pDivTempA, fCompA, pDivTempB, fCompB, nWords) ) + return Abc_Var2Lit((Abc_Var2Lit(i, 1) << 15) | Abc_Var2Lit(k, 1), 1); + } + } + return -1; +} +inline int Gia_ManFindGateGate( word * pSets[2], Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnatePairs[2], Vec_Int_t * vUnatePairsW[2], word * pDivTempA, word * pDivTempB ) +{ + int n, iLit; + for ( n = 0; n < 2; n++ ) + { + iLit = Gia_ManFindGateGateInt( pSets[n], pSets[!n], vDivs, nWords, vUnatePairs[n], vUnatePairsW[n], pDivTempA, pDivTempB ); + if ( iLit >= 0 ) + return Abc_LitNotCond( iLit, n ); + } + return -1; +} + +inline void Gia_ManSortUnatesInt( word * pOff, word * pOn, Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnateLits, Vec_Int_t * vUnateLitsW, Vec_Wec_t * vSorter ) +{ + (void)pOff; + + int i, k, iLit; + Vec_Int_t * vLevel; + Vec_WecInit( vSorter, nWords*64 ); + Vec_IntForEachEntry( vUnateLits, iLit, i ) + { + word * pDiv = (word *)Vec_PtrEntry(vDivs, Abc_Lit2Var(iLit)); + //assert( !Abc_TtIntersectOne( pOff, 0, pDiv, Abc_LitIsCompl(iLit), nWords ) ); + Vec_WecPush( vSorter, Abc_TtCountOnesVecMask(pDiv, pOn, nWords, Abc_LitIsCompl(iLit)), iLit ); + } + Vec_IntClear( vUnateLits ); + Vec_IntClear( vUnateLitsW ); + Vec_WecForEachLevelReverse( vSorter, vLevel, k ) + Vec_IntForEachEntry( vLevel, iLit, i ) + { + Vec_IntPush( vUnateLits, iLit ); + Vec_IntPush( vUnateLitsW, k ); + } + //Vec_IntPrint( Vec_WecEntry(vSorter, 0) ); + Vec_WecClear( vSorter ); +} +inline void Gia_ManSortUnates( word * pSets[2], Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnateLits[2], Vec_Int_t * vUnateLitsW[2], Vec_Wec_t * vSorter ) +{ + int n; + for ( n = 0; n < 2; n++ ) + Gia_ManSortUnatesInt( pSets[n], pSets[!n], vDivs, nWords, vUnateLits[n], vUnateLitsW[n], vSorter ); +} + +inline void Gia_ManSortPairsInt( word * pOff, word * pOn, Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnatePairs, Vec_Int_t * vUnatePairsW, Vec_Wec_t * vSorter ) +{ + (void)pOff; + + int i, k, iPair; + Vec_Int_t * vLevel; + Vec_WecInit( vSorter, nWords*64 ); + Vec_IntForEachEntry( vUnatePairs, iPair, i ) + { + int fComp = Abc_LitIsCompl(iPair); + int iLit0 = Abc_Lit2Var(iPair) & 0x7FFF; + int iLit1 = Abc_Lit2Var(iPair) >> 15; + word * pDiv0 = (word *)Vec_PtrEntry( vDivs, Abc_Lit2Var(iLit0) ); + word * pDiv1 = (word *)Vec_PtrEntry( vDivs, Abc_Lit2Var(iLit1) ); + if ( iLit0 < iLit1 ) + { + assert( !fComp ); + //assert( !Abc_TtIntersectTwo( pOff, 0, pDiv0, Abc_LitIsCompl(iLit0), pDiv1, Abc_LitIsCompl(iLit1), nWords ) ); + Vec_WecPush( vSorter, Abc_TtCountOnesVecMask2(pDiv0, pDiv1, Abc_LitIsCompl(iLit0), Abc_LitIsCompl(iLit1), pOn, nWords), iPair ); + } + else + { + assert( !Abc_LitIsCompl(iLit0) ); + assert( !Abc_LitIsCompl(iLit1) ); + //assert( !Abc_TtIntersectXor( pOff, 0, pDiv0, pDiv1, fComp, nWords ) ); + Vec_WecPush( vSorter, Abc_TtCountOnesVecXorMask(pDiv0, pDiv1, fComp, pOn, nWords), iPair ); + } + } + Vec_IntClear( vUnatePairs ); + Vec_IntClear( vUnatePairsW ); + Vec_WecForEachLevelReverse( vSorter, vLevel, k ) + Vec_IntForEachEntry( vLevel, iPair, i ) + { + Vec_IntPush( vUnatePairs, iPair ); + Vec_IntPush( vUnatePairsW, k ); + } + //Vec_IntPrint( Vec_WecEntry(vSorter, 0) ); + Vec_WecClear( vSorter ); + +} +inline void Gia_ManSortPairs( word * pSets[2], Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnateLits[2], Vec_Int_t * vUnateLitsW[2], Vec_Wec_t * vSorter ) +{ + int n; + for ( n = 0; n < 2; n++ ) + Gia_ManSortPairsInt( pSets[n], pSets[!n], vDivs, nWords, vUnateLits[n], vUnateLitsW[n], vSorter ); +} + +inline void Gia_ManSortBinate( word * pSets[2], Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vBinateVars, Vec_Wec_t * vSorter ) +{ + Vec_Int_t * vLevel; + int nMints[2] = { Abc_TtCountOnesVec(pSets[0], nWords), Abc_TtCountOnesVec(pSets[1], nWords) }; + word * pBig = nMints[0] > nMints[1] ? pSets[0] : pSets[1]; + word * pSmo = nMints[0] > nMints[1] ? pSets[1] : pSets[0]; + int Big = Abc_MaxInt( nMints[0], nMints[1] ); + int Smo = Abc_MinInt( nMints[0], nMints[1] ); + int i, k, iDiv, Gain; + + Vec_WecInit( vSorter, nWords*64 ); + Vec_IntForEachEntry( vBinateVars, iDiv, i ) + { + word * pDiv = (word *)Vec_PtrEntry( vDivs, iDiv ); + int nInter[2] = { Abc_TtCountOnesVecMask(pBig, pDiv, nWords, 0), Abc_TtCountOnesVecMask(pSmo, pDiv, nWords, 0) }; + if ( nInter[0] < Big/2 ) // complement the divisor + { + nInter[0] = Big - nInter[0]; + nInter[1] = Smo - nInter[1]; + } + assert( nInter[0] >= Big/2 ); + Gain = Abc_MaxInt( 0, nInter[0] - Big/2 + Smo/2 - nInter[1] ); + Vec_WecPush( vSorter, Gain, iDiv ); + } + + Vec_IntClear( vBinateVars ); + Vec_WecForEachLevelReverse( vSorter, vLevel, k ) + Vec_IntForEachEntry( vLevel, iDiv, i ) + Vec_IntPush( vBinateVars, iDiv ); + Vec_WecClear( vSorter ); + + if ( Vec_IntSize(vBinateVars) > 2000 ) + Vec_IntShrink( vBinateVars, 2000 ); +} + +/**Function************************************************************* + + Synopsis [Perform resubstitution.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +inline int Gia_ManResubPerform_rec( Gia_ResbMan_t * p, int nLimit ) +{ + int TopOneW[2] = {0}, TopTwoW[2] = {0}, Max1, Max2, iResLit, nVars = Vec_PtrSize(p->vDivs); + if ( p->fVerbose ) + { + int nMints[2] = { Abc_TtCountOnesVec(p->pSets[0], p->nWords), Abc_TtCountOnesVec(p->pSets[1], p->nWords) }; + printf( " " ); + printf( "ISF: " ); + printf( "0=%5d (%5.2f %%) ", nMints[0], 100.0*nMints[0]/(64*p->nWords) ); + printf( "1=%5d (%5.2f %%) ", nMints[1], 100.0*nMints[1]/(64*p->nWords) ); + } + if ( Abc_TtIsConst0( p->pSets[1], p->nWords ) ) + return 0; + if ( Abc_TtIsConst0( p->pSets[0], p->nWords ) ) + return 1; + iResLit = Gia_ManFindOneUnate( p->pSets, p->vDivs, p->nWords, p->vUnateLits, p->vNotUnateVars, p->fVerbose ); + if ( iResLit >= 0 ) // buffer + return iResLit; + if ( nLimit == 0 ) + return -1; + Gia_ManSortUnates( p->pSets, p->vDivs, p->nWords, p->vUnateLits, p->vUnateLitsW, p->vSorter ); + iResLit = Gia_ManFindTwoUnate( p->pSets, p->vDivs, p->nWords, p->vUnateLits, p->vUnateLitsW, p->fVerbose ); + if ( iResLit >= 0 ) // and + { + int iNode = nVars + Vec_IntSize(p->vGates)/2; + int fComp = Abc_LitIsCompl(iResLit); + int iDiv0 = Abc_Lit2Var(iResLit) & 0x7FFF; + int iDiv1 = Abc_Lit2Var(iResLit) >> 15; + assert( iDiv0 < iDiv1 ); + Vec_IntPushTwo( p->vGates, iDiv0, iDiv1 ); + return Abc_Var2Lit( iNode, fComp ); + } + Vec_IntTwoFindCommon( p->vNotUnateVars[0], p->vNotUnateVars[1], p->vBinateVars ); + if ( Vec_IntSize(p->vBinateVars) > p->nDivsMax ) + Vec_IntShrink( p->vBinateVars, p->nDivsMax ); + if ( p->fVerbose ) printf( " B = %3d", Vec_IntSize(p->vBinateVars) ); + //Gia_ManSortBinate( p->pSets, p->vDivs, p->nWords, p->vBinateVars, p->vSorter ); + if ( p->fUseXor ) + { + iResLit = Gia_ManFindXor( p->pSets, p->vDivs, p->nWords, p->vBinateVars, p->vUnatePairs, p->fVerbose ); + if ( iResLit >= 0 ) // xor + { + int iNode = nVars + Vec_IntSize(p->vGates)/2; + int fComp = Abc_LitIsCompl(iResLit); + int iDiv0 = Abc_Lit2Var(iResLit) & 0x7FFF; + int iDiv1 = Abc_Lit2Var(iResLit) >> 15; + assert( !Abc_LitIsCompl(iDiv0) ); + assert( !Abc_LitIsCompl(iDiv1) ); + assert( iDiv0 > iDiv1 ); + Vec_IntPushTwo( p->vGates, iDiv0, iDiv1 ); + return Abc_Var2Lit( iNode, fComp ); + } + } + if ( nLimit == 1 ) + return -1; + Gia_ManFindUnatePairs( p->pSets, p->vDivs, p->nWords, p->vBinateVars, p->vUnatePairs, p->fVerbose ); + Gia_ManSortPairs( p->pSets, p->vDivs, p->nWords, p->vUnatePairs, p->vUnatePairsW, p->vSorter ); + iResLit = Gia_ManFindDivGate( p->pSets, p->vDivs, p->nWords, p->vUnateLits, p->vUnatePairs, p->vUnateLitsW, p->vUnatePairsW, p->pDivA ); + if ( iResLit >= 0 ) // and(div,pair) + { + int iNode = nVars + Vec_IntSize(p->vGates)/2; + + int fComp = Abc_LitIsCompl(iResLit); + int iDiv0 = Abc_Lit2Var(iResLit) & 0x7FFF; // div + int iDiv1 = Abc_Lit2Var(iResLit) >> 15; // pair + + int Div1 = Vec_IntEntry( p->vUnatePairs[!fComp], Abc_Lit2Var(iDiv1) ); + int fComp1 = Abc_LitIsCompl(Div1) ^ Abc_LitIsCompl(iDiv1); + int iDiv10 = Abc_Lit2Var(Div1) & 0x7FFF; + int iDiv11 = Abc_Lit2Var(Div1) >> 15; + + Vec_IntPushTwo( p->vGates, iDiv10, iDiv11 ); + Vec_IntPushTwo( p->vGates, iDiv0, Abc_Var2Lit(iNode, fComp1) ); + return Abc_Var2Lit( iNode+1, fComp ); + } + if ( nLimit == 2 ) + return -1; + iResLit = Gia_ManFindGateGate( p->pSets, p->vDivs, p->nWords, p->vUnatePairs, p->vUnatePairsW, p->pDivA, p->pDivB ); + if ( iResLit >= 0 ) // and(pair,pair) + { + int iNode = nVars + Vec_IntSize(p->vGates)/2; + + int fComp = Abc_LitIsCompl(iResLit); + int iDiv0 = Abc_Lit2Var(iResLit) & 0x7FFF; // pair + int iDiv1 = Abc_Lit2Var(iResLit) >> 15; // pair + + int Div0 = Vec_IntEntry( p->vUnatePairs[!fComp], Abc_Lit2Var(iDiv0) ); + int fComp0 = Abc_LitIsCompl(Div0) ^ Abc_LitIsCompl(iDiv0); + int iDiv00 = Abc_Lit2Var(Div0) & 0x7FFF; + int iDiv01 = Abc_Lit2Var(Div0) >> 15; + + int Div1 = Vec_IntEntry( p->vUnatePairs[!fComp], Abc_Lit2Var(iDiv1) ); + int fComp1 = Abc_LitIsCompl(Div1) ^ Abc_LitIsCompl(iDiv1); + int iDiv10 = Abc_Lit2Var(Div1) & 0x7FFF; + int iDiv11 = Abc_Lit2Var(Div1) >> 15; + + Vec_IntPushTwo( p->vGates, iDiv00, iDiv01 ); + Vec_IntPushTwo( p->vGates, iDiv10, iDiv11 ); + Vec_IntPushTwo( p->vGates, Abc_Var2Lit(iNode, fComp0), Abc_Var2Lit(iNode+1, fComp1) ); + return Abc_Var2Lit( iNode+2, fComp ); + } + if ( nLimit == 3 ) + return -1; + if ( Vec_IntSize(p->vUnateLits[0]) + Vec_IntSize(p->vUnateLits[1]) + Vec_IntSize(p->vUnatePairs[0]) + Vec_IntSize(p->vUnatePairs[1]) == 0 ) + return -1; + + TopOneW[0] = Vec_IntSize(p->vUnateLitsW[0]) ? Vec_IntEntry(p->vUnateLitsW[0], 0) : 0; + TopOneW[1] = Vec_IntSize(p->vUnateLitsW[1]) ? Vec_IntEntry(p->vUnateLitsW[1], 0) : 0; + + TopTwoW[0] = Vec_IntSize(p->vUnatePairsW[0]) ? Vec_IntEntry(p->vUnatePairsW[0], 0) : 0; + TopTwoW[1] = Vec_IntSize(p->vUnatePairsW[1]) ? Vec_IntEntry(p->vUnatePairsW[1], 0) : 0; + + Max1 = Abc_MaxInt(TopOneW[0], TopOneW[1]); + Max2 = Abc_MaxInt(TopTwoW[0], TopTwoW[1]); + if ( Abc_MaxInt(Max1, Max2) == 0 ) + return -1; + if ( Max1 > Max2/2 ) + { + if ( Max1 == TopOneW[0] || Max1 == TopOneW[1] ) + { + int fUseOr = Max1 == TopOneW[0]; + int iDiv = Vec_IntEntry( p->vUnateLits[!fUseOr], 0 ); + int fComp = Abc_LitIsCompl(iDiv); + word * pDiv = (word *)Vec_PtrEntry( p->vDivs, Abc_Lit2Var(iDiv) ); + Abc_TtAndSharp( p->pSets[fUseOr], p->pSets[fUseOr], pDiv, p->nWords, !fComp ); + if ( p->fVerbose ) + printf( "\n" ); + iResLit = Gia_ManResubPerform_rec( p, nLimit-1 ); + if ( iResLit >= 0 ) + { + int iNode = nVars + Vec_IntSize(p->vGates)/2; + Vec_IntPushTwo( p->vGates, Abc_LitNot(iDiv), Abc_LitNotCond(iResLit, fUseOr) ); + return Abc_Var2Lit( iNode, fUseOr ); + } + } + if ( Max2 == 0 ) + return -1; +/* + if ( Max2 == TopTwoW[0] || Max2 == TopTwoW[1] ) + { + int fUseOr = Max2 == TopTwoW[0]; + int iDiv = Vec_IntEntry( p->vUnatePairs[!fUseOr], 0 ); + int fComp = Abc_LitIsCompl(iDiv); + Gia_ManDeriveDivPair( iDiv, p->vDivs, p->nWords, p->pDivA ); + Abc_TtAndSharp( p->pSets[fUseOr], p->pSets[fUseOr], p->pDivA, p->nWords, !fComp ); + if ( p->fVerbose ) + printf( "\n " ); + iResLit = Gia_ManResubPerform_rec( p, nLimit-2 ); + if ( iResLit >= 0 ) + { + int iNode = nVars + Vec_IntSize(p->vGates)/2; + int iDiv0 = Abc_Lit2Var(iDiv) & 0x7FFF; + int iDiv1 = Abc_Lit2Var(iDiv) >> 15; + Vec_IntPushTwo( p->vGates, iDiv0, iDiv1 ); + Vec_IntPushTwo( p->vGates, Abc_LitNotCond(iResLit, fUseOr), Abc_Var2Lit(iNode, !fComp) ); + return Abc_Var2Lit( iNode+1, fUseOr ); + } + } +*/ + } + else + { + if ( Max2 == TopTwoW[0] || Max2 == TopTwoW[1] ) + { + int fUseOr = Max2 == TopTwoW[0]; + int iDiv = Vec_IntEntry( p->vUnatePairs[!fUseOr], 0 ); + int fComp = Abc_LitIsCompl(iDiv); + Gia_ManDeriveDivPair( iDiv, p->vDivs, p->nWords, p->pDivA ); + Abc_TtAndSharp( p->pSets[fUseOr], p->pSets[fUseOr], p->pDivA, p->nWords, !fComp ); + if ( p->fVerbose ) + printf( "\n" ); + iResLit = Gia_ManResubPerform_rec( p, nLimit-2 ); + if ( iResLit >= 0 ) + { + int iNode = nVars + Vec_IntSize(p->vGates)/2; + int iDiv0 = Abc_Lit2Var(iDiv) & 0x7FFF; + int iDiv1 = Abc_Lit2Var(iDiv) >> 15; + Vec_IntPushTwo( p->vGates, iDiv0, iDiv1 ); + Vec_IntPushTwo( p->vGates, Abc_LitNotCond(iResLit, fUseOr), Abc_Var2Lit(iNode, !fComp) ); + return Abc_Var2Lit( iNode+1, fUseOr ); + } + } + if ( Max1 == 0 ) + return -1; +/* + if ( Max1 == TopOneW[0] || Max1 == TopOneW[1] ) + { + int fUseOr = Max1 == TopOneW[0]; + int iDiv = Vec_IntEntry( p->vUnateLits[!fUseOr], 0 ); + int fComp = Abc_LitIsCompl(iDiv); + word * pDiv = (word *)Vec_PtrEntry( p->vDivs, Abc_Lit2Var(iDiv) ); + Abc_TtAndSharp( p->pSets[fUseOr], p->pSets[fUseOr], pDiv, p->nWords, !fComp ); + if ( p->fVerbose ) + printf( "\n " ); + iResLit = Gia_ManResubPerform_rec( p, nLimit-1 ); + if ( iResLit >= 0 ) + { + int iNode = nVars + Vec_IntSize(p->vGates)/2; + Vec_IntPushTwo( p->vGates, Abc_LitNot(iDiv), Abc_LitNotCond(iResLit, fUseOr) ); + return Abc_Var2Lit( iNode, fUseOr ); + } + } +*/ + } + return -1; +} +inline void Gia_ManResubPerform( Gia_ResbMan_t * p, Vec_Ptr_t * vDivs, int nWords, int nLimit, int nDivsMax, int iChoice, int fUseXor, int fDebug, int fVerbose ) +{ + int Res; + Gia_ResbInit( p, vDivs, nWords, nLimit, nDivsMax, iChoice, fUseXor, fDebug, fVerbose, fVerbose ); + Res = Gia_ManResubPerform_rec( p, nLimit ); + if ( Res >= 0 ) Vec_IntPush( p->vGates, Res ); + if ( fVerbose ) + printf( "\n" ); +} +inline Vec_Int_t * Gia_ManResubOne( Vec_Ptr_t * vDivs, int nWords, int nLimit, int nDivsMax, int iChoice, int fUseXor, int fDebug, int fVerbose, word * pFunc ) +{ + Vec_Int_t * vRes; + Gia_ResbMan_t * p = Gia_ResbAlloc( nWords ); + Gia_ManResubPerform( p, vDivs, nWords, nLimit, nDivsMax, iChoice, fUseXor, fDebug, fVerbose ); + if ( fVerbose ) + Gia_ManResubPrint( p->vGates, Vec_PtrSize(vDivs) ); + if ( fVerbose ) + printf( "\n" ); + if ( !Gia_ManResubVerify(p, pFunc) ) + { + Gia_ManResubPrint( p->vGates, Vec_PtrSize(vDivs) ); + printf( "Verification FAILED.\n" ); + } + else if ( fDebug && fVerbose ) + printf( "Verification succeeded." ); + if ( fVerbose ) + printf( "\n" ); + vRes = Vec_IntDup( p->vGates ); + Gia_ResbFree( p ); + return vRes; +} + +/**Function************************************************************* + + Synopsis [Top level.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static Gia_ResbMan_t * s_pResbMan = NULL; + +inline void Abc_ResubPrepareManager( int nWords ) +{ + if ( s_pResbMan != NULL ) + Gia_ResbFree( s_pResbMan ); + s_pResbMan = NULL; + if ( nWords > 0 ) + s_pResbMan = Gia_ResbAlloc( nWords ); +} + +inline int Abc_ResubComputeFunction( void ** ppDivs, int nDivs, int nWords, int nLimit, int nDivsMax, int iChoice, int fUseXor, int fDebug, int fVerbose, int ** ppArray ) +{ + Vec_Ptr_t Divs = { nDivs, nDivs, ppDivs }; + assert( s_pResbMan != NULL ); // first call Abc_ResubPrepareManager() + Gia_ManResubPerform( s_pResbMan, &Divs, nWords, nLimit, nDivsMax, iChoice, fUseXor, fDebug, fVerbose==2 ); + if ( fVerbose ) + { + int nGates = Vec_IntSize(s_pResbMan->vGates)/2; + if ( nGates ) + { + printf( " Gain = %2d Gates = %2d __________ F = ", nLimit+1-nGates, nGates ); + Gia_ManResubPrint( s_pResbMan->vGates, nDivs ); + printf( "\n" ); + } + } + if ( fDebug ) + { + if ( !Gia_ManResubVerify(s_pResbMan, NULL) ) + { + Gia_ManResubPrint( s_pResbMan->vGates, nDivs ); + printf( "Verification FAILED.\n" ); + } + //else + // printf( "Verification succeeded.\n" ); + } + *ppArray = Vec_IntArray(s_pResbMan->vGates); + assert( Vec_IntSize(s_pResbMan->vGates)/2 <= nLimit ); + return Vec_IntSize(s_pResbMan->vGates); +} + +inline void Gia_ManSimPatWriteOne( FILE * pFile, word * pSim, int nWords ) +{ + int k, Digit, nDigits = nWords*16; + for ( k = 0; k < nDigits; k++ ) + { + Digit = (int)((pSim[k/16] >> ((k%16) * 4)) & 15); + if ( Digit < 10 ) + fprintf( pFile, "%d", Digit ); + else + fprintf( pFile, "%c", 'A' + Digit-10 ); + } + fprintf( pFile, "\n" ); +} +inline void Gia_ManSimPatWrite( const char * pFileName, Vec_Wrd_t * vSimsIn, int nWords ) +{ + int i, nNodes = Vec_WrdSize(vSimsIn) / nWords; + FILE * pFile = fopen( pFileName, "wb" ); + if ( pFile == NULL ) + { + printf( "Cannot open file \"%s\" for writing.\n", pFileName ); + return; + } + assert( Vec_WrdSize(vSimsIn) % nWords == 0 ); + for ( i = 0; i < nNodes; i++ ) + Gia_ManSimPatWriteOne( pFile, Vec_WrdEntryP(vSimsIn, i*nWords), nWords ); + fclose( pFile ); + printf( "Written %d words of simulation data for %d objects into file \"%s\".\n", nWords, Vec_WrdSize(vSimsIn)/nWords, pFileName ); +} + +inline void Abc_ResubDumpProblem( const char * pFileName, void ** ppDivs, int nDivs, int nWords ) +{ + Vec_Wrd_t * vSims = Vec_WrdAlloc( nDivs * nWords ); + word ** pDivs = (word **)ppDivs; + int d, w; + for ( d = 0; d < nDivs; d++ ) + for ( w = 0; w < nWords; w++ ) + Vec_WrdPush( vSims, pDivs[d][w] ); + Gia_ManSimPatWrite( pFileName, vSims, nWords ); + Vec_WrdFree( vSims ); +} + +/**Function************************************************************* + + Synopsis [Top level.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ + +#if 0 +extern void Extra_PrintHex( FILE * pFile, unsigned * pTruth, int nVars ); +extern void Dau_DsdPrintFromTruth2( word * pTruth, int nVarsInit ); + +void Gia_ManResubTest3() +{ + int nVars = 3; + int fVerbose = 1; + word Divs[6] = { 0, 0, + ABC_CONST(0xAAAAAAAAAAAAAAAA), + ABC_CONST(0xCCCCCCCCCCCCCCCC), + ABC_CONST(0xF0F0F0F0F0F0F0F0), + ABC_CONST(0xFF00FF00FF00FF00) + }; + Vec_Ptr_t * vDivs = Vec_PtrAlloc( 6 ); + Vec_Int_t * vRes = Vec_IntAlloc( 100 ); + int i, k, ArraySize, * pArray; + for ( i = 0; i < 6; i++ ) + Vec_PtrPush( vDivs, Divs+i ); + Abc_ResubPrepareManager( 1 ); + for ( i = 0; i < (1<<(1<= (1<<14) ) + { + printf( "Reducing all divs from %d to %d.\n", Vec_PtrSize(vDivs), (1<<14)-1 ); + Vec_PtrShrink( vDivs, (1<<14)-1 ); + } + assert( Vec_PtrSize(vDivs) < (1<<14) ); + Gia_ManResubPerform( p, vDivs, nWords, 100, 50, iChoice, fUseXor, 1, 1 ); + if ( Vec_IntSize(p->vGates) ) + { + Vec_Wec_t * vGates = Vec_WecStart(1); + Vec_IntAppend( Vec_WecEntry(vGates, 0), p->vGates ); + pMan = Gia_ManConstructFromGates( vGates, Vec_PtrSize(vDivs) ); + Vec_WecFree( vGates ); + } + else + printf( "Decomposition did not succeed.\n" ); + Gia_ResbFree( p ); + Vec_PtrFree( vDivs ); + Vec_WrdFree( vSims ); + return pMan; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_ManUnivTfo_rec( Gia_Man_t * p, int iObj, Vec_Int_t * vNodes, Vec_Int_t * vPos ) +{ + int i, iFan, Count = 1; + if ( Gia_ObjIsTravIdCurrentId(p, iObj) ) + return 0; + Gia_ObjSetTravIdCurrentId(p, iObj); + if ( vNodes && Gia_ObjIsCo(Gia_ManObj(p, iObj)) ) + Vec_IntPush( vNodes, iObj ); + if ( vPos && Gia_ObjIsCo(Gia_ManObj(p, iObj)) ) + Vec_IntPush( vPos, iObj ); + Gia_ObjForEachFanoutStaticId( p, iObj, iFan, i ) + Count += Gia_ManUnivTfo_rec( p, iFan, vNodes, vPos ); + return Count; +} +int Gia_ManUnivTfo( Gia_Man_t * p, int * pObjs, int nObjs, Vec_Int_t ** pvNodes, Vec_Int_t ** pvPos ) +{ + int i, Count = 0; + if ( pvNodes ) + { + if ( *pvNodes ) + Vec_IntClear( *pvNodes ); + else + *pvNodes = Vec_IntAlloc( 100 ); + } + if ( pvPos ) + { + if ( *pvPos ) + Vec_IntClear( *pvPos ); + else + *pvPos = Vec_IntAlloc( 100 ); + } + Gia_ManIncrementTravId( p ); + for ( i = 0; i < nObjs; i++ ) + Count += Gia_ManUnivTfo_rec( p, pObjs[i], pvNodes ? *pvNodes : NULL, pvPos ? *pvPos : NULL ); + if ( pvNodes ) + Vec_IntSort( *pvNodes, 0 ); + if ( pvPos ) + Vec_IntSort( *pvPos, 0 ); + return Count; +} + +/**Function************************************************************* + + Synopsis [Tuning resub.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManTryResub( Gia_Man_t * p ) +{ + int nLimit = 20; + int nDivsMax = 200; + int iChoice = 0; + int fUseXor = 1; + int fDebug = 1; + int fVerbose = 0; + abctime clk, clkResub = 0, clkStart = Abc_Clock(); + Vec_Ptr_t * vvSims = Vec_PtrAlloc( 100 ); + Vec_Wrd_t * vSims; + word * pSets[2], * pFunc; + Gia_Obj_t * pObj, * pObj2; + int i, i2, nWords, nNonDec = 0, nTotal = 0; + assert( Gia_ManCiNum(p) < 16 ); + Vec_WrdFreeP( &p->vSimsPi ); + p->vSimsPi = Vec_WrdStartTruthTables( Gia_ManCiNum(p) ); + nWords = Vec_WrdSize(p->vSimsPi) / Gia_ManCiNum(p); + //Vec_WrdPrintHex( p->vSimsPi, nWords ); + pSets[0] = ABC_CALLOC( word, nWords ); + pSets[1] = ABC_CALLOC( word, nWords ); + vSims = Gia_ManSimPatSim( p ); + Gia_ManLevelNum(p); + Gia_ManCreateRefs(p); + Abc_ResubPrepareManager( nWords ); + Gia_ManStaticFanoutStart( p ); + Gia_ManForEachAnd( p, pObj, i ) + { + Vec_Int_t vGates; + int * pArray, nArray, nTfo, iObj = Gia_ObjId(p, pObj); + int Level = Gia_ObjLevel(p, pObj); + int nMffc = Gia_NodeMffcSizeMark(p, pObj); + pFunc = Vec_WrdEntryP( vSims, nWords*iObj ); + Abc_TtCopy( pSets[0], pFunc, nWords, 1 ); + Abc_TtCopy( pSets[1], pFunc, nWords, 0 ); + Vec_PtrClear( vvSims ); + Vec_PtrPushTwo( vvSims, pSets[0], pSets[1] ); + nTfo = Gia_ManUnivTfo( p, &iObj, 1, NULL, NULL ); + Gia_ManForEachCi( p, pObj2, i2 ) + Vec_PtrPush( vvSims, Vec_WrdEntryP(vSims, nWords*Gia_ObjId(p, pObj2)) ); + Gia_ManForEachAnd( p, pObj2, i2 ) + if ( !Gia_ObjIsTravIdCurrent(p, pObj2) && !Gia_ObjIsTravIdPrevious(p, pObj2) && Gia_ObjLevel(p, pObj2) <= Level ) + Vec_PtrPush( vvSims, Vec_WrdEntryP(vSims, nWords*Gia_ObjId(p, pObj2)) ); + if ( fVerbose ) + printf( "%3d : Lev = %2d Mffc = %2d Divs = %3d Tfo = %3d\n", iObj, Level, nMffc, Vec_PtrSize(vvSims)-2, nTfo ); + clk = Abc_Clock(); + nArray = Abc_ResubComputeFunction( (void **)Vec_PtrArray(vvSims), Vec_PtrSize(vvSims), nWords, Abc_MinInt(nMffc-1, nLimit), nDivsMax, iChoice, fUseXor, fDebug, fVerbose, &pArray ); + clkResub += Abc_Clock() - clk; + vGates.nSize = vGates.nCap = nArray; + vGates.pArray = pArray; + assert( nMffc > Vec_IntSize(&vGates)/2 ); + if ( Vec_IntSize(&vGates) > 0 ) + nTotal += nMffc - Vec_IntSize(&vGates)/2; + nNonDec += Vec_IntSize(&vGates) == 0; + } + printf( "Total nodes = %5d. Non-realizable = %5d. Gain = %6d. ", Gia_ManAndNum(p), nNonDec, nTotal ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clkStart ); + Abc_PrintTime( 1, "Pure resub time", clkResub ); + Abc_ResubPrepareManager( 0 ); + Gia_ManStaticFanoutStop( p ); + Vec_PtrFree( vvSims ); + Vec_WrdFree( vSims ); + ABC_FREE( pSets[0] ); + ABC_FREE( pSets[1] ); +} +#endif + +} /* namespace abcresub */ diff --git a/lib/abcresub/abcresub/tt.hpp b/lib/abcresub/abcresub/tt.hpp new file mode 100644 index 000000000..482a3b08b --- /dev/null +++ b/lib/abcresub/abcresub/tt.hpp @@ -0,0 +1,331 @@ +/*! + \file tt.hpp + \brief Extracted from ABC + https://github.com/berkeley-abc/abc + + \author Alan Mishchenko (UC Berkeley) +*/ + +#pragma once + +namespace abcresub +{ + +// read/write/flip i-th bit of a bit string table: +inline int Abc_TtGetBit( word * p, int i ) { return (int)(p[i>>6] >> (word)(i & 63)) & 1; } +inline void Abc_TtSetBit( word * p, int i ) { p[i>>6] |= (word)(((word)1)<<(i & 63)); } +inline void Abc_TtXorBit( word * p, int i ) { p[i>>6] ^= (word)(((word)1)<<(i & 63)); } + +// read/write k-th digit d of a quaternary number: +inline int Abc_TtGetQua( word * p, int k ) { return (int)(p[k>>5] >> (word)((k<<1) & 63)) & 3; } +inline void Abc_TtSetQua( word * p, int k, int d ) { p[k>>5] |= (word)(((word)d)<<((k<<1) & 63)); } +inline void Abc_TtXorQua( word * p, int k, int d ) { p[k>>5] ^= (word)(((word)d)<<((k<<1) & 63)); } + +// read/write k-th digit d of a hexadecimal number: +inline int Abc_TtGetHex( word * p, int k ) { return (int)(p[k>>4] >> (word)((k<<2) & 63)) & 15; } +inline void Abc_TtSetHex( word * p, int k, int d ) { p[k>>4] |= (word)(((word)d)<<((k<<2) & 63)); } +inline void Abc_TtXorHex( word * p, int k, int d ) { p[k>>4] ^= (word)(((word)d)<<((k<<2) & 63)); } + +// read/write k-th digit d of a 256-base number: +inline int Abc_TtGet256( word * p, int k ) { return (int)(p[k>>3] >> (word)((k<<3) & 63)) & 255; } +inline void Abc_TtSet256( word * p, int k, int d ) { p[k>>3] |= (word)(((word)d)<<((k<<3) & 63)); } +inline void Abc_TtXor256( word * p, int k, int d ) { p[k>>3] ^= (word)(((word)d)<<((k<<3) & 63)); } + +inline int Abc_TtCountOnes( word x ) +{ + x = x - ((x >> 1) & ABC_CONST(0x5555555555555555)); + x = (x & ABC_CONST(0x3333333333333333)) + ((x >> 2) & ABC_CONST(0x3333333333333333)); + x = (x + (x >> 4)) & ABC_CONST(0x0F0F0F0F0F0F0F0F); + x = x + (x >> 8); + x = x + (x >> 16); + x = x + (x >> 32); + return (int)(x & 0xFF); +} + +inline int Abc_TtCountOnesVec( word * x, int nWords ) +{ + int w, Count = 0; + for ( w = 0; w < nWords; w++ ) + Count += Abc_TtCountOnes( x[w] ); + return Count; +} + +inline int Abc_TtCountOnesVecMask( word * x, word * pMask, int nWords, int fCompl ) +{ + int w, Count = 0; + if ( fCompl ) + for ( w = 0; w < nWords; w++ ) + Count += Abc_TtCountOnes( pMask[w] & ~x[w] ); + else + for ( w = 0; w < nWords; w++ ) + Count += Abc_TtCountOnes( pMask[w] & x[w] ); + return Count; +} + +inline int Abc_TtCountOnesVecMask2( word * x0, word * x1, int fComp0, int fComp1, word * pMask, int nWords ) +{ + int w, Count = 0; + if ( !fComp0 && !fComp1 ) + for ( w = 0; w < nWords; w++ ) + Count += Abc_TtCountOnes( pMask[w] & x0[w] & x1[w] ); + else if ( fComp0 && !fComp1 ) + for ( w = 0; w < nWords; w++ ) + Count += Abc_TtCountOnes( pMask[w] & ~x0[w] & x1[w] ); + else if ( !fComp0 && fComp1 ) + for ( w = 0; w < nWords; w++ ) + Count += Abc_TtCountOnes( pMask[w] & x0[w] & ~x1[w] ); + else + for ( w = 0; w < nWords; w++ ) + Count += Abc_TtCountOnes( pMask[w] & ~x0[w] & ~x1[w] ); + return Count; +} + +inline int Abc_TtCountOnesVecXorMask( word * x, word * y, int fCompl, word * pMask, int nWords ) +{ + int w, Count = 0; + if ( fCompl ) + for ( w = 0; w < nWords; w++ ) + Count += Abc_TtCountOnes( pMask[w] & (x[w] ^ ~y[w]) ); + else + for ( w = 0; w < nWords; w++ ) + Count += Abc_TtCountOnes( pMask[w] & (x[w] ^ y[w]) ); + return Count; +} + +inline void Abc_TtCopy( word * pOut, word * pIn, int nWords, int fCompl ) +{ + int w; + if ( fCompl ) + for ( w = 0; w < nWords; w++ ) + pOut[w] = ~pIn[w]; + else + for ( w = 0; w < nWords; w++ ) + pOut[w] = pIn[w]; +} + +inline int Abc_TtIsConst0( word * pIn1, int nWords ) +{ + int w; + for ( w = 0; w < nWords; w++ ) + if ( pIn1[w] ) + return 0; + return 1; +} + +inline void Abc_TtClear( word * pOut, int nWords ) +{ + int w; + for ( w = 0; w < nWords; w++ ) + pOut[w] = 0; +} + +inline void Abc_TtFill( word * pOut, int nWords ) +{ + int w; + for ( w = 0; w < nWords; w++ ) + pOut[w] = ~(word)0; +} + +inline void Abc_TtAndCompl( word * pOut, word * pIn1, int fCompl1, word * pIn2, int fCompl2, int nWords ) +{ + int w; + if ( fCompl1 ) + { + if ( fCompl2 ) + for ( w = 0; w < nWords; w++ ) + pOut[w] = ~pIn1[w] & ~pIn2[w]; + else + for ( w = 0; w < nWords; w++ ) + pOut[w] = ~pIn1[w] & pIn2[w]; + } + else + { + if ( fCompl2 ) + for ( w = 0; w < nWords; w++ ) + pOut[w] = pIn1[w] & ~pIn2[w]; + else + for ( w = 0; w < nWords; w++ ) + pOut[w] = pIn1[w] & pIn2[w]; + } +} + +inline void Abc_TtAndSharp( word * pOut, word * pIn1, word * pIn2, int nWords, int fCompl ) +{ + int w; + if ( fCompl ) + for ( w = 0; w < nWords; w++ ) + pOut[w] = pIn1[w] & ~pIn2[w]; + else + for ( w = 0; w < nWords; w++ ) + pOut[w] = pIn1[w] & pIn2[w]; +} + +inline void Abc_TtXor( word * pOut, word * pIn1, word * pIn2, int nWords, int fCompl ) +{ + int w; + if ( fCompl ) + for ( w = 0; w < nWords; w++ ) + pOut[w] = pIn1[w] ^ ~pIn2[w]; + else + for ( w = 0; w < nWords; w++ ) + pOut[w] = pIn1[w] ^ pIn2[w]; +} + +inline int Abc_TtIntersectOne( word * pOut, int fComp, word * pIn, int fComp0, int nWords ) +{ + int w; + if ( fComp0 ) + { + if ( fComp ) + { + for ( w = 0; w < nWords; w++ ) + if ( ~pIn[w] & ~pOut[w] ) + return 1; + } + else + { + for ( w = 0; w < nWords; w++ ) + if ( ~pIn[w] & pOut[w] ) + return 1; + } + } + else + { + if ( fComp ) + { + for ( w = 0; w < nWords; w++ ) + if ( pIn[w] & ~pOut[w] ) + return 1; + } + else + { + for ( w = 0; w < nWords; w++ ) + if ( pIn[w] & pOut[w] ) + return 1; + } + } + return 0; +} + +inline int Abc_TtIntersectTwo( word * pOut, int fComp, word * pIn0, int fComp0, word * pIn1, int fComp1, int nWords ) +{ + int w; + if ( fComp0 && fComp1 ) + { + if ( fComp ) + { + for ( w = 0; w < nWords; w++ ) + if ( ~pIn0[w] & ~pIn1[w] & ~pOut[w] ) + return 1; + } + else + { + for ( w = 0; w < nWords; w++ ) + if ( ~pIn0[w] & ~pIn1[w] & pOut[w] ) + return 1; + } + } + else if ( fComp0 ) + { + if ( fComp ) + { + for ( w = 0; w < nWords; w++ ) + if ( ~pIn0[w] & pIn1[w] & ~pOut[w] ) + return 1; + } + else + { + for ( w = 0; w < nWords; w++ ) + if ( ~pIn0[w] & pIn1[w] & pOut[w] ) + return 1; + } + } + else if ( fComp1 ) + { + if ( fComp ) + { + for ( w = 0; w < nWords; w++ ) + if ( pIn0[w] & ~pIn1[w] & ~pOut[w] ) + return 1; + } + else + { + for ( w = 0; w < nWords; w++ ) + if ( pIn0[w] & ~pIn1[w] & pOut[w] ) + return 1; + } + } + else + { + if ( fComp ) + { + for ( w = 0; w < nWords; w++ ) + if ( pIn0[w] & pIn1[w] & ~pOut[w] ) + return 1; + } + else + { + for ( w = 0; w < nWords; w++ ) + if ( pIn0[w] & pIn1[w] & pOut[w] ) + return 1; + } + } + return 0; +} + +inline int Abc_TtIntersectXor( word * pOut, int fComp, word * pIn0, word * pIn1, int fComp01, int nWords ) +{ + int w; + if ( fComp01 ) + { + if ( fComp ) + { + for ( w = 0; w < nWords; w++ ) + if ( ~(pIn0[w] ^ pIn1[w]) & ~pOut[w] ) + return 1; + } + else + { + for ( w = 0; w < nWords; w++ ) + if ( ~(pIn0[w] ^ pIn1[w]) & pOut[w] ) + return 1; + } + } + else + { + if ( fComp ) + { + for ( w = 0; w < nWords; w++ ) + if ( (pIn0[w] ^ pIn1[w]) & ~pOut[w] ) + return 1; + } + else + { + for ( w = 0; w < nWords; w++ ) + if ( (pIn0[w] ^ pIn1[w]) & pOut[w] ) + return 1; + } + } + return 0; +} + +inline word Abc_Tt6Stretch( word t, int nVars ) +{ + assert( nVars >= 0 ); + if ( nVars == 0 ) + nVars++, t = (t & 0x1) | ((t & 0x1) << 1); + if ( nVars == 1 ) + nVars++, t = (t & 0x3) | ((t & 0x3) << 2); + if ( nVars == 2 ) + nVars++, t = (t & 0xF) | ((t & 0xF) << 4); + if ( nVars == 3 ) + nVars++, t = (t & 0xFF) | ((t & 0xFF) << 8); + if ( nVars == 4 ) + nVars++, t = (t & 0xFFFF) | ((t & 0xFFFF) << 16); + if ( nVars == 5 ) + nVars++, t = (t & 0xFFFFFFFF) | ((t & 0xFFFFFFFF) << 32); + assert( nVars == 6 ); + return t; +} + +} /* abcresub */ diff --git a/lib/abcresub/abcresub/vec_int.hpp b/lib/abcresub/abcresub/vec_int.hpp new file mode 100644 index 000000000..94e2cc860 --- /dev/null +++ b/lib/abcresub/abcresub/vec_int.hpp @@ -0,0 +1,157 @@ +/*! + \file vec_int.hpp + \brief Extracted from ABC + https://github.com/berkeley-abc/abc + + \author Alan Mishchenko (UC Berkeley) +*/ + +#pragma once + +namespace abcresub +{ + +typedef struct Vec_Int_t_ Vec_Int_t; + +struct Vec_Int_t_ +{ + int nCap; + int nSize; + int * pArray; +}; + +#define Vec_IntForEachEntry( vVec, Entry, i ) \ + for ( i = 0; (i < Vec_IntSize(vVec)) && (((Entry) = Vec_IntEntry(vVec, i)), 1); i++ ) +#define Vec_IntForEachEntryStop( vVec, Entry, i, Stop ) \ + for ( i = 0; (i < Stop) && (((Entry) = Vec_IntEntry(vVec, i)), 1); i++ ) +#define Vec_IntForEachEntryDouble( vVec, Entry1, Entry2, i ) \ + for ( i = 0; (i+1 < Vec_IntSize(vVec)) && (((Entry1) = Vec_IntEntry(vVec, i)), 1) && (((Entry2) = Vec_IntEntry(vVec, i+1)), 1); i += 2 ) +#define Vec_IntForEachEntryTwo( vVec1, vVec2, Entry1, Entry2, i ) \ + for ( i = 0; (i < Vec_IntSize(vVec1)) && (((Entry1) = Vec_IntEntry(vVec1, i)), 1) && (((Entry2) = Vec_IntEntry(vVec2, i)), 1); i++ ) +#define Vec_IntForEachEntryTwoStart( vVec1, vVec2, Entry1, Entry2, i, Start ) \ + for ( i = Start; (i < Vec_IntSize(vVec1)) && (((Entry1) = Vec_IntEntry(vVec1, i)), 1) && (((Entry2) = Vec_IntEntry(vVec2, i)), 1); i++ ) + +inline Vec_Int_t * Vec_IntAlloc( int nCap ) +{ + Vec_Int_t * p; + p = ABC_ALLOC( Vec_Int_t, 1 ); + if ( nCap > 0 && nCap < 16 ) + nCap = 16; + p->nSize = 0; + p->nCap = nCap; + p->pArray = p->nCap? ABC_ALLOC( int, p->nCap ) : NULL; + return p; +} + +inline Vec_Int_t * Vec_IntStartFull( int nSize ) +{ + Vec_Int_t * p; + p = Vec_IntAlloc( nSize ); + p->nSize = nSize; + if ( p->pArray ) memset( p->pArray, 0xff, sizeof(int) * (size_t)nSize ); + return p; +} + +inline void Vec_IntWriteEntry( Vec_Int_t * p, int i, int Entry ) +{ + assert( i >= 0 && i < p->nSize ); + p->pArray[i] = Entry; +} + +inline void Vec_IntClear( Vec_Int_t * p ) +{ + p->nSize = 0; +} + +inline void Vec_IntFree( Vec_Int_t * p ) +{ + ABC_FREE( p->pArray ); + ABC_FREE( p ); +} + +inline int * Vec_IntArray( Vec_Int_t * p ) +{ + return p->pArray; +} + +inline int Vec_IntSize( Vec_Int_t * p ) +{ + return p->nSize; +} + +inline int Vec_IntEntry( Vec_Int_t * p, int i ) +{ + assert( i >= 0 && i < p->nSize ); + return p->pArray[i]; +} + +inline int Vec_IntEntryLast( Vec_Int_t * p ) +{ + assert( p->nSize > 0 ); + return p->pArray[p->nSize-1]; +} + +inline void Vec_IntGrow( Vec_Int_t * p, int nCapMin ) +{ + if ( p->nCap >= nCapMin ) + return; + p->pArray = ABC_REALLOC( int, p->pArray, nCapMin ); + assert( p->pArray ); + p->nCap = nCapMin; +} + +inline void Vec_IntShrink( Vec_Int_t * p, int nSizeNew ) +{ + assert( p->nSize >= nSizeNew ); + p->nSize = nSizeNew; +} + +inline void Vec_IntPush( Vec_Int_t * p, int Entry ) +{ + if ( p->nSize == p->nCap ) + { + if ( p->nCap < 16 ) + Vec_IntGrow( p, 16 ); + else + Vec_IntGrow( p, 2 * p->nCap ); + } + p->pArray[p->nSize++] = Entry; +} + +inline void Vec_IntPushTwo( Vec_Int_t * p, int Entry1, int Entry2 ) +{ + Vec_IntPush( p, Entry1 ); + Vec_IntPush( p, Entry2 ); +} + +inline int Vec_IntTwoFindCommon( Vec_Int_t * vArr1, Vec_Int_t * vArr2, Vec_Int_t * vArr ) +{ + int * pBeg1 = vArr1->pArray; + int * pBeg2 = vArr2->pArray; + int * pEnd1 = vArr1->pArray + vArr1->nSize; + int * pEnd2 = vArr2->pArray + vArr2->nSize; + Vec_IntClear( vArr ); + while ( pBeg1 < pEnd1 && pBeg2 < pEnd2 ) + { + if ( *pBeg1 == *pBeg2 ) + Vec_IntPush( vArr, *pBeg1 ), pBeg1++, pBeg2++; + else if ( *pBeg1 < *pBeg2 ) + pBeg1++; + else + pBeg2++; + } + return Vec_IntSize(vArr); +} + +inline Vec_Int_t * Vec_IntDup( Vec_Int_t * pVec ) +{ + Vec_Int_t * p; + p = ABC_ALLOC( Vec_Int_t, 1 ); + p->nSize = pVec->nSize; + p->nCap = pVec->nSize; + p->pArray = p->nCap? ABC_ALLOC( int, p->nCap ) : NULL; + memcpy( p->pArray, pVec->pArray, sizeof(int) * (size_t)pVec->nSize ); + return p; +} + +} /* namespace abcresub */ diff --git a/lib/abcresub/abcresub/vec_ptr.hpp b/lib/abcresub/abcresub/vec_ptr.hpp new file mode 100644 index 000000000..f65cfde52 --- /dev/null +++ b/lib/abcresub/abcresub/vec_ptr.hpp @@ -0,0 +1,94 @@ +/*! + \file vec_ptr.hpp + \brief Extracted from ABC + https://github.com/berkeley-abc/abc + + \author Alan Mishchenko (UC Berkeley) +*/ + +#pragma once + +namespace abcresub +{ + +typedef struct Vec_Ptr_t_ Vec_Ptr_t; + +struct Vec_Ptr_t_ +{ + int nCap; + int nSize; + void ** pArray; +}; + +#define Vec_PtrForEachEntry( Type, vVec, pEntry, i ) \ + for ( i = 0; (i < Vec_PtrSize(vVec)) && (((pEntry) = (Type)Vec_PtrEntry(vVec, i)), 1); i++ ) +#define Vec_PtrForEachEntryStart( Type, vVec, pEntry, i, Start ) \ + for ( i = Start; (i < Vec_PtrSize(vVec)) && (((pEntry) = (Type)Vec_PtrEntry(vVec, i)), 1); i++ ) + +inline Vec_Ptr_t * Vec_PtrAlloc( int nCap ) +{ + Vec_Ptr_t * p; + p = ABC_ALLOC( Vec_Ptr_t, 1 ); + if ( nCap > 0 && nCap < 8 ) + nCap = 8; + p->nSize = 0; + p->nCap = nCap; + p->pArray = p->nCap? ABC_ALLOC( void *, p->nCap ) : NULL; + return p; +} + +inline void * Vec_PtrEntry( Vec_Ptr_t * p, int i ) +{ + assert( i >= 0 && i < p->nSize ); + return p->pArray[i]; +} + +inline void Vec_PtrGrow( Vec_Ptr_t * p, int nCapMin ) +{ + if ( p->nCap >= nCapMin ) + return; + p->pArray = ABC_REALLOC( void *, p->pArray, nCapMin ); + p->nCap = nCapMin; +} + +inline void Vec_PtrClear( Vec_Ptr_t * p ) +{ + p->nSize = 0; +} + +inline void Vec_PtrFree( Vec_Ptr_t * p ) +{ + ABC_FREE( p->pArray ); + ABC_FREE( p ); +} + +inline void ** Vec_PtrArray( Vec_Ptr_t * p ) +{ + return p->pArray; +} + +inline int Vec_PtrSize( Vec_Ptr_t * p ) +{ + return p->nSize; +} + +inline void Vec_PtrPush( Vec_Ptr_t * p, void * Entry ) +{ + if ( p->nSize == p->nCap ) + { + if ( p->nCap < 16 ) + Vec_PtrGrow( p, 16 ); + else + Vec_PtrGrow( p, 2 * p->nCap ); + } + p->pArray[p->nSize++] = Entry; +} + +inline void Vec_PtrAppend( Vec_Ptr_t * vVec1, Vec_Ptr_t * vVec2 ) +{ + void * Entry; int i; + Vec_PtrForEachEntry( void *, vVec2, Entry, i ) + Vec_PtrPush( vVec1, Entry ); +} + +} /* abcresub */ diff --git a/lib/abcresub/abcresub/vec_wec.hpp b/lib/abcresub/abcresub/vec_wec.hpp new file mode 100644 index 000000000..d4145daaf --- /dev/null +++ b/lib/abcresub/abcresub/vec_wec.hpp @@ -0,0 +1,100 @@ +/*! + \file vec_wec.hpp + \brief Extracted from ABC + https://github.com/berkeley-abc/abc + + \author Alan Mishchenko (UC Berkeley) +*/ + +#pragma once + +namespace abcresub +{ + +typedef struct Vec_Wec_t_ Vec_Wec_t; +struct Vec_Wec_t_ +{ + int nCap; + int nSize; + Vec_Int_t * pArray; +}; + +#define Vec_WecForEachLevel( vGlob, vVec, i ) \ + for ( i = 0; (i < Vec_WecSize(vGlob)) && (((vVec) = Vec_WecEntry(vGlob, i)), 1); i++ ) +#define Vec_WecForEachLevelReverse( vGlob, vVec, i ) \ + for ( i = Vec_WecSize(vGlob)-1; (i >= 0) && (((vVec) = Vec_WecEntry(vGlob, i)), 1); i-- ) + +inline Vec_Wec_t * Vec_WecAlloc( int nCap ) +{ + Vec_Wec_t * p; + p = ABC_ALLOC( Vec_Wec_t, 1 ); + if ( nCap > 0 && nCap < 8 ) + nCap = 8; + p->nSize = 0; + p->nCap = nCap; + p->pArray = p->nCap? ABC_CALLOC( Vec_Int_t, p->nCap ) : NULL; + return p; +} + +inline void Vec_WecErase( Vec_Wec_t * p ) +{ + int i; + for ( i = 0; i < p->nCap; i++ ) + ABC_FREE( p->pArray[i].pArray ); + ABC_FREE( p->pArray ); + p->nSize = 0; + p->nCap = 0; +} + +inline void Vec_WecFree( Vec_Wec_t * p ) +{ + Vec_WecErase( p ); + ABC_FREE( p ); +} + +inline int Vec_WecSize( Vec_Wec_t * p ) +{ + return p->nSize; +} + +inline void Vec_WecGrow( Vec_Wec_t * p, int nCapMin ) +{ + if ( p->nCap >= nCapMin ) + return; + p->pArray = ABC_REALLOC( Vec_Int_t, p->pArray, nCapMin ); + memset( p->pArray + p->nCap, 0, sizeof(Vec_Int_t) * (size_t)(nCapMin - p->nCap) ); + p->nCap = nCapMin; +} + +inline void Vec_WecInit( Vec_Wec_t * p, int nSize ) +{ + Vec_WecGrow( p, nSize ); + p->nSize = nSize; +} + +inline Vec_Int_t * Vec_WecEntry( Vec_Wec_t * p, int i ) +{ + assert( i >= 0 && i < p->nSize ); + return p->pArray + i; +} + +inline void Vec_WecClear( Vec_Wec_t * p ) +{ + Vec_Int_t * vVec; + int i; + Vec_WecForEachLevel( p, vVec, i ) + Vec_IntClear( vVec ); + p->nSize = 0; +} + +inline void Vec_WecPush( Vec_Wec_t * p, int Level, int Entry ) +{ + if ( p->nSize < Level + 1 ) + { + Vec_WecGrow( p, Abc_MaxInt(2*p->nSize, Level + 1) ); + p->nSize = Level + 1; + } + Vec_IntPush( Vec_WecEntry(p, Level), Entry ); +} + +} /* namespace abcresub */ diff --git a/lib/abcresub/abcresub/vec_wrd.hpp b/lib/abcresub/abcresub/vec_wrd.hpp new file mode 100644 index 000000000..265339cbb --- /dev/null +++ b/lib/abcresub/abcresub/vec_wrd.hpp @@ -0,0 +1,82 @@ +/*! + \file vec_wrd.hpp + \brief Extracted from ABC + https://github.com/berkeley-abc/abc + + \author Alan Mishchenko (UC Berkeley) +*/ + +#pragma once + +namespace abcresub +{ + +typedef struct Vec_Wrd_t_ Vec_Wrd_t; + +struct Vec_Wrd_t_ +{ + int nCap; + int nSize; + word * pArray; +}; + +inline Vec_Wrd_t * Vec_WrdAlloc( int nCap ) +{ + Vec_Wrd_t * p; + p = ABC_ALLOC( Vec_Wrd_t, 1 ); + if ( nCap > 0 && nCap < 16 ) + nCap = 16; + p->nSize = 0; + p->nCap = nCap; + p->pArray = p->nCap? ABC_ALLOC( word, p->nCap ) : NULL; + return p; +} + +inline void Vec_WrdFree( Vec_Wrd_t * p ) +{ + ABC_FREE( p->pArray ); + ABC_FREE( p ); +} + +inline word * Vec_WrdEntryP( Vec_Wrd_t * p, int i ) +{ + assert( i >= 0 && i < p->nSize ); + return p->pArray + i; +} + +inline void Vec_WrdGrow( Vec_Wrd_t * p, int nCapMin ) +{ + if ( p->nCap >= nCapMin ) + return; + p->pArray = ABC_REALLOC( word, p->pArray, nCapMin ); + assert( p->pArray ); + p->nCap = nCapMin; +} + +inline void Vec_WrdFill( Vec_Wrd_t * p, int nSize, word Fill ) +{ + int i; + Vec_WrdGrow( p, nSize ); + for ( i = 0; i < nSize; i++ ) + p->pArray[i] = Fill; + p->nSize = nSize; +} + +inline void Vec_WrdPush( Vec_Wrd_t * p, word Entry ) +{ + if ( p->nSize == p->nCap ) + { + if ( p->nCap < 16 ) + Vec_WrdGrow( p, 16 ); + else + Vec_WrdGrow( p, 2 * p->nCap ); + } + p->pArray[p->nSize++] = Entry; +} + +inline int Vec_WrdSize( Vec_Wrd_t * p ) +{ + return p->nSize; +} + +} /* abcresub */ diff --git a/lib/bill/bill/sat/interface/abc_bsat2.hpp b/lib/bill/bill/sat/interface/abc_bsat2.hpp index 8f5d6f7e8..137993436 100644 --- a/lib/bill/bill/sat/interface/abc_bsat2.hpp +++ b/lib/bill/bill/sat/interface/abc_bsat2.hpp @@ -17,6 +17,7 @@ namespace bill { template<> class solver { using solver_type = pabc::sat_solver; + static constexpr uint32_t BUFFER_SIZE = 2048; public: #pragma region Constructors @@ -67,6 +68,7 @@ class solver { auto add_clause(std::vector::const_iterator it, std::vector::const_iterator ie) { + assert(ie-it <= BUFFER_SIZE && "clause size exceeds limit. Please increase BUFFER_SIZE in bill/sat/interface/abc_bsat2.hpp"); ++clause_counter.back(); auto counter = 0u; while (it != ie) { @@ -136,6 +138,7 @@ class solver { int result; if (assumptions.size() > 0u) { + assert(assumptions.size() <= BUFFER_SIZE && "assumption size exceeds limit. Please increase BUFFER_SIZE in bill/sat/interface/abc_bsat2.hpp"); /* solve with assumptions */ uint32_t counter = 0u; auto it = assumptions.begin(); @@ -207,7 +210,7 @@ class solver { result::states state_ = result::states::undefined; /*! \brief Temporary storage for one clause */ - pabc::lit literals[2048]; + pabc::lit literals[BUFFER_SIZE]; /*! \brief Whether to randomize initial variable values */ bool randomize = false; diff --git a/lib/bill/bill/sat/solver/abc.hpp b/lib/bill/bill/sat/solver/abc.hpp index b9418c150..f1e9b83ff 100644 --- a/lib/bill/bill/sat/solver/abc.hpp +++ b/lib/bill/bill/sat/solver/abc.hpp @@ -5918,3 +5918,10 @@ inline void glucose_print_stats(Gluco::SimpSolver& s, abctime clk) //////////////////////////////////////////////////////////////////////// ABC_NAMESPACE_IMPL_END + +#undef SAT_USE_ANALYZE_FINAL +#undef L_IND +#undef L_ind +#undef L_LIT +#undef L_lit +#undef USE_SIMP_SOLVER diff --git a/lib/bill/bill/sat/solver/abc/satSolver.h b/lib/bill/bill/sat/solver/abc/satSolver.h index dd8d32b85..25f75282a 100644 --- a/lib/bill/bill/sat/solver/abc/satSolver.h +++ b/lib/bill/bill/sat/solver/abc/satSolver.h @@ -310,13 +310,12 @@ static inline int sat_solver_set_random(sat_solver* s, int fNotUseRandom) static inline void sat_solver_bookmark(sat_solver* s) { - if (s->qtail != s->qhead) + if ( s->qtail != s->qhead ) { - int status = sat_solver_simplify(s); - assert(status!=0); - assert(s->qtail == s->qhead); + int status = sat_solver_simplify( s ); + assert( status != 0 ); (void)status; + assert( s->qtail == s->qhead ); } - assert( s->qhead == s->qtail ); s->iVarPivot = s->size; s->iTrailPivot = s->qhead; Sat_MemBookMark( &s->Mem ); diff --git a/lib/bill/bill/sat/solver/ghack.hpp b/lib/bill/bill/sat/solver/ghack.hpp index 41cee7f92..20568ad4b 100644 --- a/lib/bill/bill/sat/solver/ghack.hpp +++ b/lib/bill/bill/sat/solver/ghack.hpp @@ -2793,13 +2793,12 @@ inline void Solver::write_char (unsigned char ch) { b[e++] = ch; } //if (putc_unlocked ((int) #define write_char b[e++] = -#define DD fwrite(b, 1, e, certifiedOutput), e = 0; //= EOF) exit(1); } inline void Solver::write_lit (int n) { for (; n > 127; n >>= 7) write_char (128 | (n & 127)); - write_char (n); if (e > 1048576) DD } + write_char (n); if (e > 1048576) fwrite(b, 1, e, certifiedOutput), e = 0; } inline bool Solver::addClause_(vec& ps) { @@ -3933,7 +3932,7 @@ printf("c ==================================[ Search Statistics (every %6d confl if (vbyte) { write_char('a'); write_lit(0); - DD + fwrite(b, 1, e, certifiedOutput), e = 0; } else { fprintf(certifiedOutput, "0\n"); @@ -5074,7 +5073,16 @@ inline void SimpSolver::garbageCollect() } #undef write_char - -inline void function() -{ -} +#undef var_Undef +#undef DYNAMICNBLEVEL +#undef CONSTANTREMOVECLAUSE +#undef UPDATEVARACTIVITY +#undef RATIOREMOVECLAUSES +#undef LOWER_BOUND_FOR_BLOCKING_RESTART +#undef M +#undef Q +#undef P +#undef B +#undef S +#undef EE +#undef X diff --git a/lib/bill/bill/sat/solver/glucose.hpp b/lib/bill/bill/sat/solver/glucose.hpp index ac47b7306..e4b8df563 100644 --- a/lib/bill/bill/sat/solver/glucose.hpp +++ b/lib/bill/bill/sat/solver/glucose.hpp @@ -6384,3 +6384,15 @@ inline void SimpSolver::garbageCollect() to.moveTo(ca); } } // using namespace Glucose + +#undef BITS_LBD +#ifdef INCREMENTAL + #undef BITS_SIZEWITHOUTSEL + #undef INCREMENTAL +#endif +#undef BITS_REALSIZE +#undef DYNAMICNBLEVEL +#undef CONSTANTREMOVECLAUSE +#undef RATIOREMOVECLAUSES +#undef LOWER_BOUND_FOR_BLOCKING_RESTART +#undef coreStatsSize diff --git a/lib/bill/bill/sat/solver/maple.hpp b/lib/bill/bill/sat/solver/maple.hpp index f84c41440..34ea9959d 100644 --- a/lib/bill/bill/sat/solver/maple.hpp +++ b/lib/bill/bill/sat/solver/maple.hpp @@ -5832,3 +5832,11 @@ inline void SimpSolver::garbageCollect() to.moveTo(ca); } } + +#undef ANTI_EXPLORATION +#undef BIN_DRUP +#undef INT_QUEUE_AVG +#undef LOOSE_PROP_STAT +#undef LOCAL +#undef TIER2 +#undef COR \ No newline at end of file diff --git a/test/algorithms/resubstitution.cpp b/test/algorithms/resubstitution.cpp index 67f388833..18d1e324c 100644 --- a/test/algorithms/resubstitution.cpp +++ b/test/algorithms/resubstitution.cpp @@ -3,7 +3,6 @@ #include #include #include -#include #include #include #include @@ -16,7 +15,9 @@ #include #include +#include #include +#include using namespace mockturtle; @@ -172,3 +173,35 @@ TEST_CASE( "Resubstitution of XAG to minimize ANDs", "[resubstitution]" ) CHECK( xag.num_pos() == 1 ); CHECK( xag.num_gates() == 2 ); } + +TEST_CASE( "Simulation-guided resubstitution", "[resubstitution]" ) +{ + aig_network aig; + + const auto a = aig.create_pi(); + const auto b = aig.create_pi(); + + const auto f = aig.create_and( a, aig.create_and( b, a ) ); + aig.create_po( f ); + + CHECK( aig.size() == 5 ); + CHECK( aig.num_pis() == 2 ); + CHECK( aig.num_pos() == 1 ); + CHECK( aig.num_gates() == 2 ); + + const auto tt = simulate>( aig )[0]; + CHECK( tt._bits == 0x8 ); + + sim_resubstitution( aig ); + + aig = cleanup_dangling( aig ); + + /* check equivalence */ + const auto tt_opt = simulate>( aig )[0]; + CHECK( tt_opt._bits == tt._bits ); + + CHECK( aig.size() == 4 ); + CHECK( aig.num_pis() == 2 ); + CHECK( aig.num_pos() == 1 ); + CHECK( aig.num_gates() == 1 ); +}