Functional equivalence of circuit nodes

Header: mockturtle/algorithms/circuit_validator.hpp

This class can be used to validate potential circuit optimization choices. It checks the functional equivalence of a circuit node with an existing or non-existing signal with SAT, with optional consideration of observability don’t-care (ODC).

If more advanced SAT validation is needed, one could consider using cnf_view instead, which also constructs the CNF clauses of circuit nodes.

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.

/* 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: ";
      std::cout << v.cex[0] << v.cex[1] << "\n";
   }
}

std::vector<aig_network::node> divs;
divs.emplace_back( aig.get_node( f1 ) );
divs.emplace_back( aig.get_node( f2 ) );

xag_index_list id_list;
id_list.add_inputs( 2 );
id_list.add_and( 3, 5 ); // f3 = NOT f1 AND NOT f2
id_list.add_and( 2, 6 ); // f4 = f1 AND f3
id_list.add_output( 9 ); // NOT f4

result = v.validate( f3, divs, id_list );
if ( result && *result )
{
  std::cout << "f3 is equivalent to NOT(f1 AND (NOT f1 AND NOT f2))\n";
}

Parameters

struct validator_params

Public Members

uint32_t max_clauses = {1000}: Maximum number of clauses of the SAT solver. (incremental CNF construction)

int32_t odc_levels = {0}: Whether to consider ODC, and how many levels. 0 = No consideration. -1 = Consider TFO until PO.

uint32_t conflict_limit = {1000}: Conflict limit of the SAT solver.

uint32_t random_seed = {0}: Seed for randomized solving.

Validate with existing signals

inline std::optional<bool> mockturtle::circuit_validator::validate(signal const &f, signal const &d): Validate functional equivalence of signals f and d.

inline std::optional<bool> mockturtle::circuit_validator::validate(node const &root, signal const &d): Validate functional equivalence of node root and signal d.

inline std::optional<bool> mockturtle::circuit_validator::validate(signal const &f, bool value): Validate whether signal f is a constant of value.

inline std::optional<bool> mockturtle::circuit_validator::validate(node const &root, bool value): Validate whether node root is a constant of value.

Validate with non-existing circuit

A not-yet-created circuit built on existing nodes in the network can be represented by an index list and a list of support nodes. The index list must be one of the classes implemented in Index list.

template<class index_list_type> inline std::optional<bool> mockturtle::circuit_validator::validate(signal const &f, std::vector<node> const &divs, index_list_type const &id_list, bool inverted = false)

Validate functional equivalence of signal f with a circuit represented by an index_list.

Parameters:

id_list – The index_list representing a circuit.
divs – Existing nodes in the network, serving as PIs of id_list.
inverted – Whether to validate equivalence or inverse equivalence.

template<class index_list_type> inline std::optional<bool> mockturtle::circuit_validator::validate(node const &root, std::vector<node> const &divs, index_list_type const &id_list, bool inverted = false): Validate functional equivalence of node root with an index_list.

template<class iterator_type, class index_list_type> inline std::optional<bool> mockturtle::circuit_validator::validate(signal const &f, iterator_type divs_begin, iterator_type divs_end, index_list_type const &id_list, bool inverted = false): Validate functional equivalence of signal f with an index_list.

template<class iterator_type, class index_list_type> inline std::optional<bool> mockturtle::circuit_validator::validate(node const &root, iterator_type divs_begin, iterator_type divs_end, index_list_type const &id_list, bool inverted = false): Validate functional equivalence of node root with an index_list.

Utilizing don’t-cares

inline void mockturtle::circuit_validator::set_odc_levels(uint32_t odc_levels): Set ODC levels.

inline void mockturtle::circuit_validator::update()

Update CNF clauses.

This function should be called when the function of one or more nodes has been modified (typically when utilizing ODCs).

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<bool> 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.

template<bool enabled = use_pushpop, typename = std::enable_if_t<enabled>> inline std::vector<std::vector<bool>> mockturtle::circuit_validator::generate_pattern(signal const &f, bool value, std::vector<std::vector<bool>> const &block_patterns = {}, uint32_t num_patterns = 1u)

Generate pattern(s) for signal f to be value, optionally blocking several known patterns.

Requires use_pushpop = true, which is only supported for bsat2 and z3. If bsat2 is used, and if the network has more than 2048 PIs, the BUFFER_SIZE in lib/bill/sat/interface/abc_bsat2.hpp has to be increased to at least ntk.num_pis().

If block_patterns and the returned vector are both empty, f is validated to be a constant of !value.

Parameters:

block_patterns – Patterns to be blocked in the solver. (Will not generate any of them.)
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<bool enabled = use_pushpop, typename = std::enable_if_t<enabled>> inline std::vector<std::vector<bool>> mockturtle::circuit_validator::generate_pattern(node const &root, bool value, std::vector<std::vector<bool>> const &block_patterns = {}, uint32_t num_patterns = 1u): Generate pattern(s) for node root to be value, optionally blocking several known patterns.