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 forequivalence_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.
-
uint32_t conflict_limit = {0u}
-
struct equivalence_checking_stats
Statistics for equivalence_checking.
The data structure
equivalence_checking_stats
provides data collected by runningequivalence_checking
.
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 isnullopt
, if no solution can be found (this happens when a resource limit is set using the function’s parameters). Otherwise it returnstrue
, if the miter is equivalent orfalse
, if the miter is not equivalent. In the latter case the counter example is written to the statistics pointer as astd::vector<bool>
following the same order as the primary inputs.- Parameters:
miter – Miter network
ps – Parameters
st – Statistics