eSLIM.h File Reference

#include "misc/util/abc_namespaces.h"
#include "aig/gia/gia.h"

Include dependency graph for eSLIM.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes
struct	eSLIM_ParamStruct_

Typedefs
typedef typedefABC_NAMESPACE_HEADER_START struct eSLIM_ParamStruct_	eSLIM_ParamStruct

Functions
void	seteSLIMParams (eSLIM_ParamStruct *params)
Gia_Man_t *	applyeSLIM (Gia_Man_t *pGia, const eSLIM_ParamStruct *params)
Gia_Man_t *	applyeSLIMIncremental (Gia_Man_t *pGia, const eSLIM_ParamStruct *params, unsigned int restarts, unsigned int deepsynTimeout)

Typedef Documentation

eSLIM_ParamStruct

typedef typedefABC_NAMESPACE_HEADER_START struct eSLIM_ParamStruct_ eSLIM_ParamStruct

CFile****************************************************************

FileName [eSLIM.h]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Using Exact Synthesis with the SAT-based Local Improvement Method (eSLIM).]

Synopsis [Interface to the eSLIM package.]

Author [Franz-Xaver Reichl]

Affiliation [University of Freiburg]

Date [Ver. 1.0. Started - March 2025.]

Revision [

Id

eSLIM.h,v 1.00 2025/03/17 00:00:00 Exp

]

Definition at line 29 of file eSLIM.h.

Function Documentation

applyeSLIM()

Gia_Man_t * applyeSLIM	(	Gia_Man_t *	pGia,
		const eSLIM_ParamStruct *	params )

Definition at line 134 of file eSLIM.cpp.

                                                                         {
  eSLIM::eSLIMConfig config = getCfg(params);
  config.verbosity_level = params->verbosity_level;
 
  int eSLIM_reductions = 0;
  int deepsyn_reductions = 0;
 
  Gia_Man_t * pThis = Gia_ManDup(pGia);
  eSLIM::eSLIMLog log(params->subcircuit_size_bound);
  int initial_size = Gia_ManAndNum(pThis);
  if (params->verbosity_level > 0) {
    printSetting(params);
    std::cout << "Initial size: " << initial_size << "\n";
  }
  for (unsigned int i = 0; i < params->nruns; i++) {
    if (config.fix_seed) {
      config.seed = params->seed + i;
    }
    int size_iteration_start = Gia_ManAndNum(pThis);
    if (params->verbosity_level > 0) {
      std::cout << "Start eslim run " << i + 1 << "\n";
    }
    pThis = selectApproach(pThis, config, log, params->mode, params->forbidden_pairs);
    int size_eslim = Gia_ManAndNum(pThis);
    eSLIM_reductions += size_iteration_start - size_eslim;
 
    if (params->apply_inprocessing) {
      if (params->verbosity_level > 0) {
        std::cout << "Start inprocessing run " << i + 1 << "\n";
      }
      pThis = runInprocessing(pThis, params, i);
      if (params->verbosity_level > 0) {
        std::cout << "Inprocessing: Initial size: " << size_eslim << " final size: " << Gia_ManAndNum(pThis) << "\n";
      }
      deepsyn_reductions += size_eslim - Gia_ManAndNum(pThis);
    }
  }
  if (params->verbosity_level > 0) {
    int final_size = Gia_ManAndNum(pThis);
    std::cout << "Final size: " << final_size << "\n";
    int total_reductions = eSLIM_reductions + deepsyn_reductions;
    double reduction_ratio = 100 * static_cast<double>(total_reductions) / initial_size; 
    printf("Total reduction: %d (%.2f %%)\n", total_reductions, reduction_ratio);
    if (params->apply_inprocessing) {
      std::cout << "#Gates reduced by eSLIM: " << eSLIM_reductions << " ";
      std::cout << "#Gates reduced by deepsyn: " << deepsyn_reductions << "\n";
    } 
  }
 
  if (params->verbosity_level > 1) {
    std::cout << "Total #iterations: " << log.iteration_count << "\n";
    std::cout << "Total relation generation time (s): " << log.relation_generation_time << "\n";
    std::cout << "Total synthesis time (s): " << log.synthesis_time << "\n";
    std::cout << "#Iterations with forbidden pairs: " << log.subcircuits_with_forbidden_pairs << "\n";
  }
  if (params->verbosity_level > 2) {
    for (int i = 2; i < log.nof_analyzed_circuits_per_size.size(); i++) {
      int replaced = log.nof_replaced_circuits_per_size.size() > i ? log.nof_replaced_circuits_per_size[i] : 0;
      int reduced = log.nof_reduced_circuits_per_size.size() > i ? log.nof_reduced_circuits_per_size[i] : 0;
      std::cout << "#gates: " << i << " - #analysed: " << log.nof_analyzed_circuits_per_size[i] << " - #replaced: " << replaced << " - #reduced: " << reduced << "\n";
    }
    if (params->mode == 0) {
      for (int i = 0; i < log.nof_sat_calls_per_size.size(); i++) {
        if (log.nof_sat_calls_per_size[i] == 0) {
          std::cout << "#gates: " << i << " - avg. sat time: -\n";
        } else {
          std::cout << "#gates: " << i << " - avg. sat time: " << static_cast<double>(log.cummulative_sat_runtimes_per_size[i]) / (1000 * log.nof_sat_calls_per_size[i]) << " sec\n";
        }
      }
      for (int i = 0; i < log.nof_unsat_calls_per_size.size(); i++) {
        if (log.nof_unsat_calls_per_size[i] == 0) {
          std::cout << "#gates: " << i << " - avg. unsat time: -\n";
        } else {
          std::cout << "#gates: " << i << " - avg. unsat time: " << static_cast<double>(log.cummulative_unsat_runtimes_per_size[i]) / (1000* log.nof_unsat_calls_per_size[i]) << " sec\n";
        }
      }
    }
  }
  return pThis;
}

Here is the call graph for this function:

applyeSLIMIncremental()

Gia_Man_t * applyeSLIMIncremental	(	Gia_Man_t *	pGia,
		const eSLIM_ParamStruct *	params,
		unsigned int	restarts,
		unsigned int	deepsynTimeout )

seteSLIMParams()

void seteSLIMParams

(

eSLIM_ParamStruct *

params

)

Definition at line 54 of file eSLIM.cpp.

                                               {
  params->forbidden_pairs = 1;
  params->extended_normality_processing = 0;
  params->fill_subcircuits = 0;
  params->apply_strash = 1;
  params->fix_seed = 0;
  params->trial_limit_active = 1;
  params->apply_inprocessing = 1;
  params->timeout = 1620;
  params->timeout_inprocessing = 180;
  params->iterations = 0;
  params->subcircuit_size_bound = 6;
  params->strash_intervall = 100;
  params->nselection_trials = 100;
  params->nruns = 1;
  params->mode = 0;
  params->seed = 0;
  params->verbosity_level = 1;
  params->expansion_probability = 0.4;           
}