Functional reduction

Header: mockturtle/algorithms/functional_reduction.hpp

The following example shows how to perform functional reduction to remove constant nodes and functionally equivalent nodes in the network.

/* derive some AIG */
aig_network aig = ...;

functional_reduction( aig );

Parameters and statistics

struct functional_reduction_params

Public Members

bool progress = {false}

Show progress.

bool verbose = {false}

Be verbose.

uint32_t max_iterations = {10}

Maximum number of iterations to run. 0 = repeat until no further improvement can be found.

std::optional<std::string> pattern_filename = {}

Whether to use pre-generated patterns stored in a file. If not, by default, 256 random patterns will be used.

std::optional<std::string> save_patterns = {}

Whether to save the appended patterns (with CEXs) into file.

uint32_t max_TFI_nodes = {1000}

Maximum number of nodes in the transitive fanin cone (and their fanouts) to be compared to.

uint32_t skip_fanout_limit = {100}

Maximum fanout count of a node in the transitive fanin cone to explore its fanouts.

uint32_t conflict_limit = {100}

Conflict limit for the SAT solver.

uint32_t max_clauses = {1000}

Maximum number of clauses of the SAT solver. (incremental CNF construction)

uint32_t num_patterns = {256}

Initial number of (random) simulation patterns.

uint32_t max_patterns = {1024}

Maximum number of simulation patterns. Discards all patterns and re-seeds with random patterns when exceeded.

struct functional_reduction_stats

Public Members

stopwatch::duration time_total = {0}

Total runtime.

stopwatch::duration time_sim = {0}

Time for simulation.

stopwatch::duration time_sat = {0}

Time for SAT solving.

uint32_t num_const_accepts = {0}

Number of accepted constant nodes.

uint32_t num_equ_accepts = {0}

Number of accepted functionally equivalent nodes.

uint32_t num_cex = {0}

Number of counter-examples (SAT calls).

uint32_t num_reduction = {0}

Number of successful node reductions (UNSAT calls).

uint32_t num_timeout = {0}

Number of SAT solver timeout.

Algorithm

template<class Ntk>
void mockturtle::functional_reduction(Ntk &ntk, functional_reduction_params const &ps = {}, functional_reduction_stats *pst = nullptr)

Functional reduction.

Removes constant nodes and substitute functionally equivalent nodes.