Circuit validator

docs/algorithms/circuit_validator.rst

@@ -0,0 +1,76 @@
+Functional equivalence of circuit nodes
+---------------------------------------
+
+**Header:** ``mockturtle/algorithms/circuit_validator.hpp``
+
+**Example**
+
+The following code shows how to check functional equivalence of a root node to signals existing in the network, or created with nodes within the network. If not, get the counter example.
+
+.. code-block:: c++
+
+   /* derive some AIG (can be AIG, XAG, MIG, or XMG) */
+   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 );
+
+   circuit_validator v( aig );
+
+   auto result = v.validate( f1, f2 );
+   /* result is an optional, which is nullopt if SAT conflict limit was exceeded */
+   if ( result )
+   {
+      if ( *result )
+      {
+         std::cout << "f1 and f2 are functionally equivalent\n";
+      }
+      else
+      {
+         std::cout << "f1 and f2 have different values under PI assignment: " << v.cex[0] << v.cex[1] << "\n";
+      }
+   }
+
+   circuit_validator<aig_network>::gate::fanin fi1;
+   fi1.idx = 0; fi1.inv = true;
+   circuit_validator<aig_network>::gate::fanin fi2;
+   fi2.idx = 1; fi2.inv = true;
+   circuit_validator<aig_network>::gate g;
+   g.fanins = {fi1, fi2};
+   g.type = circuit_validator::gate_type::AND;
+
+   result = v.validate( f3, {aig.get_node( f1 ), aig.get_node( f2 )}, {g}, true );
+   if ( result && *result )
+   {
+     std::cout << "f3 is equivalent to NOT(NOT f1 AND NOT f2)\n";
+   }
+
+**Parameters**
+
+.. doxygenstruct:: mockturtle::validator_params
+   :members:
+
+**Validate with existing signals**
+
+.. doxygenfunction:: mockturtle::circuit_validator::validate( signal const&, signal const& )
+.. doxygenfunction:: mockturtle::circuit_validator::validate( node const&, signal const& )
+.. doxygenfunction:: mockturtle::circuit_validator::validate( signal const&, bool )
+.. doxygenfunction:: mockturtle::circuit_validator::validate( node const&, bool )
+
+**Validate with non-existing circuit**
+
+.. doxygenstruct:: mockturtle::circuit_validator::gate
+   :members: fanins, type
+.. doxygenstruct:: mockturtle::circuit_validator::gate::fanin
+   :members: idx, inv
+
+.. doxygenfunction:: mockturtle::circuit_validator::validate( signal const&, std::vector<node> const&, std::vector<gate> const&, bool )
+.. doxygenfunction:: mockturtle::circuit_validator::validate( node const&, std::vector<node> const&, std::vector<gate> const&, bool )
+.. doxygenfunction:: mockturtle::circuit_validator::validate( signal const&, iterator_type, iterator_type, std::vector<gate> const&, bool )
+.. doxygenfunction:: mockturtle::circuit_validator::validate( node const&, iterator_type, iterator_type, std::vector<gate> const&, bool )
+
+**Updating**
+.. doxygenfunction:: mockturtle::circuit_validator::add_node
+.. doxygenfunction:: mockturtle::circuit_validator::update

docs/changelog.rst

@@ -29,9 +29,10 @@ v0.2 (not yet released)
     - Davio decomposition (`positive_davio_decomposition`, `positive_davio_decomposition`) `#308 <https://github.com/lsils/mockturtle/pull/308>`_
     - Collapse network into single node per output network `#309 <https://github.com/lsils/mockturtle/pull/309>`_
     - Generic balancing algorithm `#340 <https://github.com/lsils/mockturtle/pull/340>`_
+    - Check functional equivalence (`circuit_validator`) `#346 <https://github.com/lsils/mockturtle/pull/346>`_
 * Views:
     - Assign names to signals and outputs (`names_view`) `#181 <https://github.com/lsils/mockturtle/pull/181>`_ `#184 <https://github.com/lsils/mockturtle/pull/184>`_
-    - Creates a CNF while creating a network (`cnf_view`) `#181 <https://github.com/lsils/mockturtle/pull/274>`_ `#184 <https://github.com/lsils/mockturtle/pull/274>`_
+    - Creates a CNF while creating a network (`cnf_view`) `#274 <https://github.com/lsils/mockturtle/pull/274>`_
 * I/O:
     - Write networks to DIMACS files for CNF (`write_dimacs`) `#146 <https://github.com/lsils/mockturtle/pull/146>`_
     - Read BLIF files using *lorina* (`blif_reader`) `#167 <https://github.com/lsils/mockturtle/pull/167>`_