DSD decomposition (#137)

* Update percy.

* Update fmt library.

* More generic exact_aig_resynthesis.

* More generic exact_resynthesis.

* Implement create_lt and create_le for AIGs and XAGs.

* DSD decomposition.

* Update kitty.

* Update kitty.

* Another test case for DSD.

* Some more binary gate functions for k-LUT network.

* Docs.

* Changelog.

* Simplify code.

docs/algorithms/dsd_decomposition.rst

@@ -0,0 +1,49 @@
+DSD decomposition
+-----------------
+
+Here is an example how DSD decomposition can be used to create a *k*-LUT network
+from a truth table.
+
+.. code-block:: c++
+
+   /* input function */
+   kitty::dynamic_truth_table table( 5u );
+   kitty::create_from_expression( table, "{a<(bc)de>}" );
+
+   klut_network ntk;
+   const auto x1 = ntk.create_pi();
+   const auto x2 = ntk.create_pi();
+   const auto x3 = ntk.create_pi();
+   const auto x4 = ntk.create_pi();
+   const auto x5 = ntk.create_pi();
+
+   auto fn = [&]( kitty::dynamic_truth_table const& remainder, std::vector<klut_network::signal> const& children ) {
+     return ntk.create_node( children, remainder );
+   };
+
+   ntk.create_po( dsd_decomposition( ntk, table, {x1, x2, x3, x4, x5}, fn ) );
+
+   write_bench( ntk, std::cout );
+
+The output is::
+
+   INPUT(n2)
+   INPUT(n3)
+   INPUT(n4)
+   INPUT(n5)
+   INPUT(n6)
+   OUTPUT(po0)
+   n0 = gnd
+   n1 = vdd
+   n7 = LUT 0x8 (n3, n4)
+   n8 = LUT 0xe8 (n7, n5, n6)
+   n9 = LUT 0xe (n2, n8)
+   po0 = LUT 0x2 (n9)
+
+That is DSD decomposition extracted the OR gate on the top and the AND gate
+on the bottom. The remaining majority-function is non-decomposable and is
+constructed as a node using the callback function.
+
+**Header:** ``mockturtle/algorithms/dsd_decomposition.hpp``
+
+.. doxygenfunction:: mockturtle::dsd_decomposition

docs/changelog.rst

@@ -35,6 +35,7 @@ v0.1 (not yet released)
     - Direct resynthesis of functions into primitives (`direct_resynthesis`) `#90 <https://github.com/lsils/mockturtle/pull/90>`_
     - XAG optimum multiplicative complexity resynthesis (`xag_minmc_resynthesis`) `#100 <https://github.com/lsils/mockturtle/pull/100>`_
     - AIG/XAG resynthesis (`xag_npn_resynthesis`) `#102 <https://github.com/lsils/mockturtle/pull/102>`_
+    - DSD decomposition (`dsd_decomposition`) `#137 <https://github.com/lsils/mockturtle/pull/137>`_
 * Views:
     - Visit nodes in topological order (`topo_view`) `#3 <https://github.com/lsils/mockturtle/pull/3>`_
     - Disable structural modifications to network (`immutable_view`) `#3 <https://github.com/lsils/mockturtle/pull/3>`_

docs/implementations.rst

@@ -52,19 +52,19 @@ All network implementations are located in `mockturtle/networks/`:
 +--------------------------------+-------------+-------------+-------------+-------------+-----------------+
 | ``create_nand``                | ✓           | ✓           | ✓           | ✓           |                 |
 +--------------------------------+-------------+-------------+-------------+-------------+-----------------+
-| ``create_or``                  | ✓           | ✓           | ✓           | ✓           |                 |
+| ``create_or``                  | ✓           | ✓           | ✓           | ✓           | ✓               |
 +--------------------------------+-------------+-------------+-------------+-------------+-----------------+
 | ``create_nor``                 | ✓           | ✓           | ✓           | ✓           |                 |
 +--------------------------------+-------------+-------------+-------------+-------------+-----------------+
-| ``create_lt``                  |             |             |             |             |                 |
+| ``create_lt``                  | ✓           |             | ✓           |             | ✓               |
 +--------------------------------+-------------+-------------+-------------+-------------+-----------------+
-| ``create_le``                  |             |             |             |             |                 |
+| ``create_le``                  | ✓           |             | ✓           |             | ✓               |
 +--------------------------------+-------------+-------------+-------------+-------------+-----------------+
 | ``create_gt``                  |             |             |             |             |                 |
 +--------------------------------+-------------+-------------+-------------+-------------+-----------------+
 | ``create_ge``                  |             |             |             |             |                 |
 +--------------------------------+-------------+-------------+-------------+-------------+-----------------+
-| ``create_xor``                 | ✓           | ✓           | ✓           | ✓           |                 |
+| ``create_xor``                 | ✓           | ✓           | ✓           | ✓           | ✓               |
 +--------------------------------+-------------+-------------+-------------+-------------+-----------------+
 | ``create_xnor``                | ✓           |             | ✓           | ✓           |                 |
 +--------------------------------+-------------+-------------+-------------+-------------+-----------------+

docs/index.rst

@@ -37,6 +37,7 @@ Welcome to mockturtle's documentation!
    algorithms/akers_synthesis
    algorithms/resubstitution
    algorithms/simulation
+   algorithms/dsd_decomposition
    algorithms/cleanup
    algorithms/reconv_cut
    algorithms/dont_cares

include/mockturtle/algorithms/dsd_decomposition.hpp

@@ -0,0 +1,219 @@
+/* mockturtle: C++ logic network library
+ * Copyright (C) 2018  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 dsd_decomposition.hpp
+  \brief DSD decomposition
+
+  \author Mathias Soeken
+*/
+
+#pragma once
+
+#include <cstdint>
+#include <vector>
+
+#include "../traits.hpp"
+
+#include <kitty/constructors.hpp>
+#include <kitty/decomposition.hpp>
+#include <kitty/dynamic_truth_table.hpp>
+#include <kitty/operators.hpp>
+
+namespace mockturtle
+{
+
+namespace detail
+{
+
+template<class Ntk, class Fn>
+class dsd_decomposition_impl
+{
+public:
+  dsd_decomposition_impl( Ntk& ntk, kitty::dynamic_truth_table const& func, std::vector<signal<Ntk>> const& children, Fn&& on_prime )
+      : _ntk( ntk ),
+        remainder( func ),
+        support( children.size() ),
+        pis( children ),
+        _on_prime( on_prime )
+  {
+    std::iota( support.begin(), support.end(), 0u );
+  }
+
+  signal<Ntk> run()
+  {
+    /* terminal cases */
+    if ( support.size() == 0u )
+    {
+      if ( kitty::is_const0( remainder ) )
+      {
+        return _ntk.get_constant( false );
+      }
+      else
+      {
+        assert( kitty::is_const0( ~remainder ) );
+        return _ntk.get_constant( true );
+      }
+    }
+
+    /* projection case */
+    if ( support.size() == 1u )
+    {
+      auto var = remainder.construct();
+      kitty::create_nth_var( var, support.front() );
+      if ( remainder == var )
+      {
+        return pis[support.front()];
+      }
+      else
+      {
+        assert( remainder == ~var );
+        return _ntk.create_not( pis[support.front()] );
+      }
+    }
+
+    /* try top decomposition */
+    for ( auto var : support )
+    {
+      if ( auto res = kitty::is_top_decomposable( remainder, var, &remainder );
+           res != kitty::top_decomposition::none )
+      {
+        /* remove var from support, pis do not change */
+        support.erase( std::remove( support.begin(), support.end(), var ), support.end() );
+        const auto right = run();
+
+        switch ( res )
+        {
+        default:
+          assert( false );
+        case kitty::top_decomposition::and_:
+          return _ntk.create_and( pis[var], right );
+        case kitty::top_decomposition::or_:
+          return _ntk.create_or( pis[var], right );
+        case kitty::top_decomposition::lt_:
+          return _ntk.create_lt( pis[var], right );
+        case kitty::top_decomposition::le_:
+          return _ntk.create_le( pis[var], right );
+        case kitty::top_decomposition::xor_:
+          return _ntk.create_xor( pis[var], right );
+        }
+      }
+    }
+
+    /* try bottom decomposition */
+    for ( auto j = 1u; j < support.size(); ++j )
+    {
+      for ( auto i = 0u; i < j; ++i )
+      {
+        if ( auto res = kitty::is_bottom_decomposable( remainder, support[i], support[j], &remainder );
+             res != kitty::bottom_decomposition::none )
+        {
+          /* update pis based on decomposition type */
+          switch ( res )
+          {
+          default:
+            assert( false );
+          case kitty::bottom_decomposition::and_:
+            pis[support[i]] = _ntk.create_and( pis[support[i]], pis[support[j]] );
+            break;
+          case kitty::bottom_decomposition::or_:
+            pis[support[i]] = _ntk.create_or( pis[support[i]], pis[support[j]] );
+            break;
+          case kitty::bottom_decomposition::lt_:
+            pis[support[i]] = _ntk.create_lt( pis[support[i]], pis[support[j]] );
+            break;
+          case kitty::bottom_decomposition::le_:
+            pis[support[i]] = _ntk.create_le( pis[support[i]], pis[support[j]] );
+            break;
+          case kitty::bottom_decomposition::xor_:
+            pis[support[i]] = _ntk.create_xor( pis[support[i]], pis[support[j]] );
+            break;
+          }
+
+          /* remove var from support */
+          support.erase( support.begin() + j );
+
+          return run();
+        }
+      }
+    }
+
+    /* cannot decompose anymore */
+    std::vector<signal<Ntk>> new_pis;
+    for ( auto var : support )
+    {
+      new_pis.push_back( pis[var] );
+    }
+    auto prime_large = remainder;
+    kitty::min_base_inplace( prime_large );
+    auto prime = kitty::shrink_to( prime_large, support.size() );
+    return _on_prime( prime, new_pis );
+  }
+
+private:
+  Ntk& _ntk;
+  kitty::dynamic_truth_table remainder;
+  std::vector<uint8_t> support;
+  std::vector<signal<Ntk>> pis;
+  Fn&& _on_prime;
+};
+
+} // namespace detail
+
+/*! \brief DSD decomposition
+ *
+ * This function applies DSD decomposition on an input truth table and
+ * constructs a network based on all possible decompositions.  If the truth
+ * table is only partially decomposable, then the remaining *prime function*
+ * is returned back to the caller using the call back `on_prime` together with
+ * the computed primary inputs for that remainder.
+ *
+ * The `on_prime` function must be of type `NtkDest::signal(
+ * kitty::dynamic_truth_table const&, std::vector<NtkDest::signal> const&)`.
+ *
+ * **Required network functions:**
+ * - `create_not`
+ * - `create_and`
+ * - `create_or`
+ * - `create_lt`
+ * - `create_le`
+ * - `create_xor`
+ */
+template<class Ntk, class Fn>
+signal<Ntk> dsd_decomposition( Ntk& ntk, kitty::dynamic_truth_table const& func, std::vector<signal<Ntk>> const& children, Fn&& on_prime )
+{
+  static_assert( is_network_type_v<Ntk>, "Ntk is not a network type" );
+  static_assert( has_create_not_v<Ntk>, "Ntk does not implement the create_not method" );
+  static_assert( has_create_and_v<Ntk>, "Ntk does not implement the create_and method" );
+  static_assert( has_create_or_v<Ntk>, "Ntk does not implement the create_or method" );
+  static_assert( has_create_lt_v<Ntk>, "Ntk does not implement the create_lt method" );
+  static_assert( has_create_le_v<Ntk>, "Ntk does not implement the create_le method" );
+  static_assert( has_create_xor_v<Ntk>, "Ntk does not implement the create_xor method" );
+
+  detail::dsd_decomposition_impl<Ntk, Fn> impl( ntk, func, children, on_prime );
+  return impl.run();
+}
+
+} // namespace mockturtle

include/mockturtle/networks/aig.hpp

@@ -355,6 +355,16 @@ class aig_network
     return create_and( !a, !b );
   }
 
+  signal create_lt( signal const& a, signal const& b )
+  {
+    return create_and( !a, b );
+  }
+
+  signal create_le( signal const& a, signal const& b )
+  {
+    return !create_and( a, !b );
+  }
+
   signal create_xor( signal const& a, signal const& b )
   {
     const auto fcompl = a.complement ^ b.complement;

include/mockturtle/networks/klut.hpp

@@ -121,6 +121,26 @@ class klut_network
     kitty::create_from_words( tt_and, &_and, &_and + 1 );
     _storage->data.cache.insert( tt_and );
 
+    static uint64_t _or = 0xe;
+    kitty::dynamic_truth_table tt_or( 2 );
+    kitty::create_from_words( tt_or, &_or, &_or + 1 );
+    _storage->data.cache.insert( tt_or );
+
+    static uint64_t _lt = 0x4;
+    kitty::dynamic_truth_table tt_lt( 2 );
+    kitty::create_from_words( tt_lt, &_lt, &_lt + 1 );
+    _storage->data.cache.insert( tt_lt );
+
+    static uint64_t _le = 0xd;
+    kitty::dynamic_truth_table tt_le( 2 );
+    kitty::create_from_words( tt_le, &_le, &_le + 1 );
+    _storage->data.cache.insert( tt_le );
+
+    static uint64_t _xor = 0x6;
+    kitty::dynamic_truth_table tt_xor( 2 );
+    kitty::create_from_words( tt_xor, &_xor, &_xor + 1 );
+    _storage->data.cache.insert( tt_xor );
+
     /* truth tables for constants */
     _storage->nodes[0].data[1].h1 = 0;
     _storage->nodes[1].data[1].h1 = 1;
@@ -188,6 +208,26 @@ class klut_network
   {
     return _create_node( {a, b}, 4 );
   }
+
+  signal create_or( signal a, signal b )
+  {
+    return _create_node( {a, b}, 6 );
+  }
+
+  signal create_lt( signal a, signal b )
+  {
+    return _create_node( {a, b}, 8 );
+  }
+
+  signal create_le( signal a, signal b )
+  {
+    return _create_node( {a, b}, 11 );
+  }
+
+  signal create_xor( signal a, signal b )
+  {
+    return _create_node( {a, b}, 12 );
+  }
 #pragma endregion
 
 #pragma region Create arbitrary functions

include/mockturtle/networks/xag.hpp

@@ -355,6 +355,16 @@ class xag_network
     return create_and( !a, !b );
   }
 
+  signal create_lt( signal const& a, signal const& b )
+  {
+    return create_and( !a, b );
+  }
+
+  signal create_le( signal const& a, signal const& b )
+  {
+    return !create_and( a, !b );
+  }
+
   signal create_xor( signal a, signal b )
   {
     /* order inputs a > b it is a XOR */