From fa283fa1649d22b5c13d6eb9c3a20c5f388ebc31 Mon Sep 17 00:00:00 2001 From: Sonia Date: Wed, 1 Jul 2020 09:55:50 +0200 Subject: [PATCH 01/23] add failing test case SegFault when providing the constant node as the first argument of `validate` --- test/algorithms/circuit_validator.cpp | 21 +++++++++++++++++++++ 1 file changed, 21 insertions(+) diff --git a/test/algorithms/circuit_validator.cpp b/test/algorithms/circuit_validator.cpp index dfef6c0cd..927260527 100644 --- a/test/algorithms/circuit_validator.cpp +++ b/test/algorithms/circuit_validator.cpp @@ -122,6 +122,27 @@ TEST_CASE( "Validating const nodes", "[validator]" ) CHECK( v.cex[1] == true ); } +TEST_CASE( "Validating with the const node", "[validator]" ) +{ + /* original circuit */ + aig_network aig; + auto const a = aig.create_pi(); + auto const b = aig.create_pi(); + auto const f1 = aig.create_and( !a, b ); + auto const f2 = aig.create_and( a, !b ); + auto const f3 = aig.create_or( f1, f2 ); // a ^ b + + auto const g1 = aig.create_and( a, b ); + auto const g2 = aig.create_and( !a, !b ); + auto const g3 = aig.create_or( g1, g2 ); // a == b + + auto const h = aig.create_and( f3, g3 ); // const 0 + + circuit_validator v( aig ); + + CHECK( *( v.validate( aig.get_constant( false ), aig.get_node( h ) ) ) == true ); +} + TEST_CASE( "Validating with ODC", "[validator]" ) { /* original circuit */ From 2a99d3cd00acaa9acbed15bc1cb3b861891331a0 Mon Sep 17 00:00:00 2001 From: Sonia Date: Wed, 1 Jul 2020 10:20:19 +0200 Subject: [PATCH 02/23] remove unnecessary assertion --- include/mockturtle/algorithms/circuit_validator.hpp | 1 - 1 file changed, 1 deletion(-) diff --git a/include/mockturtle/algorithms/circuit_validator.hpp b/include/mockturtle/algorithms/circuit_validator.hpp index d2eae5139..27e6baba7 100644 --- a/include/mockturtle/algorithms/circuit_validator.hpp +++ b/include/mockturtle/algorithms/circuit_validator.hpp @@ -251,7 +251,6 @@ class circuit_validator { construct( root ); } - assert( literals[root].variable() != bill::var_type( 0 ) ); std::optional res; if constexpr ( use_odc ) From a7cf01c3e8fc85caa6e72b85042a2deccfd94d04 Mon Sep 17 00:00:00 2001 From: Sonia Date: Wed, 1 Jul 2020 12:07:32 +0200 Subject: [PATCH 03/23] generate_pattern --- .../algorithms/circuit_validator.hpp | 80 ++++++++++++++++--- 1 file changed, 68 insertions(+), 12 deletions(-) diff --git a/include/mockturtle/algorithms/circuit_validator.hpp b/include/mockturtle/algorithms/circuit_validator.hpp index 27e6baba7..5250f0fba 100644 --- a/include/mockturtle/algorithms/circuit_validator.hpp +++ b/include/mockturtle/algorithms/circuit_validator.hpp @@ -284,6 +284,64 @@ class circuit_validator return res; } + /*! \brief Generate more patterns for node `root` to be `value`, blocking several known patterns. + * + * Requires `use_pushpop = true`. + * + * If `block_patterns` and the returned vector are both empty, `root` is validated to be a constant of `!value`. + * + * \param block_patterns Patterns to be blocked in the solver. (Will not generate any of them.) + * \param num_patterns Number of patterns to be generated, if possible. (The size of the result may be smaller than this number, but never larger.) + */ + template> + std::vector> generate_pattern( node const& root, bool value, std::vector> const& block_patterns, uint32_t num_patterns ) + { + if ( !literals.has( root ) ) + { + construct( root ); + } + + solver.push(); + + for ( auto const& pattern : block_patterns ) + { + block_pattern( pattern ); + } + + std::vector assumptions( {lit_not_cond( literals[root], !value )} ); + if constexpr ( use_odc ) + { + if ( ps.odc_levels != 0 ) + { + assumptions.emplace_back( build_odc_window( root, ~literals[root] ) ); + } + } + + std::optional res; + std::vector> generated; + for ( auto i = 0u; i < num_patterns; ++i ) + { + res = solve( assumptions ); + + if ( !res || *res ) /* timeout or UNSAT */ + { + break; + } + else /* SAT */ + { + generated.emplace_back( cex ); + block_pattern( cex ); + } + } + + solver.pop(); + if ( solver.num_clauses() > ps.max_clauses ) + { + restart(); + } + return generated; + } + /*! \brief Update CNF clauses. * * This function should be called when the function of one or more nodes @@ -316,20 +374,8 @@ class circuit_validator literals[n] = bill::lit_type( i + 1, bill::lit_type::polarities::positive ); } ); - /* compute literals for nodes */ - //uint32_t next_var = ntk.num_pis() + 1; - //ntk.foreach_gate( [&]( auto const& n ) { - // literals[n] = bill::lit_type( next_var++, bill::lit_type::polarities::positive ); - //} ); - solver.add_variables( ntk.num_pis() + 1 ); solver.add_clause( {~literals[ntk.get_constant( false )]} ); - - //generate_cnf( - // ntk, [&]( auto const& clause ) { - // solver.add_clause( clause ); - // }, - // literals ); } void construct( node const& n ) @@ -496,6 +542,16 @@ class circuit_validator return res; } + void block_pattern( std::vector const& pattern ) + { + assert( pattern.size() == ntk.num_pis() ); + std::vector clause; + ntk.foreach_pi( [&]( auto const& n, auto i ) { + clause.emplace_back( lit_not_cond( literals[n] , pattern[i] ) ); + } ); + solver.add_clause( clause ); + } + private: template> bill::lit_type build_odc_window( node const& root, bill::lit_type const& lit ) From 354fe72f245244ee528486e3532b57bac7fa949f Mon Sep 17 00:00:00 2001 From: Sonia Date: Wed, 1 Jul 2020 12:37:12 +0200 Subject: [PATCH 04/23] add testcase & API with signal --- .../algorithms/circuit_validator.hpp | 11 +++++++-- test/algorithms/circuit_validator.cpp | 23 +++++++++++++++++++ 2 files changed, 32 insertions(+), 2 deletions(-) diff --git a/include/mockturtle/algorithms/circuit_validator.hpp b/include/mockturtle/algorithms/circuit_validator.hpp index 5250f0fba..385d9ec83 100644 --- a/include/mockturtle/algorithms/circuit_validator.hpp +++ b/include/mockturtle/algorithms/circuit_validator.hpp @@ -284,16 +284,23 @@ class circuit_validator return res; } - /*! \brief Generate more patterns for node `root` to be `value`, blocking several known patterns. + /*! \brief Generate more patterns for signal `f` to be `value`, blocking several known patterns. * * Requires `use_pushpop = true`. * - * If `block_patterns` and the returned vector are both empty, `root` is validated to be a constant of `!value`. + * If `block_patterns` and the returned vector are both empty, `f` is validated to be a constant of `!value`. * * \param block_patterns Patterns to be blocked in the solver. (Will not generate any of them.) * \param num_patterns Number of patterns to be generated, if possible. (The size of the result may be smaller than this number, but never larger.) */ template> + std::vector> generate_pattern( signal const& f, bool value, std::vector> const& block_patterns, uint32_t num_patterns ) + { + return generate_pattern( ntk.get_node( f ), value ^ ntk.is_complemented( f ), block_patterns, num_patterns ); + } + + /*! \brief Generate more patterns for node `root` to be `value`, blocking several known patterns. */ + template> std::vector> generate_pattern( node const& root, bool value, std::vector> const& block_patterns, uint32_t num_patterns ) { if ( !literals.has( root ) ) diff --git a/test/algorithms/circuit_validator.cpp b/test/algorithms/circuit_validator.cpp index 927260527..46f4f1b56 100644 --- a/test/algorithms/circuit_validator.cpp +++ b/test/algorithms/circuit_validator.cpp @@ -143,6 +143,29 @@ TEST_CASE( "Validating with the const node", "[validator]" ) CHECK( *( v.validate( aig.get_constant( false ), aig.get_node( h ) ) ) == true ); } +TEST_CASE( "Generate multiple patterns", "[validator]" ) +{ + /* original circuit */ + aig_network aig; + auto const a = aig.create_pi(); + auto const b = aig.create_pi(); + auto const c = aig.create_pi(); + auto const f1 = aig.create_xor( a, b ); + auto const f2 = aig.create_xor( f1, c ); // a ^ b ^ c + + circuit_validator v( aig ); + + CHECK( *( v.validate( f2, false ) ) == false ); /* f2 is not a constant 0 */ + std::vector> block_pattern( {v.cex} ); + auto const patterns = v.generate_pattern( f2, true, block_pattern, 10 ); /* generate patterns making f2 = 1 */ + CHECK( patterns.size() == 3u ); + for ( auto const& pattern : patterns ) + { + CHECK( ( pattern[0] ^ pattern[1] ^ pattern[2] ) == true ); + CHECK( pattern != block_pattern[0] ); + } +} + TEST_CASE( "Validating with ODC", "[validator]" ) { /* original circuit */ From 6b520a7791c992aff77654782833f78acd29733b Mon Sep 17 00:00:00 2001 From: Sonia Date: Wed, 1 Jul 2020 12:38:43 +0200 Subject: [PATCH 05/23] Revert "remove unnecessary assertion" This reverts commit 2a99d3cd00acaa9acbed15bc1cb3b861891331a0. --- include/mockturtle/algorithms/circuit_validator.hpp | 1 + 1 file changed, 1 insertion(+) diff --git a/include/mockturtle/algorithms/circuit_validator.hpp b/include/mockturtle/algorithms/circuit_validator.hpp index 385d9ec83..59fb398a4 100644 --- a/include/mockturtle/algorithms/circuit_validator.hpp +++ b/include/mockturtle/algorithms/circuit_validator.hpp @@ -251,6 +251,7 @@ class circuit_validator { construct( root ); } + assert( literals[root].variable() != bill::var_type( 0 ) ); std::optional res; if constexpr ( use_odc ) From c0ecca06c420e65c73b5a4e1190da622cda62ae3 Mon Sep 17 00:00:00 2001 From: Sonia Date: Wed, 1 Jul 2020 12:40:21 +0200 Subject: [PATCH 06/23] Revert "Revert "remove unnecessary assertion"" This reverts commit 6b520a7791c992aff77654782833f78acd29733b. --- include/mockturtle/algorithms/circuit_validator.hpp | 1 - 1 file changed, 1 deletion(-) diff --git a/include/mockturtle/algorithms/circuit_validator.hpp b/include/mockturtle/algorithms/circuit_validator.hpp index 59fb398a4..385d9ec83 100644 --- a/include/mockturtle/algorithms/circuit_validator.hpp +++ b/include/mockturtle/algorithms/circuit_validator.hpp @@ -251,7 +251,6 @@ class circuit_validator { construct( root ); } - assert( literals[root].variable() != bill::var_type( 0 ) ); std::optional res; if constexpr ( use_odc ) From 13f3bc91997e9487b6f4db2fc749b46f50e21884 Mon Sep 17 00:00:00 2001 From: Sonia Date: Wed, 1 Jul 2020 12:44:45 +0200 Subject: [PATCH 07/23] correct testcase; remove another unnecessary assertion --- include/mockturtle/algorithms/circuit_validator.hpp | 1 - test/algorithms/circuit_validator.cpp | 2 +- 2 files changed, 1 insertion(+), 2 deletions(-) diff --git a/include/mockturtle/algorithms/circuit_validator.hpp b/include/mockturtle/algorithms/circuit_validator.hpp index 385d9ec83..2428df0ad 100644 --- a/include/mockturtle/algorithms/circuit_validator.hpp +++ b/include/mockturtle/algorithms/circuit_validator.hpp @@ -513,7 +513,6 @@ class circuit_validator { construct( root ); } - assert( literals[root].variable() != bill::var_type( 0 ) ); std::optional res; if constexpr ( use_odc ) diff --git a/test/algorithms/circuit_validator.cpp b/test/algorithms/circuit_validator.cpp index 46f4f1b56..e282f4ed0 100644 --- a/test/algorithms/circuit_validator.cpp +++ b/test/algorithms/circuit_validator.cpp @@ -140,7 +140,7 @@ TEST_CASE( "Validating with the const node", "[validator]" ) circuit_validator v( aig ); - CHECK( *( v.validate( aig.get_constant( false ), aig.get_node( h ) ) ) == true ); + CHECK( *( v.validate( aig.get_constant( false ), h ) ) == true ); } TEST_CASE( "Generate multiple patterns", "[validator]" ) From cb6ae968a8fdb7f91b687b0a6bda9b56e74abea1 Mon Sep 17 00:00:00 2001 From: Sonia Date: Wed, 1 Jul 2020 12:46:18 +0200 Subject: [PATCH 08/23] simplify testcase --- test/algorithms/circuit_validator.cpp | 25 ++++--------------------- 1 file changed, 4 insertions(+), 21 deletions(-) diff --git a/test/algorithms/circuit_validator.cpp b/test/algorithms/circuit_validator.cpp index e282f4ed0..cf9049a37 100644 --- a/test/algorithms/circuit_validator.cpp +++ b/test/algorithms/circuit_validator.cpp @@ -116,33 +116,16 @@ TEST_CASE( "Validating const nodes", "[validator]" ) circuit_validator v( aig ); + /* several APIs are available */ CHECK( *( v.validate( aig.get_node( h ), false ) ) == true ); + CHECK( *( v.validate( h, false ) ) == true ); + CHECK( *( v.validate( aig.get_constant( false ), h ) ) == true ); + CHECK( *( v.validate( f1, false ) ) == false ); CHECK( v.cex[0] == false ); CHECK( v.cex[1] == true ); } -TEST_CASE( "Validating with the const node", "[validator]" ) -{ - /* original circuit */ - aig_network aig; - auto const a = aig.create_pi(); - auto const b = aig.create_pi(); - auto const f1 = aig.create_and( !a, b ); - auto const f2 = aig.create_and( a, !b ); - auto const f3 = aig.create_or( f1, f2 ); // a ^ b - - auto const g1 = aig.create_and( a, b ); - auto const g2 = aig.create_and( !a, !b ); - auto const g3 = aig.create_or( g1, g2 ); // a == b - - auto const h = aig.create_and( f3, g3 ); // const 0 - - circuit_validator v( aig ); - - CHECK( *( v.validate( aig.get_constant( false ), h ) ) == true ); -} - TEST_CASE( "Generate multiple patterns", "[validator]" ) { /* original circuit */ From a24337aca051ef698b9c3f6d3d0582e5ff08719b Mon Sep 17 00:00:00 2001 From: Sonia Date: Wed, 1 Jul 2020 14:46:27 +0200 Subject: [PATCH 09/23] add tests to make sure blocking doesn't affect later validations --- test/algorithms/circuit_validator.cpp | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/test/algorithms/circuit_validator.cpp b/test/algorithms/circuit_validator.cpp index cf9049a37..d1c98435a 100644 --- a/test/algorithms/circuit_validator.cpp +++ b/test/algorithms/circuit_validator.cpp @@ -147,6 +147,10 @@ TEST_CASE( "Generate multiple patterns", "[validator]" ) CHECK( ( pattern[0] ^ pattern[1] ^ pattern[2] ) == true ); CHECK( pattern != block_pattern[0] ); } + + /* blocking patterns should not affect later validations */ + CHECK( *( v.validate( f1, false ) ) == false ); /* f1 is not a constant 0 */ + CHECK( ( v.cex[0] ^ v.cex[1] ) == true ); } TEST_CASE( "Validating with ODC", "[validator]" ) From 44ea917d66447c8fba0220ae0fefbd4306ba28f6 Mon Sep 17 00:00:00 2001 From: Sonia Date: Wed, 1 Jul 2020 15:01:50 +0200 Subject: [PATCH 10/23] provide default arguments --- include/mockturtle/algorithms/circuit_validator.hpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/include/mockturtle/algorithms/circuit_validator.hpp b/include/mockturtle/algorithms/circuit_validator.hpp index 2428df0ad..69e639ede 100644 --- a/include/mockturtle/algorithms/circuit_validator.hpp +++ b/include/mockturtle/algorithms/circuit_validator.hpp @@ -294,14 +294,14 @@ class circuit_validator * \param num_patterns Number of patterns to be generated, if possible. (The size of the result may be smaller than this number, but never larger.) */ template> - std::vector> generate_pattern( signal const& f, bool value, std::vector> const& block_patterns, uint32_t num_patterns ) + std::vector> generate_pattern( signal const& f, bool value, std::vector> const& block_patterns = {}, uint32_t num_patterns = 1u ) { return generate_pattern( ntk.get_node( f ), value ^ ntk.is_complemented( f ), block_patterns, num_patterns ); } /*! \brief Generate more patterns for node `root` to be `value`, blocking several known patterns. */ template> - std::vector> generate_pattern( node const& root, bool value, std::vector> const& block_patterns, uint32_t num_patterns ) + std::vector> generate_pattern( node const& root, bool value, std::vector> const& block_patterns = {}, uint32_t num_patterns = 1u ) { if ( !literals.has( root ) ) { From c0a76a4846ef8370c929d12de8852767fce0994f Mon Sep 17 00:00:00 2001 From: Sonia Date: Wed, 1 Jul 2020 15:07:29 +0200 Subject: [PATCH 11/23] update docs --- docs/algorithms/circuit_validator.rst | 10 ++++++++++ docs/algorithms/simulation.rst | 4 ++-- 2 files changed, 12 insertions(+), 2 deletions(-) diff --git a/docs/algorithms/circuit_validator.rst b/docs/algorithms/circuit_validator.rst index abcde6dc9..1c2d15ba5 100644 --- a/docs/algorithms/circuit_validator.rst +++ b/docs/algorithms/circuit_validator.rst @@ -79,3 +79,13 @@ The following code shows how to check functional equivalence of a root node to s **Updating** .. doxygenfunction:: mockturtle::circuit_validator::update + +**Generate multiple patterns** + +A simulation pattern is a collection of value assignments to every primary inputs. +A counter-example of a failing validation is a simulation pattern under which the nodes being validated have different simulation values. +It can be directly read from the public data member ``circuit_validator::cex`` (which is a ``std::vector`` of size ``Ntk::num_pis()``) after a call to (any type of) ``circuit_validator::validate`` which returns ``false``. +If multiple different patterns are desired, one can call ``circuit_validator::generate_pattern``. However, this is currently only supported for constant validation. + +.. doxygenfunction:: mockturtle::circuit_validator::generate_pattern( signal const&, bool, std::vector> const&, uint32_t ) +.. doxygenfunction:: mockturtle::circuit_validator::generate_pattern( node const&, bool, std::vector> const&, uint32_t ) diff --git a/docs/algorithms/simulation.rst b/docs/algorithms/simulation.rst index 65a52e54d..2e0f340d7 100644 --- a/docs/algorithms/simulation.rst +++ b/docs/algorithms/simulation.rst @@ -78,8 +78,8 @@ The following simulators are implemented: Partial simulation ~~~~~~~~~~~~~~~~~~ -With `partial_simulator`, adding new simulation patterns and re-simulation can be done. -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`. +With ``partial_simulator``, adding new simulation patterns and re-simulation can be done. +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. .. doxygenfunction:: mockturtle::partial_simulator::partial_simulator( unsigned, unsigned, std::default_random_engine::result_type ) From dc3d8518deb60083c999980589331368c76b7c9d Mon Sep 17 00:00:00 2001 From: Sonia Date: Wed, 1 Jul 2020 19:44:38 +0200 Subject: [PATCH 12/23] first try --- experiments/pattern_generation.cpp | 84 ++++ experiments/pattern_generation.json | 247 ++++++++++ include/mockturtle/algorithms/dont_cares.hpp | 77 +++ .../algorithms/pattern_generation.hpp | 451 ++++++++++++++++++ include/mockturtle/utils/node_map.hpp | 16 + 5 files changed, 875 insertions(+) create mode 100644 experiments/pattern_generation.cpp create mode 100644 experiments/pattern_generation.json create mode 100644 include/mockturtle/algorithms/pattern_generation.hpp diff --git a/experiments/pattern_generation.cpp b/experiments/pattern_generation.cpp new file mode 100644 index 000000000..33ebfcb33 --- /dev/null +++ b/experiments/pattern_generation.cpp @@ -0,0 +1,84 @@ +/* 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", "cec" ); + + for ( auto const& benchmark : epfl_benchmarks() ) + { + //if ( benchmark != "iwls2005/mem_ctrl" ) continue; + + fmt::print( "[i] processing {}\n", benchmark ); + aig_network aig; + lorina::read_aiger( benchmark_path( benchmark ), aiger_reader( aig ) ); + auto size_before = aig.num_gates(); + + patgen_params ps; + patgen_stats st; + + uint32_t num_random_pattern = 256; + std::string write_pats = "256sa1/" + benchmark + ".pat"; + + ps.num_stuck_at = 1; + //ps.observability_type1 = true; + //ps.observability_type2 = true; + //ps.odc_levels = 5; + ps.random_seed = 1689; + ps.progress = false; + //ps.verbose = true; + + partial_simulator sim( aig.num_pis(), num_random_pattern, ps.random_seed ); + + pattern_generation( aig, sim, ps, &st ); + aig = cleanup_dangling( aig ); + + sim.write_patterns( write_pats ); + + const auto cec = benchmark == "hyp" ? true : abc_cec( aig, benchmark ); + 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 ), cec ); + } + + exp.save(); + exp.table(); + + return 0; +} diff --git a/experiments/pattern_generation.json b/experiments/pattern_generation.json new file mode 100644 index 000000000..05d3dee05 --- /dev/null +++ b/experiments/pattern_generation.json @@ -0,0 +1,247 @@ +[ + { + "entries": [ + { + "#PI": 256, + "#const": 0, + "#pat": 256, + "#pat gen": 0, + "benchmark": "adder", + "cec": true, + "size": 1020, + "t_SAT": 0.0, + "t_sim": 0.0014159049605950713, + "t_total": 0.0015550010139122605 + }, + { + "#PI": 135, + "#const": 0, + "#pat": 256, + "#pat gen": 0, + "benchmark": "bar", + "cec": true, + "size": 3336, + "t_SAT": 0.0, + "t_sim": 0.004492159001529217, + "t_total": 0.004908484872430563 + }, + { + "#PI": 128, + "#const": 8, + "#pat": 279, + "#pat gen": 23, + "benchmark": "div", + "cec": true, + "size": 57247, + "t_SAT": 0.09047292917966843, + "t_sim": 0.1637018471956253, + "t_total": 0.27369004487991333 + }, + { + "#PI": 256, + "#const": 2, + "#pat": 260, + "#pat gen": 4, + "benchmark": "hyp", + "cec": true, + "size": 214335, + "t_SAT": 0.0010707159526646137, + "t_sim": 0.523285984992981, + "t_total": 0.6091689467430115 + }, + { + "#PI": 32, + "#const": 161, + "#pat": 425, + "#pat gen": 169, + "benchmark": "log2", + "cec": true, + "size": 32060, + "t_SAT": 17.49126434326172, + "t_sim": 0.2002258002758026, + "t_total": 17.75943946838379 + }, + { + "#PI": 512, + "#const": 0, + "#pat": 256, + "#pat gen": 0, + "benchmark": "max", + "cec": true, + "size": 2865, + "t_SAT": 0.0, + "t_sim": 0.00374211510643363, + "t_total": 0.004087099805474281 + }, + { + "#PI": 128, + "#const": 0, + "#pat": 257, + "#pat gen": 1, + "benchmark": "multiplier", + "cec": true, + "size": 27062, + "t_SAT": 8.262100163847208e-05, + "t_sim": 0.060651980340480804, + "t_total": 0.06559254974126816 + }, + { + "#PI": 24, + "#const": 19, + "#pat": 339, + "#pat gen": 83, + "benchmark": "sin", + "cec": true, + "size": 5416, + "t_SAT": 0.5215885639190674, + "t_sim": 0.04783011972904205, + "t_total": 0.5729691386222839 + }, + { + "#PI": 128, + "#const": 0, + "#pat": 256, + "#pat gen": 0, + "benchmark": "sqrt", + "cec": true, + "size": 24618, + "t_SAT": 0.0, + "t_sim": 0.031034482643008232, + "t_total": 0.034022312611341476 + }, + { + "#PI": 64, + "#const": 0, + "#pat": 256, + "#pat gen": 0, + "benchmark": "square", + "cec": true, + "size": 18484, + "t_SAT": 0.0, + "t_sim": 0.02168254181742668, + "t_total": 0.023898186162114143 + }, + { + "#PI": 256, + "#const": 0, + "#pat": 259, + "#pat gen": 3, + "benchmark": "arbiter", + "cec": true, + "size": 11839, + "t_SAT": 0.00020269300148356706, + "t_sim": 0.013296888209879398, + "t_total": 0.014842754229903221 + }, + { + "#PI": 10, + "#const": 0, + "#pat": 261, + "#pat gen": 5, + "benchmark": "cavlc", + "cec": true, + "size": 693, + "t_SAT": 0.00010404200293123722, + "t_sim": 0.0017267799703404307, + "t_total": 0.0019697370007634163 + }, + { + "#PI": 7, + "#const": 0, + "#pat": 256, + "#pat gen": 0, + "benchmark": "ctrl", + "cec": true, + "size": 174, + "t_SAT": 0.0, + "t_sim": 0.00019234500359743834, + "t_total": 0.00021304399706423283 + }, + { + "#PI": 8, + "#const": 0, + "#pat": 421, + "#pat gen": 165, + "benchmark": "dec", + "cec": true, + "size": 304, + "t_SAT": 0.001692189951427281, + "t_sim": 0.0021870590280741453, + "t_total": 0.004020167980343103 + }, + { + "#PI": 147, + "#const": 0, + "#pat": 302, + "#pat gen": 46, + "benchmark": "i2c", + "cec": true, + "size": 1342, + "t_SAT": 0.0016219819663092494, + "t_sim": 0.004550343845039606, + "t_total": 0.006605285219848156 + }, + { + "#PI": 11, + "#const": 0, + "#pat": 257, + "#pat gen": 1, + "benchmark": "int2float", + "cec": true, + "size": 260, + "t_SAT": 1.3675999980478082e-05, + "t_sim": 0.0004994070040993392, + "t_total": 0.000562014989554882 + }, + { + "#PI": 1204, + "#const": 1, + "#pat": 734, + "#pat gen": 478, + "benchmark": "mem_ctrl", + "cec": true, + "size": 46836, + "t_SAT": 0.09079248458147049, + "t_sim": 0.5077462196350098, + "t_total": 0.6229751706123352 + }, + { + "#PI": 128, + "#const": 0, + "#pat": 267, + "#pat gen": 11, + "benchmark": "priority", + "cec": true, + "size": 978, + "t_SAT": 0.0006275969790294766, + "t_sim": 0.002462324919179082, + "t_total": 0.0032959720119833946 + }, + { + "#PI": 60, + "#const": 0, + "#pat": 307, + "#pat gen": 51, + "benchmark": "router", + "cec": true, + "size": 257, + "t_SAT": 0.001450460054911673, + "t_sim": 0.0036068339832127094, + "t_total": 0.005179498810321093 + }, + { + "#PI": 1001, + "#const": 5, + "#pat": 305, + "#pat gen": 49, + "benchmark": "voter", + "cec": true, + "size": 13758, + "t_SAT": 2.65531587600708, + "t_sim": 0.2700190246105194, + "t_total": 2.9297537803649902 + } + ], + "version": "c0a76a4" + } +] diff --git a/include/mockturtle/algorithms/dont_cares.hpp b/include/mockturtle/algorithms/dont_cares.hpp index 438418477..309df6bf7 100644 --- a/include/mockturtle/algorithms/dont_cares.hpp +++ b/include/mockturtle/algorithms/dont_cares.hpp @@ -126,6 +126,83 @@ 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 ); + }); +} + +} /* namespace detail */ + +/* Compute the don't care input patterns in the partial simulator `sim` of node `n` with respect to `roots` +such that under these PI patterns the value of n doesn't affect outputs of roots. */ +template +kitty::partial_truth_table observability_dont_cares( Ntk const& ntk, node const& n, partial_simulator const& sim, unordered_node_map const& 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 ); }); + + unordered_node_map ttsNOT = tts.copy(); // same as tts except for TFOs + + ntk.incr_trav_id(); + detail::clearTFO_rec( ntk, ttsNOT, n, roots, levels ); + ttsNOT[n] = ~tts[n]; + simulate_nodes( ntk, ttsNOT, sim ); + + kitty::partial_truth_table care( tts[n].num_bits() ); + for ( const auto& r : roots ) + { + care |= tts[r] ^ ttsNOT[r]; + } + return ~care; +} + +/* Check if node `n` is observable with respect to `roots` +such that under input assignment `pattern` the value of `n` doesn't affect outputs of `roots`. +Returns true if is observable. (at least one PO is affected) */ +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); + unordered_node_map ttsNOT(ntk); + simulate_nodes( ntk, tts, sim ); + simulate_nodes( ntk, ttsNOT, sim ); // copying doesn't work for unordered_node_map, not sure why + + 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..8edd9e9be --- /dev/null +++ b/include/mockturtle/algorithms/pattern_generation.hpp @@ -0,0 +1,451 @@ +/* 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 +#include +#include "../utils/progress_bar.hpp" +#include "../utils/stopwatch.hpp" +#include +#include +#include +#include +#include +#include + +namespace mockturtle +{ + +struct patgen_params +{ + /*! \brief Whether to substitute constant nodes. */ + bool substitute_const{true}; + + /*! \brief Number of patterns each node should have for both values. */ + uint32_t num_stuck_at{1}; + + /*! \brief Fanout levels to consider for observability. -1 = no limit. */ + int odc_levels{-1}; + + /*! \brief Whether to check and re-generate type 1 observable patterns. */ + bool observability_type1{false}; + + /*! \brief Whether to check and re-generate type 2 observable patterns. */ + bool observability_type2{false}; + + /*! \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}; +}; + +struct patgen_stats +{ + stopwatch<>::duration time_total{0}; + + /*! \brief Time for simulations. */ + 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 found. */ + uint32_t num_constant{0}; + + /*! \brief Number of generated patterns. */ + uint32_t num_generated_patterns{0}; + + /*! \brief Number of type1 unobservable nodes. */ + uint32_t unobservable_type1{0}; + + /*! \brief Number of resolved type1 unobservable nodes. */ + uint32_t unobservable_type1_resolved{0}; + + /*! \brief Number of type2 unobservable nodes. */ + uint32_t unobservable_type2{0}; + + /*! \brief Number of resolved type2 unobservable nodes. */ + uint32_t unobservable_type2_resolved{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, patgen_params const& ps, validator_params& vps, patgen_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 ) + { + if ( ps.observability_type2 ) + { + 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 ); + }); + } + + 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 ) + { + if ( ps.observability_type1 ) + { + /* 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" ; + } + ++st.unobservable_type1; + 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_resolved; + if ( ps.verbose ) + { + assert( pattern_is_observable( ntk, n, validator.cex, ps.odc_levels ) ); + std::cout << "\t[i] unobservable pattern resolved.\n"; + } + } + else + { + if ( ps.verbose ) + { + std::cout << "\t[i] unobservable node " << n << "\n"; + } + } + } + } + } + } + + new_pattern( validator.cex ); + + if ( ps.num_stuck_at > 1 ) + { + auto generated = 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-obs2 |{0}| node = {1:>4} #pat = {2:>4}", ps.progress}; + + ntk.foreach_gate( [&]( auto const& n, auto i ) + { + pbar( i, i, 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 ) == sim.compute_constant( false ) ) + { + if ( ps.verbose ) + { + std::cout << "\t[i] under all observable patterns, node " << n << " is always 0 (type 2).\n"; + } + ++st.unobservable_type2; + + 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_resolved; + + 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[i] added generated pattern to resolve unobservability.\n"; + } + } + else + { + if ( ps.verbose ) + { + std::cout << "\t[i] unobservable node " << n << "\n"; + } + } + } + } + else if ( ( tts[n] | odc ) == sim.compute_constant( true ) ) + { + if ( ps.verbose ) + { + std::cout << "\t[i] under all observable patterns, node " << n << " is always 1 (type 2).\n"; + } + ++st.unobservable_type2; + + 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_resolved; + + 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[i] added generated pattern to resolve unobservability.\n"; + } + } + else + { + if ( ps.verbose ) + { + std::cout << "\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 = 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; + + patgen_params const& ps; + patgen_stats& st; + + validator_params& vps; + circuit_validator validator; + + TT tts; + std::vector const_nodes; + + partial_simulator& sim; +}; + +} /* namespace detail */ + +template +void pattern_generation( Ntk& ntk, partial_simulator& sim, patgen_params const& ps = {}, patgen_stats* pst = nullptr ) +{ + 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" ); + static_assert( has_foreach_gate_v, "Ntk does not implement the foreach_gate method" ); + static_assert( has_foreach_node_v, "Ntk does not implement the foreach_node method" ); + static_assert( has_get_constant_v, "Ntk does not implement the get_constant 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( has_substitute_node_v, "Ntk does not implement the has substitute_node method" ); + + patgen_stats st; + validator_params vps; + vps.conflict_limit = ps.conflict_limit; + vps.random_seed = ps.random_seed; + + if ( ps.observability_type1 || ps.observability_type2 ) + { + using fanout_view_t = fanout_view; + fanout_view 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/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 ) { From 59bcd779825d22278332de9e2d27b63d2e359a8d Mon Sep 17 00:00:00 2001 From: Sonia Date: Thu, 2 Jul 2020 11:47:22 +0200 Subject: [PATCH 13/23] clean up --- .../algorithms/pattern_generation.hpp | 242 ++++++++++-------- 1 file changed, 129 insertions(+), 113 deletions(-) diff --git a/include/mockturtle/algorithms/pattern_generation.hpp b/include/mockturtle/algorithms/pattern_generation.hpp index 8edd9e9be..748bd3f90 100644 --- a/include/mockturtle/algorithms/pattern_generation.hpp +++ b/include/mockturtle/algorithms/pattern_generation.hpp @@ -32,36 +32,30 @@ #pragma once -#include -#include #include "../utils/progress_bar.hpp" #include "../utils/stopwatch.hpp" -#include -#include -#include -#include -#include #include +#include +#include +#include +#include +#include +#include +#include namespace mockturtle { -struct patgen_params +struct pattern_generation_params { - /*! \brief Whether to substitute constant nodes. */ + /*! \brief Whether to remove constant nodes. Requires `substitute_node`. */ bool substitute_const{true}; /*! \brief Number of patterns each node should have for both values. */ uint32_t num_stuck_at{1}; - /*! \brief Fanout levels to consider for observability. -1 = no limit. */ - int odc_levels{-1}; - - /*! \brief Whether to check and re-generate type 1 observable patterns. */ - bool observability_type1{false}; - - /*! \brief Whether to check and re-generate type 2 observable patterns. */ - bool observability_type2{false}; + /*! \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}; @@ -74,13 +68,17 @@ struct patgen_params /*! \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 patgen_stats +struct pattern_generation_stats { + /*! \brief Total time. */ stopwatch<>::duration time_total{0}; - /*! \brief Time for simulations. */ + /*! \brief Time for simulation. */ stopwatch<>::duration time_sim{0}; /*! \brief Time for SAT solving. */ @@ -89,23 +87,20 @@ struct patgen_stats /*! \brief Time for ODC computation */ stopwatch<>::duration time_odc{0}; - /*! \brief Number of constant nodes found. */ + /*! \brief Number of constant nodes. */ uint32_t num_constant{0}; /*! \brief Number of generated patterns. */ uint32_t num_generated_patterns{0}; - /*! \brief Number of type1 unobservable nodes. */ + /*! \brief Number of stuck-at patterns that is re-generated because the original one was unobservable. */ uint32_t unobservable_type1{0}; - /*! \brief Number of resolved type1 unobservable nodes. */ - uint32_t unobservable_type1_resolved{0}; - - /*! \brief Number of type2 unobservable nodes. */ + /*! \brief Number of additional patterns generated because the node was unobservable with one value. */ uint32_t unobservable_type2{0}; - /*! \brief Number of resolved type2 unobservable nodes. */ - uint32_t unobservable_type2_resolved{0}; + /*! \brief Number of unobservable nodes (node for which an observable pattern can not be found). */ + uint32_t unobservable_node{0}; }; namespace detail @@ -119,10 +114,11 @@ class patgen_impl using signal = typename Ntk::signal; using TT = unordered_node_map; - explicit patgen_impl( Ntk& ntk, partial_simulator& sim, patgen_params const& ps, validator_params& vps, patgen_stats& st ) - : ntk( ntk ), ps( ps ), st( st ), vps( vps ), validator( ntk, vps ), - tts( ntk ), sim( sim ) - { } + 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() { @@ -130,7 +126,7 @@ class patgen_impl call_with_stopwatch( st.time_sim, [&]() { simulate_nodes( ntk, tts, sim ); - }); + } ); if ( ps.num_stuck_at > 0 ) { @@ -149,10 +145,7 @@ class patgen_impl if constexpr ( use_odc ) { - if ( ps.observability_type2 ) - { - observability_check(); - } + observability_check(); } } @@ -163,67 +156,64 @@ class patgen_impl kitty::partial_truth_table zero = sim.compute_constant( false ); - ntk.foreach_gate( [&]( auto const& n, auto i ) - { + 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 ); - }); + } ); } - if ( (tts[n] == zero) || (tts[n] == ~zero) ) + if ( ( tts[n] == zero ) || ( tts[n] == ~zero ) ) { - bool value = (tts[n] == zero); /* wanted value of n */ - + 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 */ + else if ( !( *res ) ) /* SAT, pattern found */ { if constexpr ( use_odc ) { - if ( ps.observability_type1 ) + /* 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 ) { - /* 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 ) { - if ( ps.verbose ) - { - std::cout << "\t[i] generated pattern is not observable (type 1). node: " << n << ", with value " << value << "\n" ; - } - ++st.unobservable_type1; - const auto res2 = call_with_stopwatch( st.time_sat, [&]() { - vps.odc_levels = ps.odc_levels; - return validator.validate( n, !value ); - }); - if ( res2 ) + 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 ) ) { - if ( !(*res2) ) + ++st.unobservable_type1; + if ( ps.verbose ) { - ++st.unobservable_type1_resolved; - if ( ps.verbose ) - { - assert( pattern_is_observable( ntk, n, validator.cex, ps.odc_levels ) ); - std::cout << "\t[i] unobservable pattern resolved.\n"; - } + assert( pattern_is_observable( ntk, n, validator.cex, ps.odc_levels ) ); + std::cout << "\t\t[i] unobservable pattern resolved.\n"; } - else + } + else + { + ++st.unobservable_node; + if ( ps.verbose ) { - if ( ps.verbose ) - { - std::cout << "\t[i] unobservable node " << n << "\n"; - } + std::cout << "\t\t[i] unobservable node " << n << "\n"; } } } @@ -234,7 +224,10 @@ class patgen_impl if ( ps.num_stuck_at > 1 ) { - auto generated = validator.generate_pattern( n, value, {validator.cex}, 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 ); @@ -268,49 +261,56 @@ class patgen_impl void observability_check() { - progress_bar pbar{ntk.size(), "patgen-obs2 |{0}| node = {1:>4} #pat = {2:>4}", ps.progress}; + progress_bar pbar{ntk.size(), "patgen-obs |{0}| node = {1:>4} #pat = {2:>4}", ps.progress}; - ntk.foreach_gate( [&]( auto const& n, auto i ) - { + 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 */ + } + } + /* compute ODC */ - auto odc = call_with_stopwatch( st.time_odc, [&]() { - return observability_dont_cares( ntk, n, sim, tts, ps.odc_levels ); - }); + 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 */ + /* check if under non-ODCs n is always the same value */ if ( ( tts[n] & ~odc ) == sim.compute_constant( false ) ) { if ( ps.verbose ) { std::cout << "\t[i] under all observable patterns, node " << n << " is always 0 (type 2).\n"; } - ++st.unobservable_type2; const auto res = call_with_stopwatch( st.time_sat, [&]() { vps.odc_levels = ps.odc_levels; return validator.validate( n, false ); - }); + } ); if ( res ) { - if ( !(*res) ) + if ( !( *res ) ) { new_pattern( validator.cex ); - ++st.unobservable_type2_resolved; + ++st.unobservable_type2; - if ( ps.verbose ) + if ( ps.verbose ) { - auto odc2 = call_with_stopwatch( st.time_odc, [&]() { return observability_dont_cares( ntk, n, sim, tts, ps.odc_levels ); }); + 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[i] added generated pattern to resolve unobservability.\n"; + std::cout << "\t\t[i] added generated pattern to resolve unobservability.\n"; } } else { + ++st.unobservable_node; if ( ps.verbose ) { - std::cout << "\t[i] unobservable node " << n << "\n"; + std::cout << "\t\t[i] unobservable node " << n << "\n"; } } } @@ -321,31 +321,31 @@ class patgen_impl { std::cout << "\t[i] under all observable patterns, node " << n << " is always 1 (type 2).\n"; } - ++st.unobservable_type2; const auto res = call_with_stopwatch( st.time_sat, [&]() { vps.odc_levels = ps.odc_levels; return validator.validate( n, true ); - }); + } ); if ( res ) { - if ( !(*res) ) + if ( !( *res ) ) { new_pattern( validator.cex ); - ++st.unobservable_type2_resolved; + ++st.unobservable_type2; - if ( ps.verbose ) + if ( ps.verbose ) { - auto odc2 = call_with_stopwatch( st.time_odc, [&]() { return observability_dont_cares( ntk, n, sim, tts, ps.odc_levels ); }); + 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[i] added generated pattern to resolve unobservability.\n"; + std::cout << "\t\t[i] added generated pattern to resolve unobservability.\n"; } } else { + ++st.unobservable_node; if ( ps.verbose ) { - std::cout << "\t[i] unobservable node " << n << "\n"; + std::cout << "\t\t[i] unobservable node " << n << "\n"; } } } @@ -366,7 +366,7 @@ class patgen_impl { call_with_stopwatch( st.time_sim, [&]() { simulate_nodes( ntk, tts, sim, false ); - }); + } ); } } @@ -379,13 +379,16 @@ class patgen_impl if ( kitty::get_bit( tt, i ) == value ) { patterns.emplace_back(); - ntk.foreach_pi( [&]( auto const& pi ){ + ntk.foreach_pi( [&]( auto const& pi ) { patterns.back().emplace_back( kitty::get_bit( tts[pi], i ) ); - }); + } ); } } - auto generated = validator.generate_pattern( n, value, patterns, ps.num_stuck_at - patterns.size() ); + 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 ); @@ -396,12 +399,12 @@ class patgen_impl private: Ntk& ntk; - patgen_params const& ps; - patgen_stats& st; + pattern_generation_params const& ps; + pattern_generation_stats& st; validator_params& vps; - circuit_validator validator; - + circuit_validator validator; + TT tts; std::vector const_nodes; @@ -410,28 +413,41 @@ class patgen_impl } /* 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 `sim.write_patterns( filename )` + * or directly be used by passing the simulator to another algorithm. + */ template -void pattern_generation( Ntk& ntk, partial_simulator& sim, patgen_params const& ps = {}, patgen_stats* pst = nullptr ) +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_fanin_v, "Ntk does not implement the foreach_fanin method" ); static_assert( has_foreach_gate_v, "Ntk does not implement the foreach_gate method" ); - static_assert( has_foreach_node_v, "Ntk does not implement the foreach_node method" ); - static_assert( has_get_constant_v, "Ntk does not implement the get_constant 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( has_substitute_node_v, "Ntk does not implement the has substitute_node method" ); - patgen_stats st; + 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.observability_type1 || ps.observability_type2 ) + if ( ps.odc_levels != 0 ) { using fanout_view_t = fanout_view; - fanout_view fanout_view{ntk}; + fanout_view_t fanout_view{ntk}; detail::patgen_impl p( fanout_view, sim, ps, vps, st ); p.run(); From d78b871cd1b5986fd5c67a68560f29b873f18e73 Mon Sep 17 00:00:00 2001 From: Sonia Date: Thu, 2 Jul 2020 11:47:31 +0200 Subject: [PATCH 14/23] add includes --- include/mockturtle/mockturtle.hpp | 2 ++ 1 file changed, 2 insertions(+) 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" From 4e9318d58bf708da8084aec5c22b4cdb87ff5793 Mon Sep 17 00:00:00 2001 From: Sonia Date: Thu, 2 Jul 2020 11:47:41 +0200 Subject: [PATCH 15/23] add docs --- docs/algorithms/pattern_generation.rst | 38 ++++++++++++++++++++++++++ 1 file changed, 38 insertions(+) create mode 100644 docs/algorithms/pattern_generation.rst diff --git a/docs/algorithms/pattern_generation.rst b/docs/algorithms/pattern_generation.rst new file mode 100644 index 000000000..85bd1edfe --- /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 ); + sim.write_patterns( "patterns.pat" ); + + +Parameters and statistics +~~~~~~~~~~~~~~~~~~~~~~~~~ + +.. doxygenstruct:: mockturtle::pattern_generation_params + :members: + +.. doxygenstruct:: mockturtle::pattern_generation_stats + :members: + +Algorithm +~~~~~~~~~ + +.. doxygenfunction:: mockturtle::pattern_generation From 245381c5ed34ddc5609e25257307d8bbd10f64f6 Mon Sep 17 00:00:00 2001 From: Sonia Date: Thu, 2 Jul 2020 17:55:12 +0200 Subject: [PATCH 16/23] solve several bugs related to observability --- .../algorithms/circuit_validator.hpp | 49 ++++++++++++++++--- include/mockturtle/algorithms/dont_cares.hpp | 33 +++++++++++-- .../algorithms/pattern_generation.hpp | 21 ++++++-- include/mockturtle/algorithms/simulation.hpp | 15 +++--- 4 files changed, 97 insertions(+), 21 deletions(-) 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 309df6bf7..995c7217c 100644 --- a/include/mockturtle/algorithms/dont_cares.hpp +++ b/include/mockturtle/algorithms/dont_cares.hpp @@ -150,27 +150,52 @@ void clearTFO_rec( Ntk const& ntk, unordered_node_map& ttsNOT, node +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 */ /* Compute the don't care input patterns in the partial simulator `sim` of node `n` with respect to `roots` such that under these PI patterns the value of n doesn't affect outputs of roots. */ template -kitty::partial_truth_table observability_dont_cares( Ntk const& ntk, node const& n, partial_simulator const& sim, unordered_node_map const& tts, int levels = -1 ) +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 ); }); - unordered_node_map ttsNOT = tts.copy(); // same as tts except for TFOs + 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]; - simulate_nodes( ntk, ttsNOT, sim ); + 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 ) { - care |= tts[r] ^ ttsNOT[r]; + if ( tts[r].num_bits() == care.num_bits() ) + { + care |= tts[r] ^ ttsNOT[r]; + } } return ~care; } diff --git a/include/mockturtle/algorithms/pattern_generation.hpp b/include/mockturtle/algorithms/pattern_generation.hpp index 748bd3f90..997d41258 100644 --- a/include/mockturtle/algorithms/pattern_generation.hpp +++ b/include/mockturtle/algorithms/pattern_generation.hpp @@ -165,6 +165,7 @@ class patgen_impl simulate_node( ntk, n, tts, sim ); } ); } + assert( zero.num_bits() == sim.num_bits() ); if ( ( tts[n] == zero ) || ( tts[n] == ~zero ) ) { @@ -263,6 +264,8 @@ class patgen_impl { 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() ); @@ -274,13 +277,21 @@ class patgen_impl } } + 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 ) == sim.compute_constant( false ) ) + if ( ( tts[n] & ~odc ) == zero ) { if ( ps.verbose ) { @@ -304,6 +315,8 @@ class patgen_impl 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 { @@ -315,7 +328,7 @@ class patgen_impl } } } - else if ( ( tts[n] | odc ) == sim.compute_constant( true ) ) + else if ( ( tts[n] | odc ) == ~zero ) { if ( ps.verbose ) { @@ -339,6 +352,8 @@ class patgen_impl 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 { @@ -403,7 +418,7 @@ class patgen_impl pattern_generation_stats& st; validator_params& vps; - circuit_validator validator; + circuit_validator validator; TT tts; std::vector const_nodes; diff --git a/include/mockturtle/algorithms/simulation.hpp b/include/mockturtle/algorithms/simulation.hpp index 9dad2e2a6..b45115fc3 100644 --- a/include/mockturtle/algorithms/simulation.hpp +++ b/include/mockturtle/algorithms/simulation.hpp @@ -483,10 +483,10 @@ void update_const_pi( Ntk const& ntk, unordered_node_map @@ -505,8 +505,11 @@ void simulate_node( Ntk const& ntk, typename Ntk::node const& n, unordered_node_ { 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 ); } From 8b37d8de20970cf0724f00d6e0d96c5e7ec40fae Mon Sep 17 00:00:00 2001 From: Sonia Date: Thu, 2 Jul 2020 18:12:13 +0200 Subject: [PATCH 17/23] update docs --- include/mockturtle/algorithms/dont_cares.hpp | 37 ++++++++++++++------ 1 file changed, 26 insertions(+), 11 deletions(-) diff --git a/include/mockturtle/algorithms/dont_cares.hpp b/include/mockturtle/algorithms/dont_cares.hpp index 995c7217c..3d2857cac 100644 --- a/include/mockturtle/algorithms/dont_cares.hpp +++ b/include/mockturtle/algorithms/dont_cares.hpp @@ -146,7 +146,7 @@ void clearTFO_rec( Ntk const& ntk, unordered_node_map& ttsNOT, node const& n, partial_simulator con } ntk.foreach_fanout( n, [&]( auto const& fo ){ - simulate_TFO_rec( ntk, fo, sim, tts, level - 1 ); + simulate_TFO_rec( ntk, fo, sim, tts, level - 1 ); }); } } /* namespace detail */ -/* Compute the don't care input patterns in the partial simulator `sim` of node `n` with respect to `roots` -such that under these PI patterns the value of n doesn't affect outputs of roots. */ +/*! \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 ) { @@ -200,20 +211,24 @@ kitty::partial_truth_table observability_dont_cares( Ntk const& ntk, node c return ~care; } -/* Check if node `n` is observable with respect to `roots` -such that under input assignment `pattern` the value of `n` doesn't affect outputs of `roots`. -Returns true if is observable. (at least one PO is affected) */ +/*! \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); - unordered_node_map ttsNOT(ntk); + default_simulator sim( pattern ); + unordered_node_map tts( ntk ); simulate_nodes( ntk, tts, sim ); - simulate_nodes( ntk, ttsNOT, sim ); // copying doesn't work for unordered_node_map, not sure why + unordered_node_map ttsNOT = tts.copy(); ntk.incr_trav_id(); detail::clearTFO_rec( ntk, ttsNOT, n, roots, levels ); From b8503a54dc7e5b1bb6a12ea6178b13ed6d6da608 Mon Sep 17 00:00:00 2001 From: Sonia Date: Thu, 2 Jul 2020 18:18:02 +0200 Subject: [PATCH 18/23] clean up experiment --- experiments/pattern_generation.cpp | 21 +-- experiments/pattern_generation.json | 190 ++++++++++++++-------------- 2 files changed, 99 insertions(+), 112 deletions(-) diff --git a/experiments/pattern_generation.cpp b/experiments/pattern_generation.cpp index 33ebfcb33..ab2b3558a 100644 --- a/experiments/pattern_generation.cpp +++ b/experiments/pattern_generation.cpp @@ -45,34 +45,21 @@ int main() for ( auto const& benchmark : epfl_benchmarks() ) { - //if ( benchmark != "iwls2005/mem_ctrl" ) continue; - fmt::print( "[i] processing {}\n", benchmark ); aig_network aig; lorina::read_aiger( benchmark_path( benchmark ), aiger_reader( aig ) ); auto size_before = aig.num_gates(); - patgen_params ps; - patgen_stats st; - - uint32_t num_random_pattern = 256; - std::string write_pats = "256sa1/" + benchmark + ".pat"; + pattern_generation_params ps; + pattern_generation_stats st; - ps.num_stuck_at = 1; - //ps.observability_type1 = true; - //ps.observability_type2 = true; - //ps.odc_levels = 5; - ps.random_seed = 1689; - ps.progress = false; - //ps.verbose = true; + uint32_t num_random_pattern = 1000; - partial_simulator sim( aig.num_pis(), num_random_pattern, ps.random_seed ); + partial_simulator sim( aig.num_pis(), num_random_pattern ); pattern_generation( aig, sim, ps, &st ); aig = cleanup_dangling( aig ); - sim.write_patterns( write_pats ); - const auto cec = benchmark == "hyp" ? true : abc_cec( aig, benchmark ); 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 ), cec ); } diff --git a/experiments/pattern_generation.json b/experiments/pattern_generation.json index 05d3dee05..f921405b5 100644 --- a/experiments/pattern_generation.json +++ b/experiments/pattern_generation.json @@ -4,244 +4,244 @@ { "#PI": 256, "#const": 0, - "#pat": 256, + "#pat": 1000, "#pat gen": 0, "benchmark": "adder", "cec": true, "size": 1020, "t_SAT": 0.0, - "t_sim": 0.0014159049605950713, - "t_total": 0.0015550010139122605 + "t_sim": 0.0016803749604150653, + "t_total": 0.0018321579555049539 }, { "#PI": 135, "#const": 0, - "#pat": 256, + "#pat": 1000, "#pat gen": 0, "benchmark": "bar", "cec": true, "size": 3336, "t_SAT": 0.0, - "t_sim": 0.004492159001529217, - "t_total": 0.004908484872430563 + "t_sim": 0.00415766192600131, + "t_total": 0.004529781173914671 }, { "#PI": 128, "#const": 8, - "#pat": 279, - "#pat gen": 23, + "#pat": 1039, + "#pat gen": 39, "benchmark": "div", "cec": true, "size": 57247, - "t_SAT": 0.09047292917966843, - "t_sim": 0.1637018471956253, - "t_total": 0.27369004487991333 + "t_SAT": 0.14518830180168152, + "t_sim": 0.25494495034217834, + "t_total": 0.4186662435531616 }, { "#PI": 256, "#const": 2, - "#pat": 260, - "#pat gen": 4, + "#pat": 1003, + "#pat gen": 3, "benchmark": "hyp", "cec": true, "size": 214335, - "t_SAT": 0.0010707159526646137, - "t_sim": 0.523285984992981, - "t_total": 0.6091689467430115 + "t_SAT": 0.00020622399460989982, + "t_sim": 0.4722563922405243, + "t_total": 0.5475164651870728 }, { "#PI": 32, - "#const": 161, - "#pat": 425, - "#pat gen": 169, + "#const": 162, + "#pat": 1093, + "#pat gen": 93, "benchmark": "log2", "cec": true, "size": 32060, - "t_SAT": 17.49126434326172, - "t_sim": 0.2002258002758026, - "t_total": 17.75943946838379 + "t_SAT": 13.866494178771973, + "t_sim": 0.1926172524690628, + "t_total": 14.143054008483887 }, { "#PI": 512, "#const": 0, - "#pat": 256, + "#pat": 1000, "#pat gen": 0, "benchmark": "max", "cec": true, "size": 2865, "t_SAT": 0.0, - "t_sim": 0.00374211510643363, - "t_total": 0.004087099805474281 + "t_sim": 0.0038299409206956625, + "t_total": 0.004194580018520355 }, { "#PI": 128, "#const": 0, - "#pat": 257, - "#pat gen": 1, + "#pat": 1008, + "#pat gen": 8, "benchmark": "multiplier", "cec": true, "size": 27062, - "t_SAT": 8.262100163847208e-05, - "t_sim": 0.060651980340480804, - "t_total": 0.06559254974126816 + "t_SAT": 0.00030344800325110555, + "t_sim": 0.08712013810873032, + "t_total": 0.09432054311037064 }, { "#PI": 24, "#const": 19, - "#pat": 339, - "#pat gen": 83, + "#pat": 1049, + "#pat gen": 49, "benchmark": "sin", "cec": true, "size": 5416, - "t_SAT": 0.5215885639190674, - "t_sim": 0.04783011972904205, - "t_total": 0.5729691386222839 + "t_SAT": 0.5346160531044006, + "t_sim": 0.0467601902782917, + "t_total": 0.5848844647407532 }, { "#PI": 128, "#const": 0, - "#pat": 256, + "#pat": 1000, "#pat gen": 0, "benchmark": "sqrt", "cec": true, "size": 24618, "t_SAT": 0.0, - "t_sim": 0.031034482643008232, - "t_total": 0.034022312611341476 + "t_sim": 0.032021693885326385, + "t_total": 0.03555260971188545 }, { "#PI": 64, "#const": 0, - "#pat": 256, - "#pat gen": 0, + "#pat": 1003, + "#pat gen": 3, "benchmark": "square", "cec": true, "size": 18484, - "t_SAT": 0.0, - "t_sim": 0.02168254181742668, - "t_total": 0.023898186162114143 + "t_SAT": 6.535099964821711e-05, + "t_sim": 0.04998838156461716, + "t_total": 0.05557524040341377 }, { "#PI": 256, "#const": 0, - "#pat": 259, - "#pat gen": 3, + "#pat": 1005, + "#pat gen": 5, "benchmark": "arbiter", "cec": true, "size": 11839, - "t_SAT": 0.00020269300148356706, - "t_sim": 0.013296888209879398, - "t_total": 0.014842754229903221 + "t_SAT": 0.0002797770139295608, + "t_sim": 0.01623448356986046, + "t_total": 0.018196318298578262 }, { "#PI": 10, "#const": 0, - "#pat": 261, - "#pat gen": 5, + "#pat": 1007, + "#pat gen": 7, "benchmark": "cavlc", "cec": true, "size": 693, - "t_SAT": 0.00010404200293123722, - "t_sim": 0.0017267799703404307, - "t_total": 0.0019697370007634163 + "t_SAT": 0.00019342100131325424, + "t_sim": 0.003920386079698801, + "t_total": 0.004497550893574953 }, { "#PI": 7, "#const": 0, - "#pat": 256, - "#pat gen": 0, + "#pat": 1008, + "#pat gen": 8, "benchmark": "ctrl", "cec": true, "size": 174, - "t_SAT": 0.0, - "t_sim": 0.00019234500359743834, - "t_total": 0.00021304399706423283 + "t_SAT": 0.00012525799684226513, + "t_sim": 0.0009255249751731753, + "t_total": 0.0011550389463081956 }, { "#PI": 8, "#const": 0, - "#pat": 421, - "#pat gen": 165, + "#pat": 1206, + "#pat gen": 206, "benchmark": "dec", "cec": true, "size": 304, - "t_SAT": 0.001692189951427281, - "t_sim": 0.0021870590280741453, - "t_total": 0.004020167980343103 + "t_SAT": 0.0034190660808235407, + "t_sim": 0.0037710380274802446, + "t_total": 0.007420113775879145 }, { "#PI": 147, "#const": 0, - "#pat": 302, - "#pat gen": 46, + "#pat": 1039, + "#pat gen": 39, "benchmark": "i2c", "cec": true, "size": 1342, - "t_SAT": 0.0016219819663092494, - "t_sim": 0.004550343845039606, - "t_total": 0.006605285219848156 + "t_SAT": 0.001595249050296843, + "t_sim": 0.006564381066709757, + "t_total": 0.00864330679178238 }, { "#PI": 11, "#const": 0, - "#pat": 257, - "#pat gen": 1, + "#pat": 1003, + "#pat gen": 3, "benchmark": "int2float", "cec": true, "size": 260, - "t_SAT": 1.3675999980478082e-05, - "t_sim": 0.0004994070040993392, - "t_total": 0.000562014989554882 + "t_SAT": 3.752100019482896e-05, + "t_sim": 0.001217360026203096, + "t_total": 0.0013280409621074796 }, { "#PI": 1204, "#const": 1, - "#pat": 734, - "#pat gen": 478, + "#pat": 1406, + "#pat gen": 406, "benchmark": "mem_ctrl", "cec": true, "size": 46836, - "t_SAT": 0.09079248458147049, - "t_sim": 0.5077462196350098, - "t_total": 0.6229751706123352 + "t_SAT": 0.1007600799202919, + "t_sim": 0.5675763487815857, + "t_total": 0.6968528032302856 }, { "#PI": 128, "#const": 0, - "#pat": 267, - "#pat gen": 11, + "#pat": 1001, + "#pat gen": 1, "benchmark": "priority", "cec": true, "size": 978, - "t_SAT": 0.0006275969790294766, - "t_sim": 0.002462324919179082, - "t_total": 0.0032959720119833946 + "t_SAT": 6.559900066349655e-05, + "t_sim": 0.0021323850378394127, + "t_total": 0.0024593030102550983 }, { "#PI": 60, "#const": 0, - "#pat": 307, - "#pat gen": 51, + "#pat": 1046, + "#pat gen": 46, "benchmark": "router", "cec": true, "size": 257, - "t_SAT": 0.001450460054911673, - "t_sim": 0.0036068339832127094, - "t_total": 0.005179498810321093 + "t_SAT": 0.0013123319949954748, + "t_sim": 0.0042546889744699, + "t_total": 0.005717279855161905 }, { "#PI": 1001, - "#const": 5, - "#pat": 305, - "#pat gen": 49, + "#const": 4, + "#pat": 1009, + "#pat gen": 9, "benchmark": "voter", "cec": true, "size": 13758, - "t_SAT": 2.65531587600708, - "t_sim": 0.2700190246105194, - "t_total": 2.9297537803649902 + "t_SAT": 1.2413805723190308, + "t_sim": 0.10608454793691635, + "t_total": 1.3518118858337402 } ], - "version": "c0a76a4" + "version": "4e9318d" } ] From d5873d4eef9c99f9161d5683e9a66d9f644246a0 Mon Sep 17 00:00:00 2001 From: Sonia Date: Thu, 2 Jul 2020 21:06:04 +0200 Subject: [PATCH 19/23] add tests --- test/algorithms/pattern_generation.cpp | 119 +++++++++++++++++++++++++ 1 file changed, 119 insertions(+) create mode 100644 test/algorithms/pattern_generation.cpp diff --git a/test/algorithms/pattern_generation.cpp b/test/algorithms/pattern_generation.cpp new file mode 100644 index 000000000..bdb0e9750 --- /dev/null +++ b/test/algorithms/pattern_generation.cpp @@ -0,0 +1,119 @@ +#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( aig, sim ); + + 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 ); +} From e873eb7820843dc05c252c3191cc0dd0d3770296 Mon Sep 17 00:00:00 2001 From: Sonia Date: Fri, 3 Jul 2020 13:01:52 +0200 Subject: [PATCH 20/23] yet another bug --- include/mockturtle/algorithms/simulation.hpp | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/include/mockturtle/algorithms/simulation.hpp b/include/mockturtle/algorithms/simulation.hpp index b45115fc3..6a7b21391 100644 --- a/include/mockturtle/algorithms/simulation.hpp +++ b/include/mockturtle/algorithms/simulation.hpp @@ -501,6 +501,11 @@ 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 ) ); @@ -519,10 +524,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 ); } } From 66a162db5170775e09cc3e725a734981ec9dc053 Mon Sep 17 00:00:00 2001 From: Sonia Date: Fri, 3 Jul 2020 14:40:50 +0200 Subject: [PATCH 21/23] change default value of substitute_const --- include/mockturtle/algorithms/pattern_generation.hpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/include/mockturtle/algorithms/pattern_generation.hpp b/include/mockturtle/algorithms/pattern_generation.hpp index 997d41258..a6039f74e 100644 --- a/include/mockturtle/algorithms/pattern_generation.hpp +++ b/include/mockturtle/algorithms/pattern_generation.hpp @@ -49,7 +49,7 @@ namespace mockturtle struct pattern_generation_params { /*! \brief Whether to remove constant nodes. Requires `substitute_node`. */ - bool substitute_const{true}; + bool substitute_const{false}; /*! \brief Number of patterns each node should have for both values. */ uint32_t num_stuck_at{1}; From 32167e74f4c32b2784df3c9b7d74eebd9af393b3 Mon Sep 17 00:00:00 2001 From: Sonia Date: Fri, 3 Jul 2020 15:10:30 +0200 Subject: [PATCH 22/23] updates according to the change of default value --- experiments/pattern_generation.cpp | 8 +- experiments/pattern_generation.json | 134 +++++++++++-------------- test/algorithms/pattern_generation.cpp | 4 +- 3 files changed, 62 insertions(+), 84 deletions(-) diff --git a/experiments/pattern_generation.cpp b/experiments/pattern_generation.cpp index ab2b3558a..a7e5ffd9b 100644 --- a/experiments/pattern_generation.cpp +++ b/experiments/pattern_generation.cpp @@ -41,7 +41,7 @@ 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", "cec" ); + experiment exp( "pattern_generation", "benchmark", "#PI", "size", "#pat", "#pat gen", "#const", "t_total", "t_sim", "t_SAT" ); for ( auto const& benchmark : epfl_benchmarks() ) { @@ -54,14 +54,10 @@ int main() 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 ); - aig = cleanup_dangling( aig ); - const auto cec = benchmark == "hyp" ? true : abc_cec( aig, benchmark ); - 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 ), cec ); + 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(); diff --git a/experiments/pattern_generation.json b/experiments/pattern_generation.json index f921405b5..e409371fc 100644 --- a/experiments/pattern_generation.json +++ b/experiments/pattern_generation.json @@ -7,11 +7,10 @@ "#pat": 1000, "#pat gen": 0, "benchmark": "adder", - "cec": true, "size": 1020, "t_SAT": 0.0, - "t_sim": 0.0016803749604150653, - "t_total": 0.0018321579555049539 + "t_sim": 0.002587138907983899, + "t_total": 0.0027476809918880463 }, { "#PI": 135, @@ -19,11 +18,10 @@ "#pat": 1000, "#pat gen": 0, "benchmark": "bar", - "cec": true, "size": 3336, "t_SAT": 0.0, - "t_sim": 0.00415766192600131, - "t_total": 0.004529781173914671 + "t_sim": 0.011206761002540588, + "t_total": 0.012046649120748043 }, { "#PI": 128, @@ -31,11 +29,10 @@ "#pat": 1039, "#pat gen": 39, "benchmark": "div", - "cec": true, "size": 57247, - "t_SAT": 0.14518830180168152, - "t_sim": 0.25494495034217834, - "t_total": 0.4186662435531616 + "t_SAT": 0.23106683790683746, + "t_sim": 0.3988635838031769, + "t_total": 0.6502119302749634 }, { "#PI": 256, @@ -43,11 +40,10 @@ "#pat": 1003, "#pat gen": 3, "benchmark": "hyp", - "cec": true, "size": 214335, - "t_SAT": 0.00020622399460989982, - "t_sim": 0.4722563922405243, - "t_total": 0.5475164651870728 + "t_SAT": 0.00014847799320705235, + "t_sim": 0.6856793761253357, + "t_total": 0.7315340042114258 }, { "#PI": 32, @@ -55,11 +51,10 @@ "#pat": 1093, "#pat gen": 93, "benchmark": "log2", - "cec": true, "size": 32060, - "t_SAT": 13.866494178771973, - "t_sim": 0.1926172524690628, - "t_total": 14.143054008483887 + "t_SAT": 23.7200870513916, + "t_sim": 0.4002784192562103, + "t_total": 24.13776969909668 }, { "#PI": 512, @@ -67,11 +62,10 @@ "#pat": 1000, "#pat gen": 0, "benchmark": "max", - "cec": true, "size": 2865, "t_SAT": 0.0, - "t_sim": 0.0038299409206956625, - "t_total": 0.004194580018520355 + "t_sim": 0.006821795832365751, + "t_total": 0.007972832769155502 }, { "#PI": 128, @@ -79,11 +73,10 @@ "#pat": 1008, "#pat gen": 8, "benchmark": "multiplier", - "cec": true, "size": 27062, - "t_SAT": 0.00030344800325110555, - "t_sim": 0.08712013810873032, - "t_total": 0.09432054311037064 + "t_SAT": 0.0003024929901584983, + "t_sim": 0.12204926460981369, + "t_total": 0.13171681761741638 }, { "#PI": 24, @@ -91,11 +84,10 @@ "#pat": 1049, "#pat gen": 49, "benchmark": "sin", - "cec": true, "size": 5416, - "t_SAT": 0.5346160531044006, - "t_sim": 0.0467601902782917, - "t_total": 0.5848844647407532 + "t_SAT": 0.7237713932991028, + "t_sim": 0.06233770772814751, + "t_total": 0.788311243057251 }, { "#PI": 128, @@ -103,11 +95,10 @@ "#pat": 1000, "#pat gen": 0, "benchmark": "sqrt", - "cec": true, "size": 24618, "t_SAT": 0.0, - "t_sim": 0.032021693885326385, - "t_total": 0.03555260971188545 + "t_sim": 0.04817450791597366, + "t_total": 0.05268986523151398 }, { "#PI": 64, @@ -115,11 +106,10 @@ "#pat": 1003, "#pat gen": 3, "benchmark": "square", - "cec": true, "size": 18484, - "t_SAT": 6.535099964821711e-05, - "t_sim": 0.04998838156461716, - "t_total": 0.05557524040341377 + "t_SAT": 6.385899905581027e-05, + "t_sim": 0.060539085417985916, + "t_total": 0.06628058850765228 }, { "#PI": 256, @@ -127,11 +117,10 @@ "#pat": 1005, "#pat gen": 5, "benchmark": "arbiter", - "cec": true, "size": 11839, - "t_SAT": 0.0002797770139295608, - "t_sim": 0.01623448356986046, - "t_total": 0.018196318298578262 + "t_SAT": 0.00031487300293520093, + "t_sim": 0.027791135013103485, + "t_total": 0.02998867630958557 }, { "#PI": 10, @@ -139,11 +128,10 @@ "#pat": 1007, "#pat gen": 7, "benchmark": "cavlc", - "cec": true, "size": 693, - "t_SAT": 0.00019342100131325424, - "t_sim": 0.003920386079698801, - "t_total": 0.004497550893574953 + "t_SAT": 0.0001512260059826076, + "t_sim": 0.0024142060428857803, + "t_total": 0.0027767519932240248 }, { "#PI": 7, @@ -151,11 +139,10 @@ "#pat": 1008, "#pat gen": 8, "benchmark": "ctrl", - "cec": true, "size": 174, - "t_SAT": 0.00012525799684226513, - "t_sim": 0.0009255249751731753, - "t_total": 0.0011550389463081956 + "t_SAT": 0.00011831099982373416, + "t_sim": 0.0005374409956857562, + "t_total": 0.0007138170185498893 }, { "#PI": 8, @@ -163,11 +150,10 @@ "#pat": 1206, "#pat gen": 206, "benchmark": "dec", - "cec": true, "size": 304, - "t_SAT": 0.0034190660808235407, - "t_sim": 0.0037710380274802446, - "t_total": 0.007420113775879145 + "t_SAT": 0.003572395071387291, + "t_sim": 0.004423268139362335, + "t_total": 0.008258773013949394 }, { "#PI": 147, @@ -175,11 +161,10 @@ "#pat": 1039, "#pat gen": 39, "benchmark": "i2c", - "cec": true, "size": 1342, - "t_SAT": 0.001595249050296843, - "t_sim": 0.006564381066709757, - "t_total": 0.00864330679178238 + "t_SAT": 0.0019028210081160069, + "t_sim": 0.007990111596882343, + "t_total": 0.010547489859163761 }, { "#PI": 11, @@ -187,11 +172,10 @@ "#pat": 1003, "#pat gen": 3, "benchmark": "int2float", - "cec": true, "size": 260, - "t_SAT": 3.752100019482896e-05, - "t_sim": 0.001217360026203096, - "t_total": 0.0013280409621074796 + "t_SAT": 0.00011678999726427719, + "t_sim": 0.0013045240193605423, + "t_total": 0.0015592729905620217 }, { "#PI": 1204, @@ -199,11 +183,10 @@ "#pat": 1406, "#pat gen": 406, "benchmark": "mem_ctrl", - "cec": true, "size": 46836, - "t_SAT": 0.1007600799202919, - "t_sim": 0.5675763487815857, - "t_total": 0.6968528032302856 + "t_SAT": 0.12108956277370453, + "t_sim": 0.6603772640228271, + "t_total": 0.8064870834350586 }, { "#PI": 128, @@ -211,11 +194,10 @@ "#pat": 1001, "#pat gen": 1, "benchmark": "priority", - "cec": true, "size": 978, - "t_SAT": 6.559900066349655e-05, - "t_sim": 0.0021323850378394127, - "t_total": 0.0024593030102550983 + "t_SAT": 5.066599987912923e-05, + "t_sim": 0.001871931948699057, + "t_total": 0.002103254897519946 }, { "#PI": 60, @@ -223,11 +205,10 @@ "#pat": 1046, "#pat gen": 46, "benchmark": "router", - "cec": true, "size": 257, - "t_SAT": 0.0013123319949954748, - "t_sim": 0.0042546889744699, - "t_total": 0.005717279855161905 + "t_SAT": 0.0015393260400742292, + "t_sim": 0.004502872005105019, + "t_total": 0.006205921061336994 }, { "#PI": 1001, @@ -235,13 +216,12 @@ "#pat": 1009, "#pat gen": 9, "benchmark": "voter", - "cec": true, "size": 13758, - "t_SAT": 1.2413805723190308, - "t_sim": 0.10608454793691635, - "t_total": 1.3518118858337402 + "t_SAT": 1.8260704278945923, + "t_sim": 0.14073464274406433, + "t_total": 1.9711337089538574 } ], - "version": "4e9318d" + "version": "b8503a5" } ] diff --git a/test/algorithms/pattern_generation.cpp b/test/algorithms/pattern_generation.cpp index bdb0e9750..bd2855fda 100644 --- a/test/algorithms/pattern_generation.cpp +++ b/test/algorithms/pattern_generation.cpp @@ -56,7 +56,9 @@ TEST_CASE( "Constant node removal", "[pattern_generation]" ) CHECK( aig.num_gates() == 7 ); partial_simulator sim( aig.num_pis(), 0 ); - pattern_generation( aig, sim ); + pattern_generation_params ps; + ps.substitute_const = true; + pattern_generation( aig, sim, ps ); CHECK( aig.num_gates() == 6 ); } From e9a7143893ad0cf42fbf9217316cf733539d1538 Mon Sep 17 00:00:00 2001 From: Sonia Date: Fri, 3 Jul 2020 16:01:02 +0200 Subject: [PATCH 23/23] move write_patterns to io --- docs/algorithms/pattern_generation.rst | 2 +- docs/algorithms/simulation.rst | 2 +- docs/index.rst | 1 + docs/io/writers.rst | 9 +++ .../algorithms/pattern_generation.hpp | 2 +- include/mockturtle/algorithms/simulation.hpp | 16 ++-- include/mockturtle/io/write_patterns.hpp | 80 +++++++++++++++++++ test/io/write_patterns.cpp | 32 ++++++++ 8 files changed, 132 insertions(+), 12 deletions(-) create mode 100644 include/mockturtle/io/write_patterns.hpp create mode 100644 test/io/write_patterns.cpp diff --git a/docs/algorithms/pattern_generation.rst b/docs/algorithms/pattern_generation.rst index 85bd1edfe..aabbd4c77 100644 --- a/docs/algorithms/pattern_generation.rst +++ b/docs/algorithms/pattern_generation.rst @@ -20,7 +20,7 @@ patterns are then written out to a file. partial_simulator sim( aig.num_pis(), 256 ); pattern_generation( aig, sim, ps ); - sim.write_patterns( "patterns.pat" ); + write_patterns( sim, "patterns.pat" ); Parameters and statistics 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/include/mockturtle/algorithms/pattern_generation.hpp b/include/mockturtle/algorithms/pattern_generation.hpp index a6039f74e..df19f5968 100644 --- a/include/mockturtle/algorithms/pattern_generation.hpp +++ b/include/mockturtle/algorithms/pattern_generation.hpp @@ -441,7 +441,7 @@ class patgen_impl * 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 `sim.write_patterns( filename )` + * patterns can then be written out with `write_patterns` * or directly be used by passing the simulator to another algorithm. */ template diff --git a/include/mockturtle/algorithms/simulation.hpp b/include/mockturtle/algorithms/simulation.hpp index 6a7b21391..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: 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/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" ); +}