diff --git a/docs/algorithms/pattern_generation.rst b/docs/algorithms/pattern_generation.rst new file mode 100644 index 000000000..aabbd4c77 --- /dev/null +++ b/docs/algorithms/pattern_generation.rst @@ -0,0 +1,38 @@ +Expressive simulation pattern generation +---------------------------------------- + +**Header:** ``mockturtle/algorithms/pattern_generation.hpp`` + +The following example shows how to generate expressive simulation patterns +for an AIG network. It starts with 256 random patterns, generates stuck-at +patterns to make every node's signature has at least 3 bits of 0 and 3 bits +of 1 which are observable at at least 5 levels of fan-out. The generated +patterns are then written out to a file. + +.. code-block:: c++ + + /* derive some AIG */ + aig_network aig = ...; + + pattern_generation_params ps; + ps.num_stuck_at = 3; + ps.odc_levels = 5; + + partial_simulator sim( aig.num_pis(), 256 ); + pattern_generation( aig, sim, ps ); + write_patterns( sim, "patterns.pat" ); + + +Parameters and statistics +~~~~~~~~~~~~~~~~~~~~~~~~~ + +.. doxygenstruct:: mockturtle::pattern_generation_params + :members: + +.. doxygenstruct:: mockturtle::pattern_generation_stats + :members: + +Algorithm +~~~~~~~~~ + +.. doxygenfunction:: mockturtle::pattern_generation diff --git a/docs/algorithms/simulation.rst b/docs/algorithms/simulation.rst index 2e0f340d7..88b6e6333 100644 --- a/docs/algorithms/simulation.rst +++ b/docs/algorithms/simulation.rst @@ -90,7 +90,7 @@ Note that currently only AIG and XAG are supported. .. doxygenfunction:: mockturtle::partial_simulator::num_bits() -.. doxygenfunction:: mockturtle::partial_simulator::write_patterns( const std::string& ) +.. doxygenfunction:: mockturtle::partial_simulator::get_patterns() .. doxygenfunction:: mockturtle::simulate_nodes( Ntk const&, unordered_node_map&, partial_simulator const&, bool ) diff --git a/docs/index.rst b/docs/index.rst index 128417df1..d582a1a15 100644 --- a/docs/index.rst +++ b/docs/index.rst @@ -53,6 +53,7 @@ Welcome to mockturtle's documentation! algorithms/xmg_optimization algorithms/equivalence_classes algorithms/circuit_validator + algorithms/pattern_generation .. toctree:: :maxdepth: 2 diff --git a/docs/io/writers.rst b/docs/io/writers.rst index 59193838b..f7a069054 100644 --- a/docs/io/writers.rst +++ b/docs/io/writers.rst @@ -36,3 +36,12 @@ Write into DOT files (Graphviz) .. doxygenfunction:: mockturtle::write_dot(Ntk const&, std::string const&, Drawer const&) .. doxygenfunction:: mockturtle::write_dot(Ntk const&, std::ostream&, Drawer const&) + +Write simulation patterns into file +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +**Header:** ``mockturtle/io/write_patterns.hpp`` + +.. doxygenfunction:: mockturtle::write_patterns(partial_simulator const&, std::string const&) + +.. doxygenfunction:: mockturtle::write_patterns(partial_simulator const&, std::ostream&) \ No newline at end of file diff --git a/experiments/pattern_generation.cpp b/experiments/pattern_generation.cpp new file mode 100644 index 000000000..a7e5ffd9b --- /dev/null +++ b/experiments/pattern_generation.cpp @@ -0,0 +1,67 @@ +/* mockturtle: C++ logic network library + * Copyright (C) 2018-2020 EPFL + * + * Permission is hereby granted, free of charge, to any person + * obtaining a copy of this software and associated documentation + * files (the "Software"), to deal in the Software without + * restriction, including without limitation the rights to use, + * copy, modify, merge, publish, distribute, sublicense, and/or sell + * copies of the Software, and to permit persons to whom the + * Software is furnished to do so, subject to the following + * conditions: + * + * The above copyright notice and this permission notice shall be + * included in all copies or substantial portions of the Software. + * + * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, + * EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES + * OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND + * NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT + * HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, + * WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING + * FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR + * OTHER DEALINGS IN THE SOFTWARE. + */ + +#include +#include + +#include +#include +#include +#include +#include +#include +#include + +#include + +int main() +{ + using namespace experiments; + using namespace mockturtle; + + experiment exp( "pattern_generation", "benchmark", "#PI", "size", "#pat", "#pat gen", "#const", "t_total", "t_sim", "t_SAT" ); + + for ( auto const& benchmark : epfl_benchmarks() ) + { + fmt::print( "[i] processing {}\n", benchmark ); + aig_network aig; + lorina::read_aiger( benchmark_path( benchmark ), aiger_reader( aig ) ); + auto size_before = aig.num_gates(); + + pattern_generation_params ps; + pattern_generation_stats st; + + uint32_t num_random_pattern = 1000; + partial_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 ) ); + } + + exp.save(); + exp.table(); + + return 0; +} diff --git a/experiments/pattern_generation.json b/experiments/pattern_generation.json new file mode 100644 index 000000000..e409371fc --- /dev/null +++ b/experiments/pattern_generation.json @@ -0,0 +1,227 @@ +[ + { + "entries": [ + { + "#PI": 256, + "#const": 0, + "#pat": 1000, + "#pat gen": 0, + "benchmark": "adder", + "size": 1020, + "t_SAT": 0.0, + "t_sim": 0.002587138907983899, + "t_total": 0.0027476809918880463 + }, + { + "#PI": 135, + "#const": 0, + "#pat": 1000, + "#pat gen": 0, + "benchmark": "bar", + "size": 3336, + "t_SAT": 0.0, + "t_sim": 0.011206761002540588, + "t_total": 0.012046649120748043 + }, + { + "#PI": 128, + "#const": 8, + "#pat": 1039, + "#pat gen": 39, + "benchmark": "div", + "size": 57247, + "t_SAT": 0.23106683790683746, + "t_sim": 0.3988635838031769, + "t_total": 0.6502119302749634 + }, + { + "#PI": 256, + "#const": 2, + "#pat": 1003, + "#pat gen": 3, + "benchmark": "hyp", + "size": 214335, + "t_SAT": 0.00014847799320705235, + "t_sim": 0.6856793761253357, + "t_total": 0.7315340042114258 + }, + { + "#PI": 32, + "#const": 162, + "#pat": 1093, + "#pat gen": 93, + "benchmark": "log2", + "size": 32060, + "t_SAT": 23.7200870513916, + "t_sim": 0.4002784192562103, + "t_total": 24.13776969909668 + }, + { + "#PI": 512, + "#const": 0, + "#pat": 1000, + "#pat gen": 0, + "benchmark": "max", + "size": 2865, + "t_SAT": 0.0, + "t_sim": 0.006821795832365751, + "t_total": 0.007972832769155502 + }, + { + "#PI": 128, + "#const": 0, + "#pat": 1008, + "#pat gen": 8, + "benchmark": "multiplier", + "size": 27062, + "t_SAT": 0.0003024929901584983, + "t_sim": 0.12204926460981369, + "t_total": 0.13171681761741638 + }, + { + "#PI": 24, + "#const": 19, + "#pat": 1049, + "#pat gen": 49, + "benchmark": "sin", + "size": 5416, + "t_SAT": 0.7237713932991028, + "t_sim": 0.06233770772814751, + "t_total": 0.788311243057251 + }, + { + "#PI": 128, + "#const": 0, + "#pat": 1000, + "#pat gen": 0, + "benchmark": "sqrt", + "size": 24618, + "t_SAT": 0.0, + "t_sim": 0.04817450791597366, + "t_total": 0.05268986523151398 + }, + { + "#PI": 64, + "#const": 0, + "#pat": 1003, + "#pat gen": 3, + "benchmark": "square", + "size": 18484, + "t_SAT": 6.385899905581027e-05, + "t_sim": 0.060539085417985916, + "t_total": 0.06628058850765228 + }, + { + "#PI": 256, + "#const": 0, + "#pat": 1005, + "#pat gen": 5, + "benchmark": "arbiter", + "size": 11839, + "t_SAT": 0.00031487300293520093, + "t_sim": 0.027791135013103485, + "t_total": 0.02998867630958557 + }, + { + "#PI": 10, + "#const": 0, + "#pat": 1007, + "#pat gen": 7, + "benchmark": "cavlc", + "size": 693, + "t_SAT": 0.0001512260059826076, + "t_sim": 0.0024142060428857803, + "t_total": 0.0027767519932240248 + }, + { + "#PI": 7, + "#const": 0, + "#pat": 1008, + "#pat gen": 8, + "benchmark": "ctrl", + "size": 174, + "t_SAT": 0.00011831099982373416, + "t_sim": 0.0005374409956857562, + "t_total": 0.0007138170185498893 + }, + { + "#PI": 8, + "#const": 0, + "#pat": 1206, + "#pat gen": 206, + "benchmark": "dec", + "size": 304, + "t_SAT": 0.003572395071387291, + "t_sim": 0.004423268139362335, + "t_total": 0.008258773013949394 + }, + { + "#PI": 147, + "#const": 0, + "#pat": 1039, + "#pat gen": 39, + "benchmark": "i2c", + "size": 1342, + "t_SAT": 0.0019028210081160069, + "t_sim": 0.007990111596882343, + "t_total": 0.010547489859163761 + }, + { + "#PI": 11, + "#const": 0, + "#pat": 1003, + "#pat gen": 3, + "benchmark": "int2float", + "size": 260, + "t_SAT": 0.00011678999726427719, + "t_sim": 0.0013045240193605423, + "t_total": 0.0015592729905620217 + }, + { + "#PI": 1204, + "#const": 1, + "#pat": 1406, + "#pat gen": 406, + "benchmark": "mem_ctrl", + "size": 46836, + "t_SAT": 0.12108956277370453, + "t_sim": 0.6603772640228271, + "t_total": 0.8064870834350586 + }, + { + "#PI": 128, + "#const": 0, + "#pat": 1001, + "#pat gen": 1, + "benchmark": "priority", + "size": 978, + "t_SAT": 5.066599987912923e-05, + "t_sim": 0.001871931948699057, + "t_total": 0.002103254897519946 + }, + { + "#PI": 60, + "#const": 0, + "#pat": 1046, + "#pat gen": 46, + "benchmark": "router", + "size": 257, + "t_SAT": 0.0015393260400742292, + "t_sim": 0.004502872005105019, + "t_total": 0.006205921061336994 + }, + { + "#PI": 1001, + "#const": 4, + "#pat": 1009, + "#pat gen": 9, + "benchmark": "voter", + "size": 13758, + "t_SAT": 1.8260704278945923, + "t_sim": 0.14073464274406433, + "t_total": 1.9711337089538574 + } + ], + "version": "b8503a5" + } +] diff --git a/include/mockturtle/algorithms/circuit_validator.hpp b/include/mockturtle/algorithms/circuit_validator.hpp index 835f26691..5205c2e52 100644 --- a/include/mockturtle/algorithms/circuit_validator.hpp +++ b/include/mockturtle/algorithms/circuit_validator.hpp @@ -215,7 +215,7 @@ class circuit_validator if constexpr ( use_pushpop ) { - solver.push(); + push(); } for ( auto g : circuit ) @@ -227,7 +227,7 @@ class circuit_validator if constexpr ( use_pushpop ) { - solver.pop(); + pop(); } if ( solver.num_clauses() > ps.max_clauses ) @@ -259,12 +259,12 @@ class circuit_validator { if constexpr ( use_pushpop ) { - solver.push(); + push(); } res = solve( {build_odc_window( root, ~literals[root] ), lit_not_cond( literals[root], value )} ); if constexpr ( use_pushpop ) { - solver.pop(); + pop(); } } else @@ -308,7 +308,7 @@ class circuit_validator construct( root ); } - solver.push(); + push(); for ( auto const& pattern : block_patterns ) { @@ -341,7 +341,7 @@ class circuit_validator } } - solver.pop(); + pop(); if ( solver.num_clauses() > ps.max_clauses ) { restart(); @@ -388,6 +388,13 @@ class circuit_validator void construct( node const& n ) { assert( !literals.has( n ) ); + if constexpr ( use_pushpop ) + { + if ( between_push_pop ) + { + tmp.emplace_back( n ); + } + } std::vector child_lits; ntk.foreach_fanin( n, [&]( auto const& f ) { @@ -425,6 +432,23 @@ class circuit_validator } } + void push() + { + solver.push(); + between_push_pop = true; + tmp.clear(); + } + + void pop() + { + solver.pop(); + for ( auto& n : tmp ) + { + literals.erase( n ); + } + between_push_pop = false; + } + bill::lit_type add_clauses_for_2input_gate( bill::lit_type a, bill::lit_type b, std::optional c = std::nullopt, gate_type type = AND ) { assert( type == AND || type == XOR ); @@ -521,12 +545,12 @@ class circuit_validator { if constexpr ( use_pushpop ) { - solver.push(); + push(); } res = solve( {build_odc_window( root, lit )} ); if constexpr ( use_pushpop ) { - solver.pop(); + pop(); } } else @@ -632,6 +656,11 @@ class circuit_validator return true; /* skip */ ntk.set_visited( fo, ntk.trav_id() ); + if ( !literals.has( fo ) ) + { + construct( fo ); + } + lits[fo] = bill::lit_type( solver.add_variable(), bill::lit_type::polarities::positive ); if ( level == ps.odc_levels ) @@ -648,6 +677,7 @@ class circuit_validator template> void add_miter_clauses( node const& n, unordered_node_map const& lits, std::vector& miter ) { + assert( literals.has( n ) && literals[n] != literals[ntk.get_constant( false )] ); miter.emplace_back( add_clauses_for_2input_gate( literals[n], lits[n], std::nullopt, XOR ) ); } @@ -659,6 +689,9 @@ class circuit_validator unordered_node_map literals; bill::solver solver; + bool between_push_pop = false; + std::vector tmp; + public: std::vector cex; }; diff --git a/include/mockturtle/algorithms/dont_cares.hpp b/include/mockturtle/algorithms/dont_cares.hpp index 438418477..3d2857cac 100644 --- a/include/mockturtle/algorithms/dont_cares.hpp +++ b/include/mockturtle/algorithms/dont_cares.hpp @@ -126,6 +126,123 @@ kitty::dynamic_truth_table observability_dont_cares( Ntk const& ntk, node c return ~care; } +namespace detail { + +template +void clearTFO_rec( Ntk const& ntk, unordered_node_map& ttsNOT, node const& n, std::vector>& roots, int level ) +{ + if ( ntk.visited( n ) == ntk.trav_id() ) /* visited */ + { + return; + } + ntk.set_visited( n, ntk.trav_id() ); + + ttsNOT.erase( n ); + + if ( level == 0 ) + { + roots.emplace_back( n ); + return; + } + + ntk.foreach_fanout( n, [&]( auto const& fo ){ + clearTFO_rec( ntk, ttsNOT, fo, roots, level - 1 ); + }); +} + +template +void simulate_TFO_rec( Ntk const& ntk, node const& n, partial_simulator const& sim, unordered_node_map& tts, int level ) +{ + if ( ntk.visited( n ) == ntk.trav_id() ) /* visited */ + { + return; + } + ntk.set_visited( n, ntk.trav_id() ); + + if ( !tts.has( n ) || tts[n].num_bits() != sim.num_bits() ) + { + simulate_node( ntk, n, tts, sim ); + } + + ntk.foreach_fanout( n, [&]( auto const& fo ){ + simulate_TFO_rec( ntk, fo, sim, tts, level - 1 ); + }); +} + +} /* namespace detail */ + +/*! \brief Compute the observability don't care patterns in a partial_simulator with respect to a node. + * + * A pattern is unobservable w.r.t. a node `n` if under this input assignment, + * replacing `n` with `!n` does not affect the value of any primary output or + * any leaf node of `levels` levels of transitive fanout cone. + * + * Return value: a `partial_truth_table` with the same length as `sim.num_bits()`. + * A `1` in it corresponds to an unobservable pattern. + * + * \param sim The `partial_simulator` containing the patterns to be tested. + * \param tts Stores the simulation signatures of each node. Can be empty or incomplete. + * \param levels Level of tansitive fanout to consider. -1 = consider until PO. + */ +template +kitty::partial_truth_table observability_dont_cares( Ntk const& ntk, node const& n, partial_simulator const& sim, unordered_node_map& tts, int levels = -1 ) +{ + std::vector> roots( ntk.num_pos() ); + ntk.foreach_po( [&]( auto const& f, auto i ){ roots.at(i) = ntk.get_node( f ); }); + + ntk.incr_trav_id(); + detail::simulate_TFO_rec( ntk, n, sim, tts, levels ); + unordered_node_map ttsNOT = tts.copy(); + + ntk.incr_trav_id(); + detail::clearTFO_rec( ntk, ttsNOT, n, roots, levels ); + ttsNOT[n] = ~tts[n]; + ntk.incr_trav_id(); + detail::simulate_TFO_rec( ntk, n, sim, ttsNOT, levels ); + + kitty::partial_truth_table care( tts[n].num_bits() ); + for ( const auto& r : roots ) + { + if ( tts[r].num_bits() == care.num_bits() ) + { + care |= tts[r] ^ ttsNOT[r]; + } + } + return ~care; +} + +/*! \brief Check if a pattern is observable with respect to a node. + * + * A pattern is unobservable w.r.t. a node `n` if under this input assignment, + * replacing `n` with `!n` does not affect the value of any primary output or + * any leaf node of `levels` levels of transitive fanout cone. + * + * \param levels Level of tansitive fanout to consider. -1 = consider until PO. + */ +template +bool pattern_is_observable( Ntk const& ntk, node const& n, std::vector const& pattern, int levels = -1 ) +{ + std::vector> roots( ntk.num_pos() ); + ntk.foreach_po( [&]( auto const& f, auto i ){ roots.at(i) = ntk.get_node( f ); }); + + default_simulator sim( pattern ); + unordered_node_map tts( ntk ); + simulate_nodes( ntk, tts, sim ); + unordered_node_map ttsNOT = tts.copy(); + + ntk.incr_trav_id(); + detail::clearTFO_rec( ntk, ttsNOT, n, roots, levels ); + ttsNOT[n] = !tts[n]; + simulate_nodes( ntk, ttsNOT, sim ); + + bool care = false; + for ( const auto& r : roots ) + { + care |= tts[r] ^ ttsNOT[r]; + } + return care; +} + /*! \brief SAT-based satisfiability don't cares checker * * Initialize this class with a network and then call `is_dont_care` on a node diff --git a/include/mockturtle/algorithms/pattern_generation.hpp b/include/mockturtle/algorithms/pattern_generation.hpp new file mode 100644 index 000000000..df19f5968 --- /dev/null +++ b/include/mockturtle/algorithms/pattern_generation.hpp @@ -0,0 +1,482 @@ +/* mockturtle: C++ logic network library + * Copyright (C) 2018-2020 EPFL + * + * Permission is hereby granted, free of charge, to any person + * obtaining a copy of this software and associated documentation + * files (the "Software"), to deal in the Software without + * restriction, including without limitation the rights to use, + * copy, modify, merge, publish, distribute, sublicense, and/or sell + * copies of the Software, and to permit persons to whom the + * Software is furnished to do so, subject to the following + * conditions: + * + * The above copyright notice and this permission notice shall be + * included in all copies or substantial portions of the Software. + * + * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, + * EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES + * OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND + * NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT + * HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, + * WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING + * FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR + * OTHER DEALINGS IN THE SOFTWARE. + */ + +/*! + \file pattern_generation.hpp + \brief Expressive Simulation Pattern Generation + + \author Siang-Yun Lee +*/ + +#pragma once + +#include "../utils/progress_bar.hpp" +#include "../utils/stopwatch.hpp" +#include +#include +#include +#include +#include +#include +#include +#include + +namespace mockturtle +{ + +struct pattern_generation_params +{ + /*! \brief Whether to remove constant nodes. Requires `substitute_node`. */ + bool substitute_const{false}; + + /*! \brief Number of patterns each node should have for both values. */ + uint32_t num_stuck_at{1}; + + /*! \brief Whether to consider observability, and how many levels. 0 = no. -1 = Consider TFO until PO. */ + int odc_levels{0}; + + /*! \brief Show progress. */ + bool progress{false}; + + /*! \brief Be verbose. Note that it will take more time to do extra ODC computation if this is turned on. */ + bool verbose{false}; + + /*! \brief Random seed. */ + std::default_random_engine::result_type random_seed{0}; + + /*! \brief Conflict limit of the SAT solver. */ + uint32_t conflict_limit{1000}; + + /*! \brief Maximum number of clauses of the SAT solver. (incremental CNF construction) */ + uint32_t max_clauses{1000}; +}; + +struct pattern_generation_stats +{ + /*! \brief Total time. */ + stopwatch<>::duration time_total{0}; + + /*! \brief Time for simulation. */ + stopwatch<>::duration time_sim{0}; + + /*! \brief Time for SAT solving. */ + stopwatch<>::duration time_sat{0}; + + /*! \brief Time for ODC computation */ + stopwatch<>::duration time_odc{0}; + + /*! \brief Number of constant nodes. */ + uint32_t num_constant{0}; + + /*! \brief Number of generated patterns. */ + uint32_t num_generated_patterns{0}; + + /*! \brief Number of stuck-at patterns that is re-generated because the original one was unobservable. */ + uint32_t unobservable_type1{0}; + + /*! \brief Number of additional patterns generated because the node was unobservable with one value. */ + uint32_t unobservable_type2{0}; + + /*! \brief Number of unobservable nodes (node for which an observable pattern can not be found). */ + uint32_t unobservable_node{0}; +}; + +namespace detail +{ + +template +class patgen_impl +{ +public: + using node = typename Ntk::node; + 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 ) + : ntk( ntk ), ps( ps ), st( st ), vps( vps ), validator( ntk, vps ), + tts( ntk ), sim( sim ) + { + } + + void run() + { + stopwatch t( st.time_total ); + + call_with_stopwatch( st.time_sim, [&]() { + simulate_nodes( ntk, tts, sim ); + } ); + + if ( ps.num_stuck_at > 0 ) + { + stuck_at_check(); + if ( ps.substitute_const ) + { + for ( auto n : const_nodes ) + { + if ( !ntk.is_dead( ntk.get_node( n ) ) ) + { + ntk.substitute_node( ntk.get_node( n ), ntk.get_constant( ntk.is_complemented( n ) ) ); + } + } + } + } + + if constexpr ( use_odc ) + { + observability_check(); + } + } + +private: + void stuck_at_check() + { + progress_bar pbar{ntk.size(), "patgen-sa |{0}| node = {1:>4} #pat = {2:>4}", ps.progress}; + + kitty::partial_truth_table zero = sim.compute_constant( false ); + + ntk.foreach_gate( [&]( auto const& n, auto i ) { + pbar( i, i, sim.num_bits() ); + + if ( tts[n].num_bits() != sim.num_bits() ) + { + call_with_stopwatch( st.time_sim, [&]() { + simulate_node( ntk, n, tts, sim ); + } ); + } + assert( zero.num_bits() == sim.num_bits() ); + + if ( ( tts[n] == zero ) || ( tts[n] == ~zero ) ) + { + bool value = ( tts[n] == zero ); /* wanted value of n */ + + const auto res = call_with_stopwatch( st.time_sat, [&]() { + vps.odc_levels = 0; + return validator.validate( n, !value ); + } ); + if ( !res ) + { + return true; /* timeout, next node */ + } + else if ( !( *res ) ) /* SAT, pattern found */ + { + if constexpr ( use_odc ) + { + /* check if the found pattern is observable */ + bool observable = call_with_stopwatch( st.time_odc, [&]() { + return pattern_is_observable( ntk, n, validator.cex, ps.odc_levels ); + } ); + if ( !observable ) + { + if ( ps.verbose ) + { + std::cout << "\t[i] generated pattern is not observable (type 1). node: " << n << ", with value " << value << "\n"; + } + + const auto res2 = call_with_stopwatch( st.time_sat, [&]() { + vps.odc_levels = ps.odc_levels; + return validator.validate( n, !value ); + } ); + if ( res2 ) + { + if ( !( *res2 ) ) + { + ++st.unobservable_type1; + if ( ps.verbose ) + { + assert( pattern_is_observable( ntk, n, validator.cex, ps.odc_levels ) ); + std::cout << "\t\t[i] unobservable pattern resolved.\n"; + } + } + else + { + ++st.unobservable_node; + if ( ps.verbose ) + { + std::cout << "\t\t[i] unobservable node " << n << "\n"; + } + } + } + } + } + + new_pattern( validator.cex ); + + if ( ps.num_stuck_at > 1 ) + { + auto generated = call_with_stopwatch( st.time_sat, [&]() { + vps.odc_levels = ps.odc_levels; + return validator.generate_pattern( n, value, {validator.cex}, ps.num_stuck_at - 1 ); + } ); + for ( auto& pattern : generated ) + { + new_pattern( pattern ); + } + } + + zero = sim.compute_constant( false ); + } + else /* UNSAT, constant node */ + { + ++st.num_constant; + const_nodes.emplace_back( value ? ntk.make_signal( n ) : !ntk.make_signal( n ) ); + return true; /* next gate */ + } + } + else if ( ps.num_stuck_at > 1 ) + { + auto const& tt = tts[n]; + if ( kitty::count_ones( tt ) < ps.num_stuck_at ) + { + generate_more_patterns( n, tt, true, zero ); + } + else if ( kitty::count_zeros( tt ) < ps.num_stuck_at ) + { + generate_more_patterns( n, tt, false, zero ); + } + } + return true; /* next gate */ + } ); + } + + void observability_check() + { + progress_bar pbar{ntk.size(), "patgen-obs |{0}| node = {1:>4} #pat = {2:>4}", ps.progress}; + + kitty::partial_truth_table zero = sim.compute_constant( false ); + + ntk.foreach_gate( [&]( auto const& n, auto i ) { + pbar( i, i, sim.num_bits() ); + + for ( auto& f : const_nodes ) + { + if ( ntk.get_node( f ) == n ) + { + return true; /* skip constant nodes */ + } + } + + if ( tts[n].num_bits() != sim.num_bits() ) + { + call_with_stopwatch( st.time_sim, [&]() { + simulate_node( ntk, n, tts, sim ); + } ); + } + assert( zero.num_bits() == sim.num_bits() ); + + /* compute ODC */ + auto odc = call_with_stopwatch( st.time_odc, [&]() { + return observability_dont_cares( ntk, n, sim, tts, ps.odc_levels ); + } ); + + /* check if under non-ODCs n is always the same value */ + if ( ( tts[n] & ~odc ) == zero ) + { + if ( ps.verbose ) + { + std::cout << "\t[i] under all observable patterns, node " << n << " is always 0 (type 2).\n"; + } + + const auto res = call_with_stopwatch( st.time_sat, [&]() { + vps.odc_levels = ps.odc_levels; + return validator.validate( n, false ); + } ); + if ( res ) + { + if ( !( *res ) ) + { + new_pattern( validator.cex ); + ++st.unobservable_type2; + + if ( ps.verbose ) + { + auto odc2 = call_with_stopwatch( st.time_odc, [&]() { return observability_dont_cares( ntk, n, sim, tts, ps.odc_levels ); } ); + assert( ( tts[n] & ~odc2 ) != sim.compute_constant( false ) ); + std::cout << "\t\t[i] added generated pattern to resolve unobservability.\n"; + } + + zero = sim.compute_constant( false ); + } + else + { + ++st.unobservable_node; + if ( ps.verbose ) + { + std::cout << "\t\t[i] unobservable node " << n << "\n"; + } + } + } + } + else if ( ( tts[n] | odc ) == ~zero ) + { + if ( ps.verbose ) + { + std::cout << "\t[i] under all observable patterns, node " << n << " is always 1 (type 2).\n"; + } + + const auto res = call_with_stopwatch( st.time_sat, [&]() { + vps.odc_levels = ps.odc_levels; + return validator.validate( n, true ); + } ); + if ( res ) + { + if ( !( *res ) ) + { + new_pattern( validator.cex ); + ++st.unobservable_type2; + + if ( ps.verbose ) + { + auto odc2 = call_with_stopwatch( st.time_odc, [&]() { return observability_dont_cares( ntk, n, sim, tts, ps.odc_levels ); } ); + assert( ( tts[n] | odc2 ) != sim.compute_constant( true ) ); + std::cout << "\t\t[i] added generated pattern to resolve unobservability.\n"; + } + + zero = sim.compute_constant( false ); + } + else + { + ++st.unobservable_node; + if ( ps.verbose ) + { + std::cout << "\t\t[i] unobservable node " << n << "\n"; + } + } + } + } + + return true; /* next gate */ + } ); + } + +private: + void new_pattern( std::vector const& pattern ) + { + sim.add_pattern( pattern ); + ++st.num_generated_patterns; + + /* re-simulate */ + if ( sim.num_bits() % 64 == 0 ) + { + call_with_stopwatch( st.time_sim, [&]() { + simulate_nodes( ntk, tts, sim, false ); + } ); + } + } + + void generate_more_patterns( node const& n, kitty::partial_truth_table const& tt, bool value, kitty::partial_truth_table& zero ) + { + /* collect the `value` patterns */ + std::vector> patterns; + for ( auto i = 0u; i < tt.num_bits(); ++i ) + { + if ( kitty::get_bit( tt, i ) == value ) + { + patterns.emplace_back(); + ntk.foreach_pi( [&]( auto const& pi ) { + patterns.back().emplace_back( kitty::get_bit( tts[pi], i ) ); + } ); + } + } + + auto generated = call_with_stopwatch( st.time_sat, [&]() { + vps.odc_levels = ps.odc_levels; + return validator.generate_pattern( n, value, patterns, ps.num_stuck_at - patterns.size() ); + } ); + for ( auto& pattern : generated ) + { + new_pattern( pattern ); + } + zero = sim.compute_constant( false ); + } + +private: + Ntk& ntk; + + pattern_generation_params const& ps; + pattern_generation_stats& st; + + validator_params& vps; + circuit_validator validator; + + TT tts; + std::vector const_nodes; + + partial_simulator& sim; +}; + +} /* namespace detail */ + +/*! \brief Expressive simulation pattern generation. + * + * This function implements two simulation pattern generation methods: + * stuck-at value checking and observability checking. Please refer to + * [1] for details of the algorithm and its purpose. + * + * [1] Simulation-Guided Boolean Resubstitution. IWLS 2020 / ICCAD 2020. + * + * \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 )`) + * 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 + * 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 ) +{ + 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" ); + + pattern_generation_stats st; + validator_params vps; + vps.conflict_limit = ps.conflict_limit; + vps.max_clauses = ps.max_clauses; + vps.random_seed = ps.random_seed; + + if ( ps.odc_levels != 0 ) + { + using fanout_view_t = fanout_view; + fanout_view_t fanout_view{ntk}; + + detail::patgen_impl p( fanout_view, sim, ps, vps, st ); + p.run(); + } + else + { + detail::patgen_impl p( ntk, sim, ps, vps, st ); + p.run(); + } + + if ( pst ) + { + *pst = st; + } +} + +} /* namespace mockturtle */ diff --git a/include/mockturtle/algorithms/simulation.hpp b/include/mockturtle/algorithms/simulation.hpp index 9dad2e2a6..65a8643ab 100644 --- a/include/mockturtle/algorithms/simulation.hpp +++ b/include/mockturtle/algorithms/simulation.hpp @@ -45,7 +45,6 @@ #include #include #include -#include #include namespace mockturtle @@ -266,15 +265,14 @@ class partial_simulator ++num_patterns; } - /*! \brief Writes the simulation patterns into a file. */ - void write_patterns( const std::string& filename ) + /*! \brief Get the simulation patterns. + * + * Returns a vector of `num_pis()` patterns stored in `kitty::partial_truth_table`s. + * + */ + std::vector get_patterns() const { - std::ofstream out( filename, std::ofstream::out ); - for ( auto i = 0u; i < patterns.size(); ++i ) - { - out << kitty::to_hex( patterns.at( i ) ) << "\n"; - } - out.close(); + return patterns; } private: @@ -483,10 +481,10 @@ void update_const_pi( Ntk const& ntk, unordered_node_map @@ -501,12 +499,20 @@ void simulate_node( Ntk const& ntk, typename Ntk::node const& n, unordered_node_ static_assert( has_compute_v, "Ntk does not implement the compute method for kitty::partial_truth_table" ); static_assert( std::is_same_v || std::is_same_v, "The partial_truth_table specialized ntk.compute is currently only implemented in AIG and XAG" ); + if ( node_to_value[ntk.get_node( ntk.get_constant( false ) )].num_bits() != sim.num_bits() ) + { + detail::update_const_pi( ntk, node_to_value, sim ); + } + if ( !node_to_value.has( n ) ) { std::vector fanin_values( ntk.fanin_size( n ) ); ntk.foreach_fanin( n, [&]( auto const& f, auto i ) { - assert( node_to_value.has( ntk.get_node( f ) ) ); - if ( node_to_value[ntk.get_node( f )].num_bits() != sim.num_bits() ) + if ( !node_to_value.has( ntk.get_node( f ) ) ) + { + simulate_node( ntk, ntk.get_node( f ), node_to_value, sim ); + } + else if ( node_to_value[ntk.get_node( f )].num_bits() != sim.num_bits() ) { detail::re_simulate_fanin_cone( ntk, ntk.get_node( f ), node_to_value, sim ); } @@ -516,10 +522,6 @@ void simulate_node( Ntk const& ntk, typename Ntk::node const& n, unordered_node_ } else if ( node_to_value[n].num_bits() != sim.num_bits() ) { - if ( node_to_value[ntk.get_node( ntk.get_constant( false ) )].num_bits() != sim.num_bits() ) - { - detail::update_const_pi( ntk, node_to_value, sim ); - } detail::re_simulate_fanin_cone( ntk, n, node_to_value, sim ); } } diff --git a/include/mockturtle/io/write_patterns.hpp b/include/mockturtle/io/write_patterns.hpp new file mode 100644 index 000000000..4f3cd772f --- /dev/null +++ b/include/mockturtle/io/write_patterns.hpp @@ -0,0 +1,80 @@ +/* mockturtle: C++ logic network library + * Copyright (C) 2018-2020 EPFL + * + * Permission is hereby granted, free of charge, to any person + * obtaining a copy of this software and associated documentation + * files (the "Software"), to deal in the Software without + * restriction, including without limitation the rights to use, + * copy, modify, merge, publish, distribute, sublicense, and/or sell + * copies of the Software, and to permit persons to whom the + * Software is furnished to do so, subject to the following + * conditions: + * + * The above copyright notice and this permission notice shall be + * included in all copies or substantial portions of the Software. + * + * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, + * EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES + * OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND + * NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT + * HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, + * WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING + * FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR + * OTHER DEALINGS IN THE SOFTWARE. + */ + +/*! + \file write_patterns.hpp + \brief Write simulation patterns + + \author Siang-Yun Lee +*/ + +#pragma once + +#include +#include +#include +#include +#include + +#include + +#include "../algorithms/simulation.hpp" + +namespace mockturtle +{ + +/*! \brief Writes simulation patterns + * + * 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 out Output stream + */ +void write_patterns( partial_simulator const& sim, std::ostream& out = std::cout ) +{ + auto const& patterns = sim.get_patterns(); + for ( auto i = 0u; i < patterns.size(); ++i ) + { + out << kitty::to_hex( patterns.at( i ) ) << "\n"; + } +} + +/*! \brief Writes simulation patterns + * + * 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 filename Filename + */ +void write_patterns( partial_simulator const& sim, std::string const& filename ) +{ + std::ofstream os( filename.c_str(), std::ofstream::out ); + write_patterns( sim, os ); + os.close(); +} + +} /* namespace mockturtle */ diff --git a/include/mockturtle/mockturtle.hpp b/include/mockturtle/mockturtle.hpp index e00a8743e..f8372165b 100644 --- a/include/mockturtle/mockturtle.hpp +++ b/include/mockturtle/mockturtle.hpp @@ -92,6 +92,8 @@ #include "mockturtle/algorithms/reconv_cut.hpp" #include "mockturtle/algorithms/resubstitution.hpp" #include "mockturtle/algorithms/aig_resub.hpp" +#include "mockturtle/algorithms/circuit_validator.hpp" +#include "mockturtle/algorithms/pattern_generation.hpp" #include "mockturtle/utils/stopwatch.hpp" #include "mockturtle/utils/truth_table_cache.hpp" #include "mockturtle/utils/string_utils.hpp" diff --git a/include/mockturtle/utils/node_map.hpp b/include/mockturtle/utils/node_map.hpp index 3367e58e5..12254b746 100644 --- a/include/mockturtle/utils/node_map.hpp +++ b/include/mockturtle/utils/node_map.hpp @@ -238,6 +238,22 @@ class node_map> return data->find( ntk.node_to_index( ntk.get_node( f ) ) ) != data->end(); } + void erase( node const& n ) + { + if ( has( n ) ) + { + data->erase( ntk.node_to_index( n ) ); + } + } + + /* Make a deep copy */ + node_map> copy() const + { + node_map> copy(ntk); + *(copy.data) = *data; + return copy; + } + /*! \brief Mutable access to value by node. */ reference operator[]( node const& n ) { diff --git a/test/algorithms/pattern_generation.cpp b/test/algorithms/pattern_generation.cpp new file mode 100644 index 000000000..bd2855fda --- /dev/null +++ b/test/algorithms/pattern_generation.cpp @@ -0,0 +1,121 @@ +#include + +#include +#include +#include +#include +#include + +#include + +using namespace mockturtle; + +TEST_CASE( "Stuck-at pattern generation", "[pattern_generation]" ) +{ + aig_network aig; + + const auto a = aig.create_pi(); + const auto b = aig.create_pi(); + const auto c = aig.create_pi(); + const auto d = aig.create_pi(); + + const auto f = aig.create_and( aig.create_and( a, b ), !aig.create_and( c, d ) ); + aig.create_po( f ); + + partial_simulator sim( aig.num_pis(), 0 ); + sim.add_pattern( {0, 0, 0, 0} ); + sim.add_pattern( {1, 1, 1, 1} ); + + pattern_generation( aig, sim ); + + CHECK( sim.num_bits() == 3 ); + CHECK( ( kitty::get_bit( sim.compute_pi( 0 ), 2 ) && kitty::get_bit( sim.compute_pi( 1 ), 2 ) ) == true ); + CHECK( ( kitty::get_bit( sim.compute_pi( 2 ), 2 ) && kitty::get_bit( sim.compute_pi( 3 ), 2 ) ) == false ); +} + +TEST_CASE( "Constant node removal", "[pattern_generation]" ) +{ + aig_network aig; + + const auto a = aig.create_pi(); + const auto b = aig.create_pi(); + + const auto f1 = aig.create_and( !a, b ); + const auto f2 = aig.create_and( a, !b ); + const auto f3 = aig.create_or( f1, f2 ); + aig.create_po( f3 ); + + const auto g1 = aig.create_and( a, b ); + const auto g2 = aig.create_and( !a, !b ); + const auto g3 = aig.create_or( g1, g2 ); + aig.create_po( g3 ); + + const auto h = aig.create_and( f3, g3 ); + aig.create_po( h ); + + CHECK( aig.num_gates() == 7 ); + + partial_simulator sim( aig.num_pis(), 0 ); + pattern_generation_params ps; + ps.substitute_const = true; + pattern_generation( aig, sim, ps ); + + CHECK( aig.num_gates() == 6 ); +} + +TEST_CASE( "Multiple stuck-at pattern generation", "[pattern_generation]" ) +{ + aig_network aig; + + const auto a = aig.create_pi(); + const auto b = aig.create_pi(); + const auto c = aig.create_pi(); + const auto d = aig.create_pi(); + + const auto f = aig.create_and( aig.create_and( a, b ), !aig.create_and( c, d ) ); + aig.create_po( f ); + + partial_simulator sim( aig.num_pis(), 0 ); + sim.add_pattern( {0, 0, 0, 0} ); + sim.add_pattern( {1, 1, 1, 1} ); + sim.add_pattern( {1, 1, 0, 1} ); + sim.add_pattern( {0, 1, 1, 1} ); + + pattern_generation_params ps; + ps.num_stuck_at = 2; + + pattern_generation( aig, sim, ps ); + + CHECK( sim.num_bits() == 5 ); + CHECK( ( kitty::get_bit( sim.compute_pi( 0 ), 4 ) && kitty::get_bit( sim.compute_pi( 1 ), 4 ) ) == true ); + CHECK( ( kitty::get_bit( sim.compute_pi( 2 ), 4 ) && kitty::get_bit( sim.compute_pi( 3 ), 4 ) ) == false ); +} + +TEST_CASE( "With observability awareness", "[pattern_generation]" ) +{ + xag_network xag; + + const auto a = xag.create_pi(); + const auto b = xag.create_pi(); + const auto c = xag.create_pi(); + + const auto f1 = xag.create_and( a, b ); + const auto f2 = xag.create_and( f1, c ); + const auto f3 = xag.create_and( !f1, !a ); + const auto f4 = xag.create_xor( f2, f3 ); + xag.create_po( f4 ); + + partial_simulator sim( xag.num_pis(), 0 ); + sim.add_pattern( {0, 1, 1} ); // this is the only pattern making f1 = 0, but it's not observable + sim.add_pattern( {1, 1, 0} ); + sim.add_pattern( {1, 1, 1} ); + + pattern_generation_params ps; + ps.odc_levels = -1; + + pattern_generation( xag, sim, ps ); + + CHECK( sim.num_bits() == 4 ); + /* the generated pattern should be either 000, 010, or 101 */ + CHECK( ( ( !kitty::get_bit( sim.compute_pi( 0 ), 3 ) && !kitty::get_bit( sim.compute_pi( 2 ), 3 ) ) || ( kitty::get_bit( sim.compute_pi( 0 ), 3 ) && !kitty::get_bit( sim.compute_pi( 1 ), 3 ) && kitty::get_bit( sim.compute_pi( 2 ), 3 ) ) ) == true ); +} diff --git a/test/io/write_patterns.cpp b/test/io/write_patterns.cpp new file mode 100644 index 000000000..680680d4d --- /dev/null +++ b/test/io/write_patterns.cpp @@ -0,0 +1,32 @@ +#include + +#include + +#include +#include + +using namespace mockturtle; + +TEST_CASE( "write patterns", "[write_patterns]" ) +{ + partial_simulator sim( 3, 0 ); + + sim.add_pattern( {0, 0, 0} ); + sim.add_pattern( {0, 0, 1} ); + sim.add_pattern( {0, 1, 0} ); + sim.add_pattern( {1, 0, 1} ); + + sim.add_pattern( {1, 1, 1} ); + sim.add_pattern( {1, 0, 0} ); + sim.add_pattern( {1, 1, 0} ); + sim.add_pattern( {0, 1, 1} ); + + sim.add_pattern( {1, 0, 1} ); + + std::ostringstream out; + write_patterns( sim, out ); + + CHECK( out.str() == "178\n" + "0d4\n" + "19a\n" ); +}