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 mockturtle::functional_reduction_params¶
Public Members
-
bool progress = {false}¶
Show progress.
-
bool verbose = {false}¶
Be verbose.
-
bool saturation = {false}¶
Whether to 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)
-
bool progress = {false}¶
-
struct mockturtle::functional_reduction_stats¶
Public Members
-
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.
-
uint32_t num_const_accepts = {0}¶
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.