From da2cf15dbe443734916fc00109c3b5e75e83d1ea Mon Sep 17 00:00:00 2001 From: Mathias Soeken Date: Sun, 31 Mar 2019 16:06:36 +0200 Subject: [PATCH] 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 | 49 ++++ docs/changelog.rst | 1 + docs/implementations.rst | 8 +- docs/index.rst | 1 + .../algorithms/dsd_decomposition.hpp | 219 ++++++++++++++++++ include/mockturtle/networks/aig.hpp | 10 + include/mockturtle/networks/klut.hpp | 40 ++++ include/mockturtle/networks/xag.hpp | 10 + test/algorithms/dsd_decomposition.cpp | 88 +++++++ 9 files changed, 422 insertions(+), 4 deletions(-) create mode 100644 docs/algorithms/dsd_decomposition.rst create mode 100644 include/mockturtle/algorithms/dsd_decomposition.hpp create mode 100644 test/algorithms/dsd_decomposition.cpp diff --git a/docs/algorithms/dsd_decomposition.rst b/docs/algorithms/dsd_decomposition.rst new file mode 100644 index 000000000..ff7b325d9 --- /dev/null +++ b/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 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 diff --git a/docs/changelog.rst b/docs/changelog.rst index c8876449e..e9d8e26d8 100644 --- a/docs/changelog.rst +++ b/docs/changelog.rst @@ -35,6 +35,7 @@ v0.1 (not yet released) - Direct resynthesis of functions into primitives (`direct_resynthesis`) `#90 `_ - XAG optimum multiplicative complexity resynthesis (`xag_minmc_resynthesis`) `#100 `_ - AIG/XAG resynthesis (`xag_npn_resynthesis`) `#102 `_ + - DSD decomposition (`dsd_decomposition`) `#137 `_ * Views: - Visit nodes in topological order (`topo_view`) `#3 `_ - Disable structural modifications to network (`immutable_view`) `#3 `_ diff --git a/docs/implementations.rst b/docs/implementations.rst index 44e1a380f..83b9cd4e3 100644 --- a/docs/implementations.rst +++ b/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`` | ✓ | | ✓ | ✓ | | +--------------------------------+-------------+-------------+-------------+-------------+-----------------+ diff --git a/docs/index.rst b/docs/index.rst index cebebde95..c0c40c242 100644 --- a/docs/index.rst +++ b/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 diff --git a/include/mockturtle/algorithms/dsd_decomposition.hpp b/include/mockturtle/algorithms/dsd_decomposition.hpp new file mode 100644 index 000000000..b7dc6acf1 --- /dev/null +++ b/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 +#include + +#include "../traits.hpp" + +#include +#include +#include +#include + +namespace mockturtle +{ + +namespace detail +{ + +template +class dsd_decomposition_impl +{ +public: + dsd_decomposition_impl( Ntk& ntk, kitty::dynamic_truth_table const& func, std::vector> 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 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> 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 support; + std::vector> 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 const&)`. + * + * **Required network functions:** + * - `create_not` + * - `create_and` + * - `create_or` + * - `create_lt` + * - `create_le` + * - `create_xor` + */ +template +signal dsd_decomposition( Ntk& ntk, kitty::dynamic_truth_table const& func, std::vector> const& children, Fn&& on_prime ) +{ + static_assert( is_network_type_v, "Ntk is not a network type" ); + static_assert( has_create_not_v, "Ntk does not implement the create_not method" ); + static_assert( has_create_and_v, "Ntk does not implement the create_and method" ); + static_assert( has_create_or_v, "Ntk does not implement the create_or method" ); + static_assert( has_create_lt_v, "Ntk does not implement the create_lt method" ); + static_assert( has_create_le_v, "Ntk does not implement the create_le method" ); + static_assert( has_create_xor_v, "Ntk does not implement the create_xor method" ); + + detail::dsd_decomposition_impl impl( ntk, func, children, on_prime ); + return impl.run(); +} + +} // namespace mockturtle diff --git a/include/mockturtle/networks/aig.hpp b/include/mockturtle/networks/aig.hpp index 2b9a3011a..a82e41374 100644 --- a/include/mockturtle/networks/aig.hpp +++ b/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; diff --git a/include/mockturtle/networks/klut.hpp b/include/mockturtle/networks/klut.hpp index 77293dc91..eb00018ce 100644 --- a/include/mockturtle/networks/klut.hpp +++ b/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 diff --git a/include/mockturtle/networks/xag.hpp b/include/mockturtle/networks/xag.hpp index 02f5d36fb..e3b224246 100644 --- a/include/mockturtle/networks/xag.hpp +++ b/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 */ diff --git a/test/algorithms/dsd_decomposition.cpp b/test/algorithms/dsd_decomposition.cpp new file mode 100644 index 000000000..b4f0d54a3 --- /dev/null +++ b/test/algorithms/dsd_decomposition.cpp @@ -0,0 +1,88 @@ +#include + +#include +#include +#include +#include +#include +#include +#include + +using namespace mockturtle; + +TEST_CASE( "Full DSD decomposition on some 4-input functions into AIGs", "[dsd_decomposition]" ) +{ + std::vector functions = {"b0bb", "00b0", "0804", "090f"}; + + for ( auto const& func : functions ) + { + kitty::dynamic_truth_table table( 4u ); + kitty::create_from_hex_string( table, func ); + + aig_network aig; + const auto x1 = aig.create_pi(); + const auto x2 = aig.create_pi(); + const auto x3 = aig.create_pi(); + const auto x4 = aig.create_pi(); + + auto fn = [&]( kitty::dynamic_truth_table const&, std::vector const& ) { + CHECK( false ); + return aig.get_constant( false ); + }; + aig.create_po( dsd_decomposition( aig, table, {x1, x2, x3, x4}, fn ) ); + + default_simulator sim( table.num_vars() ); + CHECK( simulate( aig, sim )[0] == table ); + } +} + +TEST_CASE( "Full DSD decomposition on some 10-input functions into XAGs", "[dsd_decomposition]" ) +{ + std::vector functions = {"0080004000080004ffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff", + "000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000003333bbbbf3f3fbfbff33ffbbfff3fffb", + "000000000000000000000000000000003333bbbbf3f3fbfbff33ffbbfff3fffb3333bbbbf3f3fbfbff33ffbbfff3fffb3333bbbbf3f3fbfbff33ffbbfff3fffb3333bbbbf3f3fbfbff33ffbbfff3fffb3333bbbbf3f3fbfbff33ffbbfff3fffb3333bbbbf3f3fbfbff33ffbbfff3fffb3333bbbbf3f3fbfbff33ffbbfff3fffb"}; + + for ( auto const& func : functions ) + { + kitty::dynamic_truth_table table( 10u ); + kitty::create_from_hex_string( table, func ); + + xag_network xag; + std::vector pis( 10u ); + std::generate( pis.begin(), pis.end(), [&]() { return xag.create_pi(); } ); + + auto fn = [&]( kitty::dynamic_truth_table const&, std::vector const& ) { + CHECK( false ); + return xag.get_constant( false ); + }; + xag.create_po( dsd_decomposition( xag, table, pis, fn ) ); + + default_simulator sim( table.num_vars() ); + CHECK( simulate( xag, sim )[0] == table ); + } +} + +TEST_CASE( "Partial DSD decomposition into k-LUT network", "[dsd_decomposition]" ) +{ + 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 const& children ) { + return ntk.create_node( children, remainder ); + }; + + ntk.create_po( dsd_decomposition( ntk, table, {x1, x2, x3, x4, x5}, fn ) ); + + CHECK( ntk.num_gates() == 3u ); + + default_simulator sim( table.num_vars() ); + CHECK( simulate( ntk, sim )[0] == table ); +} +