mirror of https://github.com/YosysHQ/abc.git
Add command &eslim
This commit is contained in:
Franz Reichl
parent
e7dd9151b1
commit
8ffca32372
2
Makefile
2
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 \
|
||||
|
|
|
|||
40
abclib.dsp
40
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"
|
||||
|
||||
|
|
|
|||
|
|
@ -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 <num>] [-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 <num> : the timeout in seconds for the individual deepsyn runs [default = %d]\n", deepsynTimeout );
|
||||
Abc_Print( -2, "\t-I <num> : the maximal number of iterations (0 = no limit) for the individual eSLIM runs [default = %d]\n", params.iterations );
|
||||
Abc_Print( -2, "\t-P <num> : the probability of expanding a node [default = %.2f]\n", params.expansion_probability );
|
||||
Abc_Print( -2, "\t-R <num> : the number of runs of eSLIM + Inprocessing [default = %d]\n", nruns );
|
||||
Abc_Print( -2, "\t-S <num> : the maximal size of considered subcircuits [default = %d]\n", params.subcircuit_size_bound );
|
||||
Abc_Print( -2, "\t-T <num> : the timeout in seconds for the individual eSLIM runs [default = %d]\n", params.timeout );
|
||||
Abc_Print( -2, "\t-V <num> : the verbosity level [default = %d]\n", params.verbose);
|
||||
Abc_Print( -2, "\t-Z <num> : 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 ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
|
|
|||
|
|
@ -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<eSLIM::CadicalEngine, eSLIM::RelationGeneratorABC, eSLIM::randomizedBFSFP>::applyeSLIM(pGia, params, log);
|
||||
} else {
|
||||
return eSLIM::eSLIM_Man<eSLIM::CadicalEngine, eSLIM::RelationGeneratorABC, eSLIM::randomizedBFSnoFP>::applyeSLIM(pGia, params, log);
|
||||
};
|
||||
case 1:
|
||||
if (allow_forbidden_pairs) {
|
||||
return eSLIM::eSLIM_Man<eSLIM::KissatOneShot, eSLIM::RelationGeneratorABC, eSLIM::randomizedBFSFP>::applyeSLIM(pGia, params, log);
|
||||
} else {
|
||||
return eSLIM::eSLIM_Man<eSLIM::KissatOneShot, eSLIM::RelationGeneratorABC, eSLIM::randomizedBFSnoFP>::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<double>(log.cummulative_sat_runtimes_per_size[i]) / (1000 * log.nof_sat_calls_per_size[i]) << " sec\n";
|
||||
}
|
||||
}
|
||||
for (int i = 0; i < log.nof_unsat_calls_per_size.size(); i++) {
|
||||
if (log.nof_unsat_calls_per_size[i] == 0) {
|
||||
std::cout << "#gates: " << i << " - avg. unsat time: -\n";
|
||||
} else {
|
||||
std::cout << "#gates: " << i << " - avg. unsat time: " << static_cast<double>(log.cummulative_unsat_runtimes_per_size[i]) / (1000* log.nof_unsat_calls_per_size[i]) << " sec\n";
|
||||
}
|
||||
}
|
||||
}
|
||||
return pThis;
|
||||
}
|
||||
|
||||
ABC_NAMESPACE_IMPL_END
|
||||
|
|
@ -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
|
||||
|
|
@ -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 <vector>
|
||||
#include <unordered_map>
|
||||
#include <unordered_set>
|
||||
|
||||
#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 SynthesisEngine, class RelationEngine, class SelectionEngine>
|
||||
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<int, Mini_Aig_t*> reduce( Vec_Wrd_t* vSimsDiv, Vec_Wrd_t* vSimsOut, const std::unordered_map<int, std::unordered_set<int>>& 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<int> processReplacement(Gia_Man_t* gia_man, Gia_Man_t* pNew, const Subcircuit& subcir, Mini_Aig_t* replacement, std::vector<int>&& to_process, std::vector<int>& 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<int>& 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 <typename Y, typename R, typename S>
|
||||
inline Gia_Man_t* eSLIM_Man<Y, R, S>::getCircuit() {
|
||||
return gia_man;
|
||||
}
|
||||
}
|
||||
|
||||
ABC_NAMESPACE_CXX_HEADER_END
|
||||
|
||||
#include "eSLIMMan.tpp"
|
||||
|
||||
#endif
|
||||
|
|
@ -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 <cassert>
|
||||
#include <queue>
|
||||
#include <vector>
|
||||
#include <tuple>
|
||||
#include <unordered_set>
|
||||
#include <iostream>
|
||||
#include <climits>
|
||||
|
||||
#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 <typename Y, typename R, typename S>
|
||||
Gia_Man_t* eSLIM_Man<Y, R, S>::applyeSLIM(Gia_Man_t * p, const eSLIMConfig& cfg, eSLIMLog& log) {
|
||||
eSLIM_Man<Y, R, S> 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 <typename Y, typename R, typename S>
|
||||
eSLIM_Man<Y, R, S>::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 <typename Y, typename R, typename S>
|
||||
void eSLIM_Man<Y, R, S>::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 <typename Y, typename R, typename S>
|
||||
Abc_RData_t* eSLIM_Man<Y, R, S>::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 <typename Y, typename R, typename S>
|
||||
Vec_Int_t* eSLIM_Man<Y, R, S>::generateRelationPatterns(const Subcircuit& subcir) {
|
||||
Vec_Int_t * vRes = RelationGenerator<R>::computeRelation(gia_man, subcir);
|
||||
if ( vRes == NULL ) {
|
||||
return nullptr;
|
||||
}
|
||||
return vRes;
|
||||
}
|
||||
|
||||
template <typename Y, typename R, typename S>
|
||||
Abc_RData_t* eSLIM_Man<Y, R, S>::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 <typename Y, typename R, typename S>
|
||||
Vec_Wrd_t* eSLIM_Man<Y, R, S>::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 <typename Y, typename R, typename S>
|
||||
Vec_Wrd_t* eSLIM_Man<Y, R, S>::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 <typename Y, typename R, typename S>
|
||||
void eSLIM_Man<Y, R, S>::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 <typename Y, typename R, typename S>
|
||||
Mini_Aig_t* eSLIM_Man<Y, R, S>::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 <typename Y, typename R, typename S>
|
||||
word eSLIM_Man<Y, R, S>::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 <typename Y, typename R, typename S>
|
||||
bool eSLIM_Man<Y, R, S>::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 <typename Y, typename R, typename S>
|
||||
int eSLIM_Man<Y, R, S>::getInsertionLiteral(Gia_Man_t* gia_man, const Subcircuit& subcir, Mini_Aig_t* replacement, const std::vector<int>& 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 <typename Y, typename R, typename S>
|
||||
std::vector<int> eSLIM_Man<Y, R, S>::processReplacement(Gia_Man_t* gia_man, Gia_Man_t* pNew, const Subcircuit& subcir, Mini_Aig_t* replacement, std::vector<int>&& to_process, std::vector<int>& replacement_values) {
|
||||
std::vector<int> 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 <typename Y, typename R, typename S>
|
||||
Vec_Int_t * eSLIM_Man<Y, R, S>::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 <typename Y, typename R, typename S>
|
||||
void eSLIM_Man<Y, R, S>::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<int> to_process_replacement;
|
||||
Mini_AigForEachAnd(replacement, i) {
|
||||
to_process_replacement.push_back(i);
|
||||
}
|
||||
std::vector<int> 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 <typename Y, typename R, typename S>
|
||||
std::pair<int, Mini_Aig_t*> eSLIM_Man<Y, R, S>::reduce(Vec_Wrd_t* vSimsDiv, Vec_Wrd_t* vSimsOut, const std::unordered_map<int, std::unordered_set<int>>& 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 <typename Y, typename R, typename S>
|
||||
double eSLIM_Man<Y, R, S>::getDynamicTimeout(int size) {
|
||||
if (this->log.nof_sat_calls_per_size[size] > cfg.minimum_dynamic_timeout_sample_size) {
|
||||
return std::max(static_cast<double>(cfg.minimum_sat_timeout), static_cast<double>(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 <typename Y, typename R, typename S>
|
||||
Mini_Aig_t* eSLIM_Man<Y, R, S>::computeReplacement(Y& syn_man, int size) {
|
||||
return syn_man.getCircuit(size, getDynamicTimeout(size));
|
||||
}
|
||||
|
||||
}
|
||||
|
||||
ABC_NAMESPACE_CXX_HEADER_END
|
||||
|
|
@ -0,0 +1,2 @@
|
|||
SRC += src/opt/eslim/relationGeneration.cpp \
|
||||
src/opt/eslim/eSLIM.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 <cassert>
|
||||
|
||||
#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
|
||||
|
|
@ -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 <vector>
|
||||
#include <unordered_map>
|
||||
#include <unordered_set>
|
||||
|
||||
#include "misc/util/abc_namespaces.h"
|
||||
#include <misc/util/abc_global.h>
|
||||
#include "aig/gia/gia.h"
|
||||
|
||||
#include "utils.hpp"
|
||||
// #include "satInterfaces.hpp"
|
||||
|
||||
|
||||
ABC_NAMESPACE_CXX_HEADER_START
|
||||
|
||||
namespace eSLIM {
|
||||
|
||||
template<class Derived>
|
||||
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<RelationGeneratorABC> {
|
||||
|
||||
private:
|
||||
RelationGeneratorABC(Gia_Man_t* pGia, const Subcircuit& subcir);
|
||||
void setupImpl() {};
|
||||
Vec_Int_t* getRelationImpl();
|
||||
Gia_Man_t * generateMiter();
|
||||
|
||||
std::unordered_set<int> inputs_in_forbidden_pairs;
|
||||
|
||||
friend RelationGenerator;
|
||||
};
|
||||
|
||||
|
||||
// Add other engine for the generation of relations
|
||||
// class MyRelationGenerator : public RelationGenerator<MyRelationGenerator> {
|
||||
// private:
|
||||
// void setupImpl()
|
||||
// Vec_Int_t* getRelationImpl();
|
||||
// friend RelationGenerator;
|
||||
// };
|
||||
|
||||
|
||||
template <typename T>
|
||||
inline RelationGenerator<T>::RelationGenerator(Gia_Man_t* pGia, const Subcircuit& subcir)
|
||||
: pGia(pGia), subcir(subcir) {
|
||||
}
|
||||
|
||||
template <typename T>
|
||||
inline Vec_Int_t* RelationGenerator<T>::computeRelation(Gia_Man_t* gia_man, const Subcircuit& subcir) {
|
||||
T generator(gia_man, subcir);
|
||||
generator.setup();
|
||||
return generator.getRelation();
|
||||
}
|
||||
|
||||
template <typename T>
|
||||
inline void RelationGenerator<T>::setup() {
|
||||
static_cast<T*>(this)->setupImpl();
|
||||
}
|
||||
|
||||
template <typename T>
|
||||
inline Vec_Int_t* RelationGenerator<T>::getRelation() {
|
||||
return static_cast<T*>(this)->getRelationImpl();
|
||||
}
|
||||
}
|
||||
|
||||
ABC_NAMESPACE_CXX_HEADER_END
|
||||
|
||||
#endif
|
||||
|
|
@ -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 <vector>
|
||||
#include <chrono>
|
||||
#include <iostream>
|
||||
|
||||
#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<int>& 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<std::chrono::steady_clock> 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<double> 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<int>& assumptions) {
|
||||
for (auto& l: assumptions) {
|
||||
solver.assume(l);
|
||||
}
|
||||
}
|
||||
|
||||
inline int CadicalSolver::solve() {
|
||||
std::chrono::time_point<std::chrono::steady_clock> start = std::chrono::steady_clock::now();
|
||||
int status = solver.solve();
|
||||
last_runtime = std::chrono::duration_cast<std::chrono::milliseconds>(std::chrono::steady_clock::now() - start).count();
|
||||
return status;
|
||||
}
|
||||
|
||||
inline int CadicalSolver::solve(double timeout) {
|
||||
std::chrono::time_point<std::chrono::steady_clock> 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::milliseconds>(std::chrono::steady_clock::now() - start).count();
|
||||
if (solver.state() == CaDiCaL::INVALID) {
|
||||
std::cerr<<"Solver is in invalid state"<<std::endl;
|
||||
return -1;
|
||||
}
|
||||
solver.disconnect_terminator();
|
||||
return status;
|
||||
}
|
||||
|
||||
inline Vec_Int_t* CadicalSolver::getModelVec() {
|
||||
Vec_Int_t* assignment = Vec_IntAlloc( solver.vars() );
|
||||
for (int v = 1; v <= solver.vars(); v++) {
|
||||
Vec_IntSetEntryFull( assignment, Abc_AbsInt(val(v)), val(v) > 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
|
||||
|
|
@ -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 <random>
|
||||
#include <queue>
|
||||
|
||||
#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<typename T>
|
||||
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<int, std::unordered_set<int>> 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<int, std::unordered_set<int>>& pairs, const std::unordered_map<int,int>& 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<std::mt19937::result_type> udistr;
|
||||
|
||||
};
|
||||
|
||||
template<typename T>
|
||||
class randomizedBFS : public SelectionStrategy<T> {
|
||||
private:
|
||||
randomizedBFS(Gia_Man_t*& gia_man, const eSLIMConfig& cfg, eSLIMLog& log);
|
||||
Subcircuit findSubcircuit();
|
||||
int selectRoot();
|
||||
void checkCandidate(Subcircuit& subcircuit, std::queue<int>& candidate, std::queue<int>& rejected, bool add);
|
||||
const int nPis;
|
||||
const int nPos;
|
||||
friend SelectionStrategy<T>;
|
||||
friend T;
|
||||
};
|
||||
|
||||
class randomizedBFSFP : public randomizedBFS<randomizedBFSFP> {
|
||||
public :
|
||||
randomizedBFSFP(Gia_Man_t*& gia_man, const eSLIMConfig& cfg, eSLIMLog& log);
|
||||
private:
|
||||
Subcircuit getSubcircuitImpl();
|
||||
bool filterSubcircuitImpl(const Subcircuit& subcir);
|
||||
|
||||
friend SelectionStrategy<randomizedBFSFP>;
|
||||
};
|
||||
|
||||
class randomizedBFSnoFP : public randomizedBFS<randomizedBFSnoFP> {
|
||||
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<randomizedBFSnoFP>;
|
||||
};
|
||||
|
||||
|
||||
template<typename T>
|
||||
SelectionStrategy<T>::SelectionStrategy(Gia_Man_t*& gia_man, const eSLIMConfig& cfg, eSLIMLog& log)
|
||||
: gia_man(gia_man), cfg(cfg), log(log), rng(std::random_device()()) {
|
||||
}
|
||||
|
||||
template<typename T>
|
||||
void SelectionStrategy<T>::setSeed(int seed) {
|
||||
rng.seed(seed);
|
||||
}
|
||||
|
||||
template<typename T>
|
||||
unsigned int SelectionStrategy<T>::getUniformRandomNumber(unsigned int lower, unsigned int upper) {
|
||||
udistr.param(std::uniform_int_distribution<std::mt19937::result_type>::param_type(lower, upper));
|
||||
return udistr(rng);
|
||||
}
|
||||
|
||||
template<typename T>
|
||||
bool SelectionStrategy<T>::getRandomBool() {
|
||||
return bdist(rng);
|
||||
}
|
||||
|
||||
template<typename T>
|
||||
randomizedBFS<T>::randomizedBFS(Gia_Man_t*& gia_man, const eSLIMConfig& cfg, eSLIMLog& log)
|
||||
: SelectionStrategy<T>(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<randomizedBFSFP>(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<randomizedBFSnoFP>(gia_man, cfg, log) {
|
||||
}
|
||||
|
||||
inline bool randomizedBFSFP::filterSubcircuitImpl(const Subcircuit& subcir) {
|
||||
return true;
|
||||
}
|
||||
}
|
||||
|
||||
ABC_NAMESPACE_CXX_HEADER_END
|
||||
|
||||
#include "selectionStrategy.tpp"
|
||||
|
||||
#endif
|
||||
|
|
@ -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 <queue>
|
||||
|
||||
#include "misc/util/abc_namespaces.h"
|
||||
|
||||
#include "selectionStrategy.hpp"
|
||||
|
||||
ABC_NAMESPACE_CXX_HEADER_START
|
||||
|
||||
namespace eSLIM {
|
||||
|
||||
template<typename T>
|
||||
Subcircuit SelectionStrategy<T>::getSubcircuit() {
|
||||
for (int i = 0; i < cfg.nselection_trials; i++) {
|
||||
Subcircuit subcir = static_cast<T*>(this)->getSubcircuitImpl();
|
||||
if (filterSubcircuit(subcir)) {
|
||||
return subcir;
|
||||
} else {
|
||||
subcir.free();
|
||||
}
|
||||
}
|
||||
status = false;
|
||||
Subcircuit empty_subcir;
|
||||
return empty_subcir;
|
||||
}
|
||||
|
||||
template<typename T>
|
||||
bool SelectionStrategy<T>::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<T*>(this)->filterSubcircuitImpl(subcir);
|
||||
}
|
||||
|
||||
template <typename T>
|
||||
int SelectionStrategy<T>::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 <typename T>
|
||||
std::unordered_map<int, std::unordered_set<int>> SelectionStrategy<T>::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<int,int> 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<int, std::unordered_set<int>> 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 <typename T>
|
||||
void SelectionStrategy<T>::forbiddenPairsRec(Gia_Obj_t * pObj, int input, int min_level, std::unordered_map<int, std::unordered_set<int>>& pairs, const std::unordered_map<int,int>& 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<typename T>
|
||||
int randomizedBFS<T>::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<typename T>
|
||||
void randomizedBFS<T>::checkCandidate(Subcircuit& subcircuit, std::queue<int>& candidates, std::queue<int>& 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<typename T>
|
||||
Subcircuit randomizedBFS<T>::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<int> candidates;
|
||||
candidates.push(Gia_ObjFaninId0(gia_obj, root_id));
|
||||
candidates.push(Gia_ObjFaninId1(gia_obj, root_id));
|
||||
std::queue<int> 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
|
||||
|
|
@ -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 <vector>
|
||||
#include <unordered_set>
|
||||
#include <unordered_map>
|
||||
#include <memory>
|
||||
|
||||
#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 Derived>
|
||||
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<int, std::vector<int>> connection_variables;
|
||||
const std::unordered_map<int, std::unordered_set<int>>& 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<int, std::unordered_set<int>>& 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<int, std::unordered_set<int>> computeNotInPair(const std::unordered_map<int, std::unordered_set<int>>& pairs);
|
||||
|
||||
int prepareLits(int * pLits, int& nLits);
|
||||
|
||||
friend Derived;
|
||||
};
|
||||
|
||||
// applies Cadical incrementally
|
||||
class CadicalEngine : public exactSynthesisEngine<CadicalEngine> {
|
||||
|
||||
public:
|
||||
CadicalEngine(Vec_Wrd_t * vSimsIn, Vec_Wrd_t * vSimsOut, int nIns, int nDivs, int nOuts, int nNodes,
|
||||
const std::unordered_map<int, std::unordered_set<int>>& forbidden_pairs, eSLIMLog& log, const eSLIMConfig& cfg);
|
||||
Mini_Aig_t* getCircuit(int size, double timeout);
|
||||
|
||||
private:
|
||||
using exactSynthesisEngine::addClause;
|
||||
std::vector<int> 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<int> getAssumptions(int size);
|
||||
|
||||
friend exactSynthesisEngine<CadicalEngine>;
|
||||
};
|
||||
|
||||
class OneshotEngine {
|
||||
protected:
|
||||
int getAuxilaryVariableCountDerived() {return 0;};
|
||||
int getGateEnablingLiteralImpl(int index, bool negated) {return 0;};
|
||||
// void addAssumptions(int size) {};
|
||||
void addGateDeactivatedConstraint(int idx) {};
|
||||
};
|
||||
|
||||
template <typename T>
|
||||
class OneshotManager {
|
||||
public:
|
||||
OneshotManager(Vec_Wrd_t * vSimsIn, Vec_Wrd_t * vSimsOut, int nIns, int nDivs, int nOuts, int maxnNodes,
|
||||
const std::unordered_map<int, std::unordered_set<int>>& 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<int, std::unordered_set<int>>& forbidden_pairs;
|
||||
eSLIMLog& log;
|
||||
const eSLIMConfig& cfg;
|
||||
};
|
||||
|
||||
class CadicalEngineOneShot : public exactSynthesisEngine<CadicalEngineOneShot>, public OneshotEngine {
|
||||
|
||||
public:
|
||||
CadicalEngineOneShot( Vec_Wrd_t * vSimsIn, Vec_Wrd_t * vSimsOut, int nIns, int nDivs, int nOuts, int nNodes,
|
||||
const std::unordered_map<int, std::unordered_set<int>>& 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<CadicalEngineOneShot>;
|
||||
};
|
||||
|
||||
class KissatEngineOneShot : public exactSynthesisEngine<KissatEngineOneShot>, public OneshotEngine {
|
||||
|
||||
public:
|
||||
KissatEngineOneShot( Vec_Wrd_t * vSimsIn, Vec_Wrd_t * vSimsOut, int nIns, int nDivs, int nOuts, int nNodes,
|
||||
const std::unordered_map<int, std::unordered_set<int>>& 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<KissatEngineOneShot>;
|
||||
};
|
||||
|
||||
|
||||
class KissatCmdEngine : public exactSynthesisEngine<KissatCmdEngine>, public OneshotEngine {
|
||||
|
||||
public:
|
||||
KissatCmdEngine( Vec_Wrd_t * vSimsIn, Vec_Wrd_t * vSimsOut, int nIns, int nDivs, int nOuts, int nNodes,
|
||||
const std::unordered_map<int, std::unordered_set<int>>& 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<KissatCmdEngine>;
|
||||
};
|
||||
|
||||
|
||||
template <typename T>
|
||||
inline int exactSynthesisEngine<T>::addClause(int lit1, int lit2, int lit3, int lit4) {
|
||||
int clause[4] = {lit1, lit2, lit3, lit4};
|
||||
return static_cast<T*>(this)->addClause(clause, 4);
|
||||
}
|
||||
|
||||
template <typename T>
|
||||
inline int exactSynthesisEngine<T>::getGateEnablingLiteral(int index, bool negated) {
|
||||
return static_cast<T*>(this)->getGateEnablingLiteralImpl(index, negated);
|
||||
}
|
||||
|
||||
template <typename T>
|
||||
inline int exactSynthesisEngine<T>::getAuxilaryVariableCount() {
|
||||
int ncvars = connection_variables.empty() ? 0 : connection_variables.begin()->second.size() * connection_variables.size();
|
||||
return ncvars + static_cast<T*>(this)->getAuxilaryVariableCountDerived();
|
||||
}
|
||||
|
||||
typedef OneshotManager<CadicalEngineOneShot> CadicalOneShot;
|
||||
typedef OneshotManager<KissatEngineOneShot> KissatOneShot;
|
||||
typedef OneshotManager<KissatCmdEngine> KissatCmdOneShot;
|
||||
|
||||
}
|
||||
|
||||
ABC_NAMESPACE_CXX_HEADER_END
|
||||
|
||||
#include "synthesisEngine.tpp"
|
||||
|
||||
#endif
|
||||
|
|
@ -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 <numeric>
|
||||
|
||||
#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 <typename T>
|
||||
exactSynthesisEngine<T>::exactSynthesisEngine( Vec_Wrd_t * vSimsIn, Vec_Wrd_t * vSimsOut, int nIns, int nDivs, int nOuts, int nNodes,
|
||||
const std::unordered_map<int, std::unordered_set<int>>& 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 <typename T>
|
||||
bool exactSynthesisEngine<T>::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 <typename T>
|
||||
int exactSynthesisEngine<T>::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 <typename T>
|
||||
int exactSynthesisEngine<T>::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 <typename T>
|
||||
Mini_Aig_t * exactSynthesisEngine<T>::getAig(Vec_Int_t * vValues) {
|
||||
return getAig(vValues, nNodes);
|
||||
}
|
||||
|
||||
template <typename T>
|
||||
Mini_Aig_t * exactSynthesisEngine<T>::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 <typename T>
|
||||
void exactSynthesisEngine<T>::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 <typename T>
|
||||
void exactSynthesisEngine<T>::introduceConnectionVariables() {
|
||||
std::unordered_set<int> 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<int> (nCVars, 0));
|
||||
std::iota(connection_variables[in].begin(), connection_variables[in].end(), nCnfVars);
|
||||
nCnfVars += nCVars;
|
||||
}
|
||||
}
|
||||
|
||||
template <typename T>
|
||||
void exactSynthesisEngine<T>::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 <typename T>
|
||||
void exactSynthesisEngine<T>::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 <typename T>
|
||||
void exactSynthesisEngine<T>::addCombinedCycleConstraints() {
|
||||
assert (forbidden_pairs.size() > 1 && "Combined connectivity constraints are only needed if there are forbidden pairs for multiple inputs.");
|
||||
std::unordered_map<int, std::unordered_set<int>> 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 <typename T>
|
||||
std::unordered_map<int, std::unordered_set<int>> exactSynthesisEngine<T>::computeNotInPair(const std::unordered_map<int, std::unordered_set<int>>& pairs) {
|
||||
std::unordered_set<int> 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<int, std::unordered_set<int>> 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 <typename T>
|
||||
int exactSynthesisEngine<T>::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<T*>(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<T*>(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<T*>(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 <typename T>
|
||||
void exactSynthesisEngine<T>::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<T*>(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 <typename T>
|
||||
int exactSynthesisEngine<T>::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<int, std::unordered_set<int>>& 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<int> 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<int> CadicalEngine::getAssumptions(int size) {
|
||||
std::vector<int> 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 <typename T>
|
||||
OneshotManager<T>::OneshotManager(Vec_Wrd_t * vSimsIn, Vec_Wrd_t * vSimsOut, int nIns, int nDivs, int nOuts, int maxnNodes,
|
||||
const std::unordered_map<int, std::unordered_set<int>>& 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 <typename T>
|
||||
T OneshotManager<T>::getOneshotEngine(int size) {
|
||||
assert(size <= maxnNodes);
|
||||
T oneshotEngine(vSimsIn, vSimsOut, nIns, nDivs, nOuts, size, forbidden_pairs, log, cfg);
|
||||
return oneshotEngine;
|
||||
}
|
||||
|
||||
template <typename T>
|
||||
Mini_Aig_t* OneshotManager<T>::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<int, std::unordered_set<int>>& forbidden_pairs, eSLIMLog& log, const eSLIMConfig& cfg)
|
||||
: exactSynthesisEngine<CadicalEngineOneShot>(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<int, std::unordered_set<int>>& forbidden_pairs, eSLIMLog& log, const eSLIMConfig& cfg)
|
||||
: exactSynthesisEngine<KissatEngineOneShot>(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<int, std::unordered_set<int>>& forbidden_pairs, eSLIMLog& log, const eSLIMConfig& cfg)
|
||||
: exactSynthesisEngine<KissatCmdEngine>(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
|
||||
|
|
@ -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 <vector>
|
||||
#include <unordered_map>
|
||||
#include <unordered_set>
|
||||
|
||||
#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<int> nof_analyzed_circuits_per_size;
|
||||
std::vector<int> nof_replaced_circuits_per_size;
|
||||
std::vector<int> nof_reduced_circuits_per_size;
|
||||
|
||||
std::vector<ABC_UINT64_T> cummulative_sat_runtimes_per_size;
|
||||
std::vector<int> nof_sat_calls_per_size;
|
||||
std::vector<ABC_UINT64_T> cummulative_unsat_runtimes_per_size;
|
||||
std::vector<int> 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<int, std::unordered_set<int>> 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
|
||||
Loading…
Reference in New Issue