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
andxmg_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 mockturtle::resubstitution_params¶
Parameters for resubstitution.
The data structure
resubstitution_params
holds configurable parameters with default arguments forresubstitution
.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.
-
uint32_t max_pis = {8}¶
-
struct mockturtle::resubstitution_stats¶
Statistics for resubstitution.
The data structure
resubstitution_stats
provides data collected by runningresubstitution
.
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, orsimulation_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 usingwindow_based_resub_engine
, theDivCollector
should prepare three public data members:leaves
,divs
, andmffc
(see documentation ofdefault_divisor_collector
for details). When usingsimulation_based_resub_engine
, onlydivs
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
andmffc
.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 in the whole network and uses partial truth tables to find potential resubstitutions. It then formally verifies the resubstitution candidates given by the resubstitution functor. If the validation fails, a counter-example will be added to the simulation patterns, and the functor will be invoked again with updated truth tables, looping until it returns
std::nullopt
. This engine only requires the divisor collector to preparedivs
.Please refer to the following paper for further details.
[1] A Simulation-Guided Paradigm for Logic Synthesis and Verification. TCAD, 2021.
Interfaces of the resubstitution functor:
Constructor:
resub_fn( Ntk const& ntk, resubstitution_params const& ps, ResubFnSt& st,
unordered_node_map<TT, Ntk> const& tts, node const& root, std::vector<node> const& divs )
A public
operator()
:std::optional<index_list_t> operator()
( TT const& care, MffcRes potential_gain, uint32_t& last_gain )
Compatible resubstitution functors implemented:
abc_resub_functor
: interfacing functor withabcresub
, ported from ABC (deprecated).resyn_functor
: interfacing functor with various resynthesis engines defined inresyn_engines
.
- param validator_t
Specialization of
circuit_validator
.- param ResubFn
Resubstitution functor to compute the resubstitution.
- param MffcRes
Typename of
potential_gain
needed by the resubstitution functor.
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
andmffc
to be ready for usage.leaves
: sufficient support for all divisorsdivs
: divisor nodes that can be used for resubstitutionmffc
: MFFC nodes which are needed to do simulation fromleaves
, throughdivs
andmffc
until the root node, but should be excluded from resubstitution. The last element ofmffc
is always the root node.divs
andmffc
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 mockturtle::detail::window_resub_stats¶
-
template<typename ResynSt>
struct mockturtle::detail::sim_resub_stats¶ Public Members
-
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.
-
uint32_t num_pats = {0}¶