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.
-
bool progress = {false}
-
struct 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.