Bit packing

docs/algorithms/simulation.rst

@@ -82,16 +82,34 @@ With ``partial_simulator``, adding new simulation patterns and re-simulation can
 Incremental simulation is adopted, which speeds up simulation time by only re-simulating needed nodes and only re-computing the last block of ``partial_truth_table``.
 Note that currently only AIG and XAG are supported.
 
+**Constructors**
+
 .. doxygenfunction:: mockturtle::partial_simulator::partial_simulator( unsigned, unsigned, std::default_random_engine::result_type )
 
 .. doxygenfunction:: mockturtle::partial_simulator::partial_simulator( std::vector<kitty::partial_truth_table> const& )
 
 .. doxygenfunction:: mockturtle::partial_simulator::partial_simulator( const std::string&, uint32_t )
 
+**Interfaces**
+
+.. doxygenfunction:: mockturtle::partial_simulator::add_pattern( std::vector<bool> const& )
+
 .. doxygenfunction:: mockturtle::partial_simulator::num_bits()
 
 .. doxygenfunction:: mockturtle::partial_simulator::get_patterns()
 
-.. doxygenfunction:: mockturtle::simulate_nodes( Ntk const&, unordered_node_map<kitty::partial_truth_table, Ntk>&, partial_simulator const&, bool )
+**Simulation**
+
+.. doxygenfunction:: mockturtle::simulate_nodes( Ntk const&, unordered_node_map<kitty::partial_truth_table, Ntk>&, Simulator const&, bool )
+
+.. doxygenfunction:: mockturtle::simulate_node( Ntk const&, typename Ntk::node const&, unordered_node_map<kitty::partial_truth_table, Ntk>&, Simulator const& )
+
+**Bit Packing**
+
+To reduce the size of simulation pattern set during pattern generation, ``bit_packed_simulator`` can be used instead of ``partial_simulator``, which has additional interfaces to specify care bits in patterns and to perform bit packing.
+
+.. doxygenclass:: mockturtle::bit_packed_simulator
+
+.. doxygenfunction:: mockturtle::bit_packed_simulator::add_pattern( std::vector<bool> const&, std::vector<bool> const& )
 
-.. doxygenfunction:: mockturtle::simulate_node( Ntk const&, typename Ntk::node const&, unordered_node_map<kitty::partial_truth_table, Ntk>&, partial_simulator const& )
+.. doxygenfunction:: mockturtle::bit_packed_simulator::pack_bits()

experiments/pattern_generation.cpp

@@ -54,7 +54,7 @@ int main()
     pattern_generation_stats st;
 
     uint32_t num_random_pattern = 1000;
-    partial_simulator sim( aig.num_pis(), num_random_pattern );
+    bit_packed_simulator sim( aig.num_pis(), num_random_pattern );
     pattern_generation( aig, sim, ps, &st );
 
     exp( benchmark, aig.num_pis(), size_before, sim.num_bits(), st.num_generated_patterns, st.num_constant, to_seconds( st.time_total ), to_seconds( st.time_sim ), to_seconds( st.time_sat ) );

include/mockturtle/algorithms/circuit_validator.hpp

@@ -95,7 +95,7 @@ class circuit_validator
   };
 
   explicit circuit_validator( Ntk const& ntk, validator_params const& ps = {} )
-      : ntk( ntk ), ps( ps ), literals( ntk ), cex( ntk.num_pis() )
+      : ntk( ntk ), ps( ps ), literals( ntk ), num_invoke( 0u ), cex( ntk.num_pis() )
   {
     static_assert( is_network_type_v<Ntk>, "Ntk is not a network type" );
     static_assert( has_foreach_fanin_v<Ntk>, "Ntk does not implement the foreach_fanin method" );
@@ -146,7 +146,7 @@ class circuit_validator
       construct( ntk.get_node( d ) );
     }
     auto const res = validate( ntk.get_node( f ), lit_not_cond( literals[d], ntk.is_complemented( f ) ^ ntk.is_complemented( d ) ) );
-    if ( solver.num_clauses() > ps.max_clauses )
+    if ( solver.num_clauses() > ps.max_clauses && num_invoke >= MIN_NUM_INVOKE )
     {
       restart();
     }
@@ -161,7 +161,7 @@ class circuit_validator
       construct( ntk.get_node( d ) );
     }
     auto const res = validate( root, lit_not_cond( literals[d], ntk.is_complemented( d ) ) );
-    if ( solver.num_clauses() > ps.max_clauses )
+    if ( solver.num_clauses() > ps.max_clauses && num_invoke >= MIN_NUM_INVOKE )
     {
       restart();
     }
@@ -231,7 +231,7 @@ class circuit_validator
       pop();
     }
 
-    if ( solver.num_clauses() > ps.max_clauses )
+    if ( solver.num_clauses() > ps.max_clauses && num_invoke >= MIN_NUM_INVOKE )
     {
       restart();
     }
@@ -278,7 +278,7 @@ class circuit_validator
       res = solve( {lit_not_cond( literals[root], value )} );
     }
 
-    if ( solver.num_clauses() > ps.max_clauses )
+    if ( solver.num_clauses() > ps.max_clauses && num_invoke >= MIN_NUM_INVOKE )
     {
       restart();
     }
@@ -345,7 +345,7 @@ class circuit_validator
     }
 
     pop();
-    if ( solver.num_clauses() > ps.max_clauses )
+    if ( solver.num_clauses() > ps.max_clauses && num_invoke >= MIN_NUM_INVOKE )
     {
       restart();
     }
@@ -365,6 +365,7 @@ class circuit_validator
 private:
   void restart()
   {
+    num_invoke = 0u;
     solver.restart();
     if constexpr ( randomize )
     {
@@ -516,6 +517,7 @@ class circuit_validator
 
   std::optional<bool> solve( std::vector<bill::lit_type> assumptions )
   {
+    ++num_invoke;
     auto const res = solver.solve( assumptions, ps.conflict_limit );
 
     if ( res == bill::result::states::satisfiable )
@@ -692,6 +694,9 @@ class circuit_validator
   unordered_node_map<bill::lit_type, Ntk> literals;
   bill::solver<Solver> solver;
 
+  static const uint32_t MIN_NUM_INVOKE = 20u;
+  uint32_t num_invoke;
+
   bool between_push_pop = false;
   std::vector<node> tmp;
 

include/mockturtle/algorithms/pattern_generation.hpp

@@ -111,15 +111,15 @@ struct pattern_generation_stats
 namespace detail
 {
 
-template<class Ntk, bool use_odc = false>
+template<class Ntk, class Simulator, bool use_odc = false>
 class patgen_impl
 {
 public:
   using node = typename Ntk::node;
   using signal = typename Ntk::signal;
   using TT = unordered_node_map<kitty::partial_truth_table, Ntk>;
 
-  explicit patgen_impl( Ntk& ntk, partial_simulator& sim, pattern_generation_params const& ps, validator_params& vps, pattern_generation_stats& st )
+  explicit patgen_impl( Ntk& ntk, Simulator& sim, pattern_generation_params const& ps, validator_params& vps, pattern_generation_stats& st )
       : ntk( ntk ), ps( ps ), st( st ), vps( vps ), validator( ntk, vps ),
         tts( ntk ), sim( sim )
   {
@@ -130,12 +130,20 @@ class patgen_impl
     stopwatch t( st.time_total );
 
     call_with_stopwatch( st.time_sim, [&]() {
-      simulate_nodes<Ntk>( ntk, tts, sim );
+      simulate_nodes<Ntk>( ntk, tts, sim, true );
     } );
 
     if ( ps.num_stuck_at > 0 )
     {
       stuck_at_check();
+      if constexpr( std::is_same_v<Simulator, bit_packed_simulator> )
+      {
+        sim.pack_bits();
+        call_with_stopwatch( st.time_sim, [&]() {
+          tts.reset();
+          simulate_nodes<Ntk>( ntk, tts, sim, true );
+        } );
+      }
       if ( ps.substitute_const )
       {
         for ( auto n : const_nodes )
@@ -151,6 +159,14 @@ class patgen_impl
     if constexpr ( use_odc )
     {
       observability_check();
+      if constexpr( std::is_same_v<Simulator, bit_packed_simulator> )
+      {
+        sim.pack_bits();
+        call_with_stopwatch( st.time_sim, [&]() {
+          tts.reset();
+          simulate_nodes<Ntk>( ntk, tts, sim, true );
+        } );
+      }
     }
   }
 
@@ -226,7 +242,7 @@ class patgen_impl
             }
           }
 
-          new_pattern( validator.cex );
+          new_pattern( validator.cex, n );
 
           if ( ps.num_stuck_at > 1 )
           {
@@ -236,7 +252,7 @@ class patgen_impl
             } );
             for ( auto& pattern : generated )
             {
-              new_pattern( pattern );
+              new_pattern( pattern, n );
             }
           }
 
@@ -311,7 +327,7 @@ class patgen_impl
         {
           if ( !( *res ) )
           {
-            new_pattern( validator.cex );
+            new_pattern( validator.cex, n );
             ++st.unobservable_type2;
 
             if ( ps.verbose )
@@ -348,7 +364,7 @@ class patgen_impl
         {
           if ( !( *res ) )
           {
-            new_pattern( validator.cex );
+            new_pattern( validator.cex, n );
             ++st.unobservable_type2;
 
             if ( ps.verbose )
@@ -376,9 +392,18 @@ class patgen_impl
   }
 
 private:
-  void new_pattern( std::vector<bool> const& pattern )
+  void new_pattern( std::vector<bool> const& pattern, node const& n )
   {
-    sim.add_pattern( pattern );
+    if constexpr( std::is_same_v<Simulator, bit_packed_simulator> )
+    {
+      sim.add_pattern( pattern, compute_support( n ) );
+    }
+    else
+    {
+      (void)n;
+      sim.add_pattern( pattern );
+    }
+
     ++st.num_generated_patterns;
 
     /* re-simulate */
@@ -411,11 +436,78 @@ class patgen_impl
     } );
     for ( auto& pattern : generated )
     {
-      new_pattern( pattern );
+      new_pattern( pattern, n );
     }
     zero = sim.compute_constant( false );
   }
 
+  std::vector<bool> compute_support( node const& n )
+  {
+    ntk.incr_trav_id();
+    if constexpr ( use_odc )
+    {
+      if ( ps.odc_levels != 0 )
+      {
+        std::vector<node> leaves;
+        mark_fanout_leaves_rec( n, 1, leaves );
+        ntk.foreach_po( [&]( auto const& f ) {
+          if ( ntk.visited( ntk.get_node( f ) ) == ntk.trav_id() )
+          {
+            leaves.emplace_back( ntk.get_node( f ) );
+          }
+        });
+
+        ntk.incr_trav_id();
+        for ( auto& l : leaves )
+        {
+          mark_support_rec( l );
+        }
+      }
+    }
+    mark_support_rec( n );
+
+    std::vector<bool> care( ntk.num_pis(), false );
+    ntk.foreach_pi( [&]( auto const& f, uint32_t i ) {
+      if ( ntk.visited( f ) == ntk.trav_id() )
+      {
+        care[i] = true;
+      }
+    });
+    return care;
+  }
+
+  void mark_support_rec( node const& n )
+  {
+    if ( ntk.visited( n ) == ntk.trav_id() )
+      { return; }
+    ntk.set_visited( n, ntk.trav_id() );
+
+    ntk.foreach_fanin( n, [&]( auto const& f ) {
+      if ( ntk.visited( ntk.get_node( f ) ) == ntk.trav_id() )
+        { return true; }
+      mark_support_rec( ntk.get_node( f ) );
+      return true;
+    });
+  }
+
+  void mark_fanout_leaves_rec( node const& n, int level, std::vector<node>& leaves )
+  {
+    ntk.foreach_fanout( n, [&]( auto const& fo ) {
+      if ( ntk.visited( fo ) == ntk.trav_id() )
+        { return true; }
+      ntk.set_visited( fo, ntk.trav_id() );
+
+      if ( level == ps.odc_levels )
+      {
+        leaves.emplace_back( fo );
+        return true;
+      }
+
+      mark_fanout_leaves_rec( fo, level + 1, leaves );
+      return true;
+    } );
+  }
+
 private:
   Ntk& ntk;
 
@@ -428,7 +520,7 @@ class patgen_impl
   TT tts;
   std::vector<signal> const_nodes;
 
-  partial_simulator& sim;
+  Simulator& sim;
 };
 
 } /* namespace detail */
@@ -441,22 +533,24 @@ class patgen_impl
  *
  * [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 )`)
+ * \param sim Reference of a `partial_simulator` or `bit_packed_simulator`
+ * object where the generated patterns will be stored.
+ * It can be empty (`Simulator( ntk.num_pis(), 0 )`)
  * or already containing some patterns generated from previous runs 
- * (`partial_simulator( filename )`) or randomly generated
- * (`partial_simulator( ntk.num_pis(), num_random_patterns )`). The generated
+ * (`Simulator( filename )`) or randomly generated
+ * (`Simulator( ntk.num_pis(), num_random_patterns )`). The generated
  * patterns can then be written out with `write_patterns`
  * or directly be used by passing the simulator to another algorithm.
  */
-template<class Ntk>
-void pattern_generation( Ntk& ntk, partial_simulator& sim, pattern_generation_params const& ps = {}, pattern_generation_stats* pst = nullptr )
+template<class Ntk, class Simulator>
+void pattern_generation( Ntk& ntk, Simulator& sim, pattern_generation_params const& ps = {}, pattern_generation_stats* pst = nullptr )
 {
   static_assert( is_network_type_v<Ntk>, "Ntk is not a network type" );
   static_assert( has_foreach_gate_v<Ntk>, "Ntk does not implement the foreach_gate method" );
   static_assert( has_get_node_v<Ntk>, "Ntk does not implement the get_node method" );
   static_assert( has_is_complemented_v<Ntk>, "Ntk does not implement the is_complemented method" );
   static_assert( has_make_signal_v<Ntk>, "Ntk does not implement the make_signal method" );
+  static_assert( std::is_same_v<Simulator, partial_simulator> || std::is_same_v<Simulator, bit_packed_simulator>, "Simulator should be either partial_simulator or bit_packed_simulator" );
 
   pattern_generation_stats st;
   validator_params vps;
@@ -469,7 +563,7 @@ void pattern_generation( Ntk& ntk, partial_simulator& sim, pattern_generation_pa
     using fanout_view_t = fanout_view<Ntk>;
     fanout_view_t fanout_view{ntk};
 
-    detail::patgen_impl<fanout_view_t, true> p( fanout_view, sim, ps, vps, st );
+    detail::patgen_impl<fanout_view_t, Simulator, true> p( fanout_view, sim, ps, vps, st );
     p.run();
   }
   else

include/mockturtle/algorithms/sim_resub.hpp

@@ -566,7 +566,7 @@ struct abc_resub_functor_stats
     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 ) );
+    std::cout << fmt::format( "[i]         interface:  {:>5.2f} secs\n", to_seconds( time_interface ) );
     // clang-format on
   }
 };
@@ -815,7 +815,7 @@ class simulation_based_resub_engine
 
     /* first simulation: the whole circuit; from 0 bits. */
     call_with_stopwatch( st.time_sim, [&]() {
-      simulate_nodes<Ntk>( ntk, tts, sim );
+      simulate_nodes<Ntk>( ntk, tts, sim, true );
     });
   }