From d09b1eced3a7bab36f73d6bc6c5063a7c7dffe9f Mon Sep 17 00:00:00 2001 From: Sonia Date: Wed, 25 Mar 2020 01:21:40 +0100 Subject: [PATCH 01/22] AllowModify in cnf_view Still having problem with initializing node_map; not tested yet --- include/mockturtle/views/cnf_view.hpp | 218 ++++++++++++++++++++++++-- 1 file changed, 205 insertions(+), 13 deletions(-) diff --git a/include/mockturtle/views/cnf_view.hpp b/include/mockturtle/views/cnf_view.hpp index 7937a127b..9409db76c 100644 --- a/include/mockturtle/views/cnf_view.hpp +++ b/include/mockturtle/views/cnf_view.hpp @@ -49,10 +49,12 @@ namespace mockturtle { +template /* only use to distinguish constructors */ struct cnf_view_params { /*! \brief Write DIMACS file, whenever solve is called. */ std::optional write_dimacs{}; + bool auto_update{true}; /* only used when AllowModify = true */ }; /*! \brief A view to connect logic network creation to SAT solving. @@ -71,7 +73,7 @@ struct cnf_view_params * added. Therefore, a network cannot modify or delete nodes when wrapped in a * `cnf_view`. */ -template +template class cnf_view : public Ntk { public: @@ -79,9 +81,22 @@ class cnf_view : public Ntk using node = typename Ntk::node; using signal = typename Ntk::signal; + template + struct lit_maps + { + }; + + template<> + struct lit_maps + { + node_map literals; + std::vector switches; + }; + public: // can only be constructed as empty network - explicit cnf_view( cnf_view_params const& ps = {} ) + template> + explicit cnf_view( cnf_view_params const& ps = {} ) : Ntk(), ps_( ps ) { @@ -101,11 +116,49 @@ class cnf_view : public Ntk register_events(); } + template> + cnf_view( cnf_view_params const& ps = {} ) + : Ntk(), ps_( ps ), maps_( { .literals = node_map( Ntk() ) } ) + /* TODO: should use this to initialize node_map; also, lit_type doesn't have a default constructor... */ + { + static_assert( is_network_type_v, "Ntk is not a network type" ); + static_assert( has_node_to_index_v, "Ntk does not implement the node_to_index method" ); + static_assert( has_get_node_v, "Ntk does not implement the get_node method" ); + static_assert( has_make_signal_v, "Ntk does not implement the make_signal method" ); + static_assert( has_foreach_pi_v, "Ntk does not implement the foreach_pi method" ); + static_assert( has_foreach_po_v, "Ntk does not implement the foreach_po method" ); + static_assert( has_foreach_fanin_v, "Ntk does not implement the foreach_fanin method" ); + static_assert( has_node_function_v, "Ntk does not implement the node_function method" ); + + register_events(); + + solver_.add_variables( Ntk::size() ); + + /* unit clause for constant-0 */ + solver_.add_clause( bill::lit_type( 0, bill::lit_type::polarities::positive ) ); + + Ntk::foreach_pi( [&]( auto const& n, auto i ) { + literals_[n] = bill::lit_type( i+1, bill::lit_type::polarities::positive ); + } ); + + Ntk::foreach_gate( [&]( auto const& n ) { + on_add( n, false ); + } ); + } + signal create_pi( std::string const& name = std::string() ) { const auto f = Ntk::create_pi( name ); const auto v = solver_.add_variable(); + + if constexpr ( AllowModify ) + { + literals_.resize( bill::lit_type( 0, bill::lit_type::polarities::positive ) ); + literals_[f] = bill::lit_type( v, bill::lit_type::polarities::positive ); + return f; + } + assert( v == var( Ntk::get_node( f ) ) ); (void)v; @@ -115,6 +168,8 @@ class cnf_view : public Ntk /* \brief Returns the variable associated to a node. */ inline bill::var_type var( node const& n ) const { + if constexpr ( AllowModify ) + return literals_[n].variable(); return Ntk::node_to_index( n ); } @@ -124,6 +179,14 @@ class cnf_view : public Ntk return bill::lit_type( var( Ntk::get_node( f ) ), Ntk::is_complemented( f ) ? bill::lit_type::polarities::negative : bill::lit_type::polarities::positive ); } + /*! \brief Returns the switching literal associated to a node. */ + template> + inline bill::lit_type switch_lit( node const& n ) const + { + assert( !ntk_.is_pi( n ) && !ntk_.is_constant( n ) && "PI and constant node are not switch-able" ); + return switches_[Ntk::node_to_index( n )]; + } + /*! \brief Solves the network with a set of custom assumptions. * * This function does not assert any primary output, unless specified @@ -137,6 +200,46 @@ class cnf_view : public Ntk */ inline std::optional solve( bill::result::clause_type const& assumptions, uint32_t limit = 0 ) { + if constexpr ( AllowModify ) + { + std::vector assumptions_copy = assumptions; + for ( auto i = 1u; i < switches_.size(); ++i ) + { + if ( Ntk::is_pi( Ntk::index_to_node( i ) ) ) continue; + assumptions_copy.push_back( switches_[i] ); + } + + if ( ps_.write_dimacs ) + { + for ( const auto& a : assumptions_copy ) + { + auto l = pabc::Abc_Var2Lit( a.variable(), a.is_complemented() ); + dimacs_.add_clause( &l, &l + 1 ); + } + + dimacs_.set_nr_vars( solver_.num_variables() ); + + auto fd = fopen( ps_.write_dimacs->c_str(), "w" ); + dimacs_.to_dimacs( fd ); + fclose( fd ); + } + + const auto res = solver_.solve( assumptions_copy, limit ); + + switch ( res ) + { + case bill::result::states::satisfiable: + model_ = solver_.get_model().model(); + return true; + case bill::result::states::unsatisfiable: + return false; + default: + return std::nullopt; + } + + return std::nullopt; + } + if ( ps_.write_dimacs ) { for ( const auto& a : assumptions ) @@ -206,6 +309,14 @@ class cnf_view : public Ntk return values; } + /*! \brief Whether a node is currently activated (included in CNF). */ + template> + inline bool is_activated( node const& n ) const + { + return switch_lit( n ).is_complemented(); + /* clauses are activated if switch literal is complemented */ + } + /*! \brief Blocks last model for primary input values. */ void block() { @@ -216,6 +327,22 @@ class cnf_view : public Ntk add_clause( blocking_clause ); } + /*! \brief Deactivates the clauses for a node. */ + template> + void deactivate( node const& n ) + { + if ( is_activated( n ) ) + switches_[Ntk::node_to_index( n )].complement(); + } + + /*! \brief (Re-)activates the clauses for a node. */ + template> + void activate( node const& n ) + { + if ( !is_activated( n ) ) + switches_[Ntk::node_to_index( n )].complement(); + } + /*! \brief Number of variables. */ inline uint32_t num_vars() { @@ -275,30 +402,75 @@ class cnf_view : public Ntk void register_events() { Ntk::events().on_add.push_back( [this]( auto const& n ) { on_add( n ); } ); - Ntk::events().on_modified.push_back( []( auto const& n, auto const& previous ) { - (void)n; + Ntk::events().on_modified.push_back( [this]( auto const& n, auto const& previous ) { (void)previous; + if constexpr ( AllowModify ) + { + if ( ps_.auto_update ) + on_modified( n ); + return; + } + + (void)n; assert( false && "nodes should not be modified in cnf_view" ); std::abort(); } ); - Ntk::events().on_delete.push_back( []( auto const& n ) { + Ntk::events().on_delete.push_back( [this]( auto const& n ) { + if constexpr ( AllowModify ) + { + if ( ps_.auto_update ) + on_delete( n ); + return; + } + (void)n; assert( false && "nodes should not be deleted in cnf_view" ); std::abort(); } ); } - void on_add( node const& n ) + void on_add( node const& n, bool add_var = true ) /* add_var is only used when AllowModify = true */ { - const auto v = solver_.add_variable(); - assert( v == var( n ) ); - (void)v; + bill::lit_type node_lit(0, bill::lit_type::polarities::positive); + bill::lit_type switch_lit(0, bill::lit_type::polarities::positive); + + if constexpr ( AllowModify ) + { + if ( add_var ) + { + node_lit = bill::lit_type( solver_.add_variable(), bill::lit_type::polarities::positive ); + literals_.resize( bill::lit_type(0, bill::lit_type::polarities::positive) ); + literals_[n] = node_lit; + } + else + node_lit = literals_[n]; + + switch_lit = bill::lit_type( solver_.add_variable(), bill::lit_type::polarities::positive ); + switches_.resize( Ntk::size() ); + switches_[Ntk::node_to_index( n )] = bill::lit_type( switch_lit.variable(), bill::lit_type::polarities::negative ); //lit_not( switch_lit ); + } + else + { + const auto v = solver_.add_variable(); + assert( v == var( n ) ); + (void)v; + + node_lit = lit( Ntk::make_signal( n ) ); + } const auto _add_clause = [&]( bill::result::clause_type const& clause ) { - add_clause( clause ); + if constexpr ( AllowModify ) + { + bill::result::clause_type clause_ = clause; + clause_.push_back( switch_lit ); + add_clause( clause_ ); + } + else + { + add_clause( clause ); + } }; - - const auto node_lit = lit( Ntk::make_signal( n ) ); + bill::result::clause_type child_lits; Ntk::foreach_fanin( n, [&]( auto const& f ) { child_lits.push_back( lit( f ) ); @@ -361,12 +533,32 @@ class cnf_view : public Ntk detail::on_function( node_lit, child_lits, Ntk::node_function( n ), _add_clause ); } + template> + void on_modified( node const& n ) + { + deactivate( n ); + add_clause( switch_lit( n ) ); + on_add( n, false ); + /* reuse literals_[n] (so that the fanout clauses are still valid), + but create a new switches_[n] to control a new set of gate clauses */ + } + + template> + void on_delete( node const& n ) + { + deactivate( n ); + } + private: bill::solver solver_; bill::result::model_type model_; percy::cnf_formula dimacs_; - cnf_view_params ps_; + cnf_view_params ps_; + + lit_maps maps_; + node_map& literals_ = maps_.literals; + std::vector& switches_ = maps_.switches; }; } /* namespace mockturtle */ From 2e819664f0e1cdc29d649c1f705495191a6f5f54 Mon Sep 17 00:00:00 2001 From: Sonia Date: Wed, 25 Mar 2020 15:41:47 +0100 Subject: [PATCH 02/22] default constructors in bill --- lib/bill/bill/sat/interface/types.hpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/lib/bill/bill/sat/interface/types.hpp b/lib/bill/bill/sat/interface/types.hpp index 5e5d2e003..2f1785e84 100644 --- a/lib/bill/bill/sat/interface/types.hpp +++ b/lib/bill/bill/sat/interface/types.hpp @@ -23,7 +23,7 @@ class var_type { constexpr static uint32_t max_value = (std::numeric_limits::max() >> 1); public: - constexpr var_type(uint32_t var) + constexpr var_type(uint32_t var = 0) : data_(var) { assert(var < max_value); @@ -76,7 +76,7 @@ class lit_type { negative = 1, }; - constexpr lit_type(var_type var, polarities polarity) + constexpr lit_type(var_type var = var_type(), polarities polarity = polarities::positive) : data_((var << 1) | ((polarity == polarities::positive) ? 0 : 1)) {} From fd27853ad4abe276e0415d5b94f58d7f925bea03 Mon Sep 17 00:00:00 2001 From: Sonia Date: Wed, 25 Mar 2020 15:42:23 +0100 Subject: [PATCH 03/22] restructure classes --- include/mockturtle/views/cnf_view.hpp | 236 +++++++++++++------------- 1 file changed, 120 insertions(+), 116 deletions(-) diff --git a/include/mockturtle/views/cnf_view.hpp b/include/mockturtle/views/cnf_view.hpp index 9409db76c..fe179f15d 100644 --- a/include/mockturtle/views/cnf_view.hpp +++ b/include/mockturtle/views/cnf_view.hpp @@ -49,7 +49,6 @@ namespace mockturtle { -template /* only use to distinguish constructors */ struct cnf_view_params { /*! \brief Write DIMACS file, whenever solve is called. */ @@ -57,6 +56,93 @@ struct cnf_view_params bool auto_update{true}; /* only used when AllowModify = true */ }; +/* forward declaration */ +template +class cnf_view; + +template +class cnf_view_impl : public Ntk +{ +public: + cnf_view_impl( CnfView& cnf_view ): Ntk() { (void)cnf_view; } +}; + +template +class cnf_view_impl : public Ntk +{ + friend class cnf_view; + using node = typename Ntk::node; + +public: + cnf_view_impl( CnfView& cnf_view ) + : Ntk(), cnf_view_( cnf_view ), literals_( *this ) + { } + + void init() + { + cnf_view_.solver_.add_variables( Ntk::size() ); + + /* unit clause for constant-0 */ + cnf_view_.solver_.add_clause( bill::lit_type( 0, bill::lit_type::polarities::positive ) ); + + Ntk::foreach_pi( [&]( auto const& n, auto i ) { + literals_[n] = bill::lit_type( i+1, bill::lit_type::polarities::positive ); + } ); + + Ntk::foreach_gate( [&]( auto const& n ) { + cnf_view_.on_add( n, false ); + } ); + } + + /*! \brief Returns the switching literal associated to a node. */ + inline bill::lit_type switch_lit( node const& n ) const + { + assert( !Ntk::is_pi( n ) && !Ntk::is_constant( n ) && "PI and constant node are not switch-able" ); + return switches_[Ntk::node_to_index( n )]; + } + + /*! \brief Whether a node is currently activated (included in CNF). */ + inline bool is_activated( node const& n ) const + { + return switch_lit( n ).is_complemented(); + /* clauses are activated if switch literal is complemented */ + } + + /*! \brief Deactivates the clauses for a node. */ + void deactivate( node const& n ) + { + if ( is_activated( n ) ) + switches_[Ntk::node_to_index( n )].complement(); + } + + /*! \brief (Re-)activates the clauses for a node. */ + void activate( node const& n ) + { + if ( !is_activated( n ) ) + switches_[Ntk::node_to_index( n )].complement(); + } + + void on_modified( node const& n ) + { + deactivate( n ); + cnf_view_.add_clause( switch_lit( n ) ); + cnf_view_.on_add( n, false ); + /* reuse literals_[n] (so that the fanout clauses are still valid), + but create a new switches_[n] to control a new set of gate clauses */ + } + + void on_delete( node const& n ) + { + deactivate( n ); + } + +private: + CnfView& cnf_view_; + + node_map literals_; + std::vector switches_; +}; + /*! \brief A view to connect logic network creation to SAT solving. * * When using this view to create a new network, it creates a CNF internally @@ -73,31 +159,22 @@ struct cnf_view_params * added. Therefore, a network cannot modify or delete nodes when wrapped in a * `cnf_view`. */ -template -class cnf_view : public Ntk +template +class cnf_view : public cnf_view_impl, Ntk, AllowModify, Solver> { + friend class cnf_view_impl, Ntk, AllowModify, Solver>; + public: + using cnf_view_impl_t = cnf_view_impl, Ntk, AllowModify, Solver>; + using storage = typename Ntk::storage; using node = typename Ntk::node; using signal = typename Ntk::signal; - template - struct lit_maps - { - }; - - template<> - struct lit_maps - { - node_map literals; - std::vector switches; - }; - public: // can only be constructed as empty network - template> - explicit cnf_view( cnf_view_params const& ps = {} ) - : Ntk(), + explicit cnf_view( cnf_view_params const& ps = {} ) + : cnf_view_impl_t( *this ), ps_( ps ) { static_assert( is_network_type_v, "Ntk is not a network type" ); @@ -109,41 +186,18 @@ class cnf_view : public Ntk static_assert( has_foreach_fanin_v, "Ntk does not implement the foreach_fanin method" ); static_assert( has_node_function_v, "Ntk does not implement the node_function method" ); - const auto v = solver_.add_variable(); /* for the constant input */ - assert( v == var( Ntk::get_node( Ntk::get_constant( false ) ) ) ); - (void)v; - - register_events(); - } - - template> - cnf_view( cnf_view_params const& ps = {} ) - : Ntk(), ps_( ps ), maps_( { .literals = node_map( Ntk() ) } ) - /* TODO: should use this to initialize node_map; also, lit_type doesn't have a default constructor... */ - { - static_assert( is_network_type_v, "Ntk is not a network type" ); - static_assert( has_node_to_index_v, "Ntk does not implement the node_to_index method" ); - static_assert( has_get_node_v, "Ntk does not implement the get_node method" ); - static_assert( has_make_signal_v, "Ntk does not implement the make_signal method" ); - static_assert( has_foreach_pi_v, "Ntk does not implement the foreach_pi method" ); - static_assert( has_foreach_po_v, "Ntk does not implement the foreach_po method" ); - static_assert( has_foreach_fanin_v, "Ntk does not implement the foreach_fanin method" ); - static_assert( has_node_function_v, "Ntk does not implement the node_function method" ); + if constexpr ( AllowModify ) + { + cnf_view_impl_t::init(); + } + else + { + const auto v = solver_.add_variable(); /* for the constant input */ + assert( v == var( Ntk::get_node( Ntk::get_constant( false ) ) ) ); + (void)v; + } register_events(); - - solver_.add_variables( Ntk::size() ); - - /* unit clause for constant-0 */ - solver_.add_clause( bill::lit_type( 0, bill::lit_type::polarities::positive ) ); - - Ntk::foreach_pi( [&]( auto const& n, auto i ) { - literals_[n] = bill::lit_type( i+1, bill::lit_type::polarities::positive ); - } ); - - Ntk::foreach_gate( [&]( auto const& n ) { - on_add( n, false ); - } ); } signal create_pi( std::string const& name = std::string() ) @@ -154,8 +208,8 @@ class cnf_view : public Ntk if constexpr ( AllowModify ) { - literals_.resize( bill::lit_type( 0, bill::lit_type::polarities::positive ) ); - literals_[f] = bill::lit_type( v, bill::lit_type::polarities::positive ); + cnf_view_impl_t::literals_.resize( bill::lit_type( 0, bill::lit_type::polarities::positive ) ); + cnf_view_impl_t::literals_[f] = bill::lit_type( v, bill::lit_type::polarities::positive ); return f; } @@ -169,7 +223,7 @@ class cnf_view : public Ntk inline bill::var_type var( node const& n ) const { if constexpr ( AllowModify ) - return literals_[n].variable(); + return cnf_view_impl_t::literals_[n].variable();; return Ntk::node_to_index( n ); } @@ -179,14 +233,6 @@ class cnf_view : public Ntk return bill::lit_type( var( Ntk::get_node( f ) ), Ntk::is_complemented( f ) ? bill::lit_type::polarities::negative : bill::lit_type::polarities::positive ); } - /*! \brief Returns the switching literal associated to a node. */ - template> - inline bill::lit_type switch_lit( node const& n ) const - { - assert( !ntk_.is_pi( n ) && !ntk_.is_constant( n ) && "PI and constant node are not switch-able" ); - return switches_[Ntk::node_to_index( n )]; - } - /*! \brief Solves the network with a set of custom assumptions. * * This function does not assert any primary output, unless specified @@ -203,10 +249,10 @@ class cnf_view : public Ntk if constexpr ( AllowModify ) { std::vector assumptions_copy = assumptions; - for ( auto i = 1u; i < switches_.size(); ++i ) + for ( auto i = 1u; i < cnf_view_impl_t::switches_.size(); ++i ) { if ( Ntk::is_pi( Ntk::index_to_node( i ) ) ) continue; - assumptions_copy.push_back( switches_[i] ); + assumptions_copy.push_back( cnf_view_impl_t::switches_[i] ); } if ( ps_.write_dimacs ) @@ -309,14 +355,6 @@ class cnf_view : public Ntk return values; } - /*! \brief Whether a node is currently activated (included in CNF). */ - template> - inline bool is_activated( node const& n ) const - { - return switch_lit( n ).is_complemented(); - /* clauses are activated if switch literal is complemented */ - } - /*! \brief Blocks last model for primary input values. */ void block() { @@ -327,22 +365,6 @@ class cnf_view : public Ntk add_clause( blocking_clause ); } - /*! \brief Deactivates the clauses for a node. */ - template> - void deactivate( node const& n ) - { - if ( is_activated( n ) ) - switches_[Ntk::node_to_index( n )].complement(); - } - - /*! \brief (Re-)activates the clauses for a node. */ - template> - void activate( node const& n ) - { - if ( !is_activated( n ) ) - switches_[Ntk::node_to_index( n )].complement(); - } - /*! \brief Number of variables. */ inline uint32_t num_vars() { @@ -407,11 +429,12 @@ class cnf_view : public Ntk if constexpr ( AllowModify ) { if ( ps_.auto_update ) - on_modified( n ); + cnf_view_impl_t::on_modified( n ); return; } (void)n; + (void)this; assert( false && "nodes should not be modified in cnf_view" ); std::abort(); } ); @@ -419,11 +442,12 @@ class cnf_view : public Ntk if constexpr ( AllowModify ) { if ( ps_.auto_update ) - on_delete( n ); + cnf_view_impl_t::on_delete( n ); return; } (void)n; + (void)this; assert( false && "nodes should not be deleted in cnf_view" ); std::abort(); } ); @@ -439,15 +463,15 @@ class cnf_view : public Ntk if ( add_var ) { node_lit = bill::lit_type( solver_.add_variable(), bill::lit_type::polarities::positive ); - literals_.resize( bill::lit_type(0, bill::lit_type::polarities::positive) ); - literals_[n] = node_lit; + cnf_view_impl_t::literals_.resize( bill::lit_type(0, bill::lit_type::polarities::positive) ); + cnf_view_impl_t::literals_[n] = node_lit; } else - node_lit = literals_[n]; + node_lit = cnf_view_impl_t::literals_[n]; switch_lit = bill::lit_type( solver_.add_variable(), bill::lit_type::polarities::positive ); - switches_.resize( Ntk::size() ); - switches_[Ntk::node_to_index( n )] = bill::lit_type( switch_lit.variable(), bill::lit_type::polarities::negative ); //lit_not( switch_lit ); + cnf_view_impl_t::switches_.resize( Ntk::size() ); + cnf_view_impl_t::switches_[Ntk::node_to_index( n )] = bill::lit_type( switch_lit.variable(), bill::lit_type::polarities::negative ); //lit_not( switch_lit ); } else { @@ -533,32 +557,12 @@ class cnf_view : public Ntk detail::on_function( node_lit, child_lits, Ntk::node_function( n ), _add_clause ); } - template> - void on_modified( node const& n ) - { - deactivate( n ); - add_clause( switch_lit( n ) ); - on_add( n, false ); - /* reuse literals_[n] (so that the fanout clauses are still valid), - but create a new switches_[n] to control a new set of gate clauses */ - } - - template> - void on_delete( node const& n ) - { - deactivate( n ); - } - private: bill::solver solver_; bill::result::model_type model_; percy::cnf_formula dimacs_; - cnf_view_params ps_; - - lit_maps maps_; - node_map& literals_ = maps_.literals; - std::vector& switches_ = maps_.switches; + cnf_view_params ps_; }; } /* namespace mockturtle */ From 51bfebaef4ff083b93d0ebbe506b50c6282cebac Mon Sep 17 00:00:00 2001 From: Sonia Date: Wed, 25 Mar 2020 19:02:24 +0100 Subject: [PATCH 04/22] constructor with existing network; adding unit clause for constant node --- include/mockturtle/views/cnf_view.hpp | 49 ++++++++++++++++++++++----- 1 file changed, 40 insertions(+), 9 deletions(-) diff --git a/include/mockturtle/views/cnf_view.hpp b/include/mockturtle/views/cnf_view.hpp index fe179f15d..514d30ed8 100644 --- a/include/mockturtle/views/cnf_view.hpp +++ b/include/mockturtle/views/cnf_view.hpp @@ -78,18 +78,30 @@ class cnf_view_impl : public Ntk : Ntk(), cnf_view_( cnf_view ), literals_( *this ) { } + cnf_view_impl( CnfView& cnf_view, Ntk& ntk ) + : Ntk( ntk ), cnf_view_( cnf_view ), literals_( *this ) + { } + void init() { cnf_view_.solver_.add_variables( Ntk::size() ); - /* unit clause for constant-0 */ - cnf_view_.solver_.add_clause( bill::lit_type( 0, bill::lit_type::polarities::positive ) ); + /* unit clause for constants */ + bill::lit_type lit_const( 0, bill::lit_type::polarities::negative ); + cnf_view_.add_clause( lit_const ); + literals_[Ntk::get_constant( false )] = lit_const; + if ( Ntk::get_node( Ntk::get_constant( false ) ) != Ntk::get_node( Ntk::get_constant( true ) ) ) + { + literals_[Ntk::get_constant( true )] = ~lit_const; + } - Ntk::foreach_pi( [&]( auto const& n, auto i ) { - literals_[n] = bill::lit_type( i+1, bill::lit_type::polarities::positive ); + uint32_t v = 0; + Ntk::foreach_pi( [&]( auto const& n ) { + literals_[n] = bill::lit_type( ++v, bill::lit_type::polarities::positive ); } ); Ntk::foreach_gate( [&]( auto const& n ) { + literals_[n] = bill::lit_type( ++v, bill::lit_type::polarities::positive ); cnf_view_.on_add( n, false ); } ); } @@ -194,12 +206,31 @@ class cnf_view : public cnf_view_impl, Ntk, A { const auto v = solver_.add_variable(); /* for the constant input */ assert( v == var( Ntk::get_node( Ntk::get_constant( false ) ) ) ); - (void)v; + add_clause( bill::lit_type( v, bill::lit_type::polarities::negative ) ); } register_events(); } + template> + explicit cnf_view( Ntk& ntk, cnf_view_params const& ps = {} ) + : cnf_view_impl_t( *this, ntk ), + ps_( ps ) + { + static_assert( is_network_type_v, "Ntk is not a network type" ); + static_assert( has_node_to_index_v, "Ntk does not implement the node_to_index method" ); + static_assert( has_get_node_v, "Ntk does not implement the get_node method" ); + static_assert( has_make_signal_v, "Ntk does not implement the make_signal method" ); + static_assert( has_foreach_pi_v, "Ntk does not implement the foreach_pi method" ); + static_assert( has_foreach_po_v, "Ntk does not implement the foreach_po method" ); + static_assert( has_foreach_fanin_v, "Ntk does not implement the foreach_fanin method" ); + static_assert( has_node_function_v, "Ntk does not implement the node_function method" ); + + cnf_view_impl_t::init(); + + register_events(); + } + signal create_pi( std::string const& name = std::string() ) { const auto f = Ntk::create_pi( name ); @@ -455,15 +486,15 @@ class cnf_view : public cnf_view_impl, Ntk, A void on_add( node const& n, bool add_var = true ) /* add_var is only used when AllowModify = true */ { - bill::lit_type node_lit(0, bill::lit_type::polarities::positive); - bill::lit_type switch_lit(0, bill::lit_type::polarities::positive); + bill::lit_type node_lit; + bill::lit_type switch_lit; if constexpr ( AllowModify ) { if ( add_var ) { node_lit = bill::lit_type( solver_.add_variable(), bill::lit_type::polarities::positive ); - cnf_view_impl_t::literals_.resize( bill::lit_type(0, bill::lit_type::polarities::positive) ); + cnf_view_impl_t::literals_.resize(); cnf_view_impl_t::literals_[n] = node_lit; } else @@ -471,7 +502,7 @@ class cnf_view : public cnf_view_impl, Ntk, A switch_lit = bill::lit_type( solver_.add_variable(), bill::lit_type::polarities::positive ); cnf_view_impl_t::switches_.resize( Ntk::size() ); - cnf_view_impl_t::switches_[Ntk::node_to_index( n )] = bill::lit_type( switch_lit.variable(), bill::lit_type::polarities::negative ); //lit_not( switch_lit ); + cnf_view_impl_t::switches_[Ntk::node_to_index( n )] = ~switch_lit; } else { From cc9d3e5ea9aea0be13f4e907ea8081a537793f90 Mon Sep 17 00:00:00 2001 From: Sonia Date: Wed, 25 Mar 2020 19:10:38 +0100 Subject: [PATCH 05/22] updates according to comments --- include/mockturtle/views/cnf_view.hpp | 30 ++++++++++++++++++++++----- 1 file changed, 25 insertions(+), 5 deletions(-) diff --git a/include/mockturtle/views/cnf_view.hpp b/include/mockturtle/views/cnf_view.hpp index 514d30ed8..ce90cc147 100644 --- a/include/mockturtle/views/cnf_view.hpp +++ b/include/mockturtle/views/cnf_view.hpp @@ -53,13 +53,19 @@ struct cnf_view_params { /*! \brief Write DIMACS file, whenever solve is called. */ std::optional write_dimacs{}; - bool auto_update{true}; /* only used when AllowModify = true */ + + /*! \brief Automatically update clauses when network is modified. + Only meaningful when AllowModify = true. */ + bool auto_update{true}; }; /* forward declaration */ template class cnf_view; +namespace detail +{ + template class cnf_view_impl : public Ntk { @@ -124,14 +130,18 @@ class cnf_view_impl : public Ntk void deactivate( node const& n ) { if ( is_activated( n ) ) + { switches_[Ntk::node_to_index( n )].complement(); + } } /*! \brief (Re-)activates the clauses for a node. */ void activate( node const& n ) { if ( !is_activated( n ) ) + { switches_[Ntk::node_to_index( n )].complement(); + } } void on_modified( node const& n ) @@ -155,6 +165,8 @@ class cnf_view_impl : public Ntk std::vector switches_; }; +} /* namespace detail */ + /*! \brief A view to connect logic network creation to SAT solving. * * When using this view to create a new network, it creates a CNF internally @@ -172,12 +184,12 @@ class cnf_view_impl : public Ntk * `cnf_view`. */ template -class cnf_view : public cnf_view_impl, Ntk, AllowModify, Solver> +class cnf_view : public detail::cnf_view_impl, Ntk, AllowModify, Solver> { - friend class cnf_view_impl, Ntk, AllowModify, Solver>; + friend class detail::cnf_view_impl, Ntk, AllowModify, Solver>; public: - using cnf_view_impl_t = cnf_view_impl, Ntk, AllowModify, Solver>; + using cnf_view_impl_t = detail::cnf_view_impl, Ntk, AllowModify, Solver>; using storage = typename Ntk::storage; using node = typename Ntk::node; @@ -254,7 +266,9 @@ class cnf_view : public cnf_view_impl, Ntk, A inline bill::var_type var( node const& n ) const { if constexpr ( AllowModify ) + { return cnf_view_impl_t::literals_[n].variable();; + } return Ntk::node_to_index( n ); } @@ -282,7 +296,7 @@ class cnf_view : public cnf_view_impl, Ntk, A std::vector assumptions_copy = assumptions; for ( auto i = 1u; i < cnf_view_impl_t::switches_.size(); ++i ) { - if ( Ntk::is_pi( Ntk::index_to_node( i ) ) ) continue; + if ( Ntk::is_pi( Ntk::index_to_node( i ) ) ) { continue; } assumptions_copy.push_back( cnf_view_impl_t::switches_[i] ); } @@ -460,7 +474,9 @@ class cnf_view : public cnf_view_impl, Ntk, A if constexpr ( AllowModify ) { if ( ps_.auto_update ) + { cnf_view_impl_t::on_modified( n ); + } return; } @@ -473,7 +489,9 @@ class cnf_view : public cnf_view_impl, Ntk, A if constexpr ( AllowModify ) { if ( ps_.auto_update ) + { cnf_view_impl_t::on_delete( n ); + } return; } @@ -498,7 +516,9 @@ class cnf_view : public cnf_view_impl, Ntk, A cnf_view_impl_t::literals_[n] = node_lit; } else + { node_lit = cnf_view_impl_t::literals_[n]; + } switch_lit = bill::lit_type( solver_.add_variable(), bill::lit_type::polarities::positive ); cnf_view_impl_t::switches_.resize( Ntk::size() ); From 120e3a0ea7c1aaf185fb1dee4332870f35e3f4db Mon Sep 17 00:00:00 2001 From: Sonia Date: Thu, 26 Mar 2020 12:41:22 +0100 Subject: [PATCH 06/22] add test cases --- include/mockturtle/views/cnf_view.hpp | 2 +- test/views/cnf_view.cpp | 63 +++++++++++++++++++++++++++ 2 files changed, 64 insertions(+), 1 deletion(-) diff --git a/include/mockturtle/views/cnf_view.hpp b/include/mockturtle/views/cnf_view.hpp index ce90cc147..6bf56a507 100644 --- a/include/mockturtle/views/cnf_view.hpp +++ b/include/mockturtle/views/cnf_view.hpp @@ -267,7 +267,7 @@ class cnf_view : public detail::cnf_view_impl { if constexpr ( AllowModify ) { - return cnf_view_impl_t::literals_[n].variable();; + return cnf_view_impl_t::literals_[n].variable(); } return Ntk::node_to_index( n ); } diff --git a/test/views/cnf_view.cpp b/test/views/cnf_view.cpp index 2b8e6022c..4e516b359 100644 --- a/test/views/cnf_view.cpp +++ b/test/views/cnf_view.cpp @@ -73,3 +73,66 @@ TEST_CASE( "find multiple solutions with cnf_view", "[cnf_view]" ) } CHECK( ctr == 4u ); } + +/* cnf_view with AllowModify option */ + +TEST_CASE( "modify network", "[cnf_view]" ) +{ + cnf_view xag; + const auto a = xag.create_pi(); + const auto b = xag.create_pi(); + + const auto f = xag.create_and( a, b ); + xag.create_po( f ); + const auto g = xag.create_xor( a, b ); + xag.substitute_node( xag.get_node( f ), g ); + + const auto result = xag.solve(); + CHECK( result ); + CHECK( *result ); + CHECK( xag.value( xag.get_node( a ) ) != xag.value( xag.get_node( b ) ) ); +} + +TEST_CASE( "deactivate node", "[cnf_view]" ) +{ + cnf_view xag; + const auto a = xag.create_pi(); + const auto b = xag.create_pi(); + const auto f = xag.create_xor( a, b ); + xag.create_po( f ); + + /* virtually replacing XOR with AND */ + xag.deactivate( xag.get_node( f ) ); + CHECK( !xag.is_activated( xag.get_node( f ) ) ); + xag.add_clause( xag.lit( a ), ~xag.lit( f ) ); + xag.add_clause( xag.lit( b ), ~xag.lit( f ) ); + xag.add_clause( ~xag.lit( a ), ~xag.lit( b ), xag.lit( f ) ); + + const auto result = xag.solve(); + CHECK( result ); + CHECK( *result ); + CHECK( xag.value( xag.get_node( a ) ) ); + CHECK( xag.value( xag.get_node( b ) ) ); +} + +TEST_CASE( "build cnf_view on top of existing network and create_pi afterwards", "[cnf_view]" ) +{ + mig_network mig; + const auto a = mig.create_pi(); + const auto b = mig.create_pi(); + const auto c = mig.create_pi(); + mig.create_po( mig.create_maj( a, b, c ) ); + + cnf_view view( mig ); + const auto d = view.create_pi(); + view.create_po( view.create_maj( a, b, d ) ); + view.create_po( !a ); + + const auto result = view.solve(); + CHECK( result ); + CHECK( *result ); + CHECK( !view.value( view.get_node( a ) ) ); + CHECK( view.value( view.get_node( b ) ) ); + CHECK( view.value( view.get_node( c ) ) ); + CHECK( view.value( view.get_node( d ) ) ); +} From 3a554675b1a58fc9f60732f49ec056c14de12a63 Mon Sep 17 00:00:00 2001 From: Sonia Date: Fri, 27 Mar 2020 16:41:17 +0100 Subject: [PATCH 07/22] get lit for node and add_var with AllowModify --- include/mockturtle/views/cnf_view.hpp | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/include/mockturtle/views/cnf_view.hpp b/include/mockturtle/views/cnf_view.hpp index 8a0a38024..c5951edbc 100644 --- a/include/mockturtle/views/cnf_view.hpp +++ b/include/mockturtle/views/cnf_view.hpp @@ -115,6 +115,11 @@ class cnf_view_impl : public Ntk } ); } + inline bill::var_type add_var() + { + return cnf_view_.solver_.add_variable(); + } + /*! \brief Returns the switching literal associated to a node. */ inline bill::lit_type switch_lit( node const& n ) const { @@ -275,6 +280,12 @@ class cnf_view : public detail::cnf_view_impl return Ntk::node_to_index( n ); } + /*! \brief Returns the literal associated to a node. */ + inline bill::lit_type lit( node const& n ) const + { + return bill::lit_type( var( n ), bill::lit_type::polarities::positive ); + } + /*! \brief Returns the literal associated to a signal. */ inline bill::lit_type lit( signal const& f ) const { From 4d83133921eb42bc38548a9b99f76e6c6a597b99 Mon Sep 17 00:00:00 2001 From: Sonia Date: Wed, 8 Apr 2020 12:49:27 +0200 Subject: [PATCH 08/22] fix merge error --- include/mockturtle/views/cnf_view.hpp | 5 ----- 1 file changed, 5 deletions(-) diff --git a/include/mockturtle/views/cnf_view.hpp b/include/mockturtle/views/cnf_view.hpp index 0809b7b54..7304ff5d7 100644 --- a/include/mockturtle/views/cnf_view.hpp +++ b/include/mockturtle/views/cnf_view.hpp @@ -131,11 +131,6 @@ class cnf_view_impl : public Ntk return cnf_view_.solver_.add_variable(); } - inline bill::var_type add_var() - { - return cnf_view_.solver_.add_variable(); - } - /*! \brief Returns the switching literal associated to a node. */ inline bill::lit_type switch_lit( node const& n ) const { From 952198e0abc83052ef6545764338593c999e7f81 Mon Sep 17 00:00:00 2001 From: Sonia Date: Mon, 3 Aug 2020 20:46:39 +0200 Subject: [PATCH 09/22] bit packing --- .../algorithms/pattern_generation.hpp | 2 +- include/mockturtle/algorithms/sim_resub.hpp | 2 +- include/mockturtle/algorithms/simulation.hpp | 158 ++++++++++++++++-- 3 files changed, 149 insertions(+), 13 deletions(-) diff --git a/include/mockturtle/algorithms/pattern_generation.hpp b/include/mockturtle/algorithms/pattern_generation.hpp index d0da63c68..447409e37 100644 --- a/include/mockturtle/algorithms/pattern_generation.hpp +++ b/include/mockturtle/algorithms/pattern_generation.hpp @@ -130,7 +130,7 @@ class patgen_impl stopwatch t( st.time_total ); call_with_stopwatch( st.time_sim, [&]() { - simulate_nodes( ntk, tts, sim ); + simulate_nodes( ntk, tts, sim, true ); } ); if ( ps.num_stuck_at > 0 ) diff --git a/include/mockturtle/algorithms/sim_resub.hpp b/include/mockturtle/algorithms/sim_resub.hpp index 40ce5625b..e078cf004 100644 --- a/include/mockturtle/algorithms/sim_resub.hpp +++ b/include/mockturtle/algorithms/sim_resub.hpp @@ -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, tts, sim ); + simulate_nodes( ntk, tts, sim, true ); }); } diff --git a/include/mockturtle/algorithms/simulation.hpp b/include/mockturtle/algorithms/simulation.hpp index 404ba7d7b..2fd7cc140 100644 --- a/include/mockturtle/algorithms/simulation.hpp +++ b/include/mockturtle/algorithms/simulation.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 @@ -28,6 +28,7 @@ \brief Simulate networks \author Mathias Soeken + \author Siang-Yun Lee (partial simulation) */ #pragma once @@ -35,6 +36,7 @@ #include #include #include +#include #include "../traits.hpp" #include "../utils/node_map.hpp" @@ -42,6 +44,7 @@ #include #include #include +#include #include #include @@ -167,6 +170,8 @@ class default_simulator> */ class partial_simulator { + friend class bit_packed_simulator; + public: partial_simulator() {} @@ -278,6 +283,135 @@ class partial_simulator uint32_t num_patterns; }; +class bit_packed_simulator : public partial_simulator +{ +public: + using partial_simulator::compute_constant; + using partial_simulator::compute_pi; + using partial_simulator::compute_not; + using partial_simulator::num_bits; + using partial_simulator::get_patterns; + + bit_packed_simulator() {} + + bit_packed_simulator( unsigned num_pis, unsigned num_patterns, std::default_random_engine::result_type seed = 0 ) + : partial_simulator( num_pis, num_patterns, seed ), packed_patterns( num_patterns ) + { + for ( auto i = 0u; i < num_pis; ++i ) + { + care.emplace_back( num_patterns ); + care.back() = ~care.back(); + } + } + + bit_packed_simulator( std::vector const& initial_patterns ) + : partial_simulator( initial_patterns ), packed_patterns( num_patterns ) + { + for ( auto i = 0u; i < patterns.size(); ++i ) + { + care.emplace_back( num_patterns ); + care.back() = ~care.back(); + } + } + + void add_pattern( std::vector const& pattern, std::vector const& care_bits ) + { + assert( pattern.size() == care_bits.size() ); + assert( pattern.size() == patterns.size() ); + + for ( auto i = 0u; i < pattern.size(); ++i ) + { + patterns.at( i ).add_bit( pattern.at( i ) ); + care.at( i ).add_bit( care_bits.at( i ) ); + } + ++num_patterns; + } + + /* return true when some patterns are packed (so that update of truth tables is needed) */ + bool pack_bits() + { + if ( num_patterns == 0u ) { return false; } + if ( num_patterns == packed_patterns ) { return false; } + assert( num_patterns > packed_patterns ); + + std::vector empty_slots; + /* for each unpacked pattern (at `p`), try to pack it into one of the patterns before it (at `pos` in block `block`). */ + for ( int p = num_patterns - 1; p >= (int)packed_patterns; --p ) + { + for ( auto block = p < 1024 ? 0 : std::rand() % ( p >> 6 ); block <= ( p >> 6 ); ++block ) + { + uint64_t unavailable = 0u; + /* check each PI */ + for ( auto i = 0u; i < patterns.size(); ++i ) + { + if ( !kitty::get_bit( care[i], p ) ) { continue; } /* only check for the cared PIs of p */ + unavailable |= care[i]._bits[block]; + } + auto pos = kitty::find_first_bit_in_word( ~unavailable ); + if ( pos != -1 && ( block < ( p >> 6 ) || pos < ( p % 64 ) ) ) + { + move_pattern( p, pos + ( block << 6 ) ); + empty_slots.emplace_back( p ); + } + } + } + + if ( empty_slots.size() > 0u ) + { + /* fill the empty slots (from smaller values; `empty_slots` should be reversely sorted) */ + /* `empty_slots[j]` is the smallest position where larger positions are all empty */ + int j = 0; + for ( int i = empty_slots.size() - 1; i >= 0; --i ) + { + while ( empty_slots[j] >= num_patterns - 1 && j <= i ) + { + if ( empty_slots[j] == num_patterns - 1 ) { --num_patterns; } + ++j; + } + if ( j > i ) { break; } + move_pattern( num_patterns - 1, empty_slots[i] ); + --num_patterns; + } + + assert( patterns[0].num_bits() - num_patterns == empty_slots.size() ); + for ( auto i = 0u; i < patterns.size(); ++i ) + { + patterns[i].resize( num_patterns ); + care[i].resize( num_patterns ); + } + packed_patterns = num_patterns; + return true; + } + packed_patterns = num_patterns; + return false; + } + +private: + /* move the pattern at position `from` to position `to`. */ + void move_pattern( uint32_t const from, uint32_t const to ) + { + for ( auto i = 0u; i < patterns.size(); ++i ) + { + if ( !kitty::get_bit( care[i], from ) ) { continue; } + assert( !kitty::get_bit( care[i], to ) ); + if ( kitty::get_bit( patterns[i], from ) ) + { + kitty::set_bit( patterns[i], to ); + } + else + { + kitty::clear_bit( patterns[i], to ); + } + kitty::set_bit( care[i], to ); + kitty::clear_bit( care[i], from ); + } + } + +private: + std::vector care; + uint32_t packed_patterns; +}; + /*! \brief Simulates a network with a generic simulator. * * This is a generic simulation algorithm that can simulate arbitrary values. @@ -429,8 +563,8 @@ void simulate_nodes( Ntk const& ntk, unordered_node_map& no namespace detail { -template -void simulate_fanin_cone( Ntk const& ntk, typename Ntk::node const& n, unordered_node_map& node_to_value, partial_simulator const& sim ) +template +void simulate_fanin_cone( Ntk const& ntk, typename Ntk::node const& n, unordered_node_map& node_to_value, Simulator const& sim ) { std::vector fanin_values( ntk.fanin_size( n ) ); ntk.foreach_fanin( n, [&]( auto const& f, auto i ) { @@ -444,8 +578,8 @@ void simulate_fanin_cone( Ntk const& ntk, typename Ntk::node const& n, unordered node_to_value[n] = ntk.compute( n, fanin_values.begin(), fanin_values.end() ); } -template -void re_simulate_fanin_cone( Ntk const& ntk, typename Ntk::node const& n, unordered_node_map& node_to_value, partial_simulator const& sim ) +template +void re_simulate_fanin_cone( Ntk const& ntk, typename Ntk::node const& n, unordered_node_map& node_to_value, Simulator const& sim ) { std::vector fanin_values( ntk.fanin_size( n ) ); ntk.foreach_fanin( n, [&]( auto const& f, auto i ) { @@ -459,8 +593,8 @@ void re_simulate_fanin_cone( Ntk const& ntk, typename Ntk::node const& n, unorde ntk.compute( n, node_to_value[n], fanin_values.begin(), fanin_values.end() ); } -template -void update_const_pi( Ntk const& ntk, unordered_node_map& node_to_value, partial_simulator const& sim ) +template +void update_const_pi( Ntk const& ntk, unordered_node_map& node_to_value, Simulator const& sim ) { /* constants */ node_to_value[ntk.get_node( ntk.get_constant( false ) )] = sim.compute_constant( ntk.constant_value( ntk.get_node( ntk.get_constant( false ) ) ) ); @@ -485,8 +619,8 @@ void update_const_pi( Ntk const& ntk, unordered_node_map -void simulate_node( Ntk const& ntk, typename Ntk::node const& n, unordered_node_map& node_to_value, partial_simulator const& sim ) +template +void simulate_node( Ntk const& ntk, typename Ntk::node const& n, unordered_node_map& node_to_value, Simulator const& sim ) { static_assert( is_network_type_v, "Ntk is not a network type" ); static_assert( has_get_constant_v, "Ntk does not implement the get_constant method" ); @@ -496,6 +630,7 @@ void simulate_node( Ntk const& ntk, typename Ntk::node const& n, unordered_node_ static_assert( has_foreach_fanin_v, "Ntk does not implement the foreach_fanin method" ); static_assert( has_compute_v, "Ntk does not implement the compute specialization for kitty::partial_truth_table" ); static_assert( has_compute_inplace_v, "Ntk does not implement the in-place compute specialization for kitty::partial_truth_table" ); + static_assert( std::is_same_v || std::is_same_v, "This function is specialized for partial_simulator or bit_packed_simulator" ); if ( node_to_value[ntk.get_node( ntk.get_constant( false ) )].num_bits() != sim.num_bits() ) { @@ -533,8 +668,8 @@ void simulate_node( Ntk const& ntk, typename Ntk::node const& n, unordered_node_ * In contrast, when this parameter is false, only the last block of `partial_truth_table` will be re-computed, * and it is assumed that `node_to_value.has( n )` is true for every node. */ -template -void simulate_nodes( Ntk const& ntk, unordered_node_map& node_to_value, partial_simulator const& sim, bool simulate_whole_tt = true ) +template +void simulate_nodes( Ntk const& ntk, unordered_node_map& node_to_value, Simulator const& sim, bool simulate_whole_tt ) { static_assert( is_network_type_v, "Ntk is not a network type" ); static_assert( has_get_constant_v, "Ntk does not implement the get_constant method" ); @@ -545,6 +680,7 @@ void simulate_nodes( Ntk const& ntk, unordered_node_map, "Ntk does not implement the foreach_fanin method" ); static_assert( has_compute_v, "Ntk does not implement the compute specialization for kitty::partial_truth_table" ); static_assert( has_compute_inplace_v, "Ntk does not implement the in-place compute specialization for kitty::partial_truth_table" ); + static_assert( std::is_same_v || std::is_same_v, "This function is specialized for partial_simulator or bit_packed_simulator" ); detail::update_const_pi( ntk, node_to_value, sim ); From d4260bb0b14b3d2520d3a1de2548d049269eeeca Mon Sep 17 00:00:00 2001 From: Sonia Date: Mon, 3 Aug 2020 20:46:47 +0200 Subject: [PATCH 10/22] test --- test/algorithms/simulation.cpp | 63 ++++++++++++++++++++++++++++++++++ 1 file changed, 63 insertions(+) diff --git a/test/algorithms/simulation.cpp b/test/algorithms/simulation.cpp index 153222c42..c835fc75e 100644 --- a/test/algorithms/simulation.cpp +++ b/test/algorithms/simulation.cpp @@ -190,4 +190,67 @@ TEST_CASE( "Incremental simulation with partial_simulator", "[simulation]" ) const auto f5 = aig.create_and( f2, f4 ); simulate_node( aig, aig.get_node( f5 ), node_to_value, sim ); CHECK( ( aig.is_complemented( f5 ) ? ~node_to_value[f5] : node_to_value[f5] ) == kitty::partial_truth_table( 65 ) ); +} + +TEST_CASE( "Bit packing", "[simulation]" ) +{ + std::vector pats( 5 ); + pats[0].add_bits( 0x1, 2 ); /* x0 = 01 */ + pats[1].add_bits( 0x1, 2 ); /* x1 = 01 */ + pats[2].add_bits( 0x1, 2 ); /* x2 = 01 */ + pats[3].add_bits( 0x1, 2 ); /* x3 = 01 */ + pats[4].add_bits( 0x1, 2 ); /* x4 = 01 */ + bit_packed_simulator sim( pats ); /* initial patterns are not packable (all bits are cared) */ + + std::vector p( 5 ); /* pattern */ + std::vector c( 5 ); /* care */ + + /* first pattern */ + p[0] = 0; p[1] = 1; p[2] = 0; p[3] = 1; p[4] = 1; + c[0] = 0; c[1] = 0; c[2] = 0; c[3] = 1; c[4] = 1; + sim.add_pattern( p, c ); + + /* second pattern */ + p[0] = 1; p[1] = 0; p[2] = 1; p[3] = 0; p[4] = 1; + c[0] = 0; c[1] = 0; c[2] = 1; c[3] = 0; c[4] = 1; + sim.add_pattern( p, c ); + + CHECK( sim.pack_bits() == false ); + CHECK( sim.num_bits() == 4u ); + + /* third pattern: can be packed into the third bit */ + p[0] = 1; p[1] = 0; p[2] = 1; p[3] = 0; p[4] = 0; + c[0] = 0; c[1] = 1; c[2] = 1; c[3] = 0; c[4] = 0; + sim.add_pattern( p, c ); + + CHECK( sim.pack_bits() == true ); + CHECK( sim.num_bits() == 4u ); + CHECK( ( sim.compute_pi( 0 )._bits[0] & 0x3 ) == 0x1 ); /* x0 = xxx01 -> xx01 */ + CHECK( ( sim.compute_pi( 1 )._bits[0] & 0x7 ) == 0x1 ); /* x1 = 0xx01 -> x001 */ + CHECK( ( sim.compute_pi( 2 )._bits[0] & 0xf ) == 0xd ); /* x2 = 11x01 -> 1101 */ + CHECK( ( sim.compute_pi( 3 )._bits[0] & 0x7 ) == 0x5 ); /* x3 = xx101 -> x101 */ + CHECK( ( sim.compute_pi( 4 )._bits[0] & 0xf ) == 0xd ); /* x4 = x1101 -> 1101 */ + + /* fourth pattern: can be packed into the fourth bit */ + p[0] = 1; p[1] = 0; p[2] = 0; p[3] = 1; p[4] = 0; + c[0] = 1; c[1] = 1; c[2] = 0; c[3] = 1; c[4] = 0; + sim.add_pattern( p, c ); + + /* fifth pattern */ + p[0] = 0; p[1] = 1; p[2] = 0; p[3] = 1; p[4] = 1; + c[0] = 1; c[1] = 0; c[2] = 0; c[3] = 0; c[4] = 1; + sim.add_pattern( p, c ); + + /* sixth pattern: can be packed into the third bit */ + p[0] = 1; p[1] = 0; p[2] = 0; p[3] = 1; p[4] = 0; + c[0] = 1; c[1] = 0; c[2] = 0; c[3] = 0; c[4] = 0; + sim.add_pattern( p, c ); + + CHECK( sim.pack_bits() == true ); + CHECK( sim.num_bits() == 5u ); + CHECK( ( sim.compute_pi( 0 )._bits[0] & 0x1f ) == 0x0d ); /* x0 = 101xx01 -> 01101 */ + CHECK( ( sim.compute_pi( 1 )._bits[0] & 0x0f ) == 0x01 ); /* x1 = xx0x001 -> x0001 */ + CHECK( ( sim.compute_pi( 2 )._bits[0] & 0x0f ) == 0x0d ); /* x2 = xxx1101 -> x1101 */ + CHECK( ( sim.compute_pi( 3 )._bits[0] & 0x0f ) == 0x0d ); /* x3 = xx1x101 -> x1101 */ + CHECK( ( sim.compute_pi( 4 )._bits[0] & 0x1f ) == 0x1d ); /* x4 = x1x1101 -> 11101 */ } \ No newline at end of file From b96a8f7f1c1e4b3743c9ae9059bdfcdba3f914f4 Mon Sep 17 00:00:00 2001 From: Sonia Date: Mon, 3 Aug 2020 22:09:47 +0200 Subject: [PATCH 11/22] more constructors & docs --- docs/algorithms/simulation.rst | 22 ++++++- include/mockturtle/algorithms/simulation.hpp | 65 +++++++++++++++----- 2 files changed, 71 insertions(+), 16 deletions(-) diff --git a/docs/algorithms/simulation.rst b/docs/algorithms/simulation.rst index 88b6e6333..5ba3d134e 100644 --- a/docs/algorithms/simulation.rst +++ b/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 const& ) .. doxygenfunction:: mockturtle::partial_simulator::partial_simulator( const std::string&, uint32_t ) +**Interfaces** + +.. doxygenfunction:: mockturtle::partial_simulator::add_pattern( std::vector const& ) + .. doxygenfunction:: mockturtle::partial_simulator::num_bits() .. doxygenfunction:: mockturtle::partial_simulator::get_patterns() -.. doxygenfunction:: mockturtle::simulate_nodes( Ntk const&, unordered_node_map&, partial_simulator const&, bool ) +**Simulation** + +.. doxygenfunction:: mockturtle::simulate_nodes( Ntk const&, unordered_node_map&, Simulator const&, bool ) + +.. doxygenfunction:: mockturtle::simulate_node( Ntk const&, typename Ntk::node const&, unordered_node_map&, 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 const&, std::vector const& ) -.. doxygenfunction:: mockturtle::simulate_node( Ntk const&, typename Ntk::node const&, unordered_node_map&, partial_simulator const& ) +.. doxygenfunction:: mockturtle::bit_packed_simulator::pack_bits() diff --git a/include/mockturtle/algorithms/simulation.hpp b/include/mockturtle/algorithms/simulation.hpp index 2fd7cc140..21bbf47e0 100644 --- a/include/mockturtle/algorithms/simulation.hpp +++ b/include/mockturtle/algorithms/simulation.hpp @@ -257,6 +257,10 @@ class partial_simulator return num_patterns; } + /*! \brief Add a pattern (primary input assignment) into the pattern set. + * + * \param pattern The pattern. Length should be the same as number of PIs. + */ void add_pattern( std::vector const& pattern ) { assert( pattern.size() == patterns.size() ); @@ -270,8 +274,7 @@ class partial_simulator /*! \brief Get the simulation patterns. * - * Returns a vector of `num_pis()` patterns stored in `kitty::partial_truth_table`s. - * + * \return A vector of `num_pis()` patterns stored in `kitty::partial_truth_table`s. */ std::vector get_patterns() const { @@ -283,6 +286,12 @@ class partial_simulator uint32_t num_patterns; }; +/*! \brief Simulates partial truth tables, and performs bit packing when requested. + * + * This class has the same interfaces as `partial_simulator`, except that + * (1) care bits should be provided as the second argument of `add_pattern`; and + * (2) `pack_bits` can be called to reduce the size of pattern set. + */ class bit_packed_simulator : public partial_simulator { public: @@ -297,23 +306,38 @@ class bit_packed_simulator : public partial_simulator bit_packed_simulator( unsigned num_pis, unsigned num_patterns, std::default_random_engine::result_type seed = 0 ) : partial_simulator( num_pis, num_patterns, seed ), packed_patterns( num_patterns ) { - for ( auto i = 0u; i < num_pis; ++i ) - { - care.emplace_back( num_patterns ); - care.back() = ~care.back(); - } + fill_cares( num_pis ); + } + + /* copy constructor */ + bit_packed_simulator( bit_packed_simulator const& sim ) + : partial_simulator( sim ), care( sim.care ), packed_patterns( sim.packed_patterns ) + { } + + /* copy constructor from `partial_simulator` */ + bit_packed_simulator( partial_simulator const& sim ) + : partial_simulator( sim ), packed_patterns( num_patterns ) + { + fill_cares( patterns.size() ); } bit_packed_simulator( std::vector const& initial_patterns ) : partial_simulator( initial_patterns ), packed_patterns( num_patterns ) { - for ( auto i = 0u; i < patterns.size(); ++i ) - { - care.emplace_back( num_patterns ); - care.back() = ~care.back(); - } + fill_cares( patterns.size() ); } + bit_packed_simulator( const std::string& filename, uint32_t length = 0u ) + : partial_simulator( filename, length ), packed_patterns( num_patterns ) + { + fill_cares( patterns.size() ); + } + + /*! \brief Add a pattern (primary input assignment) into the pattern set. + * + * \param pattern The pattern. Length should be the same as number of PIs. + * \param care_bits Care bits of the pattern. Length should be the same as `pattern`. + */ void add_pattern( std::vector const& pattern, std::vector const& care_bits ) { assert( pattern.size() == care_bits.size() ); @@ -327,7 +351,10 @@ class bit_packed_simulator : public partial_simulator ++num_patterns; } - /* return true when some patterns are packed (so that update of truth tables is needed) */ + /*! \brief Try to pack the newly added patterns (since the last call) into preceding patterns. + * + * \return `true` when some patterns are packed (so that update of simulated truth tables is needed) + */ bool pack_bits() { if ( num_patterns == 0u ) { return false; } @@ -387,6 +414,16 @@ class bit_packed_simulator : public partial_simulator } private: + /* all bits in patterns generated before construction are care bits */ + void fill_cares( uint32_t const num_pis ) + { + for ( auto i = 0u; i < num_pis; ++i ) + { + care.emplace_back( num_patterns ); + care.back() = ~care.back(); + } + } + /* move the pattern at position `from` to position `to`. */ void move_pattern( uint32_t const from, uint32_t const to ) { @@ -659,7 +696,7 @@ void simulate_node( Ntk const& ntk, typename Ntk::node const& n, unordered_node_ } } -/*! \brief Simulates a network with a partial simulator. +/*! \brief Simulates a network with `partial_simulator` (or `bit_packed_simulator`). * * This is the specialization for `partial_truth_table`. * This function simulates every node in the circuit. From 32f3b85e49a990e4cd76c8a637643584e9935ea0 Mon Sep 17 00:00:00 2001 From: Sonia Date: Mon, 3 Aug 2020 23:17:41 +0200 Subject: [PATCH 12/22] use bit packing in pattern generation --- experiments/pattern_generation.cpp | 2 +- .../algorithms/pattern_generation.hpp | 80 +++++++++++++++---- include/mockturtle/algorithms/simulation.hpp | 1 + include/mockturtle/io/write_patterns.hpp | 14 +++- 4 files changed, 75 insertions(+), 22 deletions(-) diff --git a/experiments/pattern_generation.cpp b/experiments/pattern_generation.cpp index a7e5ffd9b..cf2872cac 100644 --- a/experiments/pattern_generation.cpp +++ b/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 ) ); diff --git a/include/mockturtle/algorithms/pattern_generation.hpp b/include/mockturtle/algorithms/pattern_generation.hpp index 447409e37..0cace0fec 100644 --- a/include/mockturtle/algorithms/pattern_generation.hpp +++ b/include/mockturtle/algorithms/pattern_generation.hpp @@ -111,7 +111,7 @@ struct pattern_generation_stats namespace detail { -template +template class patgen_impl { public: @@ -119,7 +119,7 @@ class patgen_impl using signal = typename Ntk::signal; using TT = unordered_node_map; - 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 ) { @@ -136,6 +136,14 @@ class patgen_impl if ( ps.num_stuck_at > 0 ) { stuck_at_check(); + if constexpr( std::is_same_v ) + { + sim.pack_bits(); + call_with_stopwatch( st.time_sim, [&]() { + tts.reset(); + simulate_nodes( ntk, tts, sim, true ); + } ); + } if ( ps.substitute_const ) { for ( auto n : const_nodes ) @@ -226,7 +234,7 @@ class patgen_impl } } - new_pattern( validator.cex ); + new_pattern( validator.cex, n ); if ( ps.num_stuck_at > 1 ) { @@ -236,7 +244,7 @@ class patgen_impl } ); for ( auto& pattern : generated ) { - new_pattern( pattern ); + new_pattern( pattern, n ); } } @@ -311,7 +319,7 @@ class patgen_impl { if ( !( *res ) ) { - new_pattern( validator.cex ); + new_pattern( validator.cex, n ); ++st.unobservable_type2; if ( ps.verbose ) @@ -348,7 +356,7 @@ class patgen_impl { if ( !( *res ) ) { - new_pattern( validator.cex ); + new_pattern( validator.cex, n ); ++st.unobservable_type2; if ( ps.verbose ) @@ -376,9 +384,18 @@ class patgen_impl } private: - void new_pattern( std::vector const& pattern ) + void new_pattern( std::vector const& pattern, node const& n ) { - sim.add_pattern( pattern ); + if constexpr( std::is_same_v ) + { + sim.add_pattern( pattern, compute_support( n ) ); + } + else + { + (void)n; + sim.add_pattern( pattern ); + } + ++st.num_generated_patterns; /* re-simulate */ @@ -411,11 +428,38 @@ class patgen_impl } ); for ( auto& pattern : generated ) { - new_pattern( pattern ); + new_pattern( pattern, n ); } zero = sim.compute_constant( false ); } + std::vector compute_support( node const& n ) + { + ntk.incr_trav_id(); + ntk.set_visited( n, ntk.trav_id() ); + mark_support_rec( n ); + + std::vector 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 ) + { + ntk.foreach_fanin( n, [&]( auto const& f ) { + if ( ntk.visited( ntk.get_node( f ) ) == ntk.trav_id() ) + { return true; } + ntk.set_visited( ntk.get_node( f ), ntk.trav_id() ); + mark_support_rec( ntk.get_node( f ) ); + return true; + }); + } + private: Ntk& ntk; @@ -428,7 +472,7 @@ class patgen_impl TT tts; std::vector const_nodes; - partial_simulator& sim; + Simulator& sim; }; } /* namespace detail */ @@ -441,22 +485,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 -void pattern_generation( Ntk& ntk, partial_simulator& sim, pattern_generation_params const& ps = {}, pattern_generation_stats* pst = nullptr ) +template +void pattern_generation( Ntk& ntk, Simulator& sim, pattern_generation_params const& ps = {}, pattern_generation_stats* pst = nullptr ) { static_assert( is_network_type_v, "Ntk is not a network type" ); static_assert( has_foreach_gate_v, "Ntk does not implement the foreach_gate method" ); static_assert( has_get_node_v, "Ntk does not implement the get_node method" ); static_assert( has_is_complemented_v, "Ntk does not implement the is_complemented method" ); static_assert( has_make_signal_v, "Ntk does not implement the make_signal method" ); + static_assert( std::is_same_v || std::is_same_v, "Simulator should be either partial_simulator or bit_packed_simulator" ); pattern_generation_stats st; validator_params vps; @@ -469,7 +515,7 @@ void pattern_generation( Ntk& ntk, partial_simulator& sim, pattern_generation_pa using fanout_view_t = fanout_view; fanout_view_t fanout_view{ntk}; - detail::patgen_impl p( fanout_view, sim, ps, vps, st ); + detail::patgen_impl p( fanout_view, sim, ps, vps, st ); p.run(); } else diff --git a/include/mockturtle/algorithms/simulation.hpp b/include/mockturtle/algorithms/simulation.hpp index 21bbf47e0..ea2b8a2f3 100644 --- a/include/mockturtle/algorithms/simulation.hpp +++ b/include/mockturtle/algorithms/simulation.hpp @@ -379,6 +379,7 @@ class bit_packed_simulator : public partial_simulator { move_pattern( p, pos + ( block << 6 ) ); empty_slots.emplace_back( p ); + break; } } } diff --git a/include/mockturtle/io/write_patterns.hpp b/include/mockturtle/io/write_patterns.hpp index 83774b566..9a6c6d9ab 100644 --- a/include/mockturtle/io/write_patterns.hpp +++ b/include/mockturtle/io/write_patterns.hpp @@ -50,11 +50,14 @@ namespace mockturtle * The output contains `num_pis()` lines, each line contains a stream of * simulation values of a primary input, represented in hexadecimal. * - * \param sim The `partial_simulator` object containing simulation patterns + * \param sim The `partial_simulator` or `bit_packed_simulator` object containing simulation patterns * \param out Output stream */ -inline void write_patterns( partial_simulator const& sim, std::ostream& out = std::cout ) +template +void write_patterns( Simulator const& sim, std::ostream& out = std::cout ) { + static_assert( std::is_same_v || std::is_same_v, "This function is specialized for partial_simulator or bit_packed_simulator" ); + auto const& patterns = sim.get_patterns(); for ( auto i = 0u; i < patterns.size(); ++i ) { @@ -67,11 +70,14 @@ inline void write_patterns( partial_simulator const& sim, std::ostream& out = st * The output contains `num_pis()` lines, each line contains a stream of * simulation values of a primary input, represented in hexadecimal. * - * \param sim The `partial_simulator` object containing simulation patterns + * \param sim The `partial_simulator` or `bit_packed_simulator` object containing simulation patterns * \param filename Filename */ -inline void write_patterns( partial_simulator const& sim, std::string const& filename ) +template +void write_patterns( Simulator const& sim, std::string const& filename ) { + static_assert( std::is_same_v || std::is_same_v, "This function is specialized for partial_simulator or bit_packed_simulator" ); + std::ofstream os( filename.c_str(), std::ofstream::out ); write_patterns( sim, os ); os.close(); From f71c7b1fde73413cdb7aaf3c85d2e4e79f9dd312 Mon Sep 17 00:00:00 2001 From: Sonia Date: Tue, 4 Aug 2020 12:32:29 +0200 Subject: [PATCH 13/22] support computation with ODC window --- .../algorithms/pattern_generation.hpp | 52 ++++++++++++++++++- 1 file changed, 51 insertions(+), 1 deletion(-) diff --git a/include/mockturtle/algorithms/pattern_generation.hpp b/include/mockturtle/algorithms/pattern_generation.hpp index 0cace0fec..e5d1339bf 100644 --- a/include/mockturtle/algorithms/pattern_generation.hpp +++ b/include/mockturtle/algorithms/pattern_generation.hpp @@ -159,6 +159,14 @@ class patgen_impl if constexpr ( use_odc ) { observability_check(); + if constexpr( std::is_same_v ) + { + sim.pack_bits(); + call_with_stopwatch( st.time_sim, [&]() { + tts.reset(); + simulate_nodes( ntk, tts, sim, true ); + } ); + } } } @@ -435,8 +443,28 @@ class patgen_impl std::vector compute_support( node const& n ) { + if constexpr ( use_odc ) + { + if ( ps.odc_levels != 0 ) + { + std::vector leaves; + ntk.incr_trav_id(); + 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 ) ); + } + }); + + for ( auto& l : leaves ) + { + ntk.incr_trav_id(); + mark_support_rec( l ); + } + } + } ntk.incr_trav_id(); - ntk.set_visited( n, ntk.trav_id() ); mark_support_rec( n ); std::vector care( ntk.num_pis(), false ); @@ -451,6 +479,10 @@ class patgen_impl 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; } @@ -460,6 +492,24 @@ class patgen_impl }); } + void mark_fanout_leaves_rec( node const& n, int level, std::vector& 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; From f76f624dde07dc12984460610b24e0c6cba8edf3 Mon Sep 17 00:00:00 2001 From: Sonia Date: Mon, 10 Aug 2020 12:12:47 +0200 Subject: [PATCH 14/22] debug support computation --- include/mockturtle/algorithms/pattern_generation.hpp | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/include/mockturtle/algorithms/pattern_generation.hpp b/include/mockturtle/algorithms/pattern_generation.hpp index e5d1339bf..bf0af0c61 100644 --- a/include/mockturtle/algorithms/pattern_generation.hpp +++ b/include/mockturtle/algorithms/pattern_generation.hpp @@ -443,12 +443,12 @@ class patgen_impl std::vector compute_support( node const& n ) { + ntk.incr_trav_id(); if constexpr ( use_odc ) { if ( ps.odc_levels != 0 ) { std::vector leaves; - ntk.incr_trav_id(); mark_fanout_leaves_rec( n, 1, leaves ); ntk.foreach_po( [&]( auto const& f ) { if ( ntk.visited( ntk.get_node( f ) ) == ntk.trav_id() ) @@ -457,14 +457,13 @@ class patgen_impl } }); + ntk.incr_trav_id(); for ( auto& l : leaves ) { - ntk.incr_trav_id(); mark_support_rec( l ); } } } - ntk.incr_trav_id(); mark_support_rec( n ); std::vector care( ntk.num_pis(), false ); @@ -486,7 +485,6 @@ class patgen_impl ntk.foreach_fanin( n, [&]( auto const& f ) { if ( ntk.visited( ntk.get_node( f ) ) == ntk.trav_id() ) { return true; } - ntk.set_visited( ntk.get_node( f ), ntk.trav_id() ); mark_support_rec( ntk.get_node( f ) ); return true; }); From 88e97b513f5ada1eff7b17f90a8a00f7f7cbb0ff Mon Sep 17 00:00:00 2001 From: Sonia Date: Mon, 10 Aug 2020 12:33:05 +0200 Subject: [PATCH 15/22] try to not run test for bit packing on windows platform --- test/algorithms/simulation.cpp | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/test/algorithms/simulation.cpp b/test/algorithms/simulation.cpp index c835fc75e..e4c4b298f 100644 --- a/test/algorithms/simulation.cpp +++ b/test/algorithms/simulation.cpp @@ -194,6 +194,8 @@ TEST_CASE( "Incremental simulation with partial_simulator", "[simulation]" ) TEST_CASE( "Bit packing", "[simulation]" ) { +#if defined(WIN32) || defined(__WIN32__) || defined(_WIN32) || defined(_MSC_VER) || defined(__MINGW32__) +#else std::vector pats( 5 ); pats[0].add_bits( 0x1, 2 ); /* x0 = 01 */ pats[1].add_bits( 0x1, 2 ); /* x1 = 01 */ @@ -253,4 +255,5 @@ TEST_CASE( "Bit packing", "[simulation]" ) CHECK( ( sim.compute_pi( 2 )._bits[0] & 0x0f ) == 0x0d ); /* x2 = xxx1101 -> x1101 */ CHECK( ( sim.compute_pi( 3 )._bits[0] & 0x0f ) == 0x0d ); /* x3 = xx1x101 -> x1101 */ CHECK( ( sim.compute_pi( 4 )._bits[0] & 0x1f ) == 0x1d ); /* x4 = x1x1101 -> 11101 */ -} \ No newline at end of file +#endif +} From 5d620f2e2cd610f54014036af702f0db84539eb1 Mon Sep 17 00:00:00 2001 From: Sonia Date: Mon, 10 Aug 2020 12:52:30 +0200 Subject: [PATCH 16/22] add debug messages --- include/mockturtle/algorithms/simulation.hpp | 5 +++++ test/algorithms/simulation.cpp | 3 --- 2 files changed, 5 insertions(+), 3 deletions(-) diff --git a/include/mockturtle/algorithms/simulation.hpp b/include/mockturtle/algorithms/simulation.hpp index ea2b8a2f3..f5acee922 100644 --- a/include/mockturtle/algorithms/simulation.hpp +++ b/include/mockturtle/algorithms/simulation.hpp @@ -357,6 +357,7 @@ class bit_packed_simulator : public partial_simulator */ bool pack_bits() { + std::cout<<"[i] bit packing...\n"; if ( num_patterns == 0u ) { return false; } if ( num_patterns == packed_patterns ) { return false; } assert( num_patterns > packed_patterns ); @@ -384,6 +385,7 @@ class bit_packed_simulator : public partial_simulator } } + std::cout<<"[i] removing "< 0u ) { /* fill the empty slots (from smaller values; `empty_slots` should be reversely sorted) */ @@ -391,12 +393,15 @@ class bit_packed_simulator : public partial_simulator int j = 0; for ( int i = empty_slots.size() - 1; i >= 0; --i ) { + std::cout<<" [i] i = "<= num_patterns - 1 && j <= i ) { if ( empty_slots[j] == num_patterns - 1 ) { --num_patterns; } ++j; + std::cout<<" [i] ... j = "< i ) { break; } + std::cout<<" [i] move from "< pats( 5 ); pats[0].add_bits( 0x1, 2 ); /* x0 = 01 */ pats[1].add_bits( 0x1, 2 ); /* x1 = 01 */ @@ -255,5 +253,4 @@ TEST_CASE( "Bit packing", "[simulation]" ) CHECK( ( sim.compute_pi( 2 )._bits[0] & 0x0f ) == 0x0d ); /* x2 = xxx1101 -> x1101 */ CHECK( ( sim.compute_pi( 3 )._bits[0] & 0x0f ) == 0x0d ); /* x3 = xx1x101 -> x1101 */ CHECK( ( sim.compute_pi( 4 )._bits[0] & 0x1f ) == 0x1d ); /* x4 = x1x1101 -> 11101 */ -#endif } From e2846fda25b61b9e37d624418f82a2e3deb54d82 Mon Sep 17 00:00:00 2001 From: Sonia Date: Mon, 10 Aug 2020 13:19:58 +0200 Subject: [PATCH 17/22] add more debug messages --- include/mockturtle/algorithms/simulation.hpp | 3 +++ 1 file changed, 3 insertions(+) diff --git a/include/mockturtle/algorithms/simulation.hpp b/include/mockturtle/algorithms/simulation.hpp index f5acee922..94e46458f 100644 --- a/include/mockturtle/algorithms/simulation.hpp +++ b/include/mockturtle/algorithms/simulation.hpp @@ -340,6 +340,7 @@ class bit_packed_simulator : public partial_simulator */ void add_pattern( std::vector const& pattern, std::vector const& care_bits ) { + std::cout<<"[i] add pattern...\n"; assert( pattern.size() == care_bits.size() ); assert( pattern.size() == patterns.size() ); @@ -412,9 +413,11 @@ class bit_packed_simulator : public partial_simulator patterns[i].resize( num_patterns ); care[i].resize( num_patterns ); } + std::cout<<"[i] bit packing finished...\n"; packed_patterns = num_patterns; return true; } + std::cout<<"[i] bit packing finished...\n"; packed_patterns = num_patterns; return false; } From 1be254fd34f61c1b99cb1bd449109ec0841861c5 Mon Sep 17 00:00:00 2001 From: Sonia Date: Mon, 10 Aug 2020 13:44:23 +0200 Subject: [PATCH 18/22] more messages --- include/mockturtle/algorithms/simulation.hpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/include/mockturtle/algorithms/simulation.hpp b/include/mockturtle/algorithms/simulation.hpp index 94e46458f..2a9ced919 100644 --- a/include/mockturtle/algorithms/simulation.hpp +++ b/include/mockturtle/algorithms/simulation.hpp @@ -399,14 +399,14 @@ class bit_packed_simulator : public partial_simulator { if ( empty_slots[j] == num_patterns - 1 ) { --num_patterns; } ++j; - std::cout<<" [i] ... j = "<= num_patterns - 1 && j <= i)<< "\n"; } if ( j > i ) { break; } std::cout<<" [i] move from "< Date: Mon, 10 Aug 2020 14:01:58 +0200 Subject: [PATCH 19/22] debug & remove cout --- include/mockturtle/algorithms/simulation.hpp | 10 +--------- 1 file changed, 1 insertion(+), 9 deletions(-) diff --git a/include/mockturtle/algorithms/simulation.hpp b/include/mockturtle/algorithms/simulation.hpp index 2a9ced919..19db8c79d 100644 --- a/include/mockturtle/algorithms/simulation.hpp +++ b/include/mockturtle/algorithms/simulation.hpp @@ -340,7 +340,6 @@ class bit_packed_simulator : public partial_simulator */ void add_pattern( std::vector const& pattern, std::vector const& care_bits ) { - std::cout<<"[i] add pattern...\n"; assert( pattern.size() == care_bits.size() ); assert( pattern.size() == patterns.size() ); @@ -358,7 +357,6 @@ class bit_packed_simulator : public partial_simulator */ bool pack_bits() { - std::cout<<"[i] bit packing...\n"; if ( num_patterns == 0u ) { return false; } if ( num_patterns == packed_patterns ) { return false; } assert( num_patterns > packed_patterns ); @@ -386,7 +384,6 @@ class bit_packed_simulator : public partial_simulator } } - std::cout<<"[i] removing "< 0u ) { /* fill the empty slots (from smaller values; `empty_slots` should be reversely sorted) */ @@ -394,30 +391,25 @@ class bit_packed_simulator : public partial_simulator int j = 0; for ( int i = empty_slots.size() - 1; i >= 0; --i ) { - std::cout<<" [i] i = "<= num_patterns - 1 && j <= i ) { if ( empty_slots[j] == num_patterns - 1 ) { --num_patterns; } ++j; - std::cout<<" [i] ... j = "<= num_patterns - 1 && j <= i)<< "\n"; + if ( j == empty_slots.size() ) { break; } } if ( j > i ) { break; } - std::cout<<" [i] move from "< Date: Thu, 20 Aug 2020 22:44:01 +0200 Subject: [PATCH 20/22] add min invoke times in circuit_validator --- .../mockturtle/algorithms/circuit_validator.hpp | 17 +++++++++++------ 1 file changed, 11 insertions(+), 6 deletions(-) diff --git a/include/mockturtle/algorithms/circuit_validator.hpp b/include/mockturtle/algorithms/circuit_validator.hpp index 42f24aada..a5e771d21 100644 --- a/include/mockturtle/algorithms/circuit_validator.hpp +++ b/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 is not a network type" ); static_assert( has_foreach_fanin_v, "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 solve( std::vector 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 literals; bill::solver solver; + static const uint32_t MIN_NUM_INVOKE = 20u; + uint32_t num_invoke; + bool between_push_pop = false; std::vector tmp; From 2c5afad7070ed2e25de588ebe051bf2f93aabb01 Mon Sep 17 00:00:00 2001 From: Sonia Date: Thu, 20 Aug 2020 22:45:26 +0200 Subject: [PATCH 21/22] fix warning --- include/mockturtle/algorithms/simulation.hpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/include/mockturtle/algorithms/simulation.hpp b/include/mockturtle/algorithms/simulation.hpp index 19db8c79d..9af0b2822 100644 --- a/include/mockturtle/algorithms/simulation.hpp +++ b/include/mockturtle/algorithms/simulation.hpp @@ -395,7 +395,7 @@ class bit_packed_simulator : public partial_simulator { if ( empty_slots[j] == num_patterns - 1 ) { --num_patterns; } ++j; - if ( j == empty_slots.size() ) { break; } + if ( j == (int)empty_slots.size() ) { break; } } if ( j > i ) { break; } move_pattern( num_patterns - 1, empty_slots[i] ); From c56773f9416ad863364425163e29a15bc03f4d9c Mon Sep 17 00:00:00 2001 From: Sonia Date: Mon, 24 Aug 2020 10:56:57 +0200 Subject: [PATCH 22/22] typo in verbose report --- include/mockturtle/algorithms/sim_resub.hpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/include/mockturtle/algorithms/sim_resub.hpp b/include/mockturtle/algorithms/sim_resub.hpp index e078cf004..d57b8e241 100644 --- a/include/mockturtle/algorithms/sim_resub.hpp +++ b/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 } };