Resubstitution

Header: mockturtle/algorithms/resubstitution.hpp

Several resubstitution algorithms are implemented and can be called directly, including:

  • default_resubstitution does functional reduction within a window.

  • aig_resubstitution, mig_resubstitution and xmg_resubstitution do window-based resubstitution in the corresponding network types.

  • resubstitution_minmc_withDC minimizes multiplicative complexity in XAGs with window-based resubstitution.

  • sim_resubstitution does simulation-guided resubstitution in AIGs or XAGs.

The following example shows how to resubstitute nodes in an MIG.

/* derive some MIG */
mig_network mig = ...;

/* resubstitute nodes */
mig_resubstitution( mig );
mig = cleanup_dangling( mig );

Parameters and statistics

struct resubstitution_params

Parameters for resubstitution.

The data structure resubstitution_params holds configurable parameters with default arguments for resubstitution.

Public Members

uint32_t max_pis = {8}

Maximum number of PIs of reconvergence-driven cuts.

uint32_t max_divisors = {150}

Maximum number of divisors to consider.

uint32_t max_inserts = {2}

Maximum number of nodes added by resubstitution.

uint32_t skip_fanout_limit_for_roots = {1000}

Maximum fanout of a node to be considered as root.

uint32_t skip_fanout_limit_for_divisors = {100}

Maximum fanout of a node to be considered as divisor.

bool progress = {false}

Show progress.

bool verbose = {false}

Be verbose.

bool use_dont_cares = {false}

Use don’t cares for optimization. Only used by window-based resub engine.

uint32_t window_size = {12u}

Window size for don’t cares calculation. Only used by window-based resub engine.

bool preserve_depth = {false}

Whether to prevent from increasing depth. Currently only used by window-based resub engine.

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

Whether to use pre-generated patterns stored in a file. If not, by default, 1024 random pattern + 1x stuck-at patterns will be generated. Only used by simulation-based resub engine.

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

Whether to save the appended patterns (with CEXs) into file. Only used by simulation-based resub engine.

uint32_t max_clauses = {1000}

Maximum number of clauses of the SAT solver. Only used by simulation-based resub engine.

uint32_t conflict_limit = {1000}

Conflict limit for the SAT solver. Only used by simulation-based resub engine.

uint32_t random_seed = {1}

Random seed for the SAT solver (influences the randomness of counter-examples). Only used by simulation-based resub engine.

int32_t odc_levels = {0}

Whether to utilize ODC, and how many levels. 0 = no. -1 = Consider TFO until PO. Only used by simulation-based resub engine.

uint32_t max_trials = {100}

Maximum number of trials to call the resub functor. Only used by simulation-based resub engine.

uint32_t max_divisors_k = {50}

Maximum number of divisors to consider in k-resub engine. Only used by abc_resub_functor with simulation-based resub engine.

struct resubstitution_stats

Statistics for resubstitution.

The data structure resubstitution_stats provides data collected by running resubstitution.

Public Members

stopwatch::duration time_total = {0}

Total runtime.

stopwatch::duration time_divs = {0}

Accumulated runtime of the divisor collector.

stopwatch::duration time_resub = {0}

Accumulated runtime of the resub engine.

stopwatch::duration time_callback = {0}

Accumulated runtime of the callback function.

uint64_t num_total_divisors = {0}

Total number of divisors.

uint64_t estimated_gain = {0}

Total number of gain.

uint64_t initial_size = {0}

Initial network size (before resubstitution).

Structure

In addition to the example algorithms listed above, custom resubstitution algorithms can also be composed.

Top level

First, the top-level framework detail::resubstitution_impl is built-up with a resubstitution engine and a divisor collector.

template<class Ntk, class ResubEngine = window_based_resub_engine<Ntk, kitty::dynamic_truth_table>, class DivCollector = default_divisor_collector<Ntk>>
class resubstitution_impl

The top-level resubstitution framework.

Param ResubEngine:

The engine that computes the resubtitution for a given root node and divisors. One can choose from window_based_resub_engine which does complete simulation within small windows, or simulation_based_resub_engine which does partial simulation on the whole circuit.

Param DivCollector:

Collects divisors near a given root node, and compute the potential gain (MFFC size or its variants). Currently only default_divisor_collector is implemented, but a frontier-based approach may be integrated in the future. When using window_based_resub_engine, the DivCollector should prepare three public data members: leaves, divs, and mffc (see documentation of default_divisor_collector for details). When using simulation_based_resub_engine, only divs is needed.

inline explicit mockturtle::detail::resubstitution_impl::resubstitution_impl(Ntk &ntk, resubstitution_params const &ps, resubstitution_stats &st, engine_st_t &engine_st, collector_st_t &collector_st)

Constructor of the top-level resubstitution framework.

Parameters:

  • ntk – The network to be optimized.

  • ps – Resubstitution parameters.

  • st – Top-level resubstitution statistics.

  • engine_st – Statistics of the resubstitution engine.

  • collector_st – Statistics of the divisor collector.

  • callback – Callback function when a resubstitution is found.

ResubEngine

There are two resubstitution engines implemented: window_based_resub_engine and simulation_based_resub_engine.

template<class Ntk, class TTsim, class TTdc = kitty::dynamic_truth_table, class ResubFn = default_resub_functor<Ntk, window_simulator<Ntk, TTsim>, TTdc>, typename MffcRes = uint32_t>
class window_based_resub_engine

Window-based resubstitution engine.

This engine computes the complete truth tables of nodes within a window with the leaves as inputs. It does not verify the resubstitution candidates given by the resubstitution functor. This engine requires the divisor collector to prepare three data members: leaves, divs and mffc.

Required interfaces of the resubstitution functor:

  • Constructor: resub_fn( Ntk const& ntk, Simulator const& sim, std::vector<node> const& divs, uint32_t num_divs, ResubFnSt& st )

  • A public operator(): std::optional<signal> operator() ( node const& root, TTdc care, uint32_t required, uint32_t max_inserts, MffcRes potential_gain, uint32_t& last_gain ) const

Compatible resubstitution functors implemented:

  • default_resub_functor

  • aig_resub_functor

  • mig_resub_functor

  • xmg_resub_functor

  • xag_resub_functor

  • mig_resyn_functor

Param TTsim:

Truth table type for simulation.

Param TTdc:

Truth table type for don’t-care computation.

Param ResubFn:

Resubstitution functor to compute the resubstitution.

Param MffcRes:

Typename of potential_gain needed by the resubstitution functor.

template<class Ntk, typename validator_t = circuit_validator<Ntk, bill::solvers::bsat2, false, true, false>, class ResynEngine = xag_resyn_decompose<kitty::partial_truth_table, xag_resyn_static_params_for_sim_resub<Ntk>>, typename MffcRes = uint32_t>
class simulation_based_resub_engine

Simulation-based resubstitution engine.

This engine simulates the entire network using partial truth tables and calls a resynthesis engine (template parameter ResynEngine) to find potential resubstitutions. If a resubstitution candidate is found, it then formally verifies it with SAT solving. If the validation fails, a counter-example will be added to the simulation patterns, and resynthesis will be invoked again with updated truth tables, looping until it returns std::nullopt. This engine only requires the divisor collector to prepare divs.

Please refer to the following paper for further details.

[1] A Simulation-Guided Paradigm for Logic Synthesis and Verification. TCAD, 2022.

Required interface of ResynEngine:

  • A public operator(): std::optional<index_list_t> operator() ( TT const& target, TT const& care, iterator_type begin, iterator_type end, truth_table_storage_type const& tts, uint32_t max_size )

All classes implemented in algorithms/resyn_engines/ are compatible.

Template Parameters:

  • validator_t – Specialization of circuit_validator.

  • ResynEngine – A resynthesis solver to compute the resubstitution candidate.

  • MffcRes – Typename of potential_gain.

DivCollector

Currently, there is only one implementation:

template<class Ntk, class MffcMgr = node_mffc_inside<Ntk>, typename MffcRes = uint32_t, typename cut_comp = detail::reconvergence_driven_cut_impl<Ntk>>
class default_divisor_collector

Prepare the three public data members leaves, divs and mffc to be ready for usage.

leaves: sufficient support for all divisors divs: divisor nodes that can be used for resubstitution mffc: MFFC nodes which are needed to do simulation from leaves, through divs and mffc until the root node, but should be excluded from resubstitution. The last element of mffc is always the root node.

divs and mffc are in topological order.

Param MffcMgr:

Manager class to compute the potential gain if a resubstitution exists (number of MFFC nodes when the cost function is circuit size).

Param MffcRes:

Typename of the return value of MffcMgr.

Param cut_comp:

Manager class to compute reconvergence-driven cuts.

Example

The following example shows how to compose a customized resubstitution algorithm.

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

/* prepare the needed views */
using resub_view_t = fanout_view<depth_view<aig_network>>;
depth_view<aig_network> depth_view{aig};
resub_view_t resub_view{depth_view};

/* compose the resubstitution framework */
using validator_t = circuit_validator<Ntk, bill::solvers::bsat2, false, true, false>;
using functor_t = typename detail::sim_aig_resub_functor<resub_view_t, validator_t>;
using engine_t = typename detail::simulation_based_resub_engine<resub_view_t, validator_t, functor_t>;
using resub_impl_t = typename detail::resubstitution_impl<resub_view_t, engine_t>;

/* statistics objects */
resubstitution_stats st;
typename resub_impl_t::engine_st_t engine_st;
typename resub_impl_t::collector_st_t collector_st;

/* instantiate the framework and run it */
resubstitution_params ps;
resub_impl_t p( resub_view, ps, st, engine_st, collector_st );
p.run();

/* report statistics */
st.report();
collector_st.report();
engine_st.report();

Detailed statistics

template<typename ResubFnSt>
struct window_resub_stats

Public Members

uint32_t num_resub = {0}

Number of successful resubstitutions.

stopwatch::duration time_sim = {0}

Time for simulation.

stopwatch::duration time_dont_care = {0}

Time for don’t-care computation.

stopwatch::duration time_compute_function = {0}

Time of the resub functor.

template<typename ResynSt>
struct sim_resub_stats

Public Members

stopwatch::duration time_patgen = {0}

Time for pattern generation.

stopwatch::duration time_patsave = {0}

Time for saving patterns.

stopwatch::duration time_sim = {0}

Time for simulation.

stopwatch::duration time_sat = {0}

Time for SAT solving.

stopwatch::duration time_odc = {0}

Time for computing ODCs.

stopwatch::duration time_resyn = {0}

Time for finding dependency function.

stopwatch::duration time_interface = {0}

Time for translating from index lists to network signals.

uint32_t num_pats = {0}

Number of patterns used.

uint32_t num_cex = {0}

Number of counter-examples.

uint32_t num_resub = {0}

Number of successful resubstitutions.

uint32_t num_timeout = {0}

Number of SAT solver timeout.

uint32_t num_resyn = {0}

Number of calls to the resynthesis engine.