diff --git a/Makefile b/Makefile index a546f65fd..50cff2d17 100644 --- a/Makefile +++ b/Makefile @@ -27,7 +27,7 @@ MODULES := \ src/misc/mem src/misc/bar src/misc/bbl src/misc/parse \ src/opt/cut src/opt/fxu src/opt/fxch src/opt/rwr src/opt/mfs src/opt/sim \ src/opt/ret src/opt/fret src/opt/res src/opt/lpk src/opt/nwk src/opt/rwt src/opt/rar \ - src/opt/cgt src/opt/csw src/opt/dar src/opt/dau src/opt/dsc src/opt/sfm src/opt/sbd \ + src/opt/cgt src/opt/csw src/opt/dar src/opt/dau src/opt/dsc src/opt/sfm src/opt/sbd src/opt/eslim \ src/sat/bsat src/sat/xsat src/sat/satoko src/sat/csat src/sat/msat src/sat/psat src/sat/cnf src/sat/bmc src/sat/glucose src/sat/glucose2 src/sat/kissat src/sat/cadical \ src/bool/bdc src/bool/deco src/bool/dec src/bool/kit src/bool/lucky \ src/bool/rsb src/bool/rpo \ diff --git a/abclib.dsp b/abclib.dsp index 921030b34..2bcb6e1b8 100644 --- a/abclib.dsp +++ b/abclib.dsp @@ -4114,6 +4114,46 @@ SOURCE=.\src\opt\sbd\sbdSat.c SOURCE=.\src\opt\sbd\sbdWin.c # End Source File # End Group +# Begin Group "eslim" + +# PROP Default_Filter "" +# Begin Source File + +SOURCE=.\src\opt\eslim\eSLIM.cpp +# End Source File +# Begin Source File + +SOURCE=.\src\opt\eslim\eSLIM.h +# End Source File +# Begin Source File + +SOURCE=.\src\opt\eslim\eSLIMMan.hpp +# End Source File +# Begin Source File + +SOURCE=.\src\opt\eslim\relationGeneration.cpp +# End Source File +# Begin Source File + +SOURCE=.\src\opt\eslim\relationGeneration.hpp +# End Source File +# Begin Source File + +SOURCE=.\src\opt\eslim\satInterfaces.hpp +# End Source File +# Begin Source File + +SOURCE=.\src\opt\eslim\selectionStrategy.hpp +# End Source File +# Begin Source File + +SOURCE=.\src\opt\eslim\utils.hpp +# End Source File +# Begin Source File + +SOURCE=.\src\opt\eslim\synthesisEngine.hpp +# End Source File +# End Group # End Group # Begin Group "map" diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index faaa6f639..8ceb65167 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -65,6 +65,7 @@ #include "opt/nwk/nwkMerge.h" #include "base/acb/acbPar.h" #include "misc/extra/extra.h" +#include "opt/eslim/eSLIM.h" #ifndef _WIN32 @@ -637,6 +638,8 @@ static int Abc_CommandAbc9MulFind ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandAbc9Test ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9eSLIM ( Abc_Frame_t * pAbc, int argc, char ** argv ); + extern int Abc_CommandAbcLivenessToSafety ( Abc_Frame_t * pAbc, int argc, char ** argv ); extern int Abc_CommandAbcLivenessToSafetySim ( Abc_Frame_t * pAbc, int argc, char ** argv ); extern int Abc_CommandAbcLivenessToSafetyWithLTL( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -1451,6 +1454,8 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "ABC9", "&mulfind", Abc_CommandAbc9MulFind, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&test", Abc_CommandAbc9Test, 0 ); + + Cmd_CommandAdd( pAbc, "ABC9", "&eslim", Abc_CommandAbc9eSLIM, 0 ); { // extern Mf_ManTruthCount(); // Mf_ManTruthCount(); @@ -56445,6 +56450,161 @@ usage: return 1; } +int Abc_CommandAbc9eSLIM( Abc_Frame_t * pAbc, int argc, char ** argv ) { + extern void seteSLIMParams(eSLIM_ParamStruct* params); + extern Gia_Man_t* applyeSLIM(Gia_Man_t * pGia, const eSLIM_ParamStruct* params); + extern Gia_Man_t* applyeSLIMIncremental(Gia_Man_t * pGia, const eSLIM_ParamStruct* params, unsigned int restarts, unsigned int deepsynTimeout); + + int nruns = 0; + int deepsynTimeout = 180; + int runOneShotMode = 0; + eSLIM_ParamStruct params; + int c; + Gia_Man_t * pTemp; + seteSLIMParams(¶ms); + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "DIPRSTVZfhnos" ) ) != EOF ) { + switch ( c ) { + case 'D': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-D\" should be followed by an integer.\n" ); + goto usage; + } + deepsynTimeout = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( deepsynTimeout < 1 ) + goto usage; + break; + case 'I': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-I\" should be followed by an integer.\n" ); + goto usage; + } + params.iterations = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( params.iterations < 0 ) + goto usage; + break; + case 'P': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-P\" should be followed by a float.\n" ); + goto usage; + } + params.expansion_probability = atof(argv[globalUtilOptind]); + globalUtilOptind++; + if ( params.expansion_probability < 0 ) + goto usage; + break; + case 'R': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-R\" should be followed by an integer.\n" ); + goto usage; + } + nruns = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nruns < 0 ) + goto usage; + break; + case 'S': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-S\" should be followed by an integer.\n" ); + goto usage; + } + params.subcircuit_size_bound = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( params.subcircuit_size_bound < 2 ) + goto usage; + break; + case 'T': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-T\" should be followed by an integer.\n" ); + goto usage; + } + params.timeout = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( params.timeout < 1 ) + goto usage; + break; + case 'V': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-V\" should be followed by an integer.\n" ); + goto usage; + } + params.verbose = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( params.verbose < 0 || params.verbose > 2 ) + goto usage; + break; + case 'Z': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-Z\" should be followed by an integer.\n" ); + goto usage; + } + params.fix_seed = 1; + params.seed = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + break; + case 'f' : + params.forbidden_pairs ^= 1; + break; + case 'h': + goto usage; + case 'n' : + params.extended_normality_processing ^= 1; + break; + case 'o' : + runOneShotMode ^= 1; + break; + case 's' : + params.fill_subcircuits ^= 1; + break; + default: + goto usage; + } + } + if ( pAbc->pGia == NULL ) { + Abc_Print( -1, "Abc_CommandAbc9Test(): There is no AIG.\n" ); + return 1; + } + + if (runOneShotMode) { + pTemp = applyeSLIM(pAbc->pGia, ¶ms); + } else { + pTemp = applyeSLIMIncremental(pAbc->pGia, ¶ms, nruns, deepsynTimeout); + } + + Abc_FrameUpdateGia( pAbc, pTemp ); + return 0; + + usage: + Abc_Print( -2, "usage: &eslim [-RTIDSPAV ] [-ch]\n" ); + Abc_Print( -2, "\t circuit minimization using exact synthesis and the SAT-based local improvement method (SLIM)\n" ); + Abc_Print( -2, "\t-D : the timeout in seconds for the individual deepsyn runs [default = %d]\n", deepsynTimeout ); + Abc_Print( -2, "\t-I : the maximal number of iterations (0 = no limit) for the individual eSLIM runs [default = %d]\n", params.iterations ); + Abc_Print( -2, "\t-P : the probability of expanding a node [default = %.2f]\n", params.expansion_probability ); + Abc_Print( -2, "\t-R : the number of runs of eSLIM + Inprocessing [default = %d]\n", nruns ); + Abc_Print( -2, "\t-S : the maximal size of considered subcircuits [default = %d]\n", params.subcircuit_size_bound ); + Abc_Print( -2, "\t-T : the timeout in seconds for the individual eSLIM runs [default = %d]\n", params.timeout ); + Abc_Print( -2, "\t-V : the verbosity level [default = %d]\n", params.verbose); + Abc_Print( -2, "\t-Z : use a fixed seed\n", params.seed); + Abc_Print( -2, "\t-f : toggle using subcircuits with forbidden pairs\n"); + Abc_Print( -2, "\t-h : print the command usage\n"); + Abc_Print( -2, "\t-n : extended normality processing\n"); + Abc_Print( -2, "\t-o : single run of eSLIM without inprocessing\n"); + Abc_Print( -2, "\t-s : fill subcircuits\n"); + Abc_Print( -2, "\t\n" ); + Abc_Print( -2, "\t This command was contributed by Franz-Xaver Reichl from University of Freiburg.\n" ); + return 1; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/opt/eslim/eSLIM.cpp b/src/opt/eslim/eSLIM.cpp new file mode 100644 index 000000000..142531090 --- /dev/null +++ b/src/opt/eslim/eSLIM.cpp @@ -0,0 +1,182 @@ +/**CFile**************************************************************** + + FileName [eSLIM.cpp] + + 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.cpp,v 1.00 2025/03/17 00:00:00 Exp $] + +***********************************************************************/ + +#include "utils.hpp" +#include "eSLIMMan.hpp" +#include "relationGeneration.hpp" +#include "selectionStrategy.hpp" + +#include "misc/util/abc_namespaces.h" + +#include "eSLIM.h" + +ABC_NAMESPACE_HEADER_START + Gia_Man_t * Gia_ManDeepSyn( Gia_Man_t * pGia, int nIters, int nNoImpr, int TimeOut, int nAnds, int Seed, int fUseTwo, int fVerbose ); +ABC_NAMESPACE_HEADER_END + +ABC_NAMESPACE_IMPL_START + +eSLIM::eSLIMConfig getCfg(const eSLIM_ParamStruct* params) { + eSLIM::eSLIMConfig config; + config.extended_normality_processing = params->extended_normality_processing; + config.apply_strash = params->apply_strash; + config.fill_subcircuits = params->fill_subcircuits; + config.fix_seed = params->fix_seed; + config.trial_limit_active = params->trial_limit_active; + config.timeout = params->timeout; + config.iterations = params->iterations; + config.subcircuit_size_bound = params->subcircuit_size_bound; + config.strash_intervall = params->strash_intervall; + config.nselection_trials = params->nselection_trials; + config.seed = params->seed; + config.verbose = params->verbose; + config.expansion_probability = params->expansion_probability; + return config; +} + +void seteSLIMParams(eSLIM_ParamStruct* params) { + 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->timeout = 1620; + params->iterations = 0; + params->subcircuit_size_bound = 6; + params->strash_intervall = 100; + params->nselection_trials = 100; + params->mode = 0; + params->seed = 0; + params->verbose = 0; + params->expansion_probability = 0.4; +} + +Gia_Man_t* selectApproach(Gia_Man_t* pGia, eSLIM::eSLIMConfig params, eSLIM::eSLIMLog& log, int approach, bool allow_forbidden_pairs) { + switch (approach) { + case 0 : + if (allow_forbidden_pairs) { + return eSLIM::eSLIM_Man::applyeSLIM(pGia, params, log); + } else { + return eSLIM::eSLIM_Man::applyeSLIM(pGia, params, log); + }; + case 1: + if (allow_forbidden_pairs) { + return eSLIM::eSLIM_Man::applyeSLIM(pGia, params, log); + } else { + return eSLIM::eSLIM_Man::applyeSLIM(pGia, params, log); + }; + default: + std::cerr << "eSLIM -- Invalid mode given\n"; + assert (false && "Invalid approach selected"); + return nullptr; + } +} + +Gia_Man_t* applyeSLIM(Gia_Man_t * pGia, const eSLIM_ParamStruct* params) { + eSLIM::eSLIMConfig config = getCfg(params); + int initial_size = Gia_ManAndNum(pGia); + Gia_Man_t * temp = Gia_ManDup(pGia); + eSLIM::eSLIMLog log(params->subcircuit_size_bound); + Gia_Man_t* result = selectApproach(temp, config, log, params->mode, params->forbidden_pairs); + if (params->verbose > 0) { + std::cout << "#Iterations with forbidden pairs: " << log.subcircuits_with_forbidden_pairs << "\n"; + int new_size = initial_size - Gia_ManAndNum(result); + std::cout << "#reduced gates: " << new_size << "\n"; + } + return result; + +} + +Gia_Man_t* applyeSLIMIncremental(Gia_Man_t* pGia, const eSLIM_ParamStruct* params, unsigned int restarts, unsigned int deepsynTimeout) { + eSLIM::eSLIMConfig config = getCfg(params); + config.verbose = params->verbose > 1; + + int eSLIM_reductions = 0; + int deepsyn_reductions = 0; + + Gia_Man_t * pThis = Gia_ManDup(pGia); + Gia_Man_t * tmp; + eSLIM::eSLIMLog log(params->subcircuit_size_bound); + int initial_size = Gia_ManAndNum(pThis); + if (params->verbose > 0) { + std::cout << "Initial size: " << initial_size << "\n"; + } + + for (unsigned int i = 0; i <= restarts; i++) { + if (config.fix_seed) { + config.seed = params->seed + i; + } + + int size_iteration_start = Gia_ManAndNum(pThis); + 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->verbose > 0) { + std::cout << "Size eSLIM it-" << i << " : " << size_eslim << "\n"; + } + + tmp = Gia_ManDeepSyn( pThis, 1, ABC_INFINITY, deepsynTimeout, 0, params->seed + i, 0, 0); + int size_deepsyn = Gia_ManAndNum(tmp); + + if ( Gia_ManAndNum(pThis) > Gia_ManAndNum(tmp) ) { + Gia_ManStop( pThis ); + pThis = tmp; + deepsyn_reductions += size_eslim - size_deepsyn; + } else { + Gia_ManStop( tmp ); + } + } + + if (params->verbose > 0) { + std::cout << "#Gates reduced by eSLIM: " << eSLIM_reductions << "\n"; + std::cout << "#Gates reduced by deepsyn: " << deepsyn_reductions << "\n"; + 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"; + + 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->verbose > 1) { + 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(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(log.cummulative_unsat_runtimes_per_size[i]) / (1000* log.nof_unsat_calls_per_size[i]) << " sec\n"; + } + } + } + return pThis; +} + +ABC_NAMESPACE_IMPL_END \ No newline at end of file diff --git a/src/opt/eslim/eSLIM.h b/src/opt/eslim/eSLIM.h new file mode 100644 index 000000000..1d4bc2175 --- /dev/null +++ b/src/opt/eslim/eSLIM.h @@ -0,0 +1,59 @@ +/**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 $] + +***********************************************************************/ + +#ifndef ABC__OPT__ESLIM__ESLIM_h +#define ABC__OPT__ESLIM__ESLIM_h + +#include "misc/util/abc_namespaces.h" +#include "aig/gia/gia.h" + +ABC_NAMESPACE_HEADER_START + + typedef struct eSLIM_ParamStruct_ eSLIM_ParamStruct; + struct eSLIM_ParamStruct_ { + int forbidden_pairs; // Allow forbidden pairs in the selected subcircuits + int extended_normality_processing; // Additional checks for non normal subcircuits + double expansion_probability; // the probability that a node is added to the subcircuit + int fill_subcircuits; // If a subcircuit has fewer than subcircuit_size_bound gates, try to fill it with rejected gates. + int apply_strash; + int fix_seed; + int trial_limit_active; + + unsigned int timeout; // available time in seconds (soft limit) + unsigned int iterations; // maximal number of iterations. No limit if 0 + unsigned int subcircuit_size_bound; // upper bound for the subcircuit sizes + unsigned int strash_intervall; + unsigned int nselection_trials; + + int mode; // 0: Cadical Incremental, 1: Kissat Oneshot + int seed; + int verbose; + + }; + + 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); + + +ABC_NAMESPACE_HEADER_END + +#endif \ No newline at end of file diff --git a/src/opt/eslim/eSLIMMan.hpp b/src/opt/eslim/eSLIMMan.hpp new file mode 100644 index 000000000..5a6718099 --- /dev/null +++ b/src/opt/eslim/eSLIMMan.hpp @@ -0,0 +1,98 @@ +/**CFile**************************************************************** + + FileName [eSLIMMan.hpp] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Using Exact Synthesis with the SAT-based Local Improvement Method (eSLIM).] + + Synopsis [eSLIM manager.] + + Author [Franz-Xaver Reichl] + + Affiliation [University of Freiburg] + + Date [Ver. 1.0. Started - March 2025.] + + Revision [$Id: eSLIMMan.hpp,v 1.00 2025/03/17 00:00:00 Exp $] + +***********************************************************************/ + +#ifndef ABC__OPT__ESLIM__ESLIMMAN_h +#define ABC__OPT__ESLIM__ESLIMMAN_h + +#include +#include +#include + +#include "misc/util/abc_namespaces.h" +#include "misc/vec/vec.h" +#include "aig/gia/gia.h" +#include "misc/util/utilTruth.h" // ioResub.h depends on utilTruth.h +#include "base/io/ioResub.h" +#include "aig/miniaig/miniaig.h" + +#include "utils.hpp" +#include "selectionStrategy.hpp" + + +ABC_NAMESPACE_CXX_HEADER_START + +namespace eSLIM { + + template + class eSLIM_Man { + + public: + static Gia_Man_t* applyeSLIM(Gia_Man_t * p, const eSLIMConfig& cfg, eSLIMLog& log); + private: + + eSLIM_Man(Gia_Man_t * gia_man, const eSLIMConfig& cfg, eSLIMLog& log); + Gia_Man_t* getCircuit(); + + void minimize(); + void findReplacement(); + Mini_Aig_t* findMinimumAig(const Subcircuit& subcir); + + Abc_RData_t* generateRelation(const Subcircuit& subcir); + Vec_Int_t* generateRelationPatterns(const Subcircuit& subcir); + Abc_RData_t* constructABCRelationRepresentation(int nof_inputs, int nof_outputs, Vec_Int_t * patterns); + + Vec_Wrd_t* getSimsIn(Abc_RData_t* relation); + Vec_Wrd_t* getSimsOut(Abc_RData_t* relation); + word getAllFalseBehaviour(const Subcircuit& subcir); + bool getAllFalseBehaviourRec(Gia_Obj_t * pObj); + + std::pair reduce( Vec_Wrd_t* vSimsDiv, Vec_Wrd_t* vSimsOut, const std::unordered_map>& forbidden_pairs, + int nVars, int nDivs, int nOuts, int initial_size); + Mini_Aig_t* computeReplacement( SynthesisEngine& syn_man, int size); + double getDynamicTimeout(int size); + + void insertReplacement(Mini_Aig_t* replacement, const Subcircuit& subcir); + std::vector processReplacement(Gia_Man_t* gia_man, Gia_Man_t* pNew, const Subcircuit& subcir, Mini_Aig_t* replacement, std::vector&& to_process, std::vector& replacement_values); + Vec_Int_t * processEncompassing(Gia_Man_t* gia_man, Gia_Man_t* pNew, Vec_Int_t* to_process); + int getInsertionLiteral(Gia_Man_t* gia_man, const Subcircuit& subcir, Mini_Aig_t* replacement, const std::vector& replacement_values, int fanin_lit); + + Gia_Man_t* gia_man = nullptr; + const eSLIMConfig& cfg; + eSLIMLog& log; + SelectionEngine subcircuit_selection; + + double relation_generation_time ; + double synthesis_time ; + + bool stopeSLIM=false; + + }; + + template + inline Gia_Man_t* eSLIM_Man::getCircuit() { + return gia_man; + } +} + +ABC_NAMESPACE_CXX_HEADER_END + +#include "eSLIMMan.tpp" + +#endif \ No newline at end of file diff --git a/src/opt/eslim/eSLIMMan.tpp b/src/opt/eslim/eSLIMMan.tpp new file mode 100644 index 000000000..ae12e2bb7 --- /dev/null +++ b/src/opt/eslim/eSLIMMan.tpp @@ -0,0 +1,514 @@ +/**CFile**************************************************************** + + FileName [eSLIMMan.tpp] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Using Exact Synthesis with the SAT-based Local Improvement Method (eSLIM).] + + Synopsis [eSLIM manager.] + + Author [Franz-Xaver Reichl] + + Affiliation [University of Freiburg] + + Date [Ver. 1.0. Started - March 2025.] + + Revision [$Id: eSLIMMan.tpp,v 1.00 2025/03/17 00:00:00 Exp $] + +***********************************************************************/ + +#include +#include +#include +#include +#include +#include +#include + +#include "eSLIMMan.hpp" +#include "synthesisEngine.hpp" +#include "relationGeneration.hpp" + + +ABC_NAMESPACE_HEADER_START + Vec_Int_t* Gia_ManGenIoCombs( Gia_Man_t * pGia, Vec_Int_t * vInsOuts, int nIns, int fVerbose ); + Mini_Aig_t * Mini_AigDupCompl( Mini_Aig_t * p, int ComplIns, int ComplOuts ); + int Exa6_ManFindPolar( word First, int nOuts ); + Vec_Wrd_t * Exa6_ManTransformInputs( Vec_Wrd_t * vIns ); + Vec_Wrd_t * Exa6_ManTransformOutputs( Vec_Wrd_t * vOuts, int nOuts ); +ABC_NAMESPACE_HEADER_END + +ABC_NAMESPACE_CXX_HEADER_START + +namespace eSLIM { + + template + Gia_Man_t* eSLIM_Man::applyeSLIM(Gia_Man_t * p, const eSLIMConfig& cfg, eSLIMLog& log) { + eSLIM_Man eslim(p, cfg, log); + eslim.minimize(); + if (cfg.verbose > 0) { + std::cout << "Relation generation time: " << log.relation_generation_time - eslim.relation_generation_time << "\n"; + std::cout << "Synthesis time: " << log.synthesis_time - eslim.synthesis_time << "\n"; + } + return eslim.getCircuit(); + } + + template + eSLIM_Man::eSLIM_Man(Gia_Man_t * pGia, const eSLIMConfig& cfg, eSLIMLog& log) + : gia_man(pGia), cfg(cfg), log(log), + subcircuit_selection(gia_man, cfg, log) { + if (cfg.fix_seed) { + subcircuit_selection.setSeed(cfg.seed); + } + relation_generation_time = log.relation_generation_time; + synthesis_time = log.synthesis_time; + } + + template + void eSLIM_Man::minimize() { + abctime clkStart = Abc_Clock(); + abctime nTimeToStop = clkStart + cfg.timeout * CLOCKS_PER_SEC; + unsigned int iteration = 0; + unsigned int iterMax = cfg.iterations ? cfg.iterations - 1 : UINT_MAX; + while (Abc_Clock() <= nTimeToStop && iteration <= iterMax && !stopeSLIM) { + iteration++; + findReplacement(); + if (Gia_ManHasDangling(gia_man)) { + Gia_Man_t* pTemp = gia_man; + gia_man = Gia_ManCleanup( pTemp ); + Gia_ManStop( pTemp ); + } + if (cfg.apply_strash && iteration % cfg.strash_intervall == 0) { + Gia_Man_t* pTemp = gia_man; + gia_man = Gia_ManRehash( pTemp, 0 ); + Gia_ManStop( pTemp ); + } + } + log.iteration_count += iteration; + + if (cfg.verbose) { + printf( "Time %8.2f sec\n", (float)1.0*(Abc_Clock() - clkStart)/CLOCKS_PER_SEC ); + std::cout << "#Iterations: " << iteration << "\n"; + } + } + + template + Abc_RData_t* eSLIM_Man::generateRelation(const Subcircuit& subcir) { + int nof_outputs = Vec_IntSize(subcir.io) - subcir.nof_inputs; + assert(Vec_IntSize(subcir.io) <= 32); + abctime relation_generation_start = Abc_Clock(); + Vec_Int_t* relation_patterns_masks = generateRelationPatterns(subcir); + log.relation_generation_time += (double)1.0*(Abc_Clock() - relation_generation_start)/CLOCKS_PER_SEC; + Abc_RData_t* relation = constructABCRelationRepresentation(subcir.nof_inputs, nof_outputs, relation_patterns_masks); + Vec_IntFree(relation_patterns_masks); + return relation; + } + + template + Vec_Int_t* eSLIM_Man::generateRelationPatterns(const Subcircuit& subcir) { + Vec_Int_t * vRes = RelationGenerator::computeRelation(gia_man, subcir); + if ( vRes == NULL ) { + return nullptr; + } + return vRes; + } + + template + Abc_RData_t* eSLIM_Man::constructABCRelationRepresentation(int nof_inputs, int nof_outputs, Vec_Int_t * patterns) { + int i, mask; + int nof_vars = nof_inputs + nof_outputs; + Abc_RData_t* p = Abc_RDataStart( nof_inputs, nof_outputs, Vec_IntSize(patterns) ); + Vec_IntForEachEntry( patterns, mask, i ) { + for ( int k = 0; k < nof_vars; k++ ) { + if ( (mask >> (nof_vars-1-k)) & 1 ) { + if ( k < nof_inputs ) { + Abc_RDataSetIn( p, k, i ); + } else { + Abc_RDataSetOut( p, 2*(k-nof_inputs)+1, i ); + } + } else { + if ( k >= nof_inputs ) { + Abc_RDataSetOut( p, 2*(k-nof_inputs), i ); + } + } + } + } + Abc_RData_t* p2 = Abc_RData2Rel(p); + Abc_RDataStop(p); + return p2; + } + + template + Vec_Wrd_t* eSLIM_Man::getSimsIn(Abc_RData_t* relation) { + Vec_Wrd_t* vSimsDiv = Vec_WrdStart( relation->nPats ); + for (int k = 0; k < relation->nIns; k++) { + for (int i = 0; i < relation->nPats; i++) { + if (Abc_RDataGetIn(relation, k, i)) { + // The first bit corresponds to the constant divisor thus we have +1 + Abc_InfoSetBit((unsigned *)Vec_WrdEntryP(vSimsDiv, i), 1+k); + } + } + } + return vSimsDiv; + } + + template + Vec_Wrd_t* eSLIM_Man::getSimsOut(Abc_RData_t* relation) { + Vec_Wrd_t* vSimsOut = Vec_WrdStart(relation->nPats); + for (int k = 0; k < (1 << relation->nOuts); k++) { + for (int i = 0; i < relation->nPats; i++) { + if (Abc_RDataGetOut(relation, k, i)) { + Abc_InfoSetBit((unsigned *)Vec_WrdEntryP(vSimsOut, i), k); + } + } + } + return vSimsOut; + } + + template + void eSLIM_Man::findReplacement() { + Subcircuit subcir = subcircuit_selection.getSubcircuit(); + if (!subcircuit_selection.getStatus()) { + if (cfg.trial_limit_active) { + stopeSLIM = true; + } + return; + } + Mini_Aig_t* replacement = findMinimumAig(subcir); + if (replacement != nullptr) { + insertReplacement(replacement, subcir); + Mini_AigStop(replacement); + } + subcir.free(); + } + + // Based on Exa_ManExactSynthesis6Int and Exa_ManExactSynthesis6 + template + Mini_Aig_t* eSLIM_Man::findMinimumAig(const Subcircuit& subcir) { + + if (subcir.forbidden_pairs.size() > 0) { + log.subcircuits_with_forbidden_pairs++; + } + + Abc_RData_t* relation = generateRelation(subcir); + int nDivs = 0; + int nOuts = relation->nOuts; + int nVars = relation->nIns; + if ( nVars == 0 ) { + return nullptr; + } + assert (nVars <= 8); //Assertion from original ABC code + Vec_Wrd_t* vSimsDiv = getSimsIn(relation); + Vec_Wrd_t* vSimsOut = getSimsOut(relation); + + word original_all_false_behaviour = vSimsOut->pArray[0]; + // If the original circuit computed a non-normal circuit, but the relations allows to set the outputs to false in the all inputs false case + // ABC does not "negate" the relation but forces the circuit to yield (0,...,0) for (0,...,0). + // As a consequence it is not necessarily possible to find a same sized circuit. + // In order to prevent this behaviour, we first modify the relation such that for the (0,...,0) input pattern only the original output patterns is allowed. + vSimsOut->pArray[0] = getAllFalseBehaviour(subcir); + + int DivCompl = (int)Vec_WrdEntry(vSimsDiv, 0) >> 1; + int OutCompl = Exa6_ManFindPolar( Vec_WrdEntry(vSimsOut, 0), nOuts ); + Vec_Wrd_t* vSimsDiv2 = Exa6_ManTransformInputs( vSimsDiv ); + Vec_Wrd_t* vSimsOut2 = Exa6_ManTransformOutputs( vSimsOut, nOuts ); + Mini_Aig_t* pMini = nullptr; + int original_size = Vec_IntSize(subcir.nodes); + int size = original_size; + + if (log.nof_analyzed_circuits_per_size.size() < original_size + 1) { + log.nof_analyzed_circuits_per_size.resize(original_size + 1, 0); + log.nof_replaced_circuits_per_size.resize(original_size + 1, 0); + log.nof_reduced_circuits_per_size.resize(original_size + 1, 0); + } + log.nof_analyzed_circuits_per_size[original_size]++; + + abctime synthesis_start = Abc_Clock(); + std::tie(size, pMini) = reduce(vSimsDiv2, vSimsOut2, subcir.forbidden_pairs, nVars, nDivs, nOuts, size); + log.synthesis_time += (double)1.0*(Abc_Clock() - synthesis_start)/CLOCKS_PER_SEC; + + if (size > original_size) { + // Could not find a replacement. This can be caused by a timeout. + Abc_RDataStop(relation); + Vec_WrdFreeP( &vSimsDiv ); + Vec_WrdFreeP( &vSimsOut ); + Vec_WrdFreeP( &vSimsDiv2 ); + Vec_WrdFreeP( &vSimsOut2 ); + return nullptr; + } + + // It is possible that a better replacement is obtained with a non normal behaviour. + bool check_original_all_false_behaviour = cfg.extended_normality_processing && vSimsOut->pArray[0] != original_all_false_behaviour; + if (check_original_all_false_behaviour) { + vSimsOut->pArray[0] = original_all_false_behaviour; + int OutCompl_alt = Exa6_ManFindPolar( Vec_WrdEntry(vSimsOut, 0), nOuts ); + Vec_Wrd_t* vSimsOut2_alt = Exa6_ManTransformOutputs( vSimsOut, nOuts ); + abctime synthesis_start = Abc_Clock(); + // auto [sz, mini] = reduce(vSimsDiv2, vSimsOut2_alt, subcir.forbidden_pairs, nVars, nDivs, nOuts, size - 1, true); + auto result = reduce(vSimsDiv2, vSimsOut2_alt, subcir.forbidden_pairs, nVars, nDivs, nOuts, size - 1); + int sz = result.first; + Mini_Aig_t* mini = result.second; + log.synthesis_time += (double)1.0*(Abc_Clock() - synthesis_start)/CLOCKS_PER_SEC; + if (mini != nullptr) { + size = sz; + if (pMini) { + Mini_AigStop(pMini); + } + pMini = mini; + OutCompl = OutCompl_alt; + } + } + Abc_RDataStop(relation); + + if (pMini != nullptr) { + Mini_Aig_t* pTemp = pMini; + pMini = Mini_AigDupCompl(pTemp, DivCompl, OutCompl); + Mini_AigStop(pTemp); + + log.nof_replaced_circuits_per_size[original_size]++; + if (size < original_size) { + log.nof_reduced_circuits_per_size[original_size]++; + } + } + Vec_WrdFreeP( &vSimsDiv ); + Vec_WrdFreeP( &vSimsOut ); + Vec_WrdFreeP( &vSimsDiv2 ); + Vec_WrdFreeP( &vSimsOut2 ); + return pMini; + } + + template + word eSLIM_Man::getAllFalseBehaviour(const Subcircuit& subcir) { + Gia_ManIncrementTravId(gia_man); + Gia_Obj_t * pObj; + int i; + Gia_ManForEachObjVec( subcir.nodes, gia_man, pObj, i ) { + Gia_ObjSetTravIdCurrent(gia_man, pObj); + } + long assm_idx = 0; + Gia_ManForEachObjVecStart(subcir.io, gia_man, pObj, i, subcir.nof_inputs) { + int bit_idx = i - subcir.nof_inputs; + if (getAllFalseBehaviourRec(pObj)) { + assm_idx |= (1 << bit_idx); + } + } + return 1L << assm_idx; + } + + template + bool eSLIM_Man::getAllFalseBehaviourRec(Gia_Obj_t * pObj) { + bool valuefanin0, valuefanin1; + if (Gia_ObjIsTravIdCurrent(gia_man, Gia_ObjFanin0(pObj))) { + valuefanin0 = getAllFalseBehaviourRec(Gia_ObjFanin0(pObj)); + } else { + valuefanin0 = false; + } + valuefanin0 = valuefanin0 != pObj->fCompl0; + if (Gia_ObjIsTravIdCurrent(gia_man, Gia_ObjFanin1(pObj))) { + valuefanin1 = getAllFalseBehaviourRec(Gia_ObjFanin1(pObj)); + } else { + valuefanin1 = false; + } + valuefanin1 = valuefanin1 != pObj->fCompl1; + return valuefanin0 && valuefanin1; + } + + template + int eSLIM_Man::getInsertionLiteral(Gia_Man_t* gia_man, const Subcircuit& subcir, Mini_Aig_t* replacement, const std::vector& replacement_values, int fanin_lit) { + int fanin_idx = Abc_Lit2Var(fanin_lit); + bool fanin_negated = Abc_LitIsCompl(fanin_lit); + int fanin_value; + if (fanin_idx == 0) { // constant fanin + fanin_value = 0; + } else if (fanin_idx <= subcir.nof_inputs) { + Gia_Obj_t* pObj = Gia_ManObj(gia_man, Vec_IntEntry(subcir.io, fanin_idx - 1)); + if (Gia_ObjIsTravIdCurrent(gia_man, pObj)) { //the node has already been added + fanin_value = Gia_ManObj(gia_man, Vec_IntEntry(subcir.io, fanin_idx - 1))->Value; + } else { + return -1; + } + } else { + if (replacement_values[fanin_idx - subcir.nof_inputs - 1] == -1) { + return -1; + } + fanin_value = replacement_values[fanin_idx - subcir.nof_inputs - 1]; + } + return Abc_LitNotCond( fanin_value, fanin_negated ); + } + + template + std::vector eSLIM_Man::processReplacement(Gia_Man_t* gia_man, Gia_Man_t* pNew, const Subcircuit& subcir, Mini_Aig_t* replacement, std::vector&& to_process, std::vector& replacement_values) { + std::vector to_process_next_it; + for (int id : to_process) { + int fanin0 = getInsertionLiteral(gia_man, subcir, replacement, replacement_values, Mini_AigNodeFanin0( replacement, id)); + int fanin1 = getInsertionLiteral(gia_man, subcir, replacement, replacement_values, Mini_AigNodeFanin1( replacement, id)); + if (fanin0 == -1 || fanin1 == -1) { + to_process_next_it.push_back(id); + } else { + int idx = id - subcir.nof_inputs - 1; + replacement_values[idx] = Gia_ManAppendAnd2(pNew, fanin0, fanin1); + } + } + int i, j = 0; + Mini_AigForEachPo(replacement, i) { + int old_id = Vec_IntEntry(subcir.io, j + subcir.nof_inputs); + j++; + Gia_Obj_t* obj = Gia_ManObj(gia_man, old_id); + int fanin0_lit = Mini_AigNodeFanin0( replacement, i); + int fanin0_idx = Abc_Lit2Var(fanin0_lit); + if (fanin0_idx == 0) { // constant fanin + obj->Value = Gia_ManConst0(gia_man)->Value; + } else if (fanin0_idx <= subcir.nof_inputs) { + Gia_Obj_t* fanin_obj = Gia_ManObj(gia_man, Vec_IntEntry(subcir.io, fanin0_idx - 1)); + if (Gia_ObjIsTravIdCurrent(gia_man, fanin_obj)) { + obj->Value = fanin_obj->Value; + } else { + continue; + } + } else { + if (replacement_values[fanin0_idx - subcir.nof_inputs - 1] == -1 ) { + continue; + } else { + obj->Value = replacement_values[fanin0_idx - subcir.nof_inputs - 1]; + } + } + Gia_ObjSetTravIdCurrent(gia_man, obj); + bool fanin0_negated = Abc_LitIsCompl(fanin0_lit); + if (fanin0_negated) { + obj->fMark0 = 1; + } + } + return to_process_next_it; + } + + template + Vec_Int_t * eSLIM_Man::processEncompassing(Gia_Man_t* gia_man, Gia_Man_t* pNew, Vec_Int_t * to_process) { + int i; + Gia_Obj_t * pObj; + Vec_Int_t * to_process_remaining = Vec_IntAlloc( Vec_IntSize(to_process) ); + Gia_ManForEachObjVec( to_process, gia_man, pObj, i ) { + if (Gia_ObjIsTravIdCurrent(gia_man, Gia_ObjFanin0(pObj)) && Gia_ObjIsTravIdCurrent(gia_man, Gia_ObjFanin1(pObj))) { + Gia_ObjSetTravIdCurrent(gia_man, pObj); + bool fanin0_negated = Gia_ObjFaninC0(pObj) ^ Gia_ObjFanin0(pObj)->fMark0; + bool fanin1_negated = Gia_ObjFaninC1(pObj) ^ Gia_ObjFanin1(pObj)->fMark0; + int fanin0 = Abc_LitNotCond(Gia_ObjFanin0(pObj)->Value, fanin0_negated); + int fanin1 = Abc_LitNotCond(Gia_ObjFanin1(pObj)->Value, fanin1_negated); + pObj->Value = Gia_ManAppendAnd2( pNew, fanin0, fanin1); + } else { + Vec_IntPush(to_process_remaining, Gia_ObjId(gia_man, pObj)); + } + } + Vec_IntFree(to_process); + return to_process_remaining; + } + + template + void eSLIM_Man::insertReplacement(Mini_Aig_t* replacement, const Subcircuit& subcir) { + // A miniaig contains a constant node, nodes for each PI/PO and for each and. + int repalcement_size = Mini_AigNodeNum(replacement) - Vec_IntSize(subcir.io) - 1; + int size_diff = Vec_IntSize(subcir.nodes) - repalcement_size; + Gia_Man_t * pNew = Gia_ManStart( Gia_ManObjNum(gia_man) - size_diff ); + pNew->pName = Abc_UtilStrsav( gia_man->pName ); + pNew->pSpec = Abc_UtilStrsav( gia_man->pSpec ); + Gia_Obj_t * pObj; + int i; + Gia_ManConst0(gia_man)->Value = 0; + Gia_ManForEachPi( gia_man, pObj, i ) { + pObj->Value = Gia_ManAppendCi(pNew); + } + Gia_ManIncrementTravId(gia_man); + Gia_ManForEachObjVec( subcir.nodes, gia_man, pObj, i ) { + Gia_ObjSetTravIdCurrent(gia_man, pObj); + } + Gia_ManIncrementTravId(gia_man); + Gia_ManForEachPi( gia_man, pObj, i ) { + Gia_ObjSetTravIdCurrent(gia_man, pObj); + } + Vec_Int_t * to_process_encompassing = Vec_IntAlloc( gia_man->nObjs ); + Gia_ManForEachAnd( gia_man, pObj, i ) { + // nodes from the subcircuit shall not be added + if (Gia_ObjIsTravIdPrevious(gia_man, pObj)) { + continue; + } else if (Gia_ObjIsTravIdCurrent(gia_man, Gia_ObjFanin0(pObj)) && Gia_ObjIsTravIdCurrent(gia_man, Gia_ObjFanin1(pObj))) { + pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + Gia_ObjSetTravIdCurrent(gia_man, pObj); + } else { + Vec_IntPush(to_process_encompassing, Gia_ObjId(gia_man, pObj)); + } + } + std::vector to_process_replacement; + Mini_AigForEachAnd(replacement, i) { + to_process_replacement.push_back(i); + } + std::vector replacement_values(to_process_replacement.size(), -1); + + while (Vec_IntSize(to_process_encompassing) > 0 || to_process_replacement.size() > 0) { + to_process_replacement = processReplacement(gia_man, pNew, subcir, replacement, std::move(to_process_replacement), replacement_values); + to_process_encompassing = processEncompassing(gia_man, pNew, to_process_encompassing); + } + Vec_IntFree(to_process_encompassing); + int po_idx = 0; + Mini_AigForEachPo(replacement, i) { + Gia_Obj_t* pObj = Gia_ManObj(gia_man, Vec_IntEntry(subcir.io, subcir.nof_inputs + po_idx)); + if (!Gia_ObjIsTravIdCurrent(gia_man, pObj)) { + int fanin_lit = Mini_AigNodeFanin0( replacement, i); + int fanin_idx = Abc_Lit2Var(fanin_lit); + assert (fanin_idx <= subcir.nof_inputs); + Gia_Obj_t* fanin_obj = Gia_ManObj(gia_man, Vec_IntEntry(subcir.io, fanin_idx - 1)); + pObj->Value = fanin_obj->Value; + if (Abc_LitIsCompl(fanin_lit)) { + pObj->fMark0 = 1; + } + Gia_ObjSetTravIdCurrent(gia_man, pObj); + } + po_idx++; + } + + Gia_ManForEachPo( gia_man, pObj, i ) { + assert(Gia_ObjIsTravIdCurrent(gia_man, Gia_ObjFanin0(pObj))); + bool fanin_negated = Gia_ObjFaninC0(pObj) ^ Gia_ObjFanin0(pObj)->fMark0; + int fanin0 = Abc_LitNotCond(Gia_ObjFanin0(pObj)->Value, fanin_negated); + pObj->Value = Gia_ManAppendCo( pNew, fanin0 ); + } + Gia_ManStop(gia_man); + gia_man = pNew; + } + + template + std::pair eSLIM_Man::reduce(Vec_Wrd_t* vSimsDiv, Vec_Wrd_t* vSimsOut, const std::unordered_map>& forbidden_pairs, + int nVars, int nDivs, int nOuts, int size) { + Y synth_man(vSimsDiv,vSimsOut,nVars,1+nVars+nDivs,nOuts,size, forbidden_pairs, log, cfg); + Mini_Aig_t* result = nullptr; + while (size >= 0) { + Mini_Aig_t* pTemp = computeReplacement(synth_man, size); + if (pTemp) { + if (result) { + Mini_AigStop(result); + } + result = pTemp; + size--; + } else { + break; + } + } + return std::make_pair(size + 1, result); + } + + template + double eSLIM_Man::getDynamicTimeout(int size) { + if (this->log.nof_sat_calls_per_size[size] > cfg.minimum_dynamic_timeout_sample_size) { + return std::max(static_cast(cfg.minimum_sat_timeout), static_cast(log.cummulative_sat_runtimes_per_size[size]) / (1000*log.nof_sat_calls_per_size[size])); //logged timings are given in ms + } else { + return cfg.base_sat_timeout; + } + } + + template + Mini_Aig_t* eSLIM_Man::computeReplacement(Y& syn_man, int size) { + return syn_man.getCircuit(size, getDynamicTimeout(size)); + } + +} + +ABC_NAMESPACE_CXX_HEADER_END \ No newline at end of file diff --git a/src/opt/eslim/module.make b/src/opt/eslim/module.make new file mode 100644 index 000000000..f300a4231 --- /dev/null +++ b/src/opt/eslim/module.make @@ -0,0 +1,2 @@ +SRC += src/opt/eslim/relationGeneration.cpp \ + src/opt/eslim/eSLIM.cpp \ No newline at end of file diff --git a/src/opt/eslim/relationGeneration.cpp b/src/opt/eslim/relationGeneration.cpp new file mode 100644 index 000000000..66dc11eff --- /dev/null +++ b/src/opt/eslim/relationGeneration.cpp @@ -0,0 +1,172 @@ +/**CFile**************************************************************** + + FileName [relationGeneration.cpp] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Using Exact Synthesis with the SAT-based Local Improvement Method (eSLIM).] + + Synopsis [Procedures for computing Boolean relations.] + + Author [Franz-Xaver Reichl] + + Affiliation [University of Freiburg] + + Date [Ver. 1.0. Started - March 2025.] + + Revision [$Id: relationGeneration.cpp,v 1.00 2025/03/17 00:00:00 Exp $] + +***********************************************************************/ + +#include + +#include "misc/vec/vec.h" +#include "sat/cnf/cnf.h" +#include "sat/bsat/satSolver.h" + +#include "relationGeneration.hpp" + +ABC_NAMESPACE_HEADER_START + void * Mf_ManGenerateCnf( Gia_Man_t * pGia, int nLutSize, int fCnfObjIds, int fAddOrCla, int fMapping, int fVerbose ); + void * Cnf_DataWriteIntoSolver( Cnf_Dat_t * p, int nFrames, int fInit ); + Vec_Int_t * Gia_ManCollectNodeTfos( Gia_Man_t * p, int * pNodes, int nNodes ); + Vec_Int_t * Gia_ManCollectNodeTfis( Gia_Man_t * p, Vec_Int_t * vNodes ); +ABC_NAMESPACE_HEADER_END + +ABC_NAMESPACE_IMPL_START + + +namespace eSLIM { + + RelationGeneratorABC::RelationGeneratorABC(Gia_Man_t* pGia, const Subcircuit& subcir) + : RelationGenerator(pGia, subcir) { + + // for (const auto& [out, inputs] : subcir.forbidden_pairs) { + for (const auto& it: subcir.forbidden_pairs) { + const auto& inputs = it.second; + inputs_in_forbidden_pairs.insert(inputs.begin(), inputs.end()); + } +} + + Vec_Int_t* RelationGeneratorABC::getRelationImpl() { + abctime clkStart = Abc_Clock(); + int nTimeOut = 600, nConfLimit = 1000000; + int i, iNode, iSatVar, Iter, Mask, nSolutions = 0, RetValue = 0; + // --------------- Modification --------------- + Gia_Man_t* pMiter = generateMiter(); + // --------------- Modification --------------- + Cnf_Dat_t * pCnf = (Cnf_Dat_t*)Mf_ManGenerateCnf( pMiter, 8, 0, 0, 0, 0 ); + sat_solver * pSat = (sat_solver*)Cnf_DataWriteIntoSolver( pCnf, 1, 0 ); + int iLit = Abc_Var2Lit( 1, 0 ); // enumerating the care set (the miter output is 1) + int status = sat_solver_addclause( pSat, &iLit, &iLit + 1 ); assert( status ); + Vec_Int_t * vSatVars = Vec_IntAlloc( Vec_IntSize(subcir.io) ); + Vec_IntForEachEntry( subcir.io, iNode, i ) + Vec_IntPush( vSatVars, i < subcir.nof_inputs ? 2+i : pCnf->nVars-Vec_IntSize(subcir.io)+i ); + Vec_Int_t * vLits = Vec_IntAlloc( 100 ); + Vec_Int_t * vRes = Vec_IntAlloc( 1000 ); + for ( Iter = 0; Iter < 1000000; Iter++ ) + { + int status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)nConfLimit, 0, 0, 0 ); + if ( status == l_False ) { RetValue = 1; break; } + if ( status == l_Undef ) { RetValue = 0; break; } + nSolutions++; + // extract SAT assignment + Mask = 0; + Vec_IntClear( vLits ); + Vec_IntForEachEntry( vSatVars, iSatVar, i ) { + Vec_IntPush( vLits, Abc_Var2Lit(iSatVar, sat_solver_var_value(pSat, iSatVar)) ); + if ( sat_solver_var_value(pSat, iSatVar) ) + Mask |= 1 << (Vec_IntSize(subcir.io)-1-i); + } + Vec_IntPush( vRes, Mask ); + if ( !sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) ) ) + { RetValue = 1; break; } + if ( nTimeOut && (Abc_Clock() - clkStart)/CLOCKS_PER_SEC >= nTimeOut ) { RetValue = 0; break; } + } + // complement the set of input/output minterms + Vec_Int_t * vBits = Vec_IntStart( 1 << Vec_IntSize(subcir.io) ); + Vec_IntForEachEntry( vRes, Mask, i ) + Vec_IntWriteEntry( vBits, Mask, 1 ); + Vec_IntClear( vRes ); + Vec_IntForEachEntry( vBits, Mask, i ) + if ( !Mask ) + Vec_IntPush( vRes, i ); + Vec_IntFree( vBits ); + // cleanup + Vec_IntFree( vLits ); + Vec_IntFree( vSatVars ); + sat_solver_delete( pSat ); + Gia_ManStop( pMiter ); + Cnf_DataFree( pCnf ); + if ( RetValue == 0 ) + Vec_IntFreeP( &vRes ); + return vRes; + } + + Gia_Man_t * RelationGeneratorABC::generateMiter() { + Vec_Int_t * vInsOuts = subcir.io; + int nIns = subcir.nof_inputs; + + Vec_Int_t * vTfo = Gia_ManCollectNodeTfos( pGia, Vec_IntEntryP(vInsOuts, nIns), Vec_IntSize(vInsOuts)-nIns ); + Vec_Int_t * vTfi = Gia_ManCollectNodeTfis( pGia, vTfo ); + Vec_Int_t * vInLits = Vec_IntAlloc( nIns ); + Vec_Int_t * vOutLits = Vec_IntAlloc( Vec_IntSize(vInsOuts) - nIns ); + Gia_Man_t * pNew, * pTemp; Gia_Obj_t * pObj; int i, iLit = 0; + Gia_ManFillValue( pGia ); + pNew = Gia_ManStart( 1000 ); + pNew->pName = Abc_UtilStrsav( pGia->pName ); + Gia_ManHashAlloc( pNew ); + Gia_ManForEachObjVec( vTfi, pGia, pObj, i ) + if ( Gia_ObjIsCi(pObj) ) + pObj->Value = Gia_ManAppendCi(pNew); + for ( i = 0; i < Vec_IntSize(vInsOuts)-nIns; i++ ) + Vec_IntPush( vInLits, Gia_ManAppendCi(pNew) ); + Gia_ManForEachObjVec( vTfi, pGia, pObj, i ) + if ( Gia_ObjIsAnd(pObj) ) + pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + Gia_ManForEachObjVec( vTfo, pGia, pObj, i ) + if ( Gia_ObjIsCo(pObj) ) + pObj->Value = Gia_ObjFanin0Copy(pObj); + Gia_ManForEachObjVec( vInsOuts, pGia, pObj, i ) + if ( i < nIns ) + Vec_IntPush( vOutLits, pObj->Value ); + else + pObj->Value = Vec_IntEntry( vInLits, i-nIns ); + + Gia_ManIncrementTravId(pGia); + Gia_ManForEachObjVec( subcir.nodes, pGia, pObj, i ) { + Gia_ObjSetTravIdCurrent(pGia, pObj); + } + + Gia_ManForEachObjVec( vTfo, pGia, pObj, i ) + // in case there are forbidden pairs we have to ensure that nodes from the sucircuit are not added + if ( Gia_ObjIsAnd(pObj) && !Gia_ObjIsTravIdCurrent(pGia, pObj) ) + pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + Gia_ManForEachObjVec( vTfo, pGia, pObj, i ) + if ( Gia_ObjIsCo(pObj) ) + iLit = Gia_ManHashOr( pNew, iLit, Gia_ManHashXor(pNew, Gia_ObjFanin0Copy(pObj), pObj->Value) ); + // --------------- Modification --------------- + // In case there are forbidden pairs, the outputs of the subcircuit influence the inputs of the subcircuit. + // Therefore, we need the values of the inputs in the version of the circuit that is affected by the new outputs. + for (int inp : inputs_in_forbidden_pairs) { + int node_id = Vec_IntEntry(vInsOuts, inp); + pObj = Gia_ManObj(pGia, node_id); + Vec_IntWriteEntry(vOutLits, inp, pObj->Value); + } + // --------------- Modification --------------- + Gia_ManAppendCo( pNew, iLit ); + Vec_IntForEachEntry( vOutLits, iLit, i ) + Gia_ManAppendCo( pNew, iLit ); + Vec_IntFree( vTfo ); + Vec_IntFree( vTfi ); + Vec_IntFree( vInLits ); + Vec_IntFree( vOutLits ); + pNew = Gia_ManCleanup( pTemp = pNew ); + Gia_ManStop( pTemp ); + Gia_ManSetRegNum( pNew, Gia_ManRegNum(pGia) ); + return pNew; + } + +} + +ABC_NAMESPACE_IMPL_END \ No newline at end of file diff --git a/src/opt/eslim/relationGeneration.hpp b/src/opt/eslim/relationGeneration.hpp new file mode 100644 index 000000000..2d29fe8ef --- /dev/null +++ b/src/opt/eslim/relationGeneration.hpp @@ -0,0 +1,107 @@ +/**CFile**************************************************************** + + FileName [relationGeneration.hpp] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Using Exact Synthesis with the SAT-based Local Improvement Method (eSLIM).] + + Synopsis [Procedures for computing Boolean relations.] + + Author [Franz-Xaver Reichl] + + Affiliation [University of Freiburg] + + Date [Ver. 1.0. Started - March 2025.] + + Revision [$Id: relationGeneration.hpp,v 1.00 2025/03/17 00:00:00 Exp $] + +***********************************************************************/ + +#ifndef ABC__OPT__ESLIM__RELATIONGENERATION_h +#define ABC__OPT__ESLIM__RELATIONGENERATION_h + +#include +#include +#include + +#include "misc/util/abc_namespaces.h" +#include +#include "aig/gia/gia.h" + +#include "utils.hpp" +// #include "satInterfaces.hpp" + + +ABC_NAMESPACE_CXX_HEADER_START + +namespace eSLIM { + + template + class RelationGenerator { + + public: + static Vec_Int_t* computeRelation(Gia_Man_t* gia_man, const Subcircuit& subcir); + + private: + Gia_Man_t* pGia; + const Subcircuit& subcir; + + RelationGenerator(Gia_Man_t* pGia, const Subcircuit& subcir); + void setup(); + Vec_Int_t* getRelation(); + + friend Derived; + }; + + // The class almost entirely duplicates the functionality provided by Gia_ManGenIoCombs in giaQBF.c + // But the implementation in this class allows to take forbidden pairs into account. + class RelationGeneratorABC : public RelationGenerator { + + private: + RelationGeneratorABC(Gia_Man_t* pGia, const Subcircuit& subcir); + void setupImpl() {}; + Vec_Int_t* getRelationImpl(); + Gia_Man_t * generateMiter(); + + std::unordered_set inputs_in_forbidden_pairs; + + friend RelationGenerator; + }; + + + // Add other engine for the generation of relations + // class MyRelationGenerator : public RelationGenerator { + // private: + // void setupImpl() + // Vec_Int_t* getRelationImpl(); + // friend RelationGenerator; + // }; + + + template + inline RelationGenerator::RelationGenerator(Gia_Man_t* pGia, const Subcircuit& subcir) + : pGia(pGia), subcir(subcir) { + } + + template + inline Vec_Int_t* RelationGenerator::computeRelation(Gia_Man_t* gia_man, const Subcircuit& subcir) { + T generator(gia_man, subcir); + generator.setup(); + return generator.getRelation(); + } + + template + inline void RelationGenerator::setup() { + static_cast(this)->setupImpl(); + } + + template + inline Vec_Int_t* RelationGenerator::getRelation() { + return static_cast(this)->getRelationImpl(); + } +} + +ABC_NAMESPACE_CXX_HEADER_END + +#endif diff --git a/src/opt/eslim/satInterfaces.hpp b/src/opt/eslim/satInterfaces.hpp new file mode 100644 index 000000000..3300d9e59 --- /dev/null +++ b/src/opt/eslim/satInterfaces.hpp @@ -0,0 +1,196 @@ +/**CFile**************************************************************** + + FileName [satInterfaces.hpp] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Using Exact Synthesis with the SAT-based Local Improvement Method (eSLIM).] + + Synopsis [Interface to SAT solvers.] + + Author [Franz-Xaver Reichl] + + Affiliation [University of Freiburg] + + Date [Ver. 1.0. Started - March 2025.] + + Revision [$Id: satInterfaces.hpp,v 1.00 2025/03/17 00:00:00 Exp $] + +***********************************************************************/ + +#ifndef ABC__OPT__ESLIM__SATINTERFACE_h +#define ABC__OPT__ESLIM__SATINTERFACE_h + +#include +#include +#include + +#include "misc/util/abc_namespaces.h" +#include "misc/vec/vec.h" +#include "sat/kissat/kissat.h" +#include "sat/cadical/cadical.hpp" + +ABC_NAMESPACE_CXX_HEADER_START + +namespace eSLIM { + + class CadicalSolver { + public: + void addClause(int * pLits, int nLits ); + void assume(const std::vector& assumptions); + int solve(double timeout); + int solve(); + Vec_Int_t* getModelVec(); + double getRunTime() const; + + private: + int val(int variable); + double last_runtime; + CaDiCaL::Solver solver; + + public: + class TimeoutTerminator : public CaDiCaL::Terminator { + public: + TimeoutTerminator(double max_runtime); + bool terminate(); + + private: + double max_runtime; //in seconds + std::chrono::time_point start = std::chrono::steady_clock::now(); + }; + }; + + class KissatSolver { + public: + KissatSolver(); + ~KissatSolver(); + void init(int max_var); + void addClause(int * pLits, int nLits ); + int solve(); + // int solve(int timeout); + Vec_Int_t* getModelVec(); + + private: + + int max_var = 0; + int val(int variable); + kissat * solver = nullptr; + }; + + inline CadicalSolver::TimeoutTerminator::TimeoutTerminator(double max_runtime) : max_runtime(max_runtime) {} + + inline bool CadicalSolver::TimeoutTerminator::terminate() { + auto current_time = std::chrono::steady_clock::now(); + std::chrono::duration elapsed_seconds = current_time - start; + return elapsed_seconds.count() > max_runtime; + } + + inline double CadicalSolver::getRunTime() const { + return last_runtime; + } + + inline void CadicalSolver::addClause(int * pLits, int nLits ) { + for ( int i = 0; i < nLits; i++ ) { + if (pLits[i] == 0) { + continue;; + } + solver.add(Abc_LitIsCompl(pLits[i]) ? -Abc_Lit2Var(pLits[i]) : Abc_Lit2Var(pLits[i])); + } + solver.add(0); + } + + inline void CadicalSolver::assume(const std::vector& assumptions) { + for (auto& l: assumptions) { + solver.assume(l); + } + } + + inline int CadicalSolver::solve() { + std::chrono::time_point start = std::chrono::steady_clock::now(); + int status = solver.solve(); + last_runtime = std::chrono::duration_cast(std::chrono::steady_clock::now() - start).count(); + return status; + } + + inline int CadicalSolver::solve(double timeout) { + std::chrono::time_point start = std::chrono::steady_clock::now(); + TimeoutTerminator terminator(timeout); + solver.connect_terminator(&terminator); + int status = solver.solve(); + last_runtime = std::chrono::duration_cast(std::chrono::steady_clock::now() - start).count(); + if (solver.state() == CaDiCaL::INVALID) { + std::cerr<<"Solver is in invalid state"< 0 ); + } + return assignment; + } + + inline int CadicalSolver::val(int variable) { + auto l = solver.val(variable); + auto v = abs(l); + if (v == variable) { + return l; + } else { + return variable; + } + } + + inline KissatSolver::KissatSolver() { + solver = kissat_init(); + } + + inline KissatSolver::~KissatSolver() { + kissat_release(solver); + } + + inline void KissatSolver::init(int max_var) { + this->max_var = max_var; + kissat_reserve(solver, max_var); + } + + inline void KissatSolver::addClause(int * pLits, int nLits ) { + for ( int i = 0; i < nLits; i++ ) { + if (pLits[i] == 0) { + continue; + } + kissat_add (solver, Abc_LitIsCompl(pLits[i]) ? -Abc_Lit2Var(pLits[i]) : Abc_Lit2Var(pLits[i])); + } + kissat_add (solver, 0); + } + + inline int KissatSolver::solve() { + int status = kissat_solve(solver); + return status; + } + + inline int KissatSolver::val(int variable) { + int l = kissat_value (solver, variable); + auto v = abs(l); + if (v == variable) { + return l; + } else { + return variable; + } + } + + inline Vec_Int_t* KissatSolver::getModelVec() { + Vec_Int_t* assignment = Vec_IntAlloc( max_var ); + for (int v = 1; v <= max_var; v++) { + Vec_IntSetEntryFull( assignment, Abc_AbsInt(val(v)), val(v) > 0 ); + } + return assignment; + } +} + +ABC_NAMESPACE_CXX_HEADER_END + +#endif \ No newline at end of file diff --git a/src/opt/eslim/selectionStrategy.hpp b/src/opt/eslim/selectionStrategy.hpp new file mode 100644 index 000000000..b4f0ccf80 --- /dev/null +++ b/src/opt/eslim/selectionStrategy.hpp @@ -0,0 +1,154 @@ +/**CFile**************************************************************** + + FileName [selectionStrategy.hpp] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Using Exact Synthesis with the SAT-based Local Improvement Method (eSLIM).] + + Synopsis [Procedures for selecting subcircuits.] + + Author [Franz-Xaver Reichl] + + Affiliation [University of Freiburg] + + Date [Ver. 1.0. Started - March 2025.] + + Revision [$Id: selectionStrategy.hpp,v 1.00 2025/03/17 00:00:00 Exp $] + +***********************************************************************/ + +#ifndef ABC__OPT__ESLIM__SELECTIONSTRATEGY_h +#define ABC__OPT__ESLIM__SELECTIONSTRATEGY_h + +#include +#include + +#include "misc/util/abc_namespaces.h" +#include "misc/vec/vec.h" +#include "aig/gia/gia.h" + +#include "utils.hpp" + +ABC_NAMESPACE_CXX_HEADER_START + +namespace eSLIM { + + template + class SelectionStrategy { + public: + Subcircuit getSubcircuit(); + bool getStatus() {return status;}; + void setSeed(int seed); + + protected: + SelectionStrategy(Gia_Man_t*& gia_man, const eSLIMConfig& cfg, eSLIMLog& log); + unsigned int getUniformRandomNumber(unsigned int lower, unsigned int upper); // requires lower < upper + bool getRandomBool(); + int getSubcircuitIO(Vec_Int_t* subcircuit, Vec_Int_t* io); + // The resulting map assigns inputs of the subcircuit to outputs of the subcircuit s.t. each associated input is reachable from the output + std::unordered_map> computeForbiddenPairs(const Subcircuit& subcir); + + Gia_Man_t*& gia_man; + const eSLIMConfig& cfg; + eSLIMLog& log; + + private: + + bool filterSubcircuit(const Subcircuit& subcir); + void forbiddenPairsRec(Gia_Obj_t * pObj, int input, int min_level, std::unordered_map>& pairs, const std::unordered_map& out_ids ); + + bool status = true; //set to false if selection fails too often + static constexpr unsigned int min_size = 2; + + std::mt19937 rng; + std::bernoulli_distribution bdist; + std::uniform_int_distribution udistr; + + }; + + template + class randomizedBFS : public SelectionStrategy { + private: + randomizedBFS(Gia_Man_t*& gia_man, const eSLIMConfig& cfg, eSLIMLog& log); + Subcircuit findSubcircuit(); + int selectRoot(); + void checkCandidate(Subcircuit& subcircuit, std::queue& candidate, std::queue& rejected, bool add); + const int nPis; + const int nPos; + friend SelectionStrategy; + friend T; + }; + + class randomizedBFSFP : public randomizedBFS { + public : + randomizedBFSFP(Gia_Man_t*& gia_man, const eSLIMConfig& cfg, eSLIMLog& log); + private: + Subcircuit getSubcircuitImpl(); + bool filterSubcircuitImpl(const Subcircuit& subcir); + + friend SelectionStrategy; + }; + + class randomizedBFSnoFP : public randomizedBFS { + public: + randomizedBFSnoFP(Gia_Man_t*& gia_man, const eSLIMConfig& cfg, eSLIMLog& log); + private: + Subcircuit getSubcircuitImpl() {return findSubcircuit();}; + bool filterSubcircuitImpl(const Subcircuit& subcir); + bool filterSubcircuitRec(Gia_Obj_t * pObj, unsigned int min_level); + + friend SelectionStrategy; + }; + + + template + SelectionStrategy::SelectionStrategy(Gia_Man_t*& gia_man, const eSLIMConfig& cfg, eSLIMLog& log) + : gia_man(gia_man), cfg(cfg), log(log), rng(std::random_device()()) { + } + + template + void SelectionStrategy::setSeed(int seed) { + rng.seed(seed); + } + + template + unsigned int SelectionStrategy::getUniformRandomNumber(unsigned int lower, unsigned int upper) { + udistr.param(std::uniform_int_distribution::param_type(lower, upper)); + return udistr(rng); + } + + template + bool SelectionStrategy::getRandomBool() { + return bdist(rng); + } + + template + randomizedBFS::randomizedBFS(Gia_Man_t*& gia_man, const eSLIMConfig& cfg, eSLIMLog& log) + : SelectionStrategy(gia_man, cfg, log), nPis(Gia_ManPiNum(gia_man)), nPos(Gia_ManPoNum(gia_man)) { + } + + inline randomizedBFSFP::randomizedBFSFP(Gia_Man_t*& gia_man, const eSLIMConfig& cfg, eSLIMLog& log) + : randomizedBFS(gia_man, cfg, log){ + } + + inline Subcircuit randomizedBFSFP::getSubcircuitImpl() { + Subcircuit subcir = findSubcircuit(); + subcir.forbidden_pairs = computeForbiddenPairs(subcir); + return subcir; + } + + inline randomizedBFSnoFP::randomizedBFSnoFP(Gia_Man_t*& gia_man, const eSLIMConfig& cfg, eSLIMLog& log) + : randomizedBFS(gia_man, cfg, log) { + } + + inline bool randomizedBFSFP::filterSubcircuitImpl(const Subcircuit& subcir) { + return true; + } +} + +ABC_NAMESPACE_CXX_HEADER_END + +#include "selectionStrategy.tpp" + +#endif \ No newline at end of file diff --git a/src/opt/eslim/selectionStrategy.tpp b/src/opt/eslim/selectionStrategy.tpp new file mode 100644 index 000000000..ba150d624 --- /dev/null +++ b/src/opt/eslim/selectionStrategy.tpp @@ -0,0 +1,231 @@ +/**CFile**************************************************************** + + FileName [selectionStrategy.tpp] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Using Exact Synthesis with the SAT-based Local Improvement Method (eSLIM).] + + Synopsis [Procedures for selecting subcircuits.] + + Author [Franz-Xaver Reichl] + + Affiliation [University of Freiburg] + + Date [Ver. 1.0. Started - March 2025.] + + Revision [$Id: selectionStrategy.tpp,v 1.00 2025/03/17 00:00:00 Exp $] + +***********************************************************************/ + +#include + +#include "misc/util/abc_namespaces.h" + +#include "selectionStrategy.hpp" + +ABC_NAMESPACE_CXX_HEADER_START + +namespace eSLIM { + + template + Subcircuit SelectionStrategy::getSubcircuit() { + for (int i = 0; i < cfg.nselection_trials; i++) { + Subcircuit subcir = static_cast(this)->getSubcircuitImpl(); + if (filterSubcircuit(subcir)) { + return subcir; + } else { + subcir.free(); + } + } + status = false; + Subcircuit empty_subcir; + return empty_subcir; + } + + template + bool SelectionStrategy::filterSubcircuit(const Subcircuit& subcir) { + if (subcir.nof_inputs > 8) { + return false; + } + if (Vec_IntSize(subcir.io)-subcir.nof_inputs > 6) { + return false; + } + if (Vec_IntSize(subcir.nodes) < min_size) { + return false; + } + return static_cast(this)->filterSubcircuitImpl(subcir); + } + + template + int SelectionStrategy::getSubcircuitIO(Vec_Int_t* subcircuit, Vec_Int_t* io) { + assert(Vec_IntSize(io) == 0); + Gia_ManIncrementTravId(gia_man); + Gia_Obj_t * pObj; + int i; + Gia_ManForEachObjVec( subcircuit, gia_man, pObj, i ) { + Gia_ObjSetTravIdCurrent(gia_man, pObj); + } + Gia_ManIncrementTravId(gia_man); + + // inputs + Gia_ManForEachObjVec( subcircuit, gia_man, pObj, i ) { + // fanin0 is not in the subcircuit and was not considered yet + if (!Gia_ObjIsTravIdPrevious(gia_man, Gia_ObjFanin0(pObj)) && !Gia_ObjIsTravIdCurrent(gia_man, Gia_ObjFanin0(pObj))) { + Gia_ObjSetTravIdCurrent(gia_man, Gia_ObjFanin0(pObj)); + Vec_IntPush(io, Gia_ObjId(gia_man, Gia_ObjFanin0(pObj))); + } + // fanin1 is not in the subcircuit and was not considered yet + if (!Gia_ObjIsTravIdPrevious(gia_man, Gia_ObjFanin1(pObj)) && !Gia_ObjIsTravIdCurrent(gia_man, Gia_ObjFanin1(pObj))) { + Gia_ObjSetTravIdCurrent(gia_man, Gia_ObjFanin1(pObj)); + Vec_IntPush(io, Gia_ObjId(gia_man, Gia_ObjFanin1(pObj))); + } + } + int nof_inputs = Vec_IntSize(io); + + // outputs + Gia_ManForEachAnd( gia_man, pObj, i ) { + // If there is an object that is not contained in the subcircuit that has a fanin in the subcircuit then this fanin is an output + if (!Gia_ObjIsTravIdPrevious(gia_man, pObj)) { + if (Gia_ObjIsTravIdPrevious(gia_man, Gia_ObjFanin0(pObj))) { + Gia_ObjSetTravIdCurrent(gia_man, Gia_ObjFanin0(pObj)); + Vec_IntPush(io, Gia_ObjId(gia_man, Gia_ObjFanin0(pObj))); + } + if (Gia_ObjIsTravIdPrevious(gia_man, Gia_ObjFanin1(pObj))) { + Gia_ObjSetTravIdCurrent(gia_man, Gia_ObjFanin1(pObj)); + Vec_IntPush(io, Gia_ObjId(gia_man, Gia_ObjFanin1(pObj))); + } + } + } + + Gia_ManForEachPo( gia_man, pObj, i ) { + if (Gia_ObjIsTravIdPrevious(gia_man, Gia_ObjFanin0(pObj))) { + Gia_ObjSetTravIdCurrent(gia_man, Gia_ObjFanin0(pObj)); + Vec_IntPush(io, Gia_ObjId(gia_man, Gia_ObjFanin0(pObj))); + } + } + return nof_inputs; + } + + template + std::unordered_map> SelectionStrategy::computeForbiddenPairs(const Subcircuit& subcir) { + Gia_Obj_t * pObj; + int i; + unsigned int min_output_level = Gia_ManLevelNum(gia_man); + Gia_ManIncrementTravId(gia_man); + std::unordered_map out_id; + Gia_ManForEachObjVecStart(subcir.io, gia_man, pObj, i, subcir.nof_inputs) { + min_output_level = Gia_ObjLevel(gia_man, pObj) < min_output_level ? Gia_ObjLevel(gia_man, pObj) : min_output_level; + Gia_ObjSetTravIdCurrent(gia_man, pObj); + auto id = Gia_ObjId(gia_man, pObj); + out_id[id] = i - subcir.nof_inputs; + } + std::unordered_map> forbidden_pairs; + Gia_ManForEachObjVecStop(subcir.io, gia_man, pObj, i, subcir.nof_inputs) { + forbiddenPairsRec(pObj, i, min_output_level, forbidden_pairs, out_id); + } + return forbidden_pairs; + } + + template + void SelectionStrategy::forbiddenPairsRec(Gia_Obj_t * pObj, int input, int min_level, std::unordered_map>& pairs, const std::unordered_map& out_id) { + if (Gia_ObjIsTravIdCurrent(gia_man, pObj)) { + auto id = Gia_ObjId(gia_man, pObj); + pairs[out_id.at(id)].insert(input); + return; + } + if (Gia_ObjLevel(gia_man, pObj) < min_level) { + return; + } + forbiddenPairsRec(Gia_ObjFanin0(pObj), input, min_level, pairs, out_id); + forbiddenPairsRec(Gia_ObjFanin1(pObj), input, min_level, pairs, out_id); + } + + template + int randomizedBFS::selectRoot() { + int nof_objs = Gia_ManObjNum(this->gia_man); + int root_id = this->getUniformRandomNumber(this->nPis + 1, nof_objs - this->nPos - 1); + return root_id; + } + + template + void randomizedBFS::checkCandidate(Subcircuit& subcircuit, std::queue& candidates, std::queue& rejected, bool add) { + int obj_id = candidates.front(); + candidates.pop(); + Gia_Obj_t * gia_obj = Gia_ManObj(this->gia_man, obj_id); + if (Gia_ObjIsAnd(gia_obj) && !Gia_ObjIsTravIdCurrent(this->gia_man, gia_obj)) { + if (add) { + Gia_ObjSetTravIdCurrent(this->gia_man, gia_obj); + Vec_IntPush(subcircuit.nodes, obj_id); + candidates.push(Gia_ObjFaninId0(gia_obj, obj_id)); + candidates.push(Gia_ObjFaninId1(gia_obj, obj_id)); + } else { + rejected.push(obj_id); + } + } + } + + template + Subcircuit randomizedBFS::findSubcircuit() { + Subcircuit result; + assert (Gia_ManIsNormalized(this->gia_man)); + int root_id = selectRoot(); + Gia_Obj_t * gia_obj = Gia_ManObj(this->gia_man, root_id); + assert (Gia_ObjIsAnd(gia_obj)); + result.nodes = Vec_IntAlloc(this->cfg.subcircuit_size_bound); + result.io = Vec_IntAlloc(this->cfg.subcircuit_size_bound); + + Vec_IntPush(result.nodes, root_id); + + std::queue candidates; + candidates.push(Gia_ObjFaninId0(gia_obj, root_id)); + candidates.push(Gia_ObjFaninId1(gia_obj, root_id)); + std::queue rejected_nodes; + + Gia_ManIncrementTravId(this->gia_man); + + while (!candidates.empty() && Vec_IntSize(result.nodes) < this->cfg.subcircuit_size_bound) { + checkCandidate(result, candidates, rejected_nodes, this->getRandomBool()); + } + + if (this->cfg.fill_subcircuits) { + while (!rejected_nodes.empty() && Vec_IntSize(result.nodes) < this->cfg.subcircuit_size_bound) { + checkCandidate(result, rejected_nodes, rejected_nodes, true); + } + } + result.nof_inputs = this->getSubcircuitIO(result.nodes, result.io); + return result; + } + + inline bool randomizedBFSnoFP::filterSubcircuitImpl(const Subcircuit& subcir) { + Gia_Obj_t * pObj; + int i; + unsigned int min_output_level = Gia_ManLevelNum(gia_man); + Gia_ManIncrementTravId(gia_man); + Gia_ManForEachObjVecStart(subcir.io, gia_man, pObj, i, subcir.nof_inputs) { + min_output_level = Gia_ObjLevel(gia_man, pObj) < min_output_level ? Gia_ObjLevel(gia_man, pObj) : min_output_level; + Gia_ObjSetTravIdCurrent(gia_man, pObj); + } + Gia_ManIncrementTravId(gia_man); + Gia_ManForEachObjVecStop(subcir.io, gia_man, pObj, i, subcir.nof_inputs) { + if (!filterSubcircuitRec(pObj, min_output_level)) { + return false; + } + } + return true; + } + + inline bool randomizedBFSnoFP::filterSubcircuitRec(Gia_Obj_t * pObj, unsigned int min_level) { + if (Gia_ObjIsTravIdPrevious(gia_man, pObj)) { + return false; + } else if (Gia_ObjIsTravIdCurrent(gia_man, pObj)) { + return true; + } else if (Gia_ObjLevel(gia_man, pObj) < min_level) { + return true; + } + Gia_ObjSetTravIdCurrent(gia_man, pObj); + return filterSubcircuitRec(Gia_ObjFanin0(pObj), min_level) && filterSubcircuitRec(Gia_ObjFanin1(pObj), min_level); + } +} + +ABC_NAMESPACE_CXX_HEADER_END \ No newline at end of file diff --git a/src/opt/eslim/synthesisEngine.hpp b/src/opt/eslim/synthesisEngine.hpp new file mode 100644 index 000000000..d061e761b --- /dev/null +++ b/src/opt/eslim/synthesisEngine.hpp @@ -0,0 +1,240 @@ +/**CFile**************************************************************** + + FileName [synthesisEngine.hpp] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Using Exact Synthesis with the SAT-based Local Improvement Method (eSLIM).] + + Synopsis [Procedures for synthesising Boolean relations.] + + Author [Franz-Xaver Reichl] + + Affiliation [University of Freiburg] + + Date [Ver. 1.0. Started - March 2025.] + + Revision [$Id: synthesisEngine.hpp,v 1.00 2025/03/17 00:00:00 Exp $] + +***********************************************************************/ + +#ifndef ABC__OPT__ESLIM__SYNTHESISENGINE_h +#define ABC__OPT__ESLIM__SYNTHESISENGINE_h + +#include +#include +#include +#include + +#include "misc/util/abc_namespaces.h" +#include "aig/miniaig/miniaig.h" +#include "misc/vec/vec.h" + +#include "satInterfaces.hpp" + +ABC_NAMESPACE_CXX_HEADER_START + +#define MAJ_NOBJS 64 // Const0 + Const1 + nVars + nNodes + +namespace eSLIM { + + // Based on Exa6_ManGenStart + template + class exactSynthesisEngine { + + private: + Vec_Wrd_t * vSimsIn; // input signatures (nWords = 1, nIns <= 64) + Vec_Wrd_t * vSimsOut; // output signatures (nWords = 1, nOuts <= 6) + int nIns; + int nDivs; // divisors (const + inputs + tfi + sidedivs) + int nNodes; + int nOuts; + int nObjs; + int VarMarks[MAJ_NOBJS][2][MAJ_NOBJS] = {}; // default init the array + int nCnfVars; + int nCnfVars2; + int nCnfClauses; + + // Assign outputs to their connectivity variables + std::unordered_map> connection_variables; + const std::unordered_map>& forbidden_pairs; + eSLIMLog& log; + const eSLIMConfig& cfg; + + exactSynthesisEngine( Vec_Wrd_t * vSimsIn, Vec_Wrd_t * vSimsOut, int nIns, int nDivs, int nOuts, int nNodes, + const std::unordered_map>& forbidden_pairs, eSLIMLog& log, const eSLIMConfig& cfg); + int addClause(int lit1, int lit2, int lit3, int lit4); + static bool isNormalized( Vec_Wrd_t * vSimsIn, Vec_Wrd_t * vSimsOut ); + int markup(); + int findFanin( Vec_Int_t * vValues, int i, int k, int nof_objs); + Mini_Aig_t * getAig(Vec_Int_t * assignment, int size); + Mini_Aig_t * getAig(Vec_Int_t * assignment); + void generateCNF(int fOrderNodes, int fUniqFans); + int startEncoding(int fOrderNodes, int fUniqFans ); + void generateMinterm( int iMint); + + int getGateEnablingLiteral(int index, bool negated); + int getAuxilaryVariableCount(); + + void introduceConnectionVariables(); + void setupConnectionVariables(); + void addConnectivityConstraints(); + void addCombinedCycleConstraints(); + std::unordered_map> computeNotInPair(const std::unordered_map>& pairs); + + int prepareLits(int * pLits, int& nLits); + + friend Derived; + }; + + // applies Cadical incrementally + class CadicalEngine : public exactSynthesisEngine { + + public: + CadicalEngine(Vec_Wrd_t * vSimsIn, Vec_Wrd_t * vSimsOut, int nIns, int nDivs, int nOuts, int nNodes, + const std::unordered_map>& forbidden_pairs, eSLIMLog& log, const eSLIMConfig& cfg); + Mini_Aig_t* getCircuit(int size, double timeout); + + private: + using exactSynthesisEngine::addClause; + std::vector gate_enabling_assumptions; + CadicalSolver solver; + + + int addClause( int * pLits, int nLits ); + Vec_Int_t * solve(int size, double timeout); + int getAuxilaryVariableCountDerived(); + int getGateEnablingLiteralImpl(int index, bool negated); + void addAssumptions(int size); + void addGateDeactivatedConstraint(int out); + + std::vector getAssumptions(int size); + + friend exactSynthesisEngine; + }; + + class OneshotEngine { + protected: + int getAuxilaryVariableCountDerived() {return 0;}; + int getGateEnablingLiteralImpl(int index, bool negated) {return 0;}; + // void addAssumptions(int size) {}; + void addGateDeactivatedConstraint(int idx) {}; + }; + + template + class OneshotManager { + public: + OneshotManager(Vec_Wrd_t * vSimsIn, Vec_Wrd_t * vSimsOut, int nIns, int nDivs, int nOuts, int maxnNodes, + const std::unordered_map>& forbidden_pairs, eSLIMLog& log, const eSLIMConfig& cfg); + Mini_Aig_t* getCircuit(int size, double timeout); + + private: + T getOneshotEngine(int size); + + Vec_Wrd_t * vSimsIn; // input signatures (nWords = 1, nIns <= 64) + Vec_Wrd_t * vSimsOut; // output signatures (nWords = 1, nOuts <= 6) + int nIns; + int nDivs; // divisors (const + inputs + tfi + sidedivs) + int maxnNodes; + int nOuts; + + const std::unordered_map>& forbidden_pairs; + eSLIMLog& log; + const eSLIMConfig& cfg; + }; + + class CadicalEngineOneShot : public exactSynthesisEngine, public OneshotEngine { + + public: + CadicalEngineOneShot( Vec_Wrd_t * vSimsIn, Vec_Wrd_t * vSimsOut, int nIns, int nDivs, int nOuts, int nNodes, + const std::unordered_map>& forbidden_pairs, eSLIMLog& log, const eSLIMConfig& cfg); + Mini_Aig_t* getCircuit(int size, double timeout); + + private: + using exactSynthesisEngine::addClause; + + int addClause( int * pLits, int nLits ); + Vec_Int_t * solve(int size, double timeout); + + CadicalSolver solver; + + friend exactSynthesisEngine; + }; + + class KissatEngineOneShot : public exactSynthesisEngine, public OneshotEngine { + + public: + KissatEngineOneShot( Vec_Wrd_t * vSimsIn, Vec_Wrd_t * vSimsOut, int nIns, int nDivs, int nOuts, int nNodes, + const std::unordered_map>& forbidden_pairs, eSLIMLog& log, const eSLIMConfig& cfg); + Mini_Aig_t* getCircuit(int size, double timeout); + + private: + using exactSynthesisEngine::addClause; + + int addClause( int * pLits, int nLits ); + Vec_Int_t * solve(int size, double timeout); + + KissatSolver solver; + + friend exactSynthesisEngine; + }; + + + class KissatCmdEngine : public exactSynthesisEngine, public OneshotEngine { + + public: + KissatCmdEngine( Vec_Wrd_t * vSimsIn, Vec_Wrd_t * vSimsOut, int nIns, int nDivs, int nOuts, int nNodes, + const std::unordered_map>& forbidden_pairs, eSLIMLog& log, const eSLIMConfig& cfg); + Mini_Aig_t* getCircuit(int size, double timeout); + + private: + using exactSynthesisEngine::addClause; + + + int addClause( int * pLits, int nLits ); + Vec_Int_t * solve(int size, double timeout); + + FILE * encoding_file; + + // Ensure that there is no file with the same name in the diretory + constexpr static char * pFileNameIn = "_temp_.cnf"; + constexpr static char * pFileNameOut = "_temp_out.cnf"; + + #ifdef WIN32 + constexpr static char * pKissat = "kissat.exe"; + #else + constexpr static char * pKissat = "kissat"; + #endif + + friend exactSynthesisEngine; + }; + + + template + inline int exactSynthesisEngine::addClause(int lit1, int lit2, int lit3, int lit4) { + int clause[4] = {lit1, lit2, lit3, lit4}; + return static_cast(this)->addClause(clause, 4); + } + + template + inline int exactSynthesisEngine::getGateEnablingLiteral(int index, bool negated) { + return static_cast(this)->getGateEnablingLiteralImpl(index, negated); + } + + template + inline int exactSynthesisEngine::getAuxilaryVariableCount() { + int ncvars = connection_variables.empty() ? 0 : connection_variables.begin()->second.size() * connection_variables.size(); + return ncvars + static_cast(this)->getAuxilaryVariableCountDerived(); + } + + typedef OneshotManager CadicalOneShot; + typedef OneshotManager KissatOneShot; + typedef OneshotManager KissatCmdOneShot; + +} + +ABC_NAMESPACE_CXX_HEADER_END + +#include "synthesisEngine.tpp" + +#endif \ No newline at end of file diff --git a/src/opt/eslim/synthesisEngine.tpp b/src/opt/eslim/synthesisEngine.tpp new file mode 100644 index 000000000..cc1d3d610 --- /dev/null +++ b/src/opt/eslim/synthesisEngine.tpp @@ -0,0 +1,621 @@ +/**CFile**************************************************************** + + FileName [synthesisEngine.tpp] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Using Exact Synthesis with the SAT-based Local Improvement Method (eSLIM).] + + Synopsis [Procedures for synthesising Boolean relations.] + + Author [Franz-Xaver Reichl] + + Affiliation [University of Freiburg] + + Date [Ver. 1.0. Started - March 2025.] + + Revision [$Id: synthesisEngine.tpp,v 1.00 2025/03/17 00:00:00 Exp $] + +***********************************************************************/ + +#include + +#include "misc/util/utilTruth.h" + +#include "synthesisEngine.hpp" +#include "utils.hpp" + +ABC_NAMESPACE_HEADER_START + Vec_Int_t * Exa4_ManParse( char * pFileName ); +ABC_NAMESPACE_HEADER_END + +ABC_NAMESPACE_CXX_HEADER_START + +namespace eSLIM { + + template + exactSynthesisEngine::exactSynthesisEngine( Vec_Wrd_t * vSimsIn, Vec_Wrd_t * vSimsOut, int nIns, int nDivs, int nOuts, int nNodes, + const std::unordered_map>& forbidden_pairs, eSLIMLog& log, const eSLIMConfig& cfg) + : vSimsIn(vSimsIn), vSimsOut(vSimsOut), nIns(nIns), nDivs(nDivs), nNodes(nNodes), + nOuts(nOuts), forbidden_pairs(forbidden_pairs), log(log), cfg(cfg) { + assert( Vec_WrdSize(vSimsIn) == Vec_WrdSize(vSimsOut) ); + nObjs = nDivs + nNodes + nOuts; + nCnfVars = markup(); + introduceConnectionVariables(); + nCnfVars2 = 0; + nCnfClauses = 0; + assert( nObjs < 64 ); + } + + template + bool exactSynthesisEngine::isNormalized( Vec_Wrd_t * vSimsIn, Vec_Wrd_t * vSimsOut ) { + int i, Count = 0; word Temp; + Vec_WrdForEachEntry( vSimsIn, Temp, i ) { + if ( Temp & 1 ) { + Count++; + } + } + if ( Count ) { + return false; + } + if ( !(Vec_WrdEntry(vSimsOut, 0) & 1) ) { + return false; + } + return true; + } + + template + int exactSynthesisEngine::markup() { + int i, k, j, nVars[3] = {1 + 3*nNodes, 0, 3*nNodes*Vec_WrdSize(vSimsIn)}; + assert( nObjs <= MAJ_NOBJS ); + for ( i = nDivs; i < nDivs + nNodes; i++ ) { + for ( k = 0; k < 2; k++ ) { + for ( j = 1+!k; j < i-k; j++ ) { + VarMarks[i][k][j] = nVars[0] + nVars[1]++; + } + } + } + for ( i = nDivs + nNodes; i < nObjs; i++ ) { + for ( j = 0; j < nDivs + nNodes; j++ ) { + VarMarks[i][0][j] = nVars[0] + nVars[1]++; + } + } + return nVars[0] + nVars[1] + nVars[2]; + } + + template + int exactSynthesisEngine::findFanin( Vec_Int_t * vValues, int i, int k, int nof_objs ) { + int j, Count = 0, iVar = -1; + for ( j = 0; j < nof_objs; j++ ) { + if ( VarMarks[i][k][j] && Vec_IntEntry(vValues, VarMarks[i][k][j]) ){ + iVar = j; + Count++; + } + } + assert( Count == 1 ); + return iVar; + } + + template + Mini_Aig_t * exactSynthesisEngine::getAig(Vec_Int_t * vValues) { + return getAig(vValues, nNodes); + } + + template + Mini_Aig_t * exactSynthesisEngine::getAig(Vec_Int_t * vValues, int size) { + assert (size >= 0 && size <= nNodes && "Invalid size for AIG construction given."); + int i, k, Compl[MAJ_NOBJS] = {0}; + int nof_Objs = nDivs + size + nOuts; + Mini_Aig_t * pMini = Mini_AigStartSupport( nDivs-1, nof_Objs ); + for ( i = nDivs; i < nDivs + size; i++ ) { + int iNodes[2] = {0}; + int iVarStart = 1 + 3*(i - nDivs);// + int Val1 = Vec_IntEntry(vValues, iVarStart); + int Val2 = Vec_IntEntry(vValues, iVarStart+1); + int Val3 = Vec_IntEntry(vValues, iVarStart+2); + Compl[i] = Val1 && Val2 && Val3; + for ( k = 0; k < 2; k++ ) { + int iNode = findFanin(vValues, i, !k, nof_Objs); + int fComp = k ? !Val1 && Val2 && !Val3 : Val1 && !Val2 && !Val3; + iNodes[k] = Abc_Var2Lit(iNode, fComp ^ Compl[iNode]); + } + if ( Val1 && Val2 ) { + if ( Val3 ) { + Mini_AigOr( pMini, iNodes[0], iNodes[1] ); + } else { + Mini_AigXorSpecial( pMini, iNodes[0], iNodes[1] ); + } + } else { + Mini_AigAnd( pMini, iNodes[0], iNodes[1] ); + } + } + for ( i = nDivs + nNodes; i < nObjs; i++ ) { + int iVar = findFanin( vValues, i, 0, nof_Objs); + Mini_AigCreatePo( pMini, Abc_Var2Lit(iVar, Compl[iVar]) ); + } + assert( nof_Objs == Mini_AigNodeNum(pMini) ); + return pMini; + } + + template + void exactSynthesisEngine::generateCNF( int fOrderNodes, int fUniqFans ) { + int m; + startEncoding( fOrderNodes, fUniqFans ); + // Ignore pattern for all false input pattern (as we start with m=1) + for ( m = 1; m < Vec_WrdSize(vSimsIn); m++ ) { + generateMinterm( m ); + } + + if (forbidden_pairs.size() > 0) { + addConnectivityConstraints(); + } + } + + template + void exactSynthesisEngine::introduceConnectionVariables() { + std::unordered_set inputs_in_pairs; + // for (const auto& [out, inputs] : forbidden_pairs) { + for (const auto& it: forbidden_pairs) { + const auto& inputs = it.second; + inputs_in_pairs.insert(inputs.begin(), inputs.end()); + } + int nCVars = nObjs - 1; // The constant node does not depend on any node + for (int in : inputs_in_pairs) { + connection_variables.emplace(in, std::vector (nCVars, 0)); + std::iota(connection_variables[in].begin(), connection_variables[in].end(), nCnfVars); + nCnfVars += nCVars; + } + } + + template + void exactSynthesisEngine::setupConnectionVariables() { + // for (const auto& [in, cvars] : connection_variables) { + for (const auto& it: connection_variables) { + const auto& in = it.first; + const auto& cvars = it.second; + addClause(Abc_Var2Lit(cvars[in],0),0,0,0); + for (int i = nDivs; i < nDivs + nNodes; i++ ) { + int gate_idx = i - nDivs; + for (int j = 1; j < i - 1; j++) { + addClause(Abc_Var2Lit(VarMarks[i][0][j + 1], 1), Abc_Var2Lit(cvars[j], 1), Abc_Var2Lit(cvars[i - 1], 0), getGateEnablingLiteral(gate_idx, 1)); + addClause(Abc_Var2Lit(VarMarks[i][1][j], 1), Abc_Var2Lit(cvars[j - 1], 1), Abc_Var2Lit(cvars[i - 1], 0), getGateEnablingLiteral(gate_idx, 1)); + } + } + for (int i = nDivs + nNodes; i < nObjs; i++) { + for (int j = 1; j < nDivs + nNodes; j++) { + addClause(Abc_Var2Lit(VarMarks[i][0][j], 1), Abc_Var2Lit(cvars[j - 1], 1), Abc_Var2Lit(cvars[i - 1], 0),0); + } + } + } + } + + template + void exactSynthesisEngine::addConnectivityConstraints() { + assert (forbidden_pairs.size() > 0 && "Connectivity constraints are only needed if there are forbidden pairs."); + setupConnectionVariables(); + // If there are forbidden pairs for more than one input it is possible that a loop is obtained via two pairs + if (forbidden_pairs.size() > 1) { + addCombinedCycleConstraints(); + } + + // for (const auto& [out, inputs] : forbidden_pairs) { + for (const auto& it: forbidden_pairs) { + const auto& out = it.first; + const auto& inputs = it.second; + for (int in : inputs) { + const auto& cvars = connection_variables.at(in); + int out_obj_idx = nDivs + nNodes + out; + addClause(Abc_Var2Lit(cvars[out_obj_idx - 1], 1), 0, 0, 0); + } + } + } + + template + void exactSynthesisEngine::addCombinedCycleConstraints() { + assert (forbidden_pairs.size() > 1 && "Combined connectivity constraints are only needed if there are forbidden pairs for multiple inputs."); + std::unordered_map> not_in_pair = computeNotInPair(forbidden_pairs); + + // for (const auto& [out, inputs] : not_in_pair) { + for (const auto& it: not_in_pair) { + const auto& out = it.first; + const auto& inputs = it.second; + for (int in : inputs) { + const auto& cvars = connection_variables.at(in); + int out_obj_idx = nDivs + nNodes + out; + for (int in2 : forbidden_pairs.at(out)) { + addClause(Abc_Var2Lit(cvars[out_obj_idx - 1], 1), Abc_Var2Lit(cvars[in2], 0),0,0); + } + } + } + } + + template + std::unordered_map> exactSynthesisEngine::computeNotInPair(const std::unordered_map>& pairs) { + std::unordered_set all_inputs_in_pairs; + // for (const auto& [out, in] : pairs) { + for (const auto& it: pairs) { + const auto& in = it.second; + all_inputs_in_pairs.insert(in.begin(), in.end()); + } + std::unordered_map> not_in_pair; + // for (const auto& [out, in] : pairs) { + for (const auto& it: pairs) { + const auto& out = it.first; + const auto& in = it.second; + if (in.size() == all_inputs_in_pairs.size()) { + continue; + } + for (int i : all_inputs_in_pairs) { + if (in.find(i) == in.end()) { + not_in_pair[out].insert(i); + } + } + } + return not_in_pair; + } + + template + int exactSynthesisEngine::startEncoding(int fOrderNodes, int fUniqFans ) + { + int pLits[2*MAJ_NOBJS], i, j, k, n, m, nLits; + for ( i = nDivs; i < nDivs + nNodes; i++ ) + { + int gate_idx = i - nDivs; + int iVarStart = 1 + 3*(i - nDivs);// + for ( k = 0; k < 2; k++ ) + { + nLits = 0; + for ( j = 0; j < nObjs; j++ ) + if ( VarMarks[i][k][j] ) + pLits[nLits++] = Abc_Var2Lit( VarMarks[i][k][j], 0 ); + assert( nLits > 0 ); + static_cast(this)->addClause( pLits, nLits ); + for ( n = 0; n < nLits; n++ ) + for ( m = n+1; m < nLits; m++ ) + addClause( Abc_LitNot(pLits[n]), Abc_LitNot(pLits[m]), getGateEnablingLiteral(gate_idx, 1), 0 ); + if ( k == 1 ) + break; + for ( j = 0; j < nObjs; j++ ) if ( VarMarks[i][0][j] ) + for ( n = j; n < nObjs; n++ ) if ( VarMarks[i][1][n] ) + addClause( Abc_Var2Lit(VarMarks[i][0][j], 1), Abc_Var2Lit(VarMarks[i][1][n], 1), getGateEnablingLiteral(gate_idx, 1), 0 ); + } + if ( fOrderNodes ) + for ( j = nDivs; j < i; j++ ) + for ( n = 0; n < nObjs; n++ ) if ( VarMarks[i][0][n] ) + for ( m = n+1; m < nObjs; m++ ) if ( VarMarks[j][0][m] ) + addClause( Abc_Var2Lit(VarMarks[i][0][n], 1), Abc_Var2Lit(VarMarks[j][0][m], 1), getGateEnablingLiteral(gate_idx, 1), 0 ); + for ( j = nDivs; j < i; j++ ) + for ( k = 0; k < 2; k++ ) if ( VarMarks[i][k][j] ) + for ( n = 0; n < nObjs; n++ ) if ( VarMarks[i][!k][n] ) + for ( m = 0; m < 2; m++ ) if ( VarMarks[j][m][n] ) + addClause( Abc_Var2Lit(VarMarks[i][k][j], 1), Abc_Var2Lit(VarMarks[i][!k][n], 1), Abc_Var2Lit(VarMarks[j][m][n], 1), getGateEnablingLiteral(gate_idx, 1) ); + for ( k = 0; k < 3; k++ ) + addClause( Abc_Var2Lit(iVarStart, k==1), Abc_Var2Lit(iVarStart+1, k==2), Abc_Var2Lit(iVarStart+2, k!=0), getGateEnablingLiteral(gate_idx, 1)); + if ( !cfg.allow_xors ) + addClause( Abc_Var2Lit(iVarStart, 1), Abc_Var2Lit(iVarStart+1, 1), Abc_Var2Lit(iVarStart+2, 0), getGateEnablingLiteral(gate_idx, 1)); + + } + for ( i = nDivs; i < nDivs + nNodes; i++ ) + { + int gate_idx = i - nDivs; + nLits = 0; + for ( k = 0; k < 2; k++ ) + for ( j = i+1; j < nObjs; j++ ) + if ( VarMarks[j][k][i] ) + pLits[nLits++] = Abc_Var2Lit( VarMarks[j][k][i], 0 ); + if ( fUniqFans ) + for ( n = 0; n < nLits; n++ ) + for ( m = n+1; m < nLits; m++ ) + addClause( Abc_LitNot(pLits[n]), Abc_LitNot(pLits[m]), getGateEnablingLiteral(gate_idx, 1), 0 ); + } + for ( i = nDivs + nNodes; i < nObjs; i++ ) + { + static_cast(this)->addGateDeactivatedConstraint(i); + nLits = 0; + for ( j = 0; j < nDivs + nNodes; j++ ) if ( VarMarks[i][0][j] ) { + pLits[nLits++] = Abc_Var2Lit( VarMarks[i][0][j], 0 ); + } + static_cast(this)->addClause( pLits, nLits ); + for ( n = 0; n < nLits; n++ ) + for ( m = n+1; m < nLits; m++ ) + addClause( Abc_LitNot(pLits[n]), Abc_LitNot(pLits[m]), 0, 0 ); + } + return 1; + } + + template + void exactSynthesisEngine::generateMinterm( int iMint) { + int internalCnfVars = nCnfVars - getAuxilaryVariableCount(); // for each gate we add an assumption + int iNodeVar = internalCnfVars + 3*nNodes*(iMint - Vec_WrdSize(vSimsIn)); + int iOutMint = Abc_Tt6FirstBit( Vec_WrdEntry(vSimsOut, iMint) ); + int fOnlyOne = Abc_TtSuppOnlyOne( (int)Vec_WrdEntry(vSimsOut, iMint) ); + int i, k, n, j, VarVals[MAJ_NOBJS]; + int fAllOnes = Abc_TtCountOnes( Vec_WrdEntry(vSimsOut, iMint) ) == (1 << nOuts); + if ( fAllOnes ) + return; + assert( nObjs <= MAJ_NOBJS ); + assert( iMint < Vec_WrdSize(vSimsIn) ); + assert( nOuts <= 6 ); + for ( i = 0; i < nDivs; i++ ) { + VarVals[i] = (Vec_WrdEntry(vSimsIn, iMint) >> i) & 1; + } + for ( i = 0; i < nNodes; i++ ) { + VarVals[nDivs + i] = Abc_Var2Lit(iNodeVar + 3*i + 2, 0); + } + if ( fOnlyOne ) { + for ( i = 0; i < nOuts; i++ ) + VarVals[nDivs + nNodes + i] = (iOutMint >> i) & 1; + } else { + word t = Abc_Tt6Stretch( Vec_WrdEntry(vSimsOut, iMint), nOuts ); + int i, c, nCubes = 0, pCover[100], pLits[10]; + int iOutVar = nCnfVars + nCnfVars2; nCnfVars2 += nOuts; + for ( i = 0; i < nOuts; i++ ) { + VarVals[nDivs + nNodes + i] = Abc_Var2Lit(iOutVar + i, 0); + } + assert( t ); + if ( ~t ) { + Abc_Tt6IsopCover( ~t, ~t, nOuts, pCover, &nCubes ); + for ( c = 0; c < nCubes; c++ ) { + int nLits = 0; + for ( i = 0; i < nOuts; i++ ) { + int iLit = (pCover[c] >> (2*i)) & 3; + if ( iLit == 1 || iLit == 2 ) + pLits[nLits++] = Abc_Var2Lit(iOutVar + i, iLit != 1); + } + static_cast(this)->addClause( pLits, nLits ); + } + } + } + + for ( i = nDivs; i < nDivs + nNodes; i++ ) { + int iVarStart = 1 + 3*(i - nDivs);// + int iBaseVarI = iNodeVar + 3*(i - nDivs); + for ( k = 0; k < 2; k++ ) { + for ( j = 0; j < i; j++ ) { + if ( VarMarks[i][k][j] ) { + for ( n = 0; n < 2; n++ ) { + addClause( Abc_Var2Lit(VarMarks[i][k][j], 1), Abc_Var2Lit(iBaseVarI + k, n), Abc_LitNotCond(VarVals[j], !n), 0); + } + } + } + } + for ( k = 0; k < 4; k++ ) { + for ( n = 0; n < 2; n++ ) { + addClause( Abc_Var2Lit(iBaseVarI + 0, k&1), Abc_Var2Lit(iBaseVarI + 1, k>>1), Abc_Var2Lit(iBaseVarI + 2, !n), Abc_Var2Lit(k ? iVarStart + k-1 : 0, n)); + } + } + } + for ( i = nDivs + nNodes; i < nObjs; i++ ) { + for ( j = 0; j < nDivs + nNodes; j++ ) { + if ( VarMarks[i][0][j] ) { + for ( n = 0; n < 2; n++ ) { + addClause( Abc_Var2Lit(VarMarks[i][0][j], 1), Abc_LitNotCond(VarVals[j], n), Abc_LitNotCond(VarVals[i], !n), 0); + } + } + } + } + } + + template + int exactSynthesisEngine::prepareLits(int * pLits, int& nLits) { + int k = 0; + for ( int i = 0; i < nLits; i++ ) { + if ( pLits[i] == 1 ) + return 0; + else if ( pLits[i] == 0 ) + continue; + else if ( pLits[i] <= 2*(nCnfVars + nCnfVars2) ) + pLits[k++] = pLits[i]; + else assert( 0 ); + } + nLits = k; + return 1; + } + + inline CadicalEngine::CadicalEngine(Vec_Wrd_t * vSimsIn, Vec_Wrd_t * vSimsOut, int nIns, int nDivs, int nOuts, int nNodes, + const std::unordered_map>& forbidden_pairs, eSLIMLog& log, const eSLIMConfig& cfg) + : exactSynthesisEngine(vSimsIn, vSimsOut, nIns, nDivs, nOuts, nNodes, forbidden_pairs, log, cfg) { + gate_enabling_assumptions.reserve(nNodes); + for (int i = 0; i < nNodes; i++) { + gate_enabling_assumptions.push_back(nCnfVars + i); + } + nCnfVars += nNodes; + generateCNF(0, 0); + } + + inline int CadicalEngine::addClause( int * pLits, int nLits ) { + if (prepareLits(pLits, nLits) == 0) { + return 0; + } + assert( nLits > 0 ); + solver.addClause(pLits, nLits); + return 1; + } + + inline Vec_Int_t * CadicalEngine::solve( int size, double timeout) { + std::vector assumptions = getAssumptions(size); + solver.assume(assumptions); + int status = timeout > 0 ? solver.solve(timeout) : solver.solve(); + Vec_Int_t * vRes = status == 10 ? solver.getModelVec() : nullptr; + if (status == 10) { + log.cummulative_sat_runtimes_per_size[size] += solver.getRunTime(); + log.nof_sat_calls_per_size[size] ++; + } else if (status == 20) { + log.cummulative_unsat_runtimes_per_size[size] += solver.getRunTime(); + log.nof_unsat_calls_per_size[size] ++; + } + return vRes; + } + + Mini_Aig_t* CadicalEngine::getCircuit(int size, double timeout) { + addAssumptions(size); + Vec_Int_t * vValues = solve(size, timeout); + Mini_Aig_t * pMini = vValues ? getAig(vValues, size) : nullptr; + Vec_IntFreeP( &vValues ); + return pMini; + } + + inline std::vector CadicalEngine::getAssumptions(int size) { + std::vector assumptions(nNodes); + for (int i = 0; i < size; i++) { + assumptions[i] = gate_enabling_assumptions[i]; + } + for (int i = size; i < nNodes; i++) { + assumptions[i] = -gate_enabling_assumptions[i]; + } + return assumptions; + } + + inline void CadicalEngine::addGateDeactivatedConstraint(int out_idx) { + for (int j = nDivs; j < nDivs + nNodes; j++ ) { + int gate_idx = j - nDivs; + // if a gate is disabled then it shall not be an output + addClause( Abc_Var2Lit(VarMarks[out_idx][0][j],1), Abc_Var2Lit( gate_enabling_assumptions[gate_idx], 0 ), 0, 0 ); + } + } + + inline int CadicalEngine::getGateEnablingLiteralImpl(int index, bool negated) { + return Abc_Var2Lit( gate_enabling_assumptions[index], negated ); + } + + inline int CadicalEngine::getAuxilaryVariableCountDerived() { + return nNodes; // We add an assumption for each gate + } + + inline void CadicalEngine::addAssumptions(int size) { + solver.assume(getAssumptions(size)); + } + + template + OneshotManager::OneshotManager(Vec_Wrd_t * vSimsIn, Vec_Wrd_t * vSimsOut, int nIns, int nDivs, int nOuts, int maxnNodes, + const std::unordered_map>& forbidden_pairs, eSLIMLog& log, const eSLIMConfig& cfg) + : vSimsIn(vSimsIn), vSimsOut(vSimsOut), nIns(nIns), nDivs(nDivs), maxnNodes(maxnNodes), nOuts(nOuts), forbidden_pairs(forbidden_pairs), log(log), cfg(cfg) { + } + + template + T OneshotManager::getOneshotEngine(int size) { + assert(size <= maxnNodes); + T oneshotEngine(vSimsIn, vSimsOut, nIns, nDivs, nOuts, size, forbidden_pairs, log, cfg); + return oneshotEngine; + } + + template + Mini_Aig_t* OneshotManager::getCircuit(int size, double timeout) { + T synth = getOneshotEngine(size); + return synth.getCircuit(size, timeout); + } + + inline CadicalEngineOneShot::CadicalEngineOneShot( Vec_Wrd_t * vSimsIn, Vec_Wrd_t * vSimsOut, int nIns, int nDivs, int nOuts, int nNodes, + const std::unordered_map>& forbidden_pairs, eSLIMLog& log, const eSLIMConfig& cfg) + : exactSynthesisEngine(vSimsIn, vSimsOut, nIns, nDivs, nOuts, nNodes, forbidden_pairs, log, cfg) { + } + + inline Vec_Int_t* CadicalEngineOneShot::solve( int size, double timeout) { + int status = timeout > 0 ? solver.solve(timeout) : solver.solve(); + Vec_Int_t * vRes = status != 10 ? nullptr : solver.getModelVec(); + return vRes; + } + + Mini_Aig_t* CadicalEngineOneShot::getCircuit(int size, double timeout) { + generateCNF(0, 0); + Vec_Int_t * vValues = solve(size, timeout); + Mini_Aig_t * pMini = vValues ? getAig(vValues, size) : nullptr; + Vec_IntFreeP( &vValues ); + return pMini; + } + + inline int CadicalEngineOneShot::addClause( int * pLits, int nLits ) { + if (prepareLits(pLits, nLits) == 0) { + return 0; + } + assert( nLits > 0 ); + solver.addClause(pLits, nLits); + return 1; + } + + inline KissatEngineOneShot::KissatEngineOneShot(Vec_Wrd_t * vSimsIn, Vec_Wrd_t * vSimsOut, int nIns, int nDivs, int nOuts, int nNodes, + const std::unordered_map>& forbidden_pairs, eSLIMLog& log, const eSLIMConfig& cfg) + : exactSynthesisEngine(vSimsIn, vSimsOut, nIns, nDivs, nOuts, nNodes, forbidden_pairs, log, cfg) { + } + + Mini_Aig_t* KissatEngineOneShot::getCircuit(int size, double timeout) { + solver.init(nCnfVars); + generateCNF(0, 0); + Vec_Int_t * vValues = solve(size, timeout); + Mini_Aig_t * pMini = vValues ? getAig(vValues, size) : nullptr; + Vec_IntFreeP( &vValues ); + return pMini; + } + + inline Vec_Int_t *KissatEngineOneShot::solve( int size, double timeout) { + // TODO: The used interface does not yet allow timeouts + int status = solver.solve(); + Vec_Int_t * vRes = status != 10 ? nullptr : solver.getModelVec(); + return vRes; + } + + inline int KissatEngineOneShot::addClause( int * pLits, int nLits ) { + if (prepareLits(pLits, nLits) == 0) { + return 0; + } + assert( nLits > 0 ); + solver.addClause(pLits, nLits); + return 1; + } + + inline KissatCmdEngine::KissatCmdEngine(Vec_Wrd_t * vSimsIn, Vec_Wrd_t * vSimsOut, int nIns, int nDivs, int nOuts, int nNodes, + const std::unordered_map>& forbidden_pairs, eSLIMLog& log, const eSLIMConfig& cfg) + : exactSynthesisEngine(vSimsIn, vSimsOut, nIns, nDivs, nOuts, nNodes, forbidden_pairs, log, cfg) { + } + + Mini_Aig_t* KissatCmdEngine::getCircuit(int size, double timeout) { + encoding_file = fopen( pFileNameIn, "wb" ); + fputs( "p cnf \n", encoding_file ); + generateCNF(0, 0); + Vec_Int_t * vValues = solve(size, timeout); + Mini_Aig_t * pMini = vValues ? getAig(vValues, size) : nullptr; + Vec_IntFreeP( &vValues ); + return pMini; + } + + inline int KissatCmdEngine::addClause( int * pLits, int nLits ) { + if (prepareLits(pLits, nLits) == 0) { + return 0; + } + assert( nLits > 0 ); + if ( encoding_file ) { + nCnfClauses++; + for ( int i = 0; i < nLits; i++ ) { + fprintf( encoding_file, "%s%d ", Abc_LitIsCompl(pLits[i]) ? "-" : "", Abc_Lit2Var(pLits[i]) ); + } + fprintf( encoding_file, "0\n" ); + } + return 1; + } + + inline Vec_Int_t * KissatCmdEngine::solve(int size, double timeout) { + rewind( encoding_file ); + fprintf( encoding_file, "p cnf %d %d", nCnfVars + nCnfVars2, nCnfClauses ); + fclose( encoding_file ); + encoding_file = nullptr; + + char Command[1000], * pCommand = (char *)&Command; + + // TODO: + // if ( TimeOut ) + // sprintf( pCommand, "%s --time=%d -q %s > %s", pKissat, TimeOut, pFileNameIn, pFileNameOut ); + // else + // sprintf( pCommand, "%s -q %s > %s", pKissat, pFileNameIn, pFileNameOut ); + + sprintf( pCommand, "%s -q %s > %s", pKissat, pFileNameIn, pFileNameOut ); + if ( system( pCommand ) == -1 ) { + std::cerr << "Command " << pCommand << " failed\n"; + return nullptr; + } + Vec_Int_t * vRes = Exa4_ManParse( pFileNameOut ); + return vRes; + } + +} + +ABC_NAMESPACE_CXX_HEADER_END \ No newline at end of file diff --git a/src/opt/eslim/utils.hpp b/src/opt/eslim/utils.hpp new file mode 100644 index 000000000..bcf2262c1 --- /dev/null +++ b/src/opt/eslim/utils.hpp @@ -0,0 +1,103 @@ +/**CFile**************************************************************** + + FileName [utils.hpp] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Using Exact Synthesis with the SAT-based Local Improvement Method (eSLIM).] + + Synopsis [Utilities for the eSLIM package.] + + Author [Franz-Xaver Reichl] + + Affiliation [University of Freiburg] + + Date [Ver. 1.0. Started - March 2025.] + + Revision [$Id: utils.hpp,v 1.00 2025/03/17 00:00:00 Exp $] + +***********************************************************************/ + +#ifndef ABC__OPT__ESLIM__UTILS_h +#define ABC__OPT__ESLIM__UTILS_h + +#include +#include +#include + +#include "misc/util/abc_namespaces.h" +#include "misc/vec/vec.h" +#include "aig/gia/gia.h" + +ABC_NAMESPACE_CXX_HEADER_START + +namespace eSLIM { + + struct eSLIMConfig { + bool extended_normality_processing = false; + bool apply_strash = true; + bool fix_seed = false; + bool fill_subcircuits = false; + bool trial_limit_active = true; + bool allow_xors = false; + + unsigned int timeout = 3600; + unsigned int iterations = 0; + unsigned int subcircuit_size_bound = 6; + unsigned int strash_intervall = 100; + int seed = 0; + unsigned int nselection_trials = 100; + double expansion_probability = 0.6; + + // times given in sec + int minimum_sat_timeout = 1; + int base_sat_timeout = 120; + int minimum_dynamic_timeout_sample_size = 50; + double dynamic_timeout_buffer_factor = 1.4; + + int verbose = 0; + }; + + struct eSLIMLog { + unsigned int iteration_count = 0; + double relation_generation_time = 0; + double synthesis_time = 0; + unsigned int subcircuits_with_forbidden_pairs = 0; + + std::vector nof_analyzed_circuits_per_size; + std::vector nof_replaced_circuits_per_size; + std::vector nof_reduced_circuits_per_size; + + std::vector cummulative_sat_runtimes_per_size; + std::vector nof_sat_calls_per_size; + std::vector cummulative_unsat_runtimes_per_size; + std::vector nof_unsat_calls_per_size; + + eSLIMLog(int size); + }; + + struct Subcircuit { + Vec_Int_t* nodes; + Vec_Int_t* io; + unsigned int nof_inputs; + std::unordered_map> forbidden_pairs; + void free(); + }; + + inline void Subcircuit::free() { + Vec_IntFree(nodes); + Vec_IntFree(io); + } + + inline eSLIMLog::eSLIMLog(int size) + : nof_analyzed_circuits_per_size(size + 1, 0), nof_replaced_circuits_per_size(size + 1, 0), + nof_reduced_circuits_per_size(size + 1, 0), cummulative_sat_runtimes_per_size(size + 1, 0), + nof_sat_calls_per_size(size + 1, 0), cummulative_unsat_runtimes_per_size(size + 1, 0), + nof_unsat_calls_per_size(size + 1, 0) { + } + +} + +ABC_NAMESPACE_CXX_HEADER_END + +#endif \ No newline at end of file