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 ) diff --git a/include/mockturtle/algorithms/circuit_validator.hpp b/include/mockturtle/algorithms/circuit_validator.hpp index d2eae5139..835f26691 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 ) @@ -285,6 +284,71 @@ class circuit_validator return res; } + /*! \brief Generate pattern(s) for signal `f` to be `value`, optionally blocking several known patterns. + * + * Requires `use_pushpop = true`. + * + * 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 = 1u ) + { + return generate_pattern( ntk.get_node( f ), value ^ ntk.is_complemented( f ), block_patterns, num_patterns ); + } + + /*! \brief Generate pattern(s) for node `root` to be `value`, optionally blocking several known patterns. */ + template> + std::vector> generate_pattern( node const& root, bool value, std::vector> const& block_patterns = {}, uint32_t num_patterns = 1u ) + { + 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 @@ -317,20 +381,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 ) @@ -461,7 +513,6 @@ class circuit_validator { construct( root ); } - assert( literals[root].variable() != bill::var_type( 0 ) ); std::optional res; if constexpr ( use_odc ) @@ -497,6 +548,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 ) diff --git a/test/algorithms/circuit_validator.cpp b/test/algorithms/circuit_validator.cpp index dfef6c0cd..d1c98435a 100644 --- a/test/algorithms/circuit_validator.cpp +++ b/test/algorithms/circuit_validator.cpp @@ -116,12 +116,43 @@ 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( "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] ); + } + + /* 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]" ) { /* original circuit */