Equivalence checking

Header: mockturtle/algorithms/equivalence_checking.hpp

/* derive some AIG and make a copy */
aig_network aig = ...;
const auto orig = aig;

/* node resynthesis */
xag_npn_resynthesis<aig_network> resyn;
cut_rewriting_params ps;
ps.cut_enumeration_ps.cut_size = 4;
aig = cut_rewriting( aig, resyn, ps );

const auto miter = *miter<aig_network>( orig, aig );
const auto result = equivalence_checking( miter );

/* result is an optional, which is nullopt if no solution was found */
if ( result && *result )
{
  std::cout << "networks are equivalent\n";
}

Parameters and statistics

struct equivalence_checking_params

Parameters for equivalence_checking.

The data structure equivalence_checking_params holds configurable parameters with default arguments for equivalence_checking.

Public Members

uint32_t conflict_limit = {0u}

Conflict limit for SAT solver.

The default limit is 0, which means the number of conflicts is not used as a resource limit.

bool functional_reduction = {true}

Whether to apply functional reduction before SAT solving.

bool verbose = {false}

Be verbose.

struct equivalence_checking_stats

Statistics for equivalence_checking.

The data structure equivalence_checking_stats provides data collected by running equivalence_checking.

Public Members

stopwatch::duration time_total = {}

Total runtime.

std::vector<bool> counter_example

Counter-example, in case miter is not equivalent.

Algorithm

template<class Ntk>
std::optional<bool> mockturtle::equivalence_checking(Ntk const &miter, equivalence_checking_params const &ps = {}, equivalence_checking_stats *pst = nullptr)

Combinational equivalence checking.

This function expects as input a miter circuit that can be generated, e.g., with the function miter. It returns an optional which is nullopt, if no solution can be found (this happens when a resource limit is set using the function’s parameters). Otherwise it returns true, if the miter is equivalent or false, if the miter is not equivalent. In the latter case the counter example is written to the statistics pointer as a std::vector<bool> following the same order as the primary inputs.

Parameters:

• miter – Miter network

• ps – Parameters

• st – Statistics