summaryrefslogtreecommitdiffstats
path: root/src/base
diff options
context:
space:
mode:
Diffstat (limited to 'src/base')
-rw-r--r--src/base/abc/abc.h8
-rw-r--r--src/base/abc/abcFunc.c16
-rw-r--r--src/base/abc/abcUtil.c20
-rw-r--r--src/base/abci/abc.c515
-rw-r--r--src/base/abci/abcDetect.c2
-rw-r--r--src/base/abci/abcDress3.c344
-rw-r--r--src/base/abci/abcExact.c1696
-rw-r--r--src/base/abci/abcFx.c199
-rw-r--r--src/base/abci/abcIf.c20
-rw-r--r--src/base/abci/abcMini.c2
-rw-r--r--src/base/abci/abcPrint.c8
-rw-r--r--src/base/abci/module.make2
-rw-r--r--src/base/io/ioReadBench.c2
-rw-r--r--src/base/io/ioReadPlaMo.c79
-rw-r--r--src/base/wlc/wlc.h2
-rw-r--r--src/base/wlc/wlcBlast.c114
-rw-r--r--src/base/wlc/wlcCom.c45
-rw-r--r--src/base/wlc/wlcReadSmt.c22
-rw-r--r--src/base/wlc/wlcReadVer.c4
-rw-r--r--src/base/wlc/wlcSim.c2
20 files changed, 2904 insertions, 198 deletions
diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index 971f29bb..35b20dbe 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -642,6 +642,11 @@ extern ABC_DLL int Abc_NtkLevelReverse( Abc_Ntk_t * pNtk );
extern ABC_DLL int Abc_NtkIsAcyclic( Abc_Ntk_t * pNtk );
extern ABC_DLL int Abc_NtkIsAcyclicWithBoxes( Abc_Ntk_t * pNtk );
extern ABC_DLL Vec_Ptr_t * Abc_AigGetLevelizedOrder( Abc_Ntk_t * pNtk, int fCollectCis );
+/*=== abcExact.c ==========================================================*/
+extern ABC_DLL int Abc_ExactInputNum();
+extern ABC_DLL int Abc_ExactIsRunning();
+extern ABC_DLL Abc_Obj_t * Abc_ExactBuildNode( word * pTruth, int nVars, int * pArrTimeProfile, Abc_Obj_t ** pFanins, Abc_Ntk_t * pNtk );
+extern ABC_DLL Abc_Ntk_t * Abc_NtkFindExact( word * pTruth, int nVars, int nFunc, int nMaxDepth, int * pArrivalTimes, int fVerbose );
/*=== abcFanio.c ==========================================================*/
extern ABC_DLL void Abc_ObjAddFanin( Abc_Obj_t * pObj, Abc_Obj_t * pFanin );
extern ABC_DLL void Abc_ObjDeleteFanin( Abc_Obj_t * pObj, Abc_Obj_t * pFanin );
@@ -820,7 +825,7 @@ extern ABC_DLL void Abc_NtkDontCareFree( Odc_Man_t * p );
extern ABC_DLL int Abc_NtkDontCareCompute( Odc_Man_t * p, Abc_Obj_t * pNode, Vec_Ptr_t * vLeaves, unsigned * puTruth );
/*=== abcPrint.c ==========================================================*/
extern ABC_DLL float Abc_NtkMfsTotalSwitching( Abc_Ntk_t * pNtk );
-extern ABC_DLL void Abc_NtkPrintStats( Abc_Ntk_t * pNtk, int fFactored, int fSaveBest, int fDumpResult, int fUseLutLib, int fPrintMuxes, int fPower, int fGlitch, int fSkipBuf, int fPrintMem );
+extern ABC_DLL void Abc_NtkPrintStats( Abc_Ntk_t * pNtk, int fFactored, int fSaveBest, int fDumpResult, int fUseLutLib, int fPrintMuxes, int fPower, int fGlitch, int fSkipBuf, int fSkipSmall, int fPrintMem );
extern ABC_DLL void Abc_NtkPrintIo( FILE * pFile, Abc_Ntk_t * pNtk, int fPrintFlops );
extern ABC_DLL void Abc_NtkPrintLatch( FILE * pFile, Abc_Ntk_t * pNtk );
extern ABC_DLL void Abc_NtkPrintFanio( FILE * pFile, Abc_Ntk_t * pNtk, int fUseFanio, int fUsePio, int fUseSupp, int fUseCone );
@@ -986,6 +991,7 @@ extern ABC_DLL double Abc_NtkGetMappedArea( Abc_Ntk_t * pNtk );
extern ABC_DLL int Abc_NtkGetExorNum( Abc_Ntk_t * pNtk );
extern ABC_DLL int Abc_NtkGetMuxNum( Abc_Ntk_t * pNtk );
extern ABC_DLL int Abc_NtkGetBufNum( Abc_Ntk_t * pNtk );
+extern ABC_DLL int Abc_NtkGetLargeNodeNum( Abc_Ntk_t * pNtk );
extern ABC_DLL int Abc_NtkGetChoiceNum( Abc_Ntk_t * pNtk );
extern ABC_DLL int Abc_NtkGetFaninMax( Abc_Ntk_t * pNtk );
extern ABC_DLL int Abc_NtkGetFanoutMax( Abc_Ntk_t * pNtk );
diff --git a/src/base/abc/abcFunc.c b/src/base/abc/abcFunc.c
index 94706504..5d0261d7 100644
--- a/src/base/abc/abcFunc.c
+++ b/src/base/abc/abcFunc.c
@@ -810,7 +810,7 @@ int Abc_NtkSopToAig( Abc_Ntk_t * pNtk )
{
Abc_Obj_t * pNode;
Hop_Man_t * pMan;
- int i;
+ int i, Max;
assert( Abc_NtkHasSop(pNtk) );
@@ -819,7 +819,8 @@ int Abc_NtkSopToAig( Abc_Ntk_t * pNtk )
// start the functionality manager
pMan = Hop_ManStart();
- Hop_IthVar( pMan, Abc_NtkGetFaninMax(pNtk)-1 );
+ Max = Abc_NtkGetFaninMax(pNtk);
+ if ( Max ) Hop_IthVar( pMan, Max-1 );
// convert each node from SOP to BDD
Abc_NtkForEachNode( pNtk, pNode, i )
@@ -979,7 +980,7 @@ Gia_Man_t * Abc_NtkAigToGia( Abc_Ntk_t * p, int fGiaSimple )
Vec_Int_t * vMapping = NULL;
Vec_Ptr_t * vNodes;
Abc_Obj_t * pNode, * pFanin;
- int i, k, nObjs;
+ int i, k, nObjs, iGiaObj;
assert( Abc_NtkIsAigLogic(p) );
pHopMan = (Hop_Man_t *)p->pManFunc;
// create new manager
@@ -1015,15 +1016,14 @@ Gia_Man_t * Abc_NtkAigToGia( Abc_Ntk_t * p, int fGiaSimple )
{
assert( Abc_ObjFaninNum(pNode) <= Hop_ManPiNum(pHopMan) );
Abc_ConvertAigToGia( pNew, pHopObj );
- if ( !Gia_ObjIsAnd(Gia_ManObj(pNew, Abc_Lit2Var(pHopObj->iData))) )
- continue;
- if ( vMapping && !Vec_IntEntry(vMapping, Abc_Lit2Var(pHopObj->iData)) )
+ iGiaObj = Abc_Lit2Var( pHopObj->iData );
+ if ( vMapping && Gia_ObjIsAnd(Gia_ManObj(pNew, iGiaObj)) && !Vec_IntEntry(vMapping, iGiaObj) )
{
- Vec_IntWriteEntry( vMapping, Abc_Lit2Var(pHopObj->iData), Vec_IntSize(vMapping) );
+ Vec_IntWriteEntry( vMapping, iGiaObj, Vec_IntSize(vMapping) );
Vec_IntPush( vMapping, Abc_ObjFaninNum(pNode) );
Abc_ObjForEachFanin( pNode, pFanin, k )
Vec_IntPush( vMapping, Abc_Lit2Var(pFanin->iTemp) );
- Vec_IntPush( vMapping, Abc_Lit2Var(pHopObj->iData) );
+ Vec_IntPush( vMapping, iGiaObj );
}
}
pNode->iTemp = Abc_LitNotCond( pHopObj->iData, Hop_IsComplement( (Hop_Obj_t *)pNode->pData ) );
diff --git a/src/base/abc/abcUtil.c b/src/base/abc/abcUtil.c
index 59993614..f01ef07a 100644
--- a/src/base/abc/abcUtil.c
+++ b/src/base/abc/abcUtil.c
@@ -429,6 +429,26 @@ int Abc_NtkGetBufNum( Abc_Ntk_t * pNtk )
/**Function*************************************************************
+ Synopsis [Counts the number of exors.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_NtkGetLargeNodeNum( Abc_Ntk_t * pNtk )
+{
+ Abc_Obj_t * pNode;
+ int i, Counter = 0;
+ Abc_NtkForEachNode( pNtk, pNode, i )
+ Counter += (Abc_ObjFaninNum(pNode) > 1);
+ return Counter;
+}
+
+/**Function*************************************************************
+
Synopsis [Returns 1 if it is an AIG with choice nodes.]
Description []
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 699b5ec1..31f3a275 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -135,6 +135,10 @@ static int Abc_CommandCascade ( Abc_Frame_t * pAbc, int argc, cha
static int Abc_CommandExtract ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandVarMin ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandDetect ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandExact ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandBmsStart ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandBmsStop ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandBmsPs ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandLogic ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandComb ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -232,6 +236,7 @@ static int Abc_CommandFraigRestore ( Abc_Frame_t * pAbc, int argc, cha
static int Abc_CommandFraigClean ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandFraigSweep ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandFraigDress ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandDumpEquiv ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandRecStart3 ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandRecStop3 ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -773,6 +778,11 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Synthesis", "extract", Abc_CommandExtract, 1 );
Cmd_CommandAdd( pAbc, "Synthesis", "varmin", Abc_CommandVarMin, 0 );
Cmd_CommandAdd( pAbc, "Synthesis", "detect", Abc_CommandDetect, 0 );
+ Cmd_CommandAdd( pAbc, "Synthesis", "exact", Abc_CommandExact, 1 );
+
+ Cmd_CommandAdd( pAbc, "Exact synthesis", "bms_start", Abc_CommandBmsStart, 0 );
+ Cmd_CommandAdd( pAbc, "Exact synthesis", "bms_stop", Abc_CommandBmsStop, 0 );
+ Cmd_CommandAdd( pAbc, "Exact synthesis", "bms_ps", Abc_CommandBmsPs, 0 );
Cmd_CommandAdd( pAbc, "Various", "logic", Abc_CommandLogic, 1 );
Cmd_CommandAdd( pAbc, "Various", "comb", Abc_CommandComb, 1 );
@@ -867,6 +877,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Fraiging", "fraig_clean", Abc_CommandFraigClean, 0 );
Cmd_CommandAdd( pAbc, "Fraiging", "fraig_sweep", Abc_CommandFraigSweep, 1 );
Cmd_CommandAdd( pAbc, "Fraiging", "dress", Abc_CommandFraigDress, 1 );
+ Cmd_CommandAdd( pAbc, "Fraiging", "dump_equiv", Abc_CommandDumpEquiv, 0 );
Cmd_CommandAdd( pAbc, "Choicing", "rec_start3", Abc_CommandRecStart3, 0 );
Cmd_CommandAdd( pAbc, "Choicing", "rec_stop3", Abc_CommandRecStop3, 0 );
@@ -1223,6 +1234,7 @@ int Abc_CommandPrintStats( Abc_Frame_t * pAbc, int argc, char ** argv )
int fPower;
int fGlitch;
int fSkipBuf;
+ int fSkipSmall;
int fPrintMem;
int c;
@@ -1238,9 +1250,10 @@ int Abc_CommandPrintStats( Abc_Frame_t * pAbc, int argc, char ** argv )
fPower = 0;
fGlitch = 0;
fSkipBuf = 0;
+ fSkipSmall = 0;
fPrintMem = 0;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "fbdltmpgsuh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "fbdltmpgscuh" ) ) != EOF )
{
switch ( c )
{
@@ -1271,6 +1284,9 @@ int Abc_CommandPrintStats( Abc_Frame_t * pAbc, int argc, char ** argv )
case 's':
fSkipBuf ^= 1;
break;
+ case 'c':
+ fSkipSmall ^= 1;
+ break;
case 'u':
fPrintMem ^= 1;
break;
@@ -1291,7 +1307,7 @@ int Abc_CommandPrintStats( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Cannot print LUT delay for a non-logic network.\n" );
return 1;
}
- Abc_NtkPrintStats( pNtk, fFactor, fSaveBest, fDumpResult, fUseLutLib, fPrintMuxes, fPower, fGlitch, fSkipBuf, fPrintMem );
+ Abc_NtkPrintStats( pNtk, fFactor, fSaveBest, fDumpResult, fUseLutLib, fPrintMuxes, fPower, fGlitch, fSkipBuf, fSkipSmall, fPrintMem );
if ( fPrintTime )
{
pAbc->TimeTotal += pAbc->TimeCommand;
@@ -1301,7 +1317,7 @@ int Abc_CommandPrintStats( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- Abc_Print( -2, "usage: print_stats [-fbdltmpgsuh]\n" );
+ Abc_Print( -2, "usage: print_stats [-fbdltmpgscuh]\n" );
Abc_Print( -2, "\t prints the network statistics\n" );
Abc_Print( -2, "\t-f : toggles printing the literal count in the factored forms [default = %s]\n", fFactor? "yes": "no" );
Abc_Print( -2, "\t-b : toggles saving the best logic network in \"best.blif\" [default = %s]\n", fSaveBest? "yes": "no" );
@@ -1312,6 +1328,7 @@ usage:
Abc_Print( -2, "\t-p : toggles printing power dissipation due to switching [default = %s]\n", fPower? "yes": "no" );
Abc_Print( -2, "\t-g : toggles printing percentage of increased power due to glitching [default = %s]\n", fGlitch? "yes": "no" );
Abc_Print( -2, "\t-s : toggles not counting single-output nodes as nodes [default = %s]\n", fSkipBuf? "yes": "no" );
+ Abc_Print( -2, "\t-c : toggles not counting constants and single-output nodes as nodes [default = %s]\n", fSkipSmall? "yes": "no" );
Abc_Print( -2, "\t-u : toggles printing memory usage [default = %s]\n", fPrintMem? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
@@ -1393,7 +1410,7 @@ int Abc_CommandPrintExdc( Abc_Frame_t * pAbc, int argc, char ** argv )
}
else
Abc_Print( 1, "EXDC network statistics: \n" );
- Abc_NtkPrintStats( pNtk->pExdc, 0, 0, 0, 0, 0, 0, 0, 0, 0 );
+ Abc_NtkPrintStats( pNtk->pExdc, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0 );
return 0;
usage:
@@ -7218,15 +7235,18 @@ usage:
***********************************************************************/
int Abc_CommandDetect( Abc_Frame_t * pAbc, int argc, char ** argv )
{
- extern void Abc_NtkDetectClassesTest( Abc_Ntk_t * pNtk, int fVerbose );
+ extern void Abc_NtkDetectClassesTest( Abc_Ntk_t * pNtk, int fSeq, int fVerbose );
Abc_Ntk_t * pNtk;
- int c, fVerbose = 0;
+ int c, fSeq = 0, fVerbose = 0;
pNtk = Abc_FrameReadNtk(pAbc);
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "svh" ) ) != EOF )
{
switch ( c )
{
+ case 's':
+ fSeq ^= 1;
+ break;
case 'v':
fVerbose ^= 1;
break;
@@ -7246,12 +7266,13 @@ int Abc_CommandDetect( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Only applicable to a logic network.\n" );
return 1;
}
- Abc_NtkDetectClassesTest( pNtk, fVerbose );
+ Abc_NtkDetectClassesTest( pNtk, fSeq, fVerbose );
return 0;
usage:
- Abc_Print( -2, "usage: detect [-vh]\n" );
+ Abc_Print( -2, "usage: detect [-svh]\n" );
Abc_Print( -2, "\t detects properties of internal nodes\n" );
+ Abc_Print( -2, "\t-s : toggle using sequential circuit information [default = %s]\n", fSeq? "yes": "no" );
Abc_Print( -2, "\t-v : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
@@ -7268,6 +7289,310 @@ usage:
SeeAlso []
***********************************************************************/
+int Abc_CommandExact( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ extern Gia_Man_t * Gia_ManFindExact( word * pTruth, int nVars, int nFunc, int nMaxDepth, int * pArrivalTimes, int fVerbose );
+
+ int c, nMaxDepth = -1, fMakeAIG = 0, fTest = 0, fVerbose = 0, nVars = 0, nVarsTmp, nFunc = 0;
+ word pTruth[64];
+ Abc_Ntk_t * pNtkRes;
+ Gia_Man_t * pGiaRes;
+
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "Datvh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'D':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-D\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ nMaxDepth = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( nMaxDepth < 0 )
+ goto usage;
+ break;
+ case 'a':
+ fMakeAIG ^= 1;
+ break;
+ case 't':
+ fTest ^= 1;
+ break;
+ case 'v':
+ fVerbose ^= 1;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+
+ if ( fTest )
+ {
+ extern void Abc_ExactTest( int fVerbose );
+ extern void Abc_ExactStoreTest( int fVerbose );
+
+ printf( "run test suite, ignore all other settings\n" );
+ Abc_ExactTest( fVerbose );
+ Abc_ExactStoreTest( fVerbose );
+ return 0;
+ }
+
+ if ( argc == globalUtilOptind )
+ goto usage;
+
+ memset( pTruth, 0, 64 );
+ while ( globalUtilOptind < argc )
+ {
+ if ( nFunc == 16 )
+ {
+ Abc_Print( -1, "Too many functions (at most 16 supported).\n" );
+ goto usage;
+ }
+ nVarsTmp = Abc_TtReadHex( &pTruth[nFunc << 2], argv[globalUtilOptind++] );
+ nFunc++;
+ if ( nVars == 0 )
+ nVars = nVarsTmp;
+ else if ( nVars > 8 )
+ {
+ Abc_Print( -1, "Only 8-variable functions are supported.\n" );
+ goto usage;
+ }
+ else if ( nVars != nVarsTmp )
+ {
+ Abc_Print( -1, "All functions need to have the same size.\n" );
+ goto usage;
+ }
+ }
+
+ if ( fMakeAIG )
+ {
+ pGiaRes = Gia_ManFindExact( pTruth, nVars, nFunc, nMaxDepth, NULL, fVerbose );
+ if ( pGiaRes )
+ Abc_FrameUpdateGia( pAbc, pGiaRes );
+ else
+ Abc_Print( 0, "Could not find AIG within given resource constraints.\n" );
+ }
+ else
+ {
+ pNtkRes = Abc_NtkFindExact( pTruth, nVars, nFunc, nMaxDepth, NULL, fVerbose );
+ if ( pNtkRes )
+ {
+ Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+ Abc_FrameClearVerifStatus( pAbc );
+ }
+ else
+ Abc_Print( 0, "Could not find network within given resource constraints.\n" );
+ }
+ return 0;
+
+usage:
+ Abc_Print( -2, "usage: exact [-D <num>] [-atvh] <truth1> <truth2> ...\n" );
+ Abc_Print( -2, "\t finds optimum networks using SAT-based exact synthesis for hex truth tables <truth1> <truth2> ...\n" );
+ Abc_Print( -2, "\t-D <num> : constrain maximum depth (if too low, algorithm may not terminate)\n" );
+ Abc_Print( -2, "\t-a : toggle create AIG [default = %s]\n", fMakeAIG ? "yes" : "no" );
+ Abc_Print( -2, "\t-t : run test suite\n" );
+ Abc_Print( -2, "\t-v : toggle verbose printout [default = %s]\n", fVerbose ? "yes" : "no" );
+ Abc_Print( -2, "\t-h : print the command usage\n" );
+ Abc_Print( -2, "\t\n" );
+ Abc_Print( -2, "\t This command was contributed by Mathias Soeken from EPFL in July 2016.\n" );
+ Abc_Print( -2, "\t The author can be contacted as mathias.soeken at epfl.ch\n" );
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_CommandBmsStart( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ extern int Abc_ExactIsRunning();
+ extern void Abc_ExactStart( int nBTLimit, int fMakeAIG, int fVerbose, const char *pFilename );
+
+ int c, fMakeAIG = 0, fVerbose = 0, nBTLimit = 10000;
+ char * pFilename = NULL;
+
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "Cavh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'C':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ nBTLimit = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ break;
+ case 'a':
+ fMakeAIG ^= 1;
+ break;
+ case 'v':
+ fVerbose ^= 1;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+
+ if ( argc > globalUtilOptind )
+ {
+ pFilename = argv[globalUtilOptind++];
+ }
+
+ if ( Abc_ExactIsRunning() )
+ {
+ Abc_Print( -1, "BMS manager is already started." );
+ return 1;
+ }
+
+ Abc_ExactStart( nBTLimit, fMakeAIG, fVerbose, pFilename );
+ return 0;
+
+usage:
+ Abc_Print( -2, "usage: bms_start [-C <num>] [-avh] [<file>]\n" );
+ Abc_Print( -2, "\t starts BMS manager for recording optimum networks\n" );
+ Abc_Print( -2, "\t if <file> is specified, store entries are read from that file\n" );
+ Abc_Print( -2, "\t-C <num> : the limit on the number of conflicts [default = %d]\n", nBTLimit );
+ Abc_Print( -2, "\t-a : toggle create AIG [default = %s]\n", fMakeAIG ? "yes" : "no" );
+ Abc_Print( -2, "\t-v : toggle verbose printout [default = %s]\n", fVerbose ? "yes" : "no" );
+ Abc_Print( -2, "\t-h : print the command usage\n" );
+ Abc_Print( -2, "\t\n" );
+ Abc_Print( -2, "\t This command was contributed by Mathias Soeken from EPFL in July 2016.\n" );
+ Abc_Print( -2, "\t The author can be contacted as mathias.soeken at epfl.ch\n" );
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_CommandBmsStop( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ extern int Abc_ExactIsRunning();
+ extern void Abc_ExactStop( const char *pFilename );
+
+ int c;
+ char * pFilename = NULL;
+
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+
+ if ( argc > globalUtilOptind )
+ {
+ pFilename = argv[globalUtilOptind++];
+ }
+
+ if ( !Abc_ExactIsRunning() )
+ {
+ Abc_Print( -1, "BMS manager is not started." );
+ return 1;
+ }
+
+ Abc_ExactStop( pFilename );
+ return 0;
+
+usage:
+ Abc_Print( -2, "usage: bms_stop [-C <num>] [-vh] [<file>]\n" );
+ Abc_Print( -2, "\t stops BMS manager for recording optimum networks\n" );
+ Abc_Print( -2, "\t if <file> is specified, store entries are written to that file\n" );
+ Abc_Print( -2, "\t-h : print the command usage\n" );
+ Abc_Print( -2, "\t\n" );
+ Abc_Print( -2, "\t This command was contributed by Mathias Soeken from EPFL in July 2016.\n" );
+ Abc_Print( -2, "\t The author can be contacted as mathias.soeken at epfl.ch\n" );
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_CommandBmsPs( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ extern int Abc_ExactIsRunning();
+ extern void Abc_ExactStats();
+
+ int c;
+
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+
+ if ( !Abc_ExactIsRunning() )
+ {
+ Abc_Print( -1, "BMS manager is not started." );
+ return 1;
+ }
+
+ Abc_ExactStats();
+ return 0;
+
+usage:
+ Abc_Print( -2, "usage: bms_ps [-h]\n" );
+ Abc_Print( -2, "\t shows statistics about BMS manager\n" );
+ Abc_Print( -2, "\t-h : print the command usage\n" );
+ Abc_Print( -2, "\t\n" );
+ Abc_Print( -2, "\t This command was contributed by Mathias Soeken from EPFL in July 2016.\n" );
+ Abc_Print( -2, "\t The author can be contacted as mathias.soeken at epfl.ch\n" );
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
int Abc_CommandLogic( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Abc_Ntk_t * pNtk, * pNtkRes;
@@ -14745,6 +15070,93 @@ usage:
SeeAlso []
***********************************************************************/
+int Abc_CommandDumpEquiv( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ extern void Abc_NtkDumpEquiv( Abc_Ntk_t * pNtks[2], char * pFileName, int nConfs, int fByName, int fVerbose );
+ Abc_Ntk_t * pNtks[2] = {NULL};
+ char * pFileName[2], * pFileNameOut;
+ int c, nConfs = 1000, fByName = 1, fVerbose = 0;
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "Cnvh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'C':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ nConfs = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( nConfs < 0 )
+ goto usage;
+ break;
+ case 'n':
+ fByName ^= 1;
+ break;
+ case 'v':
+ fVerbose ^= 1;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+ if ( argc != globalUtilOptind + 3 )
+ {
+ Abc_Print( -1, "Expecting three file names on the command line.\n" );
+ goto usage;
+ }
+ pFileName[0] = argv[globalUtilOptind];
+ pFileName[1] = argv[globalUtilOptind+1];
+ pFileNameOut = argv[globalUtilOptind+2];
+ for ( c = 0; c < 2; c++ )
+ {
+ pNtks[c] = Io_Read( pFileName[c], Io_ReadFileType(pFileName[c]), 1, 0 );
+ if ( pNtks[c] == NULL )
+ goto usage;
+ Abc_NtkToAig( pNtks[c] );
+ }
+// if ( Abc_NtkCiNum(pNtks[0]) != Abc_NtkCiNum(pNtks[1]) )
+// Abc_Print( -1, "The number of primary inputs of networks \"%s\" and \"%s\" does not match.\n", Abc_NtkName(pNtks[0]), Abc_NtkName(pNtks[1]) );
+// else if ( Abc_NtkCoNum(pNtks[0]) != Abc_NtkCoNum(pNtks[1]) )
+// Abc_Print( -1, "The number of primary outputs of networks \"%s\" and \"%s\" does not match.\n", Abc_NtkName(pNtks[0]), Abc_NtkName(pNtks[1]) );
+// else
+ Abc_NtkDumpEquiv( pNtks, pFileNameOut, nConfs, fByName, fVerbose );
+ Abc_NtkDelete( pNtks[0] );
+ Abc_NtkDelete( pNtks[1] );
+ return 0;
+
+usage:
+ Abc_Print( -2, "usage: dump_equiv [-C num] [-nvh] <file1.blif> <file2.blif> <file_dump_equiv.txt>\n" );
+ Abc_Print( -2, "\t computes equivalence classes of nodes in <file1> and <file2>\n" );
+ Abc_Print( -2, "\t By default this procedure performs matching of primary inputs by name.\n" );
+ Abc_Print( -2, "\t Those inputs that cannot be matched are treated as free variables.\n" );
+ Abc_Print( -2, "\t There is no effort to match primary outputs. Indeed, if two outputs\n" );
+ Abc_Print( -2, "\t are equivalent, they will belong to the same equivalence class in the end.\n" );
+ Abc_Print( -2, "\t-C num : the maximum number of conflicts at each node [default = %d]\n", nConfs );
+ Abc_Print( -2, "\t-n : enable matching of primary inputs by name [default = %s]\n", fByName? "yes": "no" );
+ Abc_Print( -2, "\t-v : prints verbose information [default = %s]\n", fVerbose? "yes": "no" );
+ Abc_Print( -2, "\t-h : print the command usage\n");
+ Abc_Print( -2, "\t<file1> : first network whose nodes are considered\n" );
+ Abc_Print( -2, "\t<file2> : second network whose nodes are considered\n" );
+ Abc_Print( -2, "\t<file_dump_equiv> : text file with node equivalence classes\n" );
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
int Abc_CommandRecStart3( Abc_Frame_t * pAbc, int argc, char ** argv )
{
char * FileName, * pTemp;
@@ -16277,7 +16689,7 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
If_ManSetDefaultPars( pPars );
pPars->pLutLib = (If_LibLut_t *)Abc_FrameReadLibLut();
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "KCFAGRNTXYDEWSqaflepmrsdbgxyojiktncvh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "KCFAGRNTXYDEWSqaflepmrsdbgxyuojiktncvh" ) ) != EOF )
{
switch ( c )
{
@@ -16482,6 +16894,9 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'y':
pPars->fUserRecLib ^= 1;
break;
+ case 'u':
+ pPars->fUserSesLib ^= 1;
+ break;
case 'o':
pPars->fUseBuffs ^= 1;
break;
@@ -16625,7 +17040,7 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
pPars->fExpRed = 0;
}
// modify the subgraph recording
- if ( pPars->fUserRecLib )
+ if ( pPars->fUserRecLib || pPars->fUserSesLib )
{
pPars->fTruth = 1;
pPars->fCutMin = 1;
@@ -16699,7 +17114,21 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
}
if ( Abc_NtkRecInputNum3() != pPars->nLutSize )
{
- printf( "The number of library inputs (%d) different from the K parameters (%d).\n", Abc_NtkRecInputNum3(), pPars->nLutSize );
+ printf( "The number of library inputs (%d) is different from the K parameters (%d).\n", Abc_NtkRecInputNum3(), pPars->nLutSize );
+ return 0;
+ }
+ }
+
+ if ( pPars->fUserSesLib )
+ {
+ if ( !Abc_ExactIsRunning() )
+ {
+ printf( "BMS manager is not running (use \"bms_start\").\n" );
+ return 0;
+ }
+ if ( Abc_ExactInputNum() < pPars->nLutSize )
+ {
+ printf( "The number of library inputs (%d) is smaller than the K parameters (%d).\n", Abc_ExactInputNum(), pPars->nLutSize );
return 0;
}
}
@@ -16766,7 +17195,7 @@ usage:
sprintf(LutSize, "library" );
else
sprintf(LutSize, "%d", pPars->nLutSize );
- Abc_Print( -2, "usage: if [-KCFAGRNTXY num] [-DEW float] [-S str] [-qarlepmsdbgxyojiktncvh]\n" );
+ Abc_Print( -2, "usage: if [-KCFAGRNTXY num] [-DEW float] [-S str] [-qarlepmsdbgxyuojiktncvh]\n" );
Abc_Print( -2, "\t performs FPGA technology mapping of the network\n" );
Abc_Print( -2, "\t-K num : the number of LUT inputs (2 < num < %d) [default = %s]\n", IF_MAX_LUTSIZE+1, LutSize );
Abc_Print( -2, "\t-C num : the max number of priority cuts (0 < num < 2^12) [default = %d]\n", pPars->nCutsMax );
@@ -16795,6 +17224,7 @@ usage:
Abc_Print( -2, "\t-g : toggles delay optimization by SOP balancing [default = %s]\n", pPars->fDelayOpt? "yes": "no" );
Abc_Print( -2, "\t-x : toggles delay optimization by DSD balancing [default = %s]\n", pPars->fDsdBalance? "yes": "no" );
Abc_Print( -2, "\t-y : toggles delay optimization with recorded library [default = %s]\n", pPars->fUserRecLib? "yes": "no" );
+ Abc_Print( -2, "\t-u : toggles delay optimization with SAT-based library [default = %s]\n", pPars->fUserSesLib? "yes": "no" );
Abc_Print( -2, "\t-o : toggles using buffers to decouple combinational outputs [default = %s]\n", pPars->fUseBuffs? "yes": "no" );
Abc_Print( -2, "\t-j : toggles enabling additional check [default = %s]\n", pPars->fEnableCheck07? "yes": "no" );
Abc_Print( -2, "\t-i : toggles using cofactoring variables [default = %s]\n", pPars->fUseCofVars? "yes": "no" );
@@ -26955,7 +27385,7 @@ usage:
Abc_Print( -2, "\t converts the current network into GIA and moves it to the &-space\n" );
Abc_Print( -2, "\t (if the network is a sequential logic network, normalizes the flops\n" );
Abc_Print( -2, "\t to have const-0 initial values, equivalent to \"undc; st; zero\")\n" );
- Abc_Print( -2, "\t-c : toggles allowing simple GIA to be improved [default = %s]\n", fGiaSimple? "yes": "no" );
+ Abc_Print( -2, "\t-c : toggles allowing simple GIA to be imported [default = %s]\n", fGiaSimple? "yes": "no" );
Abc_Print( -2, "\t-m : toggles preserving the current mapping [default = %s]\n", fMapped? "yes": "no" );
Abc_Print( -2, "\t-n : toggles saving CI/CO names of the AIG [default = %s]\n", fNames? "yes": "no" );
Abc_Print( -2, "\t-v : toggles additional verbose output [default = %s]\n", fVerbose? "yes": "no" );
@@ -27110,7 +27540,7 @@ usage:
SeeAlso []
***********************************************************************/
-static inline int Gia_ManCompareWithBest( Gia_Man_t * pBest, Gia_Man_t * p, int * pnBestLuts, int * pnBestEdges, int * pnBestLevels )
+static inline int Gia_ManCompareWithBest( Gia_Man_t * pBest, Gia_Man_t * p, int * pnBestLuts, int * pnBestEdges, int * pnBestLevels, int fArea )
{
int nCurLuts, nCurEdges, nCurLevels;
Gia_ManLutParams( p, &nCurLuts, &nCurEdges, &nCurLevels );
@@ -27119,8 +27549,9 @@ static inline int Gia_ManCompareWithBest( Gia_Man_t * pBest, Gia_Man_t * p, int
Gia_ManPoNum(pBest) != Gia_ManPoNum(p) ||
Gia_ManRegNum(pBest) != Gia_ManRegNum(p) ||
strcmp(Gia_ManName(pBest), Gia_ManName(p)) ||
- (*pnBestLevels > nCurLevels) ||
- (*pnBestLevels == nCurLevels && 2*(*pnBestLuts) + *pnBestEdges > 2*nCurLuts + nCurEdges) )
+ (!fArea && (*pnBestLevels > nCurLevels || (*pnBestLevels == nCurLevels && 2*(*pnBestLuts) + *pnBestEdges > 2*nCurLuts + nCurEdges))) ||
+ ( fArea && (*pnBestLuts > nCurLuts || (*pnBestLuts == nCurLuts && *pnBestLevels > nCurLevels)))
+ )
{
*pnBestLuts = nCurLuts;
*pnBestEdges = nCurEdges;
@@ -27143,12 +27574,15 @@ static inline int Gia_ManCompareWithBest( Gia_Man_t * pBest, Gia_Man_t * p, int
***********************************************************************/
int Abc_CommandAbc9Save( Abc_Frame_t * pAbc, int argc, char ** argv )
{
- int c;
+ int c, fArea = 0;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "ah" ) ) != EOF )
{
switch ( c )
{
+ case 'a':
+ fArea ^= 1;
+ break;
case 'h':
goto usage;
default:
@@ -27165,7 +27599,7 @@ int Abc_CommandAbc9Save( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "GIA has no mapping.\n" );
return 1;
}
- if ( !Gia_ManCompareWithBest( pAbc->pGiaBest, pAbc->pGia, &pAbc->nBestLuts, &pAbc->nBestEdges, &pAbc->nBestLevels ) )
+ if ( !Gia_ManCompareWithBest( pAbc->pGiaBest, pAbc->pGia, &pAbc->nBestLuts, &pAbc->nBestEdges, &pAbc->nBestLevels, fArea ) )
return 0;
// save the design as best
Gia_ManStopP( &pAbc->pGiaBest );
@@ -27173,8 +27607,9 @@ int Abc_CommandAbc9Save( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- Abc_Print( -2, "usage: &save [-h]\n" );
+ Abc_Print( -2, "usage: &save [-ah]\n" );
Abc_Print( -2, "\t compares and possibly saves AIG with mapping\n" );
+ Abc_Print( -2, "\t-a : toggle using area as the primary metric [default = %s]\n", fArea? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
}
@@ -33363,7 +33798,7 @@ int Abc_CommandAbc9If( Abc_Frame_t * pAbc, int argc, char ** argv )
{
if ( !Abc_FrameReadFlag("silentmode") )
Abc_Print( -1, "Empty GIA network.\n" );
- return 1;
+ return 0;
}
if ( Gia_ManBufNum(pAbc->pGia) )
{
@@ -35224,14 +35659,23 @@ int Abc_CommandAbc9Edge( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern int Edg_ManAssignEdgeNew( Gia_Man_t * p, int nEdges, int fVerbose );
extern void Seg_ManComputeDelay( Gia_Man_t * pGia, int Delay, int nFanouts, int fTwo, int fVerbose );
- extern void Sle_ManExplore( Gia_Man_t * pGia, int DelayInit, int fVerbose );
+ extern void Sle_ManExplore( Gia_Man_t * pGia, int nBTLimit, int DelayInit, int fDynamic, int fTwoEdges, int fVerbose );
- int c, DelayMax = 0, nFanouts = 0, nEdges = 1, fReverse = 0, fUsePack = 0, fUseOld = 0, fMapping = 0, fVerbose = 0;
+ int c, nBTLimit = 0, DelayMax = 0, nFanouts = 0, nEdges = 1, fReverse = 0, fUsePack = 0, fUseOld = 0, fMapping = 0, fDynamic = 1, fVerbose = 0;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "DFErpomvh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "CDFErpomdvh" ) ) != EOF )
{
switch ( c )
{
+ case 'C':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-C\" should be followed by a positive integer.\n" );
+ goto usage;
+ }
+ nBTLimit = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ break;
case 'D':
if ( globalUtilOptind >= argc )
{
@@ -35276,6 +35720,9 @@ int Abc_CommandAbc9Edge( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'm':
fMapping ^= 1;
break;
+ case 'd':
+ fDynamic ^= 1;
+ break;
case 'v':
fVerbose ^= 1;
break;
@@ -35289,16 +35736,16 @@ int Abc_CommandAbc9Edge( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Empty GIA network.\n" );
return 1;
}
+ if ( fMapping )
+ {
+ Sle_ManExplore( pAbc->pGia, nBTLimit, DelayMax, fDynamic, nEdges==2, fVerbose );
+ return 0;
+ }
if ( !Gia_ManHasMapping(pAbc->pGia) )
{
Abc_Print( -1, "Current AIG has no mapping. Run \"&if\".\n" );
return 1;
}
- if ( fMapping )
- {
- Sle_ManExplore( pAbc->pGia, DelayMax, fVerbose );
- return 0;
- }
if ( Gia_ManLutSizeMax(pAbc->pGia) > 6 )
{
Abc_Print( 0, "Current AIG has mapping into %d-LUTs.\n", Gia_ManLutSizeMax(pAbc->pGia) );
@@ -35333,8 +35780,9 @@ int Abc_CommandAbc9Edge( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- Abc_Print( -2, "usage: &edge [-DFE num] [-rpomvh]\n" );
+ Abc_Print( -2, "usage: &edge [-CDFE num] [-rpomdvh]\n" );
Abc_Print( -2, "\t find edge assignment of the LUT-mapped network\n" );
+ Abc_Print( -2, "\t-C num : the SAT solver conflict limit (0 = unused) [default = %d]\n", nBTLimit );
Abc_Print( -2, "\t-D num : the upper bound on delay [default = %d]\n", DelayMax );
Abc_Print( -2, "\t-F num : skip using edge if fanout higher than this [default = %d]\n", nFanouts );
Abc_Print( -2, "\t-E num : the limit on the number of edges (1 <= num <= 2) [default = %d]\n", nEdges );
@@ -35342,6 +35790,7 @@ usage:
Abc_Print( -2, "\t-p : toggles deriving edges from packing [default = %s]\n", fUsePack? "yes": "no" );
Abc_Print( -2, "\t-o : toggles using old algorithm [default = %s]\n", fUseOld? "yes": "no" );
Abc_Print( -2, "\t-m : toggles combining edge assignment with mapping [default = %s]\n", fMapping? "yes": "no" );
+ Abc_Print( -2, "\t-d : toggles dynamic addition of clauses [default = %s]\n", fDynamic? "yes": "no" );
Abc_Print( -2, "\t-v : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : prints the command usage\n");
return 1;
@@ -35505,6 +35954,8 @@ int Abc_CommandAbc9Unmap( Abc_Frame_t * pAbc, int argc, char ** argv )
Vec_IntFreeP( &pAbc->pGia->vMapping );
Vec_IntFreeP( &pAbc->pGia->vPacking );
Vec_IntFreeP( &pAbc->pGia->vCellMapping );
+ Vec_IntFreeP( &pAbc->pGia->vEdge1 );
+ Vec_IntFreeP( &pAbc->pGia->vEdge2 );
return 0;
usage:
@@ -39675,7 +40126,7 @@ usage:
int Abc_CommandAbc9Polyn( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Vec_Int_t * vOrder = NULL;
- int c, fSimple = 0, fSigned = 0, fVerbose = 0, fVeryVerbose = 0;
+ int c, fSimple = 1, fSigned = 0, fVerbose = 0, fVeryVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "asvwh" ) ) != EOF )
{
diff --git a/src/base/abci/abcDetect.c b/src/base/abci/abcDetect.c
index 8fa395e8..c87169b5 100644
--- a/src/base/abci/abcDetect.c
+++ b/src/base/abci/abcDetect.c
@@ -193,7 +193,7 @@ finish:
SeeAlso []
***********************************************************************/
-void Abc_NtkDetectClassesTest( Abc_Ntk_t * pNtk, int fVerbose )
+void Abc_NtkDetectClassesTest( Abc_Ntk_t * pNtk, int fSeq, int fVerbose )
{
printf( "This procedure is currently not used.\n" );
}
diff --git a/src/base/abci/abcDress3.c b/src/base/abci/abcDress3.c
new file mode 100644
index 00000000..33545f0a
--- /dev/null
+++ b/src/base/abci/abcDress3.c
@@ -0,0 +1,344 @@
+/**CFile****************************************************************
+
+ FileName [abcDress3.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Network and node package.]
+
+ Synopsis [Transfers names from one netlist to the other.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: abcDress3.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "base/abc/abc.h"
+#include "base/io/ioAbc.h"
+#include "proof/cec/cec.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Compute equivalence classes of nodes.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_NtkComputeGiaEquivs( Gia_Man_t * pGia, int nConfs, int fVerbose )
+{
+ Gia_Man_t * pTemp;
+ Cec_ParFra_t ParsFra, * pPars = &ParsFra;
+ Cec_ManFraSetDefaultParams( pPars );
+ pPars->fUseOrigIds = 1;
+ pPars->fSatSweeping = 1;
+ pPars->nBTLimit = nConfs;
+ pPars->fVerbose = fVerbose;
+ pTemp = Cec_ManSatSweeping( pGia, pPars, 0 );
+ Gia_ManStop( pTemp );
+ pTemp = Gia_ManOrigIdsReduce( pGia, pGia->vIdsEquiv );
+ Gia_ManStop( pTemp );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Converts AIG from HOP to GIA.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_ConvertHopToGia_rec1( Gia_Man_t * p, Hop_Obj_t * pObj )
+{
+ assert( !Hop_IsComplement(pObj) );
+ if ( !Hop_ObjIsNode(pObj) || Hop_ObjIsMarkA(pObj) )
+ return;
+ Abc_ConvertHopToGia_rec1( p, Hop_ObjFanin0(pObj) );
+ Abc_ConvertHopToGia_rec1( p, Hop_ObjFanin1(pObj) );
+ pObj->iData = Gia_ManHashAnd( p, Hop_ObjChild0CopyI(pObj), Hop_ObjChild1CopyI(pObj) );
+ assert( !Hop_ObjIsMarkA(pObj) ); // loop detection
+ Hop_ObjSetMarkA( pObj );
+}
+void Abc_ConvertHopToGia_rec2( Hop_Obj_t * pObj )
+{
+ assert( !Hop_IsComplement(pObj) );
+ if ( !Hop_ObjIsNode(pObj) || !Hop_ObjIsMarkA(pObj) )
+ return;
+ Abc_ConvertHopToGia_rec2( Hop_ObjFanin0(pObj) );
+ Abc_ConvertHopToGia_rec2( Hop_ObjFanin1(pObj) );
+ assert( Hop_ObjIsMarkA(pObj) ); // loop detection
+ Hop_ObjClearMarkA( pObj );
+}
+int Abc_ConvertHopToGia( Gia_Man_t * p, Hop_Obj_t * pRoot )
+{
+ assert( !Hop_IsComplement(pRoot) );
+ if ( Hop_ObjIsConst1( pRoot ) )
+ return 1;
+ Abc_ConvertHopToGia_rec1( p, pRoot );
+ Abc_ConvertHopToGia_rec2( pRoot );
+ return pRoot->iData;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Add logic from pNtk to the AIG manager p.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_NtkAigToGiaOne( Gia_Man_t * p, Abc_Ntk_t * pNtk, Vec_Int_t * vMap )
+{
+ Hop_Man_t * pHopMan;
+ Hop_Obj_t * pHopObj;
+ Vec_Ptr_t * vNodes;
+ Abc_Obj_t * pNode, * pFanin;
+ int i, k;
+ assert( Abc_NtkIsAigLogic(pNtk) );
+ pHopMan = (Hop_Man_t *)pNtk->pManFunc;
+ Hop_ManConst1(pHopMan)->iData = 1;
+ // image primary inputs
+ Abc_NtkCleanCopy( pNtk );
+ Abc_NtkForEachCi( pNtk, pNode, i )
+ pNode->iTemp = Gia_ManCiLit(p, Vec_IntEntry(vMap, i));
+ // iterate through nodes used in the mapping
+ vNodes = Abc_NtkDfs( pNtk, 1 );
+ Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pNode, i )
+ {
+ Abc_ObjForEachFanin( pNode, pFanin, k )
+ Hop_ManPi(pHopMan, k)->iData = pFanin->iTemp;
+ pHopObj = Hop_Regular( (Hop_Obj_t *)pNode->pData );
+ assert( Abc_ObjFaninNum(pNode) <= Hop_ManPiNum(pHopMan) );
+ if ( Hop_DagSize(pHopObj) > 0 )
+ Abc_ConvertHopToGia( p, pHopObj );
+ pNode->iTemp = Abc_LitNotCond( pHopObj->iData, Hop_IsComplement( (Hop_Obj_t *)pNode->pData ) );
+ }
+ Vec_PtrFree( vNodes );
+ // create primary outputs
+ Abc_NtkForEachCo( pNtk, pNode, i )
+ Gia_ManAppendCo( p, Abc_ObjFanin0(pNode)->iTemp );
+}
+Gia_Man_t * Abc_NtkAigToGiaTwo( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fByName )
+{
+ Gia_Man_t * p;
+ Gia_Obj_t * pObj;
+ Abc_Obj_t * pNode;
+ Vec_Int_t * vMap1, * vMap2;
+ int i, Index = 0;
+ assert( Abc_NtkIsAigLogic(pNtk1) );
+ assert( Abc_NtkIsAigLogic(pNtk2) );
+ // find common variables
+ if ( fByName )
+ {
+ int nCommon = 0;
+ vMap1 = Vec_IntStartNatural( Abc_NtkCiNum(pNtk1) );
+ vMap2 = Vec_IntAlloc( Abc_NtkCiNum(pNtk2) );
+ Abc_NtkForEachCi( pNtk1, pNode, i )
+ pNode->iTemp = Index++;
+ assert( Index == Abc_NtkCiNum(pNtk1) );
+ Abc_NtkForEachCi( pNtk2, pNode, i )
+ {
+ int Num = Nm_ManFindIdByName( pNtk1->pManName, Abc_ObjName(pNode), ABC_OBJ_PI );
+ if ( Num < 0 )
+ Num = Nm_ManFindIdByName( pNtk1->pManName, Abc_ObjName(pNode), ABC_OBJ_BO );
+ assert( Num < 0 || Abc_ObjIsCi(Abc_NtkObj(pNtk1, Num)) );
+ if ( Num >= 0 )
+ Vec_IntPush( vMap2, Abc_NtkObj(pNtk1, Num)->iTemp ), nCommon++;
+ else
+ Vec_IntPush( vMap2, Index++ );
+ }
+ // report
+ printf( "Matched %d vars by name.", nCommon );
+ if ( nCommon != Abc_NtkCiNum(pNtk1) )
+ printf( " Netlist1 has %d unmatched vars.", Abc_NtkCiNum(pNtk1) - nCommon );
+ if ( nCommon != Abc_NtkCiNum(pNtk2) )
+ printf( " Netlist2 has %d unmatched vars.", Abc_NtkCiNum(pNtk2) - nCommon );
+ printf( "\n" );
+ }
+ else
+ {
+ vMap1 = Vec_IntStartNatural( Abc_NtkCiNum(pNtk1) );
+ vMap2 = Vec_IntStartNatural( Abc_NtkCiNum(pNtk2) );
+ Index = Abc_MaxInt( Vec_IntSize(vMap1), Vec_IntSize(vMap2) );
+ // report
+ printf( "Matched %d vars by order.", Abc_MinInt(Abc_NtkCiNum(pNtk1), Abc_NtkCiNum(pNtk2)) );
+ if ( Abc_NtkCiNum(pNtk1) < Abc_NtkCiNum(pNtk2) )
+ printf( " The last %d vars of Netlist2 are unmatched vars.", Abc_NtkCiNum(pNtk2) - Abc_NtkCiNum(pNtk1) );
+ if ( Abc_NtkCiNum(pNtk1) > Abc_NtkCiNum(pNtk2) )
+ printf( " The last %d vars of Netlist1 are unmatched vars.", Abc_NtkCiNum(pNtk1) - Abc_NtkCiNum(pNtk2) );
+ printf( "\n" );
+ }
+ // create new manager
+ p = Gia_ManStart( 10000 );
+ p->pName = Abc_UtilStrsav( Abc_NtkName(pNtk1) );
+ p->pSpec = Abc_UtilStrsav( Abc_NtkSpec(pNtk1) );
+ for ( i = 0; i < Index; i++ )
+ Gia_ManAppendCi(p);
+ // add logic
+ Gia_ManHashAlloc( p );
+ Abc_NtkAigToGiaOne( p, pNtk1, vMap1 );
+ Abc_NtkAigToGiaOne( p, pNtk2, vMap2 );
+ Gia_ManHashStop( p );
+ Vec_IntFree( vMap1 );
+ Vec_IntFree( vMap2 );
+ // add extra POs to dangling nodes
+ Gia_ManCreateValueRefs( p );
+ Gia_ManForEachAnd( p, pObj, i )
+ if ( pObj->Value == 0 )
+ Gia_ManAppendCo( p, Abc_Var2Lit(i, 0) );
+ return p;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Collect equivalence class information.]
+
+ Description [Each class is represented as follows:
+ <num_entries><entry1><entry2>...<entryN>
+ where <entry> is nodeId with 1-bit for complement and 1-bit for network.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline void Abc_NtkCollectAddOne( int iNtk, int iObj, int iGiaLit, Gia_Man_t * pGia, Vec_Int_t * vGia2Cla, Vec_Int_t * vNexts[2] )
+{
+ int iRepr = Gia_ObjReprSelf( pGia, Abc_Lit2Var(iGiaLit) );
+ int Compl = Abc_LitIsCompl(iGiaLit) ^ Gia_ObjPhase(Gia_ManObj(pGia, iRepr)) ^ Gia_ObjPhase(Gia_ManObj(pGia, Abc_Lit2Var(iGiaLit)));
+ int Added = Abc_Var2Lit( Abc_Var2Lit(iObj, Compl), iNtk );
+ int Entry = Vec_IntEntry( vGia2Cla, iRepr );
+ Vec_IntWriteEntry( vNexts[iNtk], iObj, Entry );
+ Vec_IntWriteEntry( vGia2Cla, iRepr, Added );
+}
+Vec_Int_t * Abc_NtkCollectEquivClasses( Abc_Ntk_t * pNtks[2], Gia_Man_t * pGia )
+{
+ Vec_Int_t * vClass = Vec_IntAlloc( 100 );
+ Vec_Int_t * vClasses = Vec_IntAlloc( 1000 );
+ Vec_Int_t * vGia2Cla = Vec_IntStartFull( Gia_ManObjNum(pGia) ); // mapping objId into classId
+ Vec_Int_t * vNexts[2] = { Vec_IntStartFull(Abc_NtkObjNumMax(pNtks[0])), Vec_IntStartFull(Abc_NtkObjNumMax(pNtks[1])) };
+ Abc_Obj_t * pObj;
+ int n, i, k, Entry, fCompl;
+ Abc_NtkForEachCi( pNtks[0], pObj, i )
+ Abc_NtkCollectAddOne( 0, Abc_ObjId(pObj), pObj->iTemp, pGia, vGia2Cla, vNexts );
+ for ( n = 0; n < 2; n++ )
+ Abc_NtkForEachNode( pNtks[n], pObj, i )
+ Abc_NtkCollectAddOne( n, Abc_ObjId(pObj), pObj->iTemp, pGia, vGia2Cla, vNexts );
+ Vec_IntForEachEntry( vGia2Cla, Entry, i )
+ {
+ Vec_IntClear( vClass );
+ for ( ; Entry >= 0; Entry = Vec_IntEntry(vNexts[Entry&1], Entry>>2) )
+ Vec_IntPush( vClass, Entry );
+ if ( Vec_IntSize(vClass) < 2 )
+ continue;
+ Vec_IntReverseOrder( vClass );
+ fCompl = 2 & Vec_IntEntry( vClass, 0 );
+ Vec_IntForEachEntry( vClass, Entry, k )
+ Vec_IntWriteEntry( vClass, k, Entry ^ fCompl );
+ Vec_IntPush( vClasses, Vec_IntSize(vClass) );
+ Vec_IntAppend( vClasses, vClass );
+ }
+ Vec_IntFree( vGia2Cla );
+ Vec_IntFree( vNexts[0] );
+ Vec_IntFree( vNexts[1] );
+ Vec_IntFree( vClass );
+ return vClasses;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Write the output file.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_NtkDumpEquivFile( char * pFileName, Vec_Int_t * vClasses, Abc_Ntk_t * pNtks[2] )
+{
+ int i, c, k, Entry;
+ FILE * pFile = fopen( pFileName, "wb" );
+ if ( pFile == NULL ) { printf( "Cannot open file %s for writing.\n", pFileName ); return; }
+ fprintf( pFile, "# Node equivalences computed by ABC for networks \"%s\" and \"%s\" on %s\n\n", Abc_NtkName(pNtks[0]), Abc_NtkName(pNtks[1]), Extra_TimeStamp() );
+ for ( i = c = 0; i < Vec_IntSize(vClasses); c++, i += 1 + Vec_IntEntry(vClasses, i) )
+ {
+ Vec_IntForEachEntryStartStop( vClasses, Entry, k, i + 1, i + 1 + Vec_IntEntry(vClasses, i) )
+ {
+ Abc_Ntk_t * pNtk = pNtks[Entry & 1];
+ char * pObjName = Abc_ObjName( Abc_NtkObj(pNtk, Entry>>2) );
+ fprintf( pFile, "%d:%s:%s%s\n", c+1, Abc_NtkName(pNtk), (Entry&2) ? "NOT:":"", pObjName );
+ }
+ fprintf( pFile, "\n" );
+ }
+ fclose( pFile );
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Compute and dump equivalent name classes.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_NtkDumpEquiv( Abc_Ntk_t * pNtks[2], char * pFileName, int nConfs, int fByName, int fVerbose )
+{
+ //abctime clk = Abc_Clock();
+ Vec_Int_t * vClasses;
+ // derive shared AIG for the two networks
+ Gia_Man_t * pGia = Abc_NtkAigToGiaTwo( pNtks[0], pNtks[1], fByName );
+ if ( fVerbose )
+ printf( "Computing equivalences for networks \"%s\" and \"%s\" with conflict limit %d.\n", Abc_NtkName(pNtks[0]), Abc_NtkName(pNtks[1]), nConfs );
+ // compute equivalences in this AIG
+ Abc_NtkComputeGiaEquivs( pGia, nConfs, fVerbose );
+ //if ( fVerbose )
+ // Abc_PrintTime( 1, "Equivalence computation time", Abc_Clock() - clk );
+ if ( fVerbose )
+ Gia_ManPrintStats( pGia, NULL );
+ // collect equivalence class information
+ vClasses = Abc_NtkCollectEquivClasses( pNtks, pGia );
+ Gia_ManStop( pGia );
+ // dump information into the output file
+ Abc_NtkDumpEquivFile( pFileName, vClasses, pNtks );
+ Vec_IntFree( vClasses );
+}
+
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/base/abci/abcExact.c b/src/base/abci/abcExact.c
new file mode 100644
index 00000000..8c508b63
--- /dev/null
+++ b/src/base/abci/abcExact.c
@@ -0,0 +1,1696 @@
+/**CFile****************************************************************
+
+ FileName [abcExact.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Network and node package.]
+
+ Synopsis [Find minimum size networks with a SAT solver.]
+
+ Author [Mathias Soeken]
+
+ Affiliation [EPFL]
+
+ Date [Ver. 1.0. Started - July 15, 2016.]
+
+ Revision [$Id: abcFanio.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+/* This implementation is based on Exercises 477 and 478 in
+ * Donald E. Knuth TAOCP Fascicle 6 (Satisfiability) Section 7.2.2.2
+ */
+
+#include "base/abc/abc.h"
+
+#include "aig/gia/gia.h"
+#include "bool/kit/kit.h"
+#include "misc/util/utilTruth.h"
+#include "misc/vec/vecInt.h"
+#include "misc/vec/vecPtr.h"
+#include "proof/cec/cec.h"
+#include "sat/bsat/satSolver.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+static word s_Truths8[32] = {
+ ABC_CONST(0xAAAAAAAAAAAAAAAA), ABC_CONST(0xAAAAAAAAAAAAAAAA), ABC_CONST(0xAAAAAAAAAAAAAAAA), ABC_CONST(0xAAAAAAAAAAAAAAAA),
+ ABC_CONST(0xCCCCCCCCCCCCCCCC), ABC_CONST(0xCCCCCCCCCCCCCCCC), ABC_CONST(0xCCCCCCCCCCCCCCCC), ABC_CONST(0xCCCCCCCCCCCCCCCC),
+ ABC_CONST(0xF0F0F0F0F0F0F0F0), ABC_CONST(0xF0F0F0F0F0F0F0F0), ABC_CONST(0xF0F0F0F0F0F0F0F0), ABC_CONST(0xF0F0F0F0F0F0F0F0),
+ ABC_CONST(0xFF00FF00FF00FF00), ABC_CONST(0xFF00FF00FF00FF00), ABC_CONST(0xFF00FF00FF00FF00), ABC_CONST(0xFF00FF00FF00FF00),
+ ABC_CONST(0xFFFF0000FFFF0000), ABC_CONST(0xFFFF0000FFFF0000), ABC_CONST(0xFFFF0000FFFF0000), ABC_CONST(0xFFFF0000FFFF0000),
+ ABC_CONST(0xFFFFFFFF00000000), ABC_CONST(0xFFFFFFFF00000000), ABC_CONST(0xFFFFFFFF00000000), ABC_CONST(0xFFFFFFFF00000000),
+ ABC_CONST(0x0000000000000000), ABC_CONST(0xFFFFFFFFFFFFFFFF), ABC_CONST(0x0000000000000000), ABC_CONST(0xFFFFFFFFFFFFFFFF),
+ ABC_CONST(0x0000000000000000), ABC_CONST(0x0000000000000000), ABC_CONST(0xFFFFFFFFFFFFFFFF), ABC_CONST(0xFFFFFFFFFFFFFFFF)
+};
+
+#define ABC_EXACT_SOL_NVARS 0
+#define ABC_EXACT_SOL_NFUNC 1
+#define ABC_EXACT_SOL_NGATES 2
+
+typedef struct Ses_Man_t_ Ses_Man_t;
+struct Ses_Man_t_
+{
+ sat_solver * pSat; /* SAT solver */
+
+ word * pSpec; /* specification */
+ int bSpecInv; /* remembers whether spec was inverted for normalization */
+ int nSpecVars; /* number of variables in specification */
+ int nSpecFunc; /* number of functions to synthesize */
+ int nRows; /* number of rows in the specification (without 0) */
+ int nMaxDepth; /* maximum depth (-1 if depth is not constrained) */
+ int * pArrTimeProfile; /* arrival times of inputs (NULL if arrival times are ignored) */
+ int nArrTimeDelta; /* delta to the original arrival times (arrival times are normalized to have 0 as minimum element) */
+ int nArrTimeMax; /* maximum normalized arrival time */
+ int nBTLimit; /* conflict limit */
+ int fMakeAIG; /* create AIG instead of general network */
+ int fVerbose; /* be verbose */
+ int fVeryVerbose; /* be very verbose */
+
+ int nGates; /* number of gates */
+
+ int nSimVars; /* number of simulation vars x(i, t) */
+ int nOutputVars; /* number of output variables g(h, i) */
+ int nGateVars; /* number of gate variables f(i, p, q) */
+ int nSelectVars; /* number of select variables s(i, j, k) */
+ int nDepthVars; /* number of depth variables d(i, j) */
+
+ int nOutputOffset; /* offset where output variables start */
+ int nGateOffset; /* offset where gate variables start */
+ int nSelectOffset; /* offset where select variables start */
+ int nDepthOffset; /* offset where depth variables start */
+
+ abctime timeSat; /* SAT runtime */
+ abctime timeSatSat; /* SAT runtime (sat instance) */
+ abctime timeSatUnsat; /* SAT runtime (unsat instance) */
+ abctime timeTotal; /* all runtime */
+};
+
+/***********************************************************************
+
+ Synopsis [Store truth tables based on normalized arrival times.]
+
+***********************************************************************/
+
+// The hash table is a list of pointers to Ses_TruthEntry_t elements, which
+// are arranged in a linked list, each of which pointing to a linked list
+// of Ses_TimesEntry_t elements which contain the char* representation of the
+// optimum netlist according to then normalized arrival times:
+
+typedef struct Ses_TimesEntry_t_ Ses_TimesEntry_t;
+struct Ses_TimesEntry_t_
+{
+ int pArrTimeProfile[8]; /* normalized arrival time profile */
+ Ses_TimesEntry_t * next; /* linked list pointer */
+ char * pNetwork; /* pointer to char array representation of optimum network */
+};
+
+typedef struct Ses_TruthEntry_t_ Ses_TruthEntry_t;
+struct Ses_TruthEntry_t_
+{
+ word pTruth[4]; /* truth table for comparison */
+ int nVars; /* number of variables */
+ Ses_TruthEntry_t * next; /* linked list pointer */
+ Ses_TimesEntry_t * head; /* pointer to head of sub list with arrival times */
+};
+
+#define SES_STORE_TABLE_SIZE 1024
+typedef struct Ses_Store_t_ Ses_Store_t;
+struct Ses_Store_t_
+{
+ int fMakeAIG; /* create AIG instead of general network */
+ int fVerbose; /* be verbose */
+ int nBTLimit; /* conflict limit */
+ int nEntriesCount; /* number of entries */
+ Ses_TruthEntry_t * pEntries[SES_STORE_TABLE_SIZE]; /* hash table for truth table entries */
+
+ unsigned long nCutCount;
+ unsigned long pCutCount[9];
+ unsigned long nCacheHit;
+};
+
+static Ses_Store_t * s_pSesStore = NULL;
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+static int Abc_NormalizeArrivalTimes( int * pArrTimeProfile, int nVars, int * maxNormalized )
+{
+ int * p = pArrTimeProfile, * pEnd = pArrTimeProfile + nVars;
+ int delta = *p;
+
+ while ( ++p < pEnd )
+ if ( *p < delta )
+ delta = *p;
+
+ *maxNormalized = 0;
+ p = pArrTimeProfile;
+ while ( p < pEnd )
+ {
+ *p -= delta;
+ if ( *p > *maxNormalized )
+ *maxNormalized = *p;
+ ++p;
+ }
+
+ *maxNormalized += 1;
+
+ return delta;
+}
+
+static inline Ses_Store_t * Ses_StoreAlloc( int nBTLimit, int fMakeAIG, int fVerbose )
+{
+ Ses_Store_t * pStore = ABC_CALLOC( Ses_Store_t, 1 );
+ pStore->fMakeAIG = fMakeAIG;
+ pStore->fVerbose = fVerbose;
+ pStore->nBTLimit = nBTLimit;
+ pStore->nEntriesCount = 0;
+ memset( pStore->pEntries, 0, SES_STORE_TABLE_SIZE );
+
+ pStore->nCutCount = 0;
+ memset( pStore->pCutCount, 0, 9 );
+ pStore->nCacheHit = 0;
+
+ return pStore;
+}
+
+static inline void Ses_StoreClean( Ses_Store_t * pStore )
+{
+ int i;
+ Ses_TruthEntry_t * pTEntry, * pTEntry2;
+ Ses_TimesEntry_t * pTiEntry, * pTiEntry2;
+
+ for ( i = 0; i < SES_STORE_TABLE_SIZE; ++i )
+ if ( pStore->pEntries[i] )
+ {
+ pTEntry = pStore->pEntries[i];
+
+ while ( pTEntry )
+ {
+ pTiEntry = pTEntry->head;
+ while ( pTiEntry )
+ {
+ ABC_FREE( pTiEntry->pNetwork );
+ pTiEntry2 = pTiEntry;
+ pTiEntry = pTiEntry->next;
+ ABC_FREE( pTiEntry2 );
+ }
+ pTEntry2 = pTEntry;
+ pTEntry = pTEntry->next;
+ ABC_FREE( pTEntry2 );
+ }
+ }
+
+ ABC_FREE( pStore );
+}
+
+static inline int Ses_StoreTableHash( word * pTruth, int nVars )
+{
+ static int s_Primes[4] = { 1291, 1699, 1999, 2357 };
+ int i;
+ unsigned uHash = 0;
+ for ( i = 0; i < Kit_TruthWordNum( nVars ); ++i )
+ uHash ^= pTruth[i] * s_Primes[i & 0xf];
+ return (int)(uHash % SES_STORE_TABLE_SIZE );
+}
+
+static inline int Ses_StoreTruthEqual( Ses_TruthEntry_t * pEntry, word * pTruth, int nVars )
+{
+ int i;
+
+ if ( pEntry->nVars != nVars )
+ return 0;
+
+ for ( i = 0; i < Kit_TruthWordNum( nVars ); ++i )
+ if ( pEntry->pTruth[i] != pTruth[i] )
+ return 0;
+ return 1;
+}
+
+static inline void Ses_StoreTruthCopy( Ses_TruthEntry_t * pEntry, word * pTruthSrc, int nVars )
+{
+ int i;
+ pEntry->nVars = nVars;
+ for ( i = 0; i < Kit_TruthWordNum( nVars ); ++i )
+ pEntry->pTruth[i] = pTruthSrc[i];
+}
+
+static inline int Ses_StoreTimesEqual( int * pTimes1, int * pTimes2, int nVars )
+{
+ int i;
+ for ( i = 0; i < nVars; ++i )
+ if ( pTimes1[i] != pTimes2[i] )
+ return 0;
+ return 1;
+}
+
+static inline void Ses_StoreTimesCopy( int * pTimesDest, int * pTimesSrc, int nVars )
+{
+ int i;
+ for ( i = 0; i < nVars; ++i )
+ pTimesDest[i] = pTimesSrc[i];
+}
+
+// pArrTimeProfile is not normalized
+// returns 1 if and only if a new TimesEntry has been created
+int Ses_StoreAddEntry( Ses_Store_t * pStore, word * pTruth, int nVars, int * pArrTimeProfile, char * pSol )
+{
+ int i, nDelta, maxNormalized, key, fAdded;
+ Ses_TruthEntry_t * pTEntry;
+ Ses_TimesEntry_t * pTiEntry;
+
+ nDelta = Abc_NormalizeArrivalTimes( pArrTimeProfile, nVars, &maxNormalized );
+
+ key = Ses_StoreTableHash( pTruth, nVars );
+ pTEntry = pStore->pEntries[key];
+
+ /* does truth table already exist? */
+ while ( pTEntry )
+ {
+ if ( Ses_StoreTruthEqual( pTEntry, pTruth, nVars ) )
+ break;
+ else
+ pTEntry = pTEntry->next;
+ }
+
+ /* entry does not yet exist, so create new one and enqueue */
+ if ( !pTEntry )
+ {
+ pTEntry = ABC_CALLOC( Ses_TruthEntry_t, 1 );
+ Ses_StoreTruthCopy( pTEntry, pTruth, nVars );
+ pTEntry->next = pStore->pEntries[key];
+ pStore->pEntries[key] = pTEntry;
+ }
+
+ /* does arrival time already exist? */
+ pTiEntry = pTEntry->head;
+ while ( pTiEntry )
+ {
+ if ( Ses_StoreTimesEqual( pArrTimeProfile, pTiEntry->pArrTimeProfile, nVars ) )
+ break;
+ else
+ pTiEntry = pTiEntry->next;
+ }
+
+ /* entry does not yet exist, so create new one and enqueue */
+ if ( !pTiEntry )
+ {
+ pTiEntry = ABC_CALLOC( Ses_TimesEntry_t, 1 );
+ Ses_StoreTimesCopy( pTiEntry->pArrTimeProfile, pArrTimeProfile, nVars );
+ pTiEntry->pNetwork = pSol;
+ pTiEntry->next = pTEntry->head;
+ pTEntry->head = pTiEntry;
+
+ /* item has been added */
+ fAdded = 1;
+ pStore->nEntriesCount++;
+ }
+ else
+ /* item was already present */
+ fAdded = 0;
+
+ for ( i = 0; i < nVars; ++i )
+ pArrTimeProfile[i] += nDelta;
+ return fAdded;
+}
+
+// pArrTimeProfile is not normalized
+// returns 0 if no solution was found
+char * Ses_StoreGetEntry( Ses_Store_t * pStore, word * pTruth, int nVars, int * pArrTimeProfile )
+{
+ int i, nDelta, maxNormalized, key;
+ Ses_TruthEntry_t * pTEntry;
+ Ses_TimesEntry_t * pTiEntry;
+
+ key = Ses_StoreTableHash( pTruth, nVars );
+ pTEntry = pStore->pEntries[key];
+
+ /* find truth table entry */
+ while ( pTEntry )
+ {
+ if ( Ses_StoreTruthEqual( pTEntry, pTruth, nVars ) )
+ break;
+ else
+ pTEntry = pTEntry->next;
+ }
+
+ /* no entry found? */
+ if ( !pTEntry )
+ return 0;
+
+ nDelta = Abc_NormalizeArrivalTimes( pArrTimeProfile, nVars, &maxNormalized );
+
+ /* find times entry */
+ pTiEntry = pTEntry->head;
+ while ( pTiEntry )
+ {
+ if ( Ses_StoreTimesEqual( pArrTimeProfile, pTiEntry->pArrTimeProfile, nVars ) )
+ break;
+ else
+ pTiEntry = pTiEntry->next;
+ }
+
+ for ( i = 0; i < nVars; ++i )
+ pArrTimeProfile[i] += nDelta;
+
+ /* no entry found? */
+ if ( !pTiEntry )
+ return 0;
+
+ return pTiEntry->pNetwork;
+}
+
+static void Ses_StoreWrite( Ses_Store_t * pStore, const char * pFilename )
+{
+ int i;
+ Ses_TruthEntry_t * pTEntry;
+ Ses_TimesEntry_t * pTiEntry;
+ FILE * pFile;
+
+ pFile = fopen( pFilename, "wb" );
+ if (pFile == NULL)
+ {
+ printf( "cannot open file \"%s\" for writing\n", pFilename );
+ return;
+ }
+
+ fwrite( &pStore->nEntriesCount, sizeof( int ), 1, pFile );
+
+ for ( i = 0; i < SES_STORE_TABLE_SIZE; ++i )
+ if ( pStore->pEntries[i] )
+ {
+ pTEntry = pStore->pEntries[i];
+
+ while ( pTEntry )
+ {
+ pTiEntry = pTEntry->head;
+ while ( pTiEntry )
+ {
+ fwrite( pTEntry->pTruth, sizeof( word ), 4, pFile );
+ fwrite( &pTEntry->nVars, sizeof( int ), 1, pFile );
+ fwrite( pTiEntry->pArrTimeProfile, sizeof( int ), 8, pFile );
+ fwrite( pTiEntry->pNetwork, sizeof( char ), 3 + 4 * pTiEntry->pNetwork[ABC_EXACT_SOL_NGATES] + 2 + pTiEntry->pNetwork[ABC_EXACT_SOL_NVARS], pFile );
+ pTiEntry = pTiEntry->next;
+ }
+ pTEntry = pTEntry->next;
+ }
+ }
+
+
+ fclose( pFile );
+}
+
+static void Ses_StoreRead( Ses_Store_t * pStore, const char * pFilename )
+{
+ int i, nEntries;
+ word pTruth[4];
+ int nVars;
+ int pArrTimeProfile[8];
+ char pHeader[3];
+ char * pNetwork;
+ FILE * pFile;
+ int value;
+
+ pFile = fopen( pFilename, "rb" );
+ if (pFile == NULL)
+ {
+ printf( "cannot open file \"%s\" for reading\n", pFilename );
+ return;
+ }
+
+ value = fread( &nEntries, sizeof( int ), 1, pFile );
+
+ for ( i = 0; i < nEntries; ++i )
+ {
+ value = fread( pTruth, sizeof( word ), 4, pFile );
+ value = fread( &nVars, sizeof( int ), 1, pFile );
+ value = fread( pArrTimeProfile, sizeof( int ), 8, pFile );
+ value = fread( pHeader, sizeof( char ), 3, pFile );
+
+ pNetwork = ABC_CALLOC( char, 3 + 4 * pHeader[ABC_EXACT_SOL_NGATES] + 2 + pHeader[ABC_EXACT_SOL_NVARS] );
+ pNetwork[0] = pHeader[0];
+ pNetwork[1] = pHeader[1];
+ pNetwork[2] = pHeader[2];
+
+ value = fread( pNetwork + 3, sizeof( char ), 4 * pHeader[ABC_EXACT_SOL_NGATES] + 2 + pHeader[ABC_EXACT_SOL_NVARS], pFile );
+
+ Ses_StoreAddEntry( pStore, pTruth, nVars, pArrTimeProfile, pNetwork );
+ }
+
+ fclose( pFile );
+}
+
+static inline Ses_Man_t * Ses_ManAlloc( word * pTruth, int nVars, int nFunc, int nMaxDepth, int * pArrTimeProfile, int fMakeAIG, int fVerbose )
+{
+ int h, i;
+
+ Ses_Man_t * p = ABC_CALLOC( Ses_Man_t, 1 );
+ p->pSat = NULL;
+ p->bSpecInv = 0;
+ for ( h = 0; h < nFunc; ++h )
+ if ( pTruth[h << 2] & 1 )
+ {
+ for ( i = 0; i < 4; ++i )
+ pTruth[(h << 2) + i] = ~pTruth[(h << 2) + i];
+ p->bSpecInv |= ( 1 << h );
+ }
+ p->pSpec = pTruth;
+ p->nSpecVars = nVars;
+ p->nSpecFunc = nFunc;
+ p->nRows = ( 1 << nVars ) - 1;
+ p->nMaxDepth = nMaxDepth;
+ p->pArrTimeProfile = nMaxDepth >= 0 ? pArrTimeProfile : NULL;
+ if ( p->pArrTimeProfile )
+ p->nArrTimeDelta = Abc_NormalizeArrivalTimes( p->pArrTimeProfile, nVars, &p->nArrTimeMax );
+ else
+ p->nArrTimeDelta = p->nArrTimeMax = 0;
+ p->fMakeAIG = fMakeAIG;
+ p->nBTLimit = nMaxDepth >= 0 ? 50000 : 0;
+ p->fVerbose = fVerbose;
+ p->fVeryVerbose = 0;
+
+ return p;
+}
+
+static inline void Ses_ManClean( Ses_Man_t * pSes )
+{
+ int h, i;
+ for ( h = 0; h < pSes->nSpecFunc; ++h )
+ if ( ( pSes->bSpecInv >> h ) & 1 )
+ for ( i = 0; i < 4; ++i )
+ pSes->pSpec[(h << 2) + i] = ~( pSes->pSpec[(h << 2) + i] );
+
+ if ( pSes->pArrTimeProfile )
+ for ( i = 0; i < pSes->nSpecVars; ++i )
+ pSes->pArrTimeProfile[i] += pSes->nArrTimeDelta;
+
+ if ( pSes->pSat )
+ sat_solver_delete( pSes->pSat );
+
+ ABC_FREE( pSes );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Access variables based on indexes.]
+
+***********************************************************************/
+static inline int Ses_ManSimVar( Ses_Man_t * pSes, int i, int t )
+{
+ assert( i < pSes->nGates );
+ assert( t < pSes->nRows );
+
+ return pSes->nRows * i + t;
+}
+
+static inline int Ses_ManOutputVar( Ses_Man_t * pSes, int h, int i )
+{
+ assert( h < pSes->nSpecFunc );
+ assert( i < pSes->nGates );
+
+ return pSes->nOutputOffset + pSes->nGates * h + i;
+}
+
+static inline int Ses_ManGateVar( Ses_Man_t * pSes, int i, int p, int q )
+{
+ assert( i < pSes->nGates );
+ assert( p < 2 );
+ assert( q < 2 );
+ assert( p > 0 || q > 0 );
+
+ return pSes->nGateOffset + i * 3 + ( p << 1 ) + q - 1;
+}
+
+static inline int Ses_ManSelectVar( Ses_Man_t * pSes, int i, int j, int k )
+{
+ int a;
+ int offset;
+
+ assert( i < pSes->nGates );
+ assert( k < pSes->nSpecVars + i );
+ assert( j < k );
+
+ offset = pSes->nSelectOffset;
+ for ( a = pSes->nSpecVars; a < pSes->nSpecVars + i; ++a )
+ offset += a * ( a - 1 ) / 2;
+
+ return offset + ( -j * ( 1 + j - 2 * ( pSes->nSpecVars + i ) ) ) / 2 + ( k - j - 1 );
+}
+
+static inline int Ses_ManDepthVar( Ses_Man_t * pSes, int i, int j )
+{
+ assert( i < pSes->nGates );
+ assert( j <= pSes->nArrTimeMax + i );
+
+ return pSes->nDepthOffset + i * pSes->nArrTimeMax + ( ( i * ( i + 1 ) ) / 2 ) + j;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Setup variables to find network with nGates gates.]
+
+***********************************************************************/
+static void Ses_ManCreateVars( Ses_Man_t * pSes, int nGates )
+{
+ int i;
+
+ if ( pSes->fVerbose )
+ {
+ printf( "create variables for network with %d functions over %d variables and %d gates\n", pSes->nSpecFunc, pSes->nSpecVars, nGates );
+ }
+
+ pSes->nGates = nGates;
+ pSes->nSimVars = nGates * pSes->nRows;
+ pSes->nOutputVars = pSes->nSpecFunc * nGates;
+ pSes->nGateVars = nGates * 3;
+ pSes->nSelectVars = 0;
+ for ( i = pSes->nSpecVars; i < pSes->nSpecVars + nGates; ++i )
+ pSes->nSelectVars += ( i * ( i - 1 ) ) / 2;
+ pSes->nDepthVars = pSes->nMaxDepth > 0 ? nGates * pSes->nArrTimeMax + ( nGates * ( nGates + 1 ) ) / 2 : 0;
+
+ pSes->nOutputOffset = pSes->nSimVars;
+ pSes->nGateOffset = pSes->nSimVars + pSes->nOutputVars;
+ pSes->nSelectOffset = pSes->nSimVars + pSes->nOutputVars + pSes->nGateVars;
+ pSes->nDepthOffset = pSes->nSimVars + pSes->nOutputVars + pSes->nGateVars + pSes->nSelectVars;
+
+ if ( pSes->pSat )
+ sat_solver_delete( pSes->pSat );
+ pSes->pSat = sat_solver_new();
+ sat_solver_setnvars( pSes->pSat, pSes->nSimVars + pSes->nOutputVars + pSes->nGateVars + pSes->nSelectVars + pSes->nDepthVars );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Create clauses.]
+
+***********************************************************************/
+static inline void Ses_ManCreateMainClause( Ses_Man_t * pSes, int t, int i, int j, int k, int a, int b, int c )
+{
+ int pLits[5], ctr = 0, value;
+
+ pLits[ctr++] = Abc_Var2Lit( Ses_ManSelectVar( pSes, i, j, k ), 1 );
+ pLits[ctr++] = Abc_Var2Lit( Ses_ManSimVar( pSes, i, t ), a );
+
+ if ( j < pSes->nSpecVars )
+ {
+ if ( Abc_TtGetBit( s_Truths8 + ( j << 2 ), t + 1 ) != b ) /* 1 in clause, we can omit the clause */
+ return;
+ }
+ else
+ pLits[ctr++] = Abc_Var2Lit( Ses_ManSimVar( pSes, j - pSes->nSpecVars, t ), b );
+
+ if ( k < pSes->nSpecVars )
+ {
+ if ( Abc_TtGetBit( s_Truths8 + ( k << 2 ), t + 1 ) != c ) /* 1 in clause, we can omit the clause */
+ return;
+ }
+ else
+ pLits[ctr++] = Abc_Var2Lit( Ses_ManSimVar( pSes, k - pSes->nSpecVars, t ), c );
+
+ if ( b > 0 || c > 0 )
+ pLits[ctr++] = Abc_Var2Lit( Ses_ManGateVar( pSes, i, b, c ), 1 - a );
+
+ value = sat_solver_addclause( pSes->pSat, pLits, pLits + ctr );
+ assert( value );
+}
+
+static int Ses_ManCreateClauses( Ses_Man_t * pSes )
+{
+ extern int Extra_TruthVarsSymm( unsigned * pTruth, int nVars, int iVar0, int iVar1 );
+
+ int h, i, j, k, t, ii, jj, kk, p, q, d;
+ int pLits[3];
+ Vec_Int_t * vLits;
+
+ for ( t = 0; t < pSes->nRows; ++t )
+ for ( i = 0; i < pSes->nGates; ++i )
+ {
+ /* main clauses */
+ for ( j = 0; j < pSes->nSpecVars + i; ++j )
+ for ( k = j + 1; k < pSes->nSpecVars + i; ++k )
+ {
+ Ses_ManCreateMainClause( pSes, t, i, j, k, 0, 0, 1 );
+ Ses_ManCreateMainClause( pSes, t, i, j, k, 0, 1, 0 );
+ Ses_ManCreateMainClause( pSes, t, i, j, k, 0, 1, 1 );
+ Ses_ManCreateMainClause( pSes, t, i, j, k, 1, 0, 0 );
+ Ses_ManCreateMainClause( pSes, t, i, j, k, 1, 0, 1 );
+ Ses_ManCreateMainClause( pSes, t, i, j, k, 1, 1, 0 );
+ Ses_ManCreateMainClause( pSes, t, i, j, k, 1, 1, 1 );
+ }
+
+ /* output clauses */
+ for ( h = 0; h < pSes->nSpecFunc; ++h )
+ {
+ pLits[0] = Abc_Var2Lit( Ses_ManOutputVar( pSes, h, i ), 1 );
+ pLits[1] = Abc_Var2Lit( Ses_ManSimVar( pSes, i, t ), 1 - Abc_TtGetBit( &pSes->pSpec[h << 2], t + 1 ) );
+ assert( sat_solver_addclause( pSes->pSat, pLits, pLits + 2 ) );
+ }
+ }
+
+ /* some output is selected */
+ for ( h = 0; h < pSes->nSpecFunc; ++h )
+ {
+ vLits = Vec_IntAlloc( pSes->nGates );
+ for ( i = 0; i < pSes->nGates; ++i )
+ Vec_IntPush( vLits, Abc_Var2Lit( Ses_ManOutputVar( pSes, h, i ), 0 ) );
+ assert( sat_solver_addclause( pSes->pSat, Vec_IntArray( vLits ), Vec_IntLimit( vLits ) ) );
+ Vec_IntFree( vLits );
+ }
+
+ /* each gate has two operands */
+ for ( i = 0; i < pSes->nGates; ++i )
+ {
+ vLits = Vec_IntAlloc( ( ( pSes->nSpecVars + i ) * ( pSes->nSpecVars + i - 1 ) ) / 2 );
+ for ( j = 0; j < pSes->nSpecVars + i; ++j )
+ for ( k = j + 1; k < pSes->nSpecVars + i; ++k )
+ Vec_IntPush( vLits, Abc_Var2Lit( Ses_ManSelectVar( pSes, i, j, k ), 0 ) );
+ assert( sat_solver_addclause( pSes->pSat, Vec_IntArray( vLits ), Vec_IntLimit( vLits ) ) );
+ Vec_IntFree( vLits );
+ }
+
+ /* only AIG */
+ if ( pSes->fMakeAIG )
+ {
+ for ( i = 0; i < pSes->nGates; ++i )
+ {
+ /* not 2 ones */
+ pLits[0] = Abc_Var2Lit( Ses_ManGateVar( pSes, i, 0, 1 ), 1 );
+ pLits[1] = Abc_Var2Lit( Ses_ManGateVar( pSes, i, 1, 0 ), 1 );
+ pLits[2] = Abc_Var2Lit( Ses_ManGateVar( pSes, i, 1, 1 ), 0 );
+ assert( sat_solver_addclause( pSes->pSat, pLits, pLits + 3 ) );
+
+ pLits[0] = Abc_Var2Lit( Ses_ManGateVar( pSes, i, 0, 1 ), 1 );
+ pLits[1] = Abc_Var2Lit( Ses_ManGateVar( pSes, i, 1, 0 ), 0 );
+ pLits[2] = Abc_Var2Lit( Ses_ManGateVar( pSes, i, 1, 1 ), 1 );
+ assert( sat_solver_addclause( pSes->pSat, pLits, pLits + 3 ) );
+
+ pLits[0] = Abc_Var2Lit( Ses_ManGateVar( pSes, i, 0, 1 ), 0 );
+ pLits[1] = Abc_Var2Lit( Ses_ManGateVar( pSes, i, 1, 0 ), 1 );
+ pLits[2] = Abc_Var2Lit( Ses_ManGateVar( pSes, i, 1, 1 ), 1 );
+ assert( sat_solver_addclause( pSes->pSat, pLits, pLits + 3 ) );
+ }
+ }
+
+ /* EXTRA clauses: use gate i at least once */
+ for ( i = 0; i < pSes->nGates; ++i )
+ {
+ vLits = Vec_IntAlloc( 0 );
+ for ( h = 0; h < pSes->nSpecFunc; ++h )
+ Vec_IntPush( vLits, Abc_Var2Lit( Ses_ManOutputVar( pSes, h, i ), 0 ) );
+ for ( ii = i + 1; ii < pSes->nGates; ++ii )
+ {
+ for ( j = 0; j < pSes->nSpecVars + i; ++j )
+ Vec_IntPush( vLits, Abc_Var2Lit( Ses_ManSelectVar( pSes, ii, j, pSes->nSpecVars + i ), 0 ) );
+ for ( j = pSes->nSpecVars + i + 1; j < pSes->nSpecVars + ii; ++j )
+ Vec_IntPush( vLits, Abc_Var2Lit( Ses_ManSelectVar( pSes, ii, pSes->nSpecVars + i, j ), 0 ) );
+ }
+ assert( sat_solver_addclause( pSes->pSat, Vec_IntArray( vLits ), Vec_IntLimit( vLits ) ) );
+ Vec_IntFree( vLits );
+ }
+
+ /* EXTRA clauses: co-lexicographic order */
+ for ( i = 0; i < pSes->nGates - 1; ++i )
+ {
+ for ( k = 2; k < pSes->nSpecVars + i; ++k )
+ {
+ for ( j = 1; j < k; ++j )
+ for ( jj = 0; jj < j; ++jj )
+ {
+ pLits[0] = Abc_Var2Lit( Ses_ManSelectVar( pSes, i, j, k ), 1 );
+ pLits[1] = Abc_Var2Lit( Ses_ManSelectVar( pSes, i + 1, jj, k ), 1 );
+ }
+
+ for ( j = 0; j < k; ++j )
+ for ( kk = 1; kk < k; ++kk )
+ for ( jj = 0; jj < kk; ++jj )
+ {
+ pLits[0] = Abc_Var2Lit( Ses_ManSelectVar( pSes, i, j, k ), 1 );
+ pLits[1] = Abc_Var2Lit( Ses_ManSelectVar( pSes, i + 1, jj, kk ), 1 );
+ }
+ }
+ }
+
+ /* EXTRA clauses: symmetric variables */
+ if ( pSes->nSpecFunc == 1 ) /* only check if there is one output function */
+ for ( q = 1; q < pSes->nSpecVars; ++q )
+ for ( p = 0; p < q; ++p )
+ if ( Extra_TruthVarsSymm( (unsigned*)( &pSes->pSpec[h << 2] ), pSes->nSpecVars, p, q ) )
+ {
+ if ( pSes->fVeryVerbose )
+ printf( "variables %d and %d are symmetric\n", p, q );
+ for ( i = 0; i < pSes->nGates; ++i )
+ for ( j = 0; j < q; ++j )
+ {
+ if ( j == p ) continue;
+
+ vLits = Vec_IntAlloc( 0 );
+ Vec_IntPush( vLits, Abc_Var2Lit( Ses_ManSelectVar( pSes, i, j, q ), 1 ) );
+ for ( ii = 0; ii < i; ++ii )
+ for ( kk = 1; kk < pSes->nSpecVars + ii; ++kk )
+ for ( jj = 0; jj < kk; ++jj )
+ if ( jj == p || kk == p )
+ Vec_IntPush( vLits, Abc_Var2Lit( Ses_ManSelectVar( pSes, ii, jj, kk ), 0 ) );
+ assert( sat_solver_addclause( pSes->pSat, Vec_IntArray( vLits ), Vec_IntLimit( vLits ) ) );
+ Vec_IntFree( vLits );
+ }
+ }
+
+ /* DEPTH clauses */
+ if ( pSes->nMaxDepth > 0 )
+ {
+ for ( i = 0; i < pSes->nGates; ++i )
+ {
+ /* propagate depths from children */
+ for ( k = 1; k < i; ++k )
+ for ( j = 0; j < k; ++j )
+ {
+ pLits[0] = Abc_Var2Lit( Ses_ManSelectVar( pSes, i, pSes->nSpecVars + j, pSes->nSpecVars + k ), 1 );
+ for ( jj = 0; jj <= pSes->nArrTimeMax + j; ++jj )
+ {
+ pLits[1] = Abc_Var2Lit( Ses_ManDepthVar( pSes, j, jj ), 1 );
+ pLits[2] = Abc_Var2Lit( Ses_ManDepthVar( pSes, i, jj + 1 ), 0 );
+ assert( sat_solver_addclause( pSes->pSat, pLits, pLits + 3 ) );
+ }
+ }
+
+ for ( k = 0; k < i; ++k )
+ for ( j = 0; j < pSes->nSpecVars + k; ++j )
+ {
+ pLits[0] = Abc_Var2Lit( Ses_ManSelectVar( pSes, i, j, pSes->nSpecVars + k ), 1 );
+ for ( kk = 0; kk <= pSes->nArrTimeMax + k; ++kk )
+ {
+ pLits[1] = Abc_Var2Lit( Ses_ManDepthVar( pSes, k, kk ), 1 );
+ pLits[2] = Abc_Var2Lit( Ses_ManDepthVar( pSes, i, kk + 1 ), 0 );
+ assert( sat_solver_addclause( pSes->pSat, pLits, pLits + 3 ) );
+ }
+ }
+
+ /* propagate depths from arrival times at PIs */
+ if ( pSes->pArrTimeProfile )
+ {
+ for ( k = 1; k < pSes->nSpecVars + i; ++k )
+ for ( j = 0; j < ( ( k < pSes->nSpecVars ) ? k : pSes->nSpecVars ); ++j )
+ {
+ d = pSes->pArrTimeProfile[j];
+ if ( k < pSes->nSpecVars && pSes->pArrTimeProfile[k] > d )
+ d = pSes->pArrTimeProfile[k];
+
+ pLits[0] = Abc_Var2Lit( Ses_ManSelectVar( pSes, i, j, k ), 1 );
+ pLits[1] = Abc_Var2Lit( Ses_ManDepthVar( pSes, i, d + 1 ), 0 );
+ assert( sat_solver_addclause( pSes->pSat, pLits, pLits + 2 ) );
+ }
+ }
+ else
+ {
+ /* arrival times are 0 */
+ pLits[0] = Abc_Var2Lit( Ses_ManDepthVar( pSes, i, 0 ), 0 );
+ assert( sat_solver_addclause( pSes->pSat, pLits, pLits + 1 ) );
+ }
+
+ /* reverse order encoding of depth variables */
+ for ( j = 1; j <= pSes->nArrTimeMax + i; ++j )
+ {
+ pLits[0] = Abc_Var2Lit( Ses_ManDepthVar( pSes, i, j ), 1 );
+ pLits[1] = Abc_Var2Lit( Ses_ManDepthVar( pSes, i, j - 1 ), 0 );
+ assert( sat_solver_addclause( pSes->pSat, pLits, pLits + 2 ) );
+ }
+
+ /* constrain maximum depth */
+ if ( pSes->nMaxDepth < pSes->nArrTimeMax + i )
+ for ( h = 0; h < pSes->nSpecFunc; ++h )
+ {
+ pLits[0] = Abc_Var2Lit( Ses_ManOutputVar( pSes, h, i ), 1 );
+ pLits[1] = Abc_Var2Lit( Ses_ManDepthVar( pSes, i, pSes->nMaxDepth ), 1 );
+ if ( !sat_solver_addclause( pSes->pSat, pLits, pLits + 2 ) )
+ return 0;
+ }
+ }
+ }
+
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Solve.]
+
+***********************************************************************/
+static inline int Ses_ManSolve( Ses_Man_t * pSes )
+{
+ int status;
+ abctime timeStart, timeDelta;
+
+ if ( pSes->fVeryVerbose )
+ {
+ printf( "solve SAT instance with %d clauses and %d variables\n", sat_solver_nclauses( pSes->pSat ), sat_solver_nvars( pSes->pSat ) );
+ }
+
+ timeStart = Abc_Clock();
+ status = sat_solver_solve( pSes->pSat, NULL, NULL, pSes->nBTLimit, 0, 0, 0 );
+ timeDelta = Abc_Clock() - timeStart;
+
+ pSes->timeSat += timeDelta;
+
+ if ( status == l_True )
+ {
+ pSes->timeSatSat += timeDelta;
+ return 1;
+ }
+ else if ( status == l_False )
+ {
+ pSes->timeSatUnsat += timeDelta;
+ return 0;
+ }
+ else
+ {
+ if ( pSes->fVerbose )
+ {
+ printf( "resource limit reached\n" );
+ }
+ return 2;
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Extract solution.]
+
+***********************************************************************/
+// char is an array of short integers that stores the synthesized network
+// using the following format
+// | nvars | nfunc | ngates | gate[1] | ... | gate[ngates] | func[1] | .. | func[nfunc] |
+// nvars: integer with number of variables
+// nfunc: integer with number of functions
+// ngates: integer with number of gates
+// gate[i]: | op | nfanin | fanin[1] | ... | fanin[nfanin] |
+// op: integer of gate's truth table (divided by 2, because gate is normal)
+// nfanin[i]: integer with number of fanins
+// fanin: integer to primary input or other gate
+// func[i]: | fanin | delay | pin[1] | ... | pin[nvars] |
+// fanin: integer as literal to some gate (not primary input), can be complemented
+// delay: maximum delay to output (taking arrival times into account, not normalized) or 0 if not specified
+// pin[i]: pin to pin delay to input i or 0 if not specified or if there is no connection to input i
+// NOTE: since outputs can only point to gates, delay and pin-to-pin times cannot be 0
+static char * Ses_ManExtractSolution( Ses_Man_t * pSes )
+{
+ int nSol, h, i, j, k, l, aj, ak, d, nOp;
+ char * pSol, * p;
+ int * pPerm = NULL; /* will be a 2d array [i][l] where is is gate id and l is PI id */
+
+ /* compute length of solution, for now all gates have 2 inputs */
+ nSol = 3 + pSes->nGates * 4 + pSes->nSpecFunc * ( 2 + pSes->nSpecVars );
+
+ p = pSol = ABC_CALLOC( char, nSol );
+
+ /* header */
+ *p++ = pSes->nSpecVars;
+ *p++ = pSes->nSpecFunc;
+ *p++ = pSes->nGates;
+
+ /* gates */
+ for ( i = 0; i < pSes->nGates; ++i )
+ {
+ nOp = sat_solver_var_value( pSes->pSat, Ses_ManGateVar( pSes, i, 0, 1 ) );
+ nOp |= sat_solver_var_value( pSes->pSat, Ses_ManGateVar( pSes, i, 1, 0 ) ) << 1;
+ nOp |= sat_solver_var_value( pSes->pSat, Ses_ManGateVar( pSes, i, 1, 1 ) ) << 2;
+
+ *p++ = nOp;
+ *p++ = 2;
+
+ if ( pSes->fVeryVerbose )
+ printf( "add gate %d with operation %d", pSes->nSpecVars + i, nOp );
+
+ for ( k = 0; k < pSes->nSpecVars + i; ++k )
+ for ( j = 0; j < k; ++j )
+ if ( sat_solver_var_value( pSes->pSat, Ses_ManSelectVar( pSes, i, j, k ) ) )
+ {
+ if ( pSes->fVeryVerbose )
+ printf( " and operands %d and %d", j, k );
+ *p++ = j;
+ *p++ = k;
+ break;
+ }
+
+ if ( pSes->fVeryVerbose )
+ {
+ if ( pSes->nMaxDepth > 0 )
+ {
+ printf( " and depth vector " );
+ for ( j = 0; j <= pSes->nArrTimeMax + i; ++j )
+ printf( "%d", sat_solver_var_value( pSes->pSat, Ses_ManDepthVar( pSes, i, j ) ) );
+ }
+ printf( "\n" );
+ }
+ }
+
+ /* pin-to-pin delay */
+ if ( pSes->nMaxDepth != -1 )
+ {
+ pPerm = ABC_CALLOC( int, pSes->nGates * pSes->nSpecVars );
+ for ( i = 0; i < pSes->nGates; ++i )
+ {
+ /* since all gates are binary for now */
+ j = pSol[3 + i * 4 + 2];
+ k = pSol[3 + i * 4 + 3];
+
+ for ( l = 0; l < pSes->nSpecVars; ++l )
+ {
+ /* pin-to-pin delay to input l of child nodes */
+ aj = j < pSes->nSpecVars ? 0 : pPerm[(j - pSes->nSpecVars) * pSes->nSpecVars + l];
+ ak = k < pSes->nSpecVars ? 0 : pPerm[(k - pSes->nSpecVars) * pSes->nSpecVars + l];
+
+ if ( aj == 0 && ak == 0 )
+ pPerm[i * pSes->nSpecVars + l] = ( l == j || l == k ) ? 1 : 0;
+ else
+ pPerm[i * pSes->nSpecVars + l] = Abc_MaxInt( aj, ak ) + 1;
+ }
+ }
+ }
+
+ /* outputs */
+ for ( h = 0; h < pSes->nSpecFunc; ++h )
+ for ( i = 0; i < pSes->nGates; ++i )
+ if ( sat_solver_var_value( pSes->pSat, Ses_ManOutputVar( pSes, h, i ) ) )
+ {
+ *p++ = Abc_Var2Lit( i, ( pSes->bSpecInv >> h ) & 1 );
+ d = 0;
+ if ( pSes->nMaxDepth != -1 )
+ while ( d < pSes->nArrTimeMax + i && sat_solver_var_value( pSes->pSat, Ses_ManDepthVar( pSes, i, d ) ) )
+ ++d;
+ *p++ = d + pSes->nArrTimeDelta;
+ if ( pSes->fVeryVerbose )
+ printf( "output %d points to %d and has normalized delay %d\n", h, i, d );
+ for ( l = 0; l < pSes->nSpecVars; ++l )
+ {
+ d = ( pSes->nMaxDepth != -1 ) ? pPerm[i * pSes->nSpecVars + l] : 0;
+ if ( pSes->fVeryVerbose )
+ printf( " pin-to-pin arrival time from input %d is %d\n", l, d );
+ *p++ = d;
+ }
+ }
+
+ /* pin-to-pin delays */
+ if ( pSes->nMaxDepth != -1 )
+ ABC_FREE( pPerm );
+
+ /* have we used all the fields? */
+ assert( ( p - pSol ) == nSol );
+
+ return pSol;
+}
+
+static Abc_Ntk_t * Ses_ManExtractNtk( char const * pSol )
+{
+ int h, i;
+ char const * p;
+ Abc_Ntk_t * pNtk;
+ Abc_Obj_t * pObj;
+ Vec_Ptr_t * pGates, * vNames;
+ char pGateTruth[5];
+ char * pSopCover;
+
+ pNtk = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_SOP, 1 );
+ pNtk->pName = Extra_UtilStrsav( "exact" );
+ pGates = Vec_PtrAlloc( pSol[ABC_EXACT_SOL_NVARS] + pSol[ABC_EXACT_SOL_NGATES] );
+ pGateTruth[3] = '0';
+ pGateTruth[4] = '\0';
+ vNames = Abc_NodeGetFakeNames( pSol[ABC_EXACT_SOL_NVARS] + pSol[ABC_EXACT_SOL_NFUNC] );
+
+ /* primary inputs */
+ Vec_PtrPush( pNtk->vObjs, NULL );
+ for ( i = 0; i < pSol[ABC_EXACT_SOL_NVARS]; ++i )
+ {
+ pObj = Abc_NtkCreatePi( pNtk );
+ Abc_ObjAssignName( pObj, (char*)Vec_PtrEntry( vNames, i ), NULL );
+ Vec_PtrPush( pGates, pObj );
+ }
+
+ /* gates */
+ p = pSol + 3;
+ for ( i = 0; i < pSol[ABC_EXACT_SOL_NGATES]; ++i )
+ {
+ pGateTruth[2] = '0' + ( *p & 1 );
+ pGateTruth[1] = '0' + ( ( *p >> 1 ) & 1 );
+ pGateTruth[0] = '0' + ( ( *p >> 2 ) & 1 );
+ ++p;
+
+ assert( *p == 2 ); /* binary gate */
+ ++p;
+
+ pSopCover = Abc_SopFromTruthBin( pGateTruth );
+ pObj = Abc_NtkCreateNode( pNtk );
+ pObj->pData = Abc_SopRegister( (Mem_Flex_t*)pNtk->pManFunc, pSopCover );
+ Vec_PtrPush( pGates, pObj );
+ ABC_FREE( pSopCover );
+
+ Abc_ObjAddFanin( pObj, (Abc_Obj_t *)Vec_PtrEntry( pGates, *p++ ) );
+ Abc_ObjAddFanin( pObj, (Abc_Obj_t *)Vec_PtrEntry( pGates, *p++ ) );
+ }
+
+ /* outputs */
+ for ( h = 0; h < pSol[ABC_EXACT_SOL_NFUNC]; ++h )
+ {
+ pObj = Abc_NtkCreatePo( pNtk );
+ Abc_ObjAssignName( pObj, (char*)Vec_PtrEntry( vNames, pSol[ABC_EXACT_SOL_NVARS] + h ), NULL );
+ if ( Abc_LitIsCompl( *p ) )
+ Abc_ObjAddFanin( pObj, Abc_NtkCreateNodeInv( pNtk, (Abc_Obj_t *)Vec_PtrEntry( pGates, pSol[ABC_EXACT_SOL_NVARS] + Abc_Lit2Var( *p ) ) ) );
+ else
+ Abc_ObjAddFanin( pObj, (Abc_Obj_t *)Vec_PtrEntry( pGates, pSol[ABC_EXACT_SOL_NVARS] + Abc_Lit2Var( *p ) ) );
+ p += ( 2 + pSol[ABC_EXACT_SOL_NVARS] );
+ }
+ Abc_NodeFreeNames( vNames );
+
+ Vec_PtrFree( pGates );
+
+ if ( !Abc_NtkCheck( pNtk ) )
+ printf( "Ses_ManExtractSolution(): Network check has failed.\n" );
+
+ return pNtk;
+}
+
+static Gia_Man_t * Ses_ManExtractGia( char const * pSol )
+{
+ int h, i;
+ char const * p;
+ Gia_Man_t * pGia;
+ Vec_Int_t * pGates;
+ Vec_Ptr_t * vNames;
+ int nObj, nChild1, nChild2, fChild1Comp, fChild2Comp;
+
+ pGia = Gia_ManStart( pSol[ABC_EXACT_SOL_NVARS] + pSol[ABC_EXACT_SOL_NGATES] + pSol[ABC_EXACT_SOL_NFUNC] + 1 );
+ pGia->nConstrs = 0;
+ pGia->pName = Extra_UtilStrsav( "exact" );
+
+ pGates = Vec_IntAlloc( pSol[ABC_EXACT_SOL_NVARS] + pSol[ABC_EXACT_SOL_NGATES] );
+ vNames = Abc_NodeGetFakeNames( pSol[ABC_EXACT_SOL_NVARS] + pSol[ABC_EXACT_SOL_NFUNC] );
+
+ /* primary inputs */
+ pGia->vNamesIn = Vec_PtrStart( pSol[ABC_EXACT_SOL_NVARS] );
+ for ( i = 0; i < pSol[ABC_EXACT_SOL_NVARS]; ++i )
+ {
+ nObj = Gia_ManAppendCi( pGia );
+ Vec_IntPush( pGates, nObj );
+ Vec_PtrSetEntry( pGia->vNamesIn, i, Extra_UtilStrsav( Vec_PtrEntry( vNames, i ) ) );
+ }
+
+ /* gates */
+ p = pSol + 3;
+ for ( i = 0; i < pSol[ABC_EXACT_SOL_NGATES]; ++i )
+ {
+ assert( p[1] == 2 );
+ nChild1 = Vec_IntEntry( pGates, p[2] );
+ nChild2 = Vec_IntEntry( pGates, p[3] );
+ fChild1Comp = fChild2Comp = 0;
+
+ if ( *p & 1 )
+ {
+ nChild1 = Abc_LitNot( nChild1 );
+ fChild1Comp = 1;
+ }
+ if ( ( *p >> 1 ) & 1 )
+ {
+ nChild2 = Abc_LitNot( nChild2 );
+ fChild2Comp = 1;
+ }
+ nObj = Gia_ManAppendAnd( pGia, nChild1, nChild2 );
+ if ( fChild1Comp && fChild2Comp )
+ {
+ assert( ( *p >> 2 ) & 1 );
+ nObj = Abc_LitNot( nObj );
+ }
+
+ Vec_IntPush( pGates, nObj );
+
+ p += 4;
+ }
+
+ /* outputs */
+ pGia->vNamesOut = Vec_PtrStart( pSol[ABC_EXACT_SOL_NFUNC] );
+ for ( h = 0; h < pSol[ABC_EXACT_SOL_NFUNC]; ++h )
+ {
+ nObj = Vec_IntEntry( pGates, pSol[ABC_EXACT_SOL_NVARS] + Abc_Lit2Var( *p ) );
+ if ( Abc_LitIsCompl( *p ) )
+ nObj = Abc_LitNot( nObj );
+ Gia_ManAppendCo( pGia, nObj );
+ Vec_PtrSetEntry( pGia->vNamesOut, h, Extra_UtilStrsav( Vec_PtrEntry( vNames, pSol[ABC_EXACT_SOL_NVARS] + h ) ) );
+ p += ( 2 + pSol[ABC_EXACT_SOL_NVARS] );
+ }
+ Abc_NodeFreeNames( vNames );
+
+ Vec_IntFree( pGates );
+
+ return pGia;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Debug.]
+
+***********************************************************************/
+static void Ses_ManPrintRuntime( Ses_Man_t * pSes )
+{
+ printf( "Runtime breakdown:\n" );
+ ABC_PRTP( "Sat ", pSes->timeSat, pSes->timeTotal );
+ ABC_PRTP( " Sat ", pSes->timeSatSat, pSes->timeTotal );
+ ABC_PRTP( " Unsat", pSes->timeSatUnsat, pSes->timeTotal );
+ ABC_PRTP( "ALL ", pSes->timeTotal, pSes->timeTotal );
+}
+
+static inline void Ses_ManPrintFuncs( Ses_Man_t * pSes )
+{
+ int h;
+
+ printf( "find optimum circuit for %d %d-variable functions:\n", pSes->nSpecFunc, pSes->nSpecVars );
+ for ( h = 0; h < pSes->nSpecFunc; ++h )
+ {
+ printf( " func %d: ", h + 1 );
+ Abc_TtPrintHexRev( stdout, &pSes->pSpec[h >> 2], pSes->nSpecVars );
+ printf( "\n" );
+ }
+}
+
+static inline void Ses_ManPrintVars( Ses_Man_t * pSes )
+{
+ int h, i, j, k, p, q, t;
+
+ for ( i = 0; i < pSes->nGates; ++i )
+ for ( t = 0; t < pSes->nRows; ++t )
+ printf( "x(%d, %d) : %d\n", i, t, Ses_ManSimVar( pSes, i, t ) );
+
+ for ( h = 0; h < pSes->nSpecFunc; ++h )
+ for ( i = 0; i < pSes->nGates; ++i )
+ printf( "h(%d, %d) : %d\n", h, i, Ses_ManOutputVar( pSes, h, i ) );
+
+ for ( i = 0; i < pSes->nGates; ++i )
+ for ( p = 0; p <= 1; ++p )
+ for ( q = 0; q <= 1; ++ q)
+ {
+ if ( p == 0 && q == 0 ) { continue; }
+ printf( "f(%d, %d, %d) : %d\n", i, p, q, Ses_ManGateVar( pSes, i, p, q ) );
+ }
+
+ for ( i = 0; i < pSes->nGates; ++i )
+ for ( j = 0; j < pSes->nSpecVars + i; ++j )
+ for ( k = j + 1; k < pSes->nSpecVars + i; ++k )
+ printf( "s(%d, %d, %d) : %d\n", i, j, k, Ses_ManSelectVar( pSes, i, j, k ) );
+
+ if ( pSes->nMaxDepth > 0 )
+ for ( i = 0; i < pSes->nGates; ++i )
+ for ( j = 0; j <= i; ++j )
+ printf( "d(%d, %d) : %d\n", i, j, Ses_ManDepthVar( pSes, i, j ) );
+
+}
+
+/**Function*************************************************************
+
+ Synopsis [Synthesis algorithm.]
+
+***********************************************************************/
+static int Ses_ManFindMinimumSize( Ses_Man_t * pSes )
+{
+ int nGates = 0;
+
+ while ( true )
+ {
+ ++nGates;
+
+ /* give up if number of gates is impossible for given depth */
+ if ( pSes->nMaxDepth != -1 && nGates >= ( 1 << pSes->nMaxDepth ) )
+ return 0;
+
+ Ses_ManCreateVars( pSes, nGates );
+ if ( !Ses_ManCreateClauses( pSes ) )
+ return 0; /* proven UNSAT while creating clauses */
+
+ switch ( Ses_ManSolve( pSes ) )
+ {
+ case 1: return 1; /* SAT */
+ case 2: return 0; /* resource limit */
+ }
+ }
+
+ return 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Find minimum size networks with a SAT solver.]
+
+ Description [If nMaxDepth is -1, then depth constraints are ignored.
+ If nMaxDepth is not -1, one can set pArrTimeProfile which should have the length of nVars.
+ One can ignore pArrTimeProfile by setting it to NULL.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkFindExact( word * pTruth, int nVars, int nFunc, int nMaxDepth, int * pArrTimeProfile, int fVerbose )
+{
+ Ses_Man_t * pSes;
+ char * pSol;
+ Abc_Ntk_t * pNtk = NULL;
+ abctime timeStart;
+
+ /* some checks */
+ assert( nVars >= 2 && nVars <= 8 );
+
+ timeStart = Abc_Clock();
+
+ pSes = Ses_ManAlloc( pTruth, nVars, nFunc, nMaxDepth, pArrTimeProfile, 0, fVerbose );
+ if ( fVerbose )
+ Ses_ManPrintFuncs( pSes );
+
+ if ( Ses_ManFindMinimumSize( pSes ) )
+ {
+ pSol = Ses_ManExtractSolution( pSes );
+ pNtk = Ses_ManExtractNtk( pSol );
+ ABC_FREE( pSol );
+ }
+
+ pSes->timeTotal = Abc_Clock() - timeStart;
+
+ if ( fVerbose )
+ Ses_ManPrintRuntime( pSes );
+
+ /* cleanup */
+ Ses_ManClean( pSes );
+
+ return pNtk;
+}
+
+Gia_Man_t * Gia_ManFindExact( word * pTruth, int nVars, int nFunc, int nMaxDepth, int * pArrTimeProfile, int fVerbose )
+{
+ Ses_Man_t * pSes;
+ char * pSol;
+ Gia_Man_t * pGia = NULL;
+ abctime timeStart;
+
+ /* some checks */
+ assert( nVars >= 2 && nVars <= 8 );
+
+ timeStart = Abc_Clock();
+
+ pSes = Ses_ManAlloc( pTruth, nVars, nFunc, nMaxDepth, pArrTimeProfile, 1, fVerbose );
+ if ( fVerbose )
+ Ses_ManPrintFuncs( pSes );
+
+ if ( Ses_ManFindMinimumSize( pSes ) )
+ {
+ pSol = Ses_ManExtractSolution( pSes );
+ pGia = Ses_ManExtractGia( pSol );
+ ABC_FREE( pSol );
+ }
+
+ pSes->timeTotal = Abc_Clock() - timeStart;
+
+ if ( fVerbose )
+ Ses_ManPrintRuntime( pSes );
+
+ /* cleanup */
+ Ses_ManClean( pSes );
+
+ return pGia;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Some test cases.]
+
+***********************************************************************/
+
+Abc_Ntk_t * Abc_NtkFromTruthTable( word * pTruth, int nVars )
+{
+ Abc_Ntk_t * pNtk;
+ Mem_Flex_t * pMan;
+ char * pSopCover;
+
+ pMan = Mem_FlexStart();
+ pSopCover = Abc_SopCreateFromTruth( pMan, nVars, (unsigned*)pTruth );
+ pNtk = Abc_NtkCreateWithNode( pSopCover );
+ Abc_NtkShortNames( pNtk );
+ Mem_FlexStop( pMan, 0 );
+
+ return pNtk;
+}
+
+void Abc_ExactTestSingleOutput( int fVerbose )
+{
+ extern void Abc_NtkCecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int nInsLimit );
+
+ word pTruth[4] = {0xcafe, 0, 0, 0};
+ Abc_Ntk_t * pNtk, * pNtk2, * pNtk3, * pNtk4;
+ int pArrTimeProfile[4] = {6, 2, 8, 5};
+
+ pNtk = Abc_NtkFromTruthTable( pTruth, 4 );
+
+ pNtk2 = Abc_NtkFindExact( pTruth, 4, 1, -1, NULL, fVerbose );
+ Abc_NtkShortNames( pNtk2 );
+ Abc_NtkCecSat( pNtk, pNtk2, 10000, 0 );
+ assert( pNtk2 );
+ assert( Abc_NtkNodeNum( pNtk2 ) == 6 );
+ Abc_NtkDelete( pNtk2 );
+
+ pNtk3 = Abc_NtkFindExact( pTruth, 4, 1, 3, NULL, fVerbose );
+ Abc_NtkShortNames( pNtk3 );
+ Abc_NtkCecSat( pNtk, pNtk3, 10000, 0 );
+ assert( pNtk3 );
+ assert( Abc_NtkLevel( pNtk3 ) <= 3 );
+ Abc_NtkDelete( pNtk3 );
+
+ pNtk4 = Abc_NtkFindExact( pTruth, 4, 1, 9, pArrTimeProfile, fVerbose );
+ Abc_NtkShortNames( pNtk4 );
+ Abc_NtkCecSat( pNtk, pNtk4, 10000, 0 );
+ assert( pNtk4 );
+ assert( Abc_NtkLevel( pNtk4 ) <= 9 );
+ Abc_NtkDelete( pNtk4 );
+
+ assert( !Abc_NtkFindExact( pTruth, 4, 1, 2, NULL, fVerbose ) );
+
+ assert( !Abc_NtkFindExact( pTruth, 4, 1, 8, pArrTimeProfile, fVerbose ) );
+
+ Abc_NtkDelete( pNtk );
+}
+
+void Abc_ExactTestSingleOutputAIG( int fVerbose )
+{
+ word pTruth[4] = {0xcafe, 0, 0, 0};
+ Abc_Ntk_t * pNtk;
+ Gia_Man_t * pGia, * pGia2, * pGia3, * pGia4, * pMiter;
+ Cec_ParCec_t ParsCec, * pPars = &ParsCec;
+ int pArrTimeProfile[4] = {6, 2, 8, 5};
+
+ Cec_ManCecSetDefaultParams( pPars );
+
+ pNtk = Abc_NtkFromTruthTable( pTruth, 4 );
+ Abc_NtkToAig( pNtk );
+ pGia = Abc_NtkAigToGia( pNtk, 1 );
+
+ pGia2 = Gia_ManFindExact( pTruth, 4, 1, -1, NULL, fVerbose );
+ pMiter = Gia_ManMiter( pGia, pGia2, 0, 1, 0, 0, 1 );
+ assert( pMiter );
+ Cec_ManVerify( pMiter, pPars );
+ Gia_ManStop( pMiter );
+
+ pGia3 = Gia_ManFindExact( pTruth, 4, 1, 3, NULL, fVerbose );
+ pMiter = Gia_ManMiter( pGia, pGia3, 0, 1, 0, 0, 1 );
+ assert( pMiter );
+ Cec_ManVerify( pMiter, pPars );
+ Gia_ManStop( pMiter );
+
+ pGia4 = Gia_ManFindExact( pTruth, 4, 1, 9, pArrTimeProfile, fVerbose );
+ pMiter = Gia_ManMiter( pGia, pGia4, 0, 1, 0, 0, 1 );
+ assert( pMiter );
+ Cec_ManVerify( pMiter, pPars );
+ Gia_ManStop( pMiter );
+
+ assert( !Gia_ManFindExact( pTruth, 4, 1, 2, NULL, fVerbose ) );
+
+ assert( !Gia_ManFindExact( pTruth, 4, 1, 8, pArrTimeProfile, fVerbose ) );
+
+ Gia_ManStop( pGia );
+ Gia_ManStop( pGia2 );
+ Gia_ManStop( pGia3 );
+ Gia_ManStop( pGia4 );
+}
+
+void Abc_ExactTest( int fVerbose )
+{
+ Abc_ExactTestSingleOutput( fVerbose );
+ Abc_ExactTestSingleOutputAIG( fVerbose );
+
+ printf( "\n" );
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [APIs for integraging with the mapper.]
+
+***********************************************************************/
+// may need to have a static pointer to the SAT-based synthesis engine and/or loaded library
+// this procedure should return 1, if the engine/library are available, and 0 otherwise
+int Abc_ExactIsRunning()
+{
+ return s_pSesStore != NULL;
+}
+// this procedure returns the number of inputs of the library
+// for example, somebody may try to map into 10-cuts while the library only contains 8-functions
+int Abc_ExactInputNum()
+{
+ return 8;
+}
+// start exact store manager
+void Abc_ExactStart( int nBTLimit, int fMakeAIG, int fVerbose, const char * pFilename )
+{
+ if ( !s_pSesStore )
+ {
+ s_pSesStore = Ses_StoreAlloc( nBTLimit, fMakeAIG, fVerbose );
+ if ( pFilename )
+ Ses_StoreRead( s_pSesStore, pFilename );
+ }
+ else
+ printf( "BMS manager already started\n" );
+}
+// stop exact store manager
+void Abc_ExactStop( const char * pFilename )
+{
+ if ( s_pSesStore )
+ {
+ if ( pFilename )
+ Ses_StoreWrite( s_pSesStore, pFilename );
+ Ses_StoreClean( s_pSesStore );
+ }
+ else
+ printf( "BMS manager has not been started\n" );
+}
+// show statistics about store manager
+void Abc_ExactStats()
+{
+ int i;
+
+ if ( !s_pSesStore )
+ {
+ printf( "BMS manager has not been started\n" );
+ return;
+ }
+
+ printf( "number of considered cuts :" );
+ for ( i = 2; i < 9; ++i )
+ printf( " %d = %lu ", i, s_pSesStore->pCutCount[i] );
+ printf( " total = %lu\n", s_pSesStore->nCutCount );
+ printf( "cache hits : %lu\n", s_pSesStore->nCacheHit );
+ printf( "number of entries : %d\n", s_pSesStore->nEntriesCount );
+}
+// this procedure takes TT and input arrival times (pArrTimeProfile) and return the smallest output arrival time;
+// it also returns the pin-to-pin delays (pPerm) between each cut leaf and the cut output and the cut area cost (Cost)
+// the area cost should not exceed 2048, if the cut is implementable; otherwise, it should be ABC_INFINITY
+int Abc_ExactDelayCost( word * pTruth, int nVars, int * pArrTimeProfile, char * pPerm, int * Cost, int AigLevel )
+{
+ int i, l, fExists = 0;
+ Ses_Man_t * pSes = NULL;
+ char * pSol = NULL, * p;
+ int Delay = ABC_INFINITY, nMaxDepth;
+ abctime timeStart;
+
+ /* some checks */
+ if ( nVars < 0 || nVars > 8 )
+ {
+ printf( "invalid truth table size %d\n", nVars );
+ assert( 0 );
+ }
+
+ if ( nVars == 0 )
+ {
+ *Cost = 0;
+ return 0;
+ }
+
+ if ( nVars == 1 )
+ {
+ *Cost = 0;
+ pPerm[0] = (char)0;
+ return pArrTimeProfile[0];
+ }
+
+ /* statistics */
+ s_pSesStore->nCutCount++;
+ s_pSesStore->pCutCount[nVars]++;
+
+ pSol = Ses_StoreGetEntry( s_pSesStore, pTruth, nVars, pArrTimeProfile );
+ if ( pSol )
+ {
+ s_pSesStore->nCacheHit++;
+ fExists = 1;
+ }
+ else
+ {
+ nMaxDepth = pArrTimeProfile[0];
+ for ( i = 1; i < nVars; ++i )
+ nMaxDepth = Abc_MaxInt( nMaxDepth, pArrTimeProfile[i] );
+ nMaxDepth = Abc_MinInt( AigLevel, nMaxDepth + nVars + 1 );
+
+ timeStart = Abc_Clock();
+
+ *Cost = ABC_INFINITY;
+
+ pSes = Ses_ManAlloc( pTruth, nVars, 1 /* fSpecFunc */, nMaxDepth, pArrTimeProfile, s_pSesStore->fMakeAIG, s_pSesStore->fVerbose );
+ pSes->nBTLimit = s_pSesStore->nBTLimit;
+
+ while ( 1 ) /* there is improvement */
+ {
+ if ( Ses_ManFindMinimumSize( pSes ) )
+ {
+ if ( pSol )
+ ABC_FREE( pSol );
+ pSol = Ses_ManExtractSolution( pSes );
+ pSes->nMaxDepth--;
+ }
+ else
+ break;
+ }
+
+ pSes->timeTotal = Abc_Clock() - timeStart;
+
+ /* cleanup */
+ Ses_ManClean( pSes );
+ }
+
+ if ( pSol )
+ {
+ *Cost = pSol[ABC_EXACT_SOL_NGATES];
+ p = pSol + 3 + 4 * pSol[ABC_EXACT_SOL_NGATES] + 1;
+ Delay = *p++;
+ for ( l = 0; l < nVars; ++l )
+ pPerm[l] = *p++;
+
+ /* store solution */
+ if ( !fExists )
+ Ses_StoreAddEntry( s_pSesStore, pTruth, nVars, pArrTimeProfile, pSol );
+ }
+
+ return Delay;
+}
+// this procedure returns a new node whose output in terms of the given fanins
+// has the smallest possible arrival time (in agreement with the above Abc_ExactDelayCost)
+Abc_Obj_t * Abc_ExactBuildNode( word * pTruth, int nVars, int * pArrTimeProfile, Abc_Obj_t ** pFanins, Abc_Ntk_t * pNtk )
+{
+ char * pSol;
+ int i, j;
+ char const * p;
+ Abc_Obj_t * pObj;
+ Vec_Ptr_t * pGates;
+ char pGateTruth[5];
+ char * pSopCover;
+
+ if ( nVars == 0 )
+ return (pTruth[0] & 1) ? Abc_NtkCreateNodeConst1(pNtk) : Abc_NtkCreateNodeConst0(pNtk);
+ if ( nVars == 1 )
+ return (pTruth[0] & 1) ? Abc_NtkCreateNodeInv(pNtk, pFanins[0]) : Abc_NtkCreateNodeBuf(pNtk, pFanins[0]);
+
+ pSol = Ses_StoreGetEntry( s_pSesStore, pTruth, nVars, pArrTimeProfile );
+ if ( !pSol )
+ return NULL;
+
+ assert( pSol[ABC_EXACT_SOL_NVARS] == nVars );
+ assert( pSol[ABC_EXACT_SOL_NFUNC] == 1 );
+
+ pGates = Vec_PtrAlloc( nVars + pSol[ABC_EXACT_SOL_NGATES] );
+ pGateTruth[3] = '0';
+ pGateTruth[4] = '\0';
+
+ /* primary inputs */
+ for ( i = 0; i < nVars; ++i )
+ {
+ Vec_PtrPush( pGates, pFanins[i] );
+ }
+
+ /* gates */
+ p = pSol + 3;
+ for ( i = 0; i < pSol[ABC_EXACT_SOL_NGATES]; ++i )
+ {
+ pGateTruth[2] = '0' + ( *p & 1 );
+ pGateTruth[1] = '0' + ( ( *p >> 1 ) & 1 );
+ pGateTruth[0] = '0' + ( ( *p >> 2 ) & 1 );
+ ++p;
+
+ assert( *p == 2 ); /* binary gate */
+ ++p;
+
+ /* invert truth table if we are last gate and inverted */
+ if ( i + 1 == pSol[ABC_EXACT_SOL_NGATES] && Abc_LitIsCompl( *( p + 2 ) ) )
+ for ( j = 0; j < 4; ++j )
+ pGateTruth[j] = ( pGateTruth[j] == '0' ) ? '1' : '0';
+
+ pSopCover = Abc_SopFromTruthBin( pGateTruth );
+ pObj = Abc_NtkCreateNode( pNtk );
+ pObj->pData = Abc_SopRegister( (Mem_Flex_t*)pNtk->pManFunc, pSopCover );
+ Vec_PtrPush( pGates, pObj );
+ ABC_FREE( pSopCover );
+
+ Abc_ObjAddFanin( pObj, (Abc_Obj_t *)Vec_PtrEntry( pGates, *p++ ) );
+ Abc_ObjAddFanin( pObj, (Abc_Obj_t *)Vec_PtrEntry( pGates, *p++ ) );
+ }
+
+ /* output */
+ pObj = (Abc_Obj_t *)Vec_PtrEntry( pGates, nVars + Abc_Lit2Var( *p ) );
+
+ Vec_PtrFree( pGates );
+
+ return pObj;
+}
+
+void Abc_ExactStoreTest( int fVerbose )
+{
+ int i;
+ word pTruth[4] = {0xcafe, 0, 0, 0};
+ int pArrTimeProfile[4] = {6, 2, 8, 5};
+ Abc_Ntk_t * pNtk;
+ Abc_Obj_t * pFanins[4];
+ Vec_Ptr_t * vNames;
+ char pPerm[4];
+ int Cost;
+
+ pNtk = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_SOP, 1 );
+ pNtk->pName = Extra_UtilStrsav( "exact" );
+ vNames = Abc_NodeGetFakeNames( 4u );
+
+ /* primary inputs */
+ Vec_PtrPush( pNtk->vObjs, NULL );
+ for ( i = 0; i < 4; ++i )
+ {
+ pFanins[i] = Abc_NtkCreatePi( pNtk );
+ Abc_ObjAssignName( pFanins[i], (char*)Vec_PtrEntry( vNames, i ), NULL );
+ }
+ Abc_NodeFreeNames( vNames );
+
+ Abc_ExactStart( 10000, 1, fVerbose, NULL );
+
+ assert( !Abc_ExactBuildNode( pTruth, 4, pArrTimeProfile, pFanins, pNtk ) );
+
+ assert( Abc_ExactDelayCost( pTruth, 4, pArrTimeProfile, pPerm, &Cost, 12 ) == 1 );
+
+ assert( Abc_ExactBuildNode( pTruth, 4, pArrTimeProfile, pFanins, pNtk ) );
+
+ (*pArrTimeProfile)++;
+ assert( !Abc_ExactBuildNode( pTruth, 4, pArrTimeProfile, pFanins, pNtk ) );
+ (*pArrTimeProfile)--;
+
+ Abc_ExactStop( NULL );
+
+ Abc_NtkDelete( pNtk );
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
diff --git a/src/base/abci/abcFx.c b/src/base/abci/abcFx.c
index 60f2e562..81b3e802 100644
--- a/src/base/abci/abcFx.c
+++ b/src/base/abci/abcFx.c
@@ -8,9 +8,9 @@
Synopsis [Implementation of traditional "fast_extract" algorithm.]
- Author [Alan Mishchenko]
+ Author [Alan Mishchenko, Bruno Schmitt]
- Affiliation [UC Berkeley]
+ Affiliation [UC Berkeley, UFRGS]
Date [Ver. 1.0. Started - April 26, 2013.]
@@ -103,6 +103,7 @@ struct Fx_Man_t_
Vec_Int_t * vCompls; // complemented attribute of each cube pair
Vec_Int_t * vCubeFree; // cube-free divisor
Vec_Int_t * vDiv; // selected divisor
+ Vec_Int_t * vSCC; // single cubes containment cubes
// statistics
abctime timeStart; // starting time
int nVars; // original problem variables
@@ -312,11 +313,6 @@ int Abc_NtkFxPerform( Abc_Ntk_t * pNtk, int nNewNodesMax, int LitCountMax, int f
printf( "Abc_NtkFastExtract: Nodes have duplicated fanins. FX is not performed.\n" );
return 0;
}
- // sweep removes useless nodes
- Abc_NtkCleanup( pNtk, 0 );
-// Abc_NtkOrderFanins( pNtk );
- // makes sure the SOPs are SCC-free and D1C-free
- Abc_NtkMakeLegit( pNtk );
// collect information about the covers
vCubes = Abc_NtkFxRetrieve( pNtk );
// call the fast extract procedure
@@ -359,6 +355,7 @@ Fx_Man_t * Fx_ManStart( Vec_Wec_t * vCubes )
p->vCompls = Vec_IntAlloc( 100 );
p->vCubeFree = Vec_IntAlloc( 100 );
p->vDiv = Vec_IntAlloc( 100 );
+ p->vSCC = Vec_IntAlloc( 100 );
return p;
}
void Fx_ManStop( Fx_Man_t * p )
@@ -377,6 +374,7 @@ void Fx_ManStop( Fx_Man_t * p )
Vec_IntFree( p->vCompls );
Vec_IntFree( p->vCubeFree );
Vec_IntFree( p->vDiv );
+ Vec_IntFree( p->vSCC );
ABC_FREE( p );
}
@@ -435,39 +433,16 @@ void Fx_ManComputeLevel( Fx_Man_t * p )
SeeAlso []
***********************************************************************/
-static inline char Fx_PrintDivLit( int Lit ) { return (Abc_LitIsCompl(Lit) ? 'A' : 'a') + Abc_Lit2Var(Lit); }
-static inline void Fx_PrintDivOneReal( Vec_Int_t * vDiv )
-{
- int i, Lit;
- Vec_IntForEachEntry( vDiv, Lit, i )
- if ( !Abc_LitIsCompl(Lit) )
- printf( "%c", Fx_PrintDivLit(Abc_Lit2Var(Lit)) );
- printf( " + " );
- Vec_IntForEachEntry( vDiv, Lit, i )
- if ( Abc_LitIsCompl(Lit) )
- printf( "%c", Fx_PrintDivLit(Abc_Lit2Var(Lit)) );
-}
-static inline void Fx_PrintDivOne( Vec_Int_t * vDiv )
-{
- int i, Lit;
- Vec_IntForEachEntry( vDiv, Lit, i )
- if ( !Abc_LitIsCompl(Lit) )
- printf( "%c", Fx_PrintDivLit( Abc_Var2Lit(i, Abc_LitIsCompl(Lit)) ) );
- printf( " + " );
- Vec_IntForEachEntry( vDiv, Lit, i )
- if ( Abc_LitIsCompl(Lit) )
- printf( "%c", Fx_PrintDivLit( Abc_Var2Lit(i, Abc_LitIsCompl(Lit)) ) );
-}
static inline void Fx_PrintDivArray( Vec_Int_t * vDiv )
{
int i, Lit;
Vec_IntForEachEntry( vDiv, Lit, i )
if ( !Abc_LitIsCompl(Lit) )
- printf( "%d(1) ", Abc_Lit2Var(Lit) );
+ printf( "%d(1)", Abc_Lit2Var(Lit) );
printf( " + " );
Vec_IntForEachEntry( vDiv, Lit, i )
if ( Abc_LitIsCompl(Lit) )
- printf( "%d(2) ", Abc_Lit2Var(Lit) );
+ printf( "%d(2)", Abc_Lit2Var(Lit) );
}
static inline void Fx_PrintDiv( Fx_Man_t * p, int iDiv )
{
@@ -475,8 +450,7 @@ static inline void Fx_PrintDiv( Fx_Man_t * p, int iDiv )
printf( "%4d : ", p->nDivs );
printf( "Div %7d : ", iDiv );
printf( "Weight %12.5f ", Vec_FltEntry(p->vWeights, iDiv) );
-// printf( "Compl %4d ", p->nCompls );
- Fx_PrintDivOne( Hsh_VecReadEntry(p->pHash, iDiv) );
+ Fx_PrintDivArray( Hsh_VecReadEntry(p->pHash, iDiv) );
for ( i = Vec_IntSize(Hsh_VecReadEntry(p->pHash, iDiv)) + 3; i < 16; i++ )
printf( " " );
printf( "Lits =%7d ", p->nLits );
@@ -489,45 +463,6 @@ static void Fx_PrintDivisors( Fx_Man_t * p )
for ( iDiv = 0; iDiv < Vec_FltSize(p->vWeights); iDiv++ )
Fx_PrintDiv( p, iDiv );
}
-static void Fx_PrintLiterals( Fx_Man_t * p )
-{
- Vec_Int_t * vTemp;
- int i;
- Vec_WecForEachLevel( p->vLits, vTemp, i )
- {
- printf( "%c : ", Fx_PrintDivLit(i) );
- Vec_IntPrint( vTemp );
- }
-}
-static void Fx_PrintMatrix( Fx_Man_t * p )
-{
- Vec_Int_t * vCube;
- int i, v, Lit, nObjs;
- char * pLine;
- if ( Vec_WecSize(p->vLits)/2 > 26 )
- return;
- printf( " " );
- nObjs = Vec_WecSize(p->vLits)/2;
- for ( i = 0; i < Abc_MinInt(nObjs, 26); i++ )
- printf( "%c", 'a' + i );
- printf( "\n" );
- pLine = ABC_CALLOC( char, nObjs+1 );
- Vec_WecForEachLevel( p->vCubes, vCube, i )
- {
- if ( Vec_IntSize(vCube) == 0 )
- continue;
- memset( pLine, '-', nObjs );
- Vec_IntForEachEntryStart( vCube, Lit, v, 1 )
- {
- assert( Abc_Lit2Var(Lit) < nObjs );
- pLine[Abc_Lit2Var(Lit)] = Abc_LitIsCompl(Lit) ? '0' : '1';
- }
- printf( "%6d : %s %4d\n", i, pLine, Vec_IntEntry(vCube, 0) );
- }
- ABC_FREE( pLine );
- Fx_PrintLiterals( p );
- Fx_PrintDivisors( p );
-}
static void Fx_PrintStats( Fx_Man_t * p, abctime clk )
{
printf( "Cubes =%8d ", Vec_WecSizeUsed(p->vCubes) );
@@ -536,11 +471,7 @@ static void Fx_PrintStats( Fx_Man_t * p, abctime clk )
printf( "Divs+ =%8d ", Vec_QueSize(p->vPrio) );
printf( "Compl =%8d ", p->nDivMux[1] );
printf( "Extr =%7d ", p->nDivs );
-// printf( "DivsS =%6d ", p->nDivsS );
-// printf( "PairS =%6d ", p->nPairsS );
-// printf( "PairD =%6d ", p->nPairsD );
Abc_PrintTime( 1, "Time", clk );
-// printf( "\n" );
}
/**Function*************************************************************
@@ -638,10 +569,10 @@ static int Fx_ManDivNormalize( Vec_Int_t * vCubeFree ) // return 1 if complement
***********************************************************************/
int Fx_ManDivFindCubeFree( Vec_Int_t * vArr1, Vec_Int_t * vArr2, Vec_Int_t * vCubeFree, int * fWarning )
{
- int * pBeg1 = vArr1->pArray + 1; // skip variable ID
- int * pBeg2 = vArr2->pArray + 1; // skip variable ID
- int * pEnd1 = vArr1->pArray + vArr1->nSize;
- int * pEnd2 = vArr2->pArray + vArr2->nSize;
+ int * pBeg1 = Vec_IntArray( vArr1 ) + 1; // skip variable ID
+ int * pBeg2 = Vec_IntArray( vArr2 ) + 1; // skip variable ID
+ int * pEnd1 = Vec_IntLimit( vArr1 );
+ int * pEnd2 = Vec_IntLimit( vArr2 );
int Counter = 0, fAttr0 = 0, fAttr1 = 1;
Vec_IntClear( vCubeFree );
while ( pBeg1 < pEnd1 && pBeg2 < pEnd2 )
@@ -664,9 +595,38 @@ int Fx_ManDivFindCubeFree( Vec_Int_t * vArr1, Vec_Int_t * vArr2, Vec_Int_t * vCu
if ( Vec_IntSize(vCubeFree) == 0 )
printf( "The SOP has duplicated cubes.\n" );
else if ( Vec_IntSize(vCubeFree) == 1 )
- printf( "The SOP has contained cubes.\n" );
-// else if ( Vec_IntSize(vCubeFree) == 2 && Abc_Lit2Var(Abc_Lit2Var(Vec_IntEntry(vCubeFree, 0))) == Abc_Lit2Var(Abc_Lit2Var(Vec_IntEntry(vCubeFree, 1))) && !*fWarning )
-// printf( "The SOP has distance-1 cubes or it is not a prime cover. Please make sure the result verifies.\n" ), *fWarning = 1;
+ return -1;
+ else if ( Vec_IntSize( vCubeFree ) == 3 )
+ {
+ int * pArray = Vec_IntArray( vCubeFree );
+
+ if ( Abc_Lit2Var( pArray[0] ) == Abc_LitNot( Abc_Lit2Var( pArray[1] ) ) )
+ {
+ if ( Abc_LitIsCompl( pArray[0] ) == Abc_LitIsCompl( pArray[2] ) )
+ Vec_IntDrop( vCubeFree, 0 );
+ else
+ Vec_IntDrop( vCubeFree, 1 );
+ }
+ else if ( Abc_Lit2Var( pArray[1] ) == Abc_LitNot( Abc_Lit2Var( pArray[2] ) ) )
+ {
+ if ( Abc_LitIsCompl( pArray[1] ) == Abc_LitIsCompl( pArray[0] ) )
+ Vec_IntDrop( vCubeFree, 1 );
+ else
+ Vec_IntDrop( vCubeFree, 2 );
+ }
+
+ if ( Vec_IntSize( vCubeFree ) == 2 )
+ {
+ int Lit0 = Abc_Lit2Var( pArray[0] ),
+ Lit1 = Abc_Lit2Var( pArray[1] );
+
+ if ( Lit0 > Lit1 )
+ ABC_SWAP( int, Lit0, Lit1 );
+
+ Vec_IntWriteEntry( vCubeFree, 0, Abc_Var2Lit( Lit0, 0 ) );
+ Vec_IntWriteEntry( vCubeFree, 1, Abc_Var2Lit( Lit1, 1 ) );
+ }
+ }
assert( !Abc_LitIsCompl(Vec_IntEntry(vCubeFree, 0)) );
return Counter;
}
@@ -708,7 +668,11 @@ static inline int Fx_ManDivRemoveLits( Vec_Int_t * vCube, Vec_Int_t * vDiv, int
int i, Lit, Count = 0;
assert( !fCompl || Vec_IntSize(vDiv) == 4 );
Vec_IntForEachEntry( vDiv, Lit, i )
+ {
Count += Vec_IntRemove1( vCube, Abc_Lit2Var(Lit) ^ (fCompl && i > 1) ); // the last two lits can be complemented
+ if ( Vec_IntSize( vDiv ) == 2 )
+ Count += Vec_IntRemove1( vCube, Abc_LitNot( Abc_Lit2Var(Lit) ) );
+ }
return Count;
}
static inline void Fx_ManDivAddLits( Vec_Int_t * vCube, Vec_Int_t * vCube2, Vec_Int_t * vDiv )
@@ -833,6 +797,17 @@ void Fx_ManCubeDoubleCubeDivisors( Fx_Man_t * p, int iFirst, Vec_Int_t * vPivot,
if ( Vec_IntEntry(vCube, 0) != Vec_IntEntry(vPivot, 0) )
break;
Base = Fx_ManDivFindCubeFree( vCube, vPivot, p->vCubeFree, fWarning );
+ if ( Base == -1 )
+ {
+ if ( fRemove == 0 )
+ {
+ if ( Vec_IntSize( vCube ) > Vec_IntSize( vPivot ) )
+ Vec_IntPush( p->vSCC, Vec_WecLevelId( p->vCubes, vCube ) );
+ else
+ Vec_IntPush( p->vSCC, Vec_WecLevelId( p->vCubes, vPivot ) );
+ }
+ continue;
+ }
if ( Vec_IntSize(p->vCubeFree) == 4 )
{
int Value = Fx_ManDivNormalize( p->vCubeFree );
@@ -988,10 +963,9 @@ void Fx_ManFindCommonPairs( Vec_Wec_t * vCubes, Vec_Int_t * vPart0, Vec_Int_t *
***********************************************************************/
void Fx_ManUpdate( Fx_Man_t * p, int iDiv, int * fWarning )
{
- Vec_Int_t * vCube, * vCube2, * vLitP, * vLitN;
+ Vec_Int_t * vCube, * vCube2, * vLitP = NULL, * vLitN = NULL;
Vec_Int_t * vDiv = p->vDiv;
- int nLitsNew = p->nLits - (int)Vec_FltEntry(p->vWeights, iDiv);
- int i, k, Lit0, Lit1, iVarNew, RetValue, Level;
+ int i, k, Lit0, Lit1, iVarNew = 0, RetValue, Level;
float Diff = Vec_FltEntry(p->vWeights, iDiv) - (float)((int)Vec_FltEntry(p->vWeights, iDiv));
assert( Diff > 0.0 && Diff < 1.0 );
@@ -1002,10 +976,6 @@ void Fx_ManUpdate( Fx_Man_t * p, int iDiv, int * fWarning )
Fx_ManDivFindPivots( vDiv, &Lit0, &Lit1 );
assert( Lit0 >= 0 && Lit1 >= 0 );
- // if the input cover is not prime, it may happen that we are extracting divisor (x + !x)
- // although it is not strictly correct, it seems to be fine to just skip such divisors
- if ( Abc_Lit2Var(Lit0) == Abc_Lit2Var(Lit1) && Vec_IntSize(Hsh_VecReadEntry(p->pHash, iDiv)) == 2 )
- return;
// collect single-cube-divisor cubes
Vec_IntClear( p->vCubesS );
@@ -1041,6 +1011,9 @@ void Fx_ManUpdate( Fx_Man_t * p, int iDiv, int * fWarning )
Vec_WecUnmarkLevels( p->vCubes, p->vCubesS );
Vec_WecUnmarkLevels( p->vCubes, p->vCubesD );
+ if ( Abc_Lit2Var(Lit0) == Abc_Lit2Var(Lit1) && Vec_IntSize(Hsh_VecReadEntry(p->pHash, iDiv)) == 2 )
+ goto ExtractFromPairs;
+
// create new divisor
iVarNew = Vec_WecSize( p->vLits ) / 2;
assert( Vec_IntSize(p->vVarCube) == iVarNew );
@@ -1080,6 +1053,7 @@ void Fx_ManUpdate( Fx_Man_t * p, int iDiv, int * fWarning )
p->nLits--;
}
// create updated double-cube divisor cube pairs
+ExtractFromPairs:
k = 0;
p->nCompls = 0;
assert( Vec_IntSize(p->vCubesD) % 2 == 0 );
@@ -1092,18 +1066,22 @@ void Fx_ManUpdate( Fx_Man_t * p, int iDiv, int * fWarning )
vCube2 = Vec_WecEntry( p->vCubes, Vec_IntEntry(p->vCubesD, i+1) );
RetValue = Fx_ManDivRemoveLits( vCube, vDiv, fCompl ); // cube 2*i
RetValue += Fx_ManDivRemoveLits( vCube2, vDiv, fCompl ); // cube 2*i+1
- assert( RetValue == Vec_IntSize(vDiv) );
- if ( Vec_IntSize(vDiv) == 2 || fCompl )
+ assert( RetValue == Vec_IntSize(vDiv) || RetValue == Vec_IntSize( vDiv ) + 1);
+ if ( iVarNew > 0 )
{
- Vec_IntPush( vCube, Abc_Var2Lit(iVarNew, 1) );
- Vec_IntPush( vLitN, Vec_WecLevelId(p->vCubes, vCube) ); // MAKE SURE vCube IS SORTED BY ID
- }
- else
- {
- Vec_IntPush( vCube, Abc_Var2Lit(iVarNew, 0) );
- Vec_IntPush( vLitP, Vec_WecLevelId(p->vCubes, vCube) ); // MAKE SURE vCube IS SORTED BY ID
+ if ( Vec_IntSize(vDiv) == 2 || fCompl )
+ {
+ Vec_IntPush( vCube, Abc_Var2Lit(iVarNew, 1) );
+ Vec_IntPush( vLitN, Vec_WecLevelId(p->vCubes, vCube) ); // MAKE SURE vCube IS SORTED BY ID
+ }
+ else
+ {
+ Vec_IntPush( vCube, Abc_Var2Lit(iVarNew, 0) );
+ Vec_IntPush( vLitP, Vec_WecLevelId(p->vCubes, vCube) ); // MAKE SURE vCube IS SORTED BY ID
+ }
}
p->nLits -= Vec_IntSize(vDiv) + Vec_IntSize(vCube2) - 2;
+
// remove second cube
Vec_IntWriteEntry( p->vCubesD, k++, Vec_WecLevelId(p->vCubes, vCube) );
Vec_IntClear( vCube2 );
@@ -1134,6 +1112,17 @@ void Fx_ManUpdate( Fx_Man_t * p, int iDiv, int * fWarning )
Vec_WecUnmarkLevels( p->vCubes, p->vCubesS );
Vec_WecUnmarkLevels( p->vCubes, p->vCubesD );
+ // Deal with SCC
+ if ( Vec_IntSize( p->vSCC ) )
+ {
+ Vec_IntUniqify( p->vSCC );
+ Fx_ManForEachCubeVec( p->vSCC, p->vCubes, vCube, i )
+ {
+ Fx_ManCubeDoubleCubeDivisors( p, Fx_ManGetFirstVarCube(p, vCube), vCube, 1, 1, fWarning ); // remove - update
+ Vec_IntClear( vCube );
+ }
+ Vec_IntClear( p->vSCC );
+ }
// add cost of the new divisor
if ( Vec_IntSize(vDiv) > 2 )
{
@@ -1151,12 +1140,10 @@ void Fx_ManUpdate( Fx_Man_t * p, int iDiv, int * fWarning )
Vec_IntForEachEntry( vDiv, Lit0, i )
{
Vec_IntTwoRemove( Vec_WecEntry(p->vLits, Abc_Lit2Var(Lit0)), p->vCubesD );
- if ( p->nCompls && i > 1 ) // the last two lits are possibly complemented
+ if ( (p->nCompls && i > 1) || Vec_IntSize( vDiv ) == 2 ) // the last two lits are possibly complemented
Vec_IntTwoRemove( Vec_WecEntry(p->vLits, Abc_LitNot(Abc_Lit2Var(Lit0))), p->vCubesD );
}
-
- // check predicted improvement: (new SOP lits == old SOP lits - divisor weight)
- assert( p->nLits == nLitsNew );
+
}
/**Function*************************************************************
@@ -1186,7 +1173,7 @@ int Fx_FastExtract( Vec_Wec_t * vCubes, int ObjIdMax, int nNewNodesMax, int LitC
Fx_ManComputeLevel( p );
Fx_ManCreateDivisors( p );
if ( fVeryVerbose )
- Fx_PrintMatrix( p );
+ Fx_PrintDivisors( p );
if ( fVerbose )
Fx_PrintStats( p, Abc_Clock() - clk );
// perform extraction
@@ -1198,7 +1185,7 @@ int Fx_FastExtract( Vec_Wec_t * vCubes, int ObjIdMax, int nNewNodesMax, int LitC
Fx_PrintDiv( p, iDiv );
Fx_ManUpdate( p, iDiv, &fWarning );
if ( fVeryVeryVerbose )
- Fx_PrintMatrix( p );
+ Fx_PrintDivisors( p );
}
if ( fVerbose )
Fx_PrintStats( p, Abc_Clock() - clk );
diff --git a/src/base/abci/abcIf.c b/src/base/abci/abcIf.c
index c45eaec5..08e2a560 100644
--- a/src/base/abci/abcIf.c
+++ b/src/base/abci/abcIf.c
@@ -116,7 +116,7 @@ Abc_Ntk_t * Abc_NtkIf( Abc_Ntk_t * pNtk, If_Par_t * pPars )
pPars->pTimesReq = Abc_NtkGetCoRequiredFloats(pNtk);
// update timing info to reflect logic level
- if ( (pPars->fDelayOpt || pPars->fDsdBalance || pPars->fUserRecLib) && pNtk->pManTime )
+ if ( (pPars->fDelayOpt || pPars->fDsdBalance || pPars->fUserRecLib || pPars->fUserSesLib) && pNtk->pManTime )
{
int c;
if ( pNtk->AndGateDelay == 0.0 )
@@ -318,7 +318,7 @@ Abc_Ntk_t * Abc_NtkFromIf( If_Man_t * pIfMan, Abc_Ntk_t * pNtk )
// create the new network
if ( pIfMan->pPars->fUseBdds || pIfMan->pPars->fUseCnfs || pIfMan->pPars->fUseMv )
pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_BDD );
- else if ( pIfMan->pPars->fUseSops || pIfMan->pPars->nGateSize > 0 )
+ else if ( pIfMan->pPars->fUseSops || pIfMan->pPars->fUserSesLib || pIfMan->pPars->nGateSize > 0 )
pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_SOP );
else
pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_AIG );
@@ -445,12 +445,22 @@ Abc_Obj_t * Abc_NodeFromIf_rec( Abc_Ntk_t * pNtkNew, If_Man_t * pIfMan, If_Obj_t
return pNodeNew;
assert( pIfObj->Type == IF_AND );
// get the parameters of the best cut
+ pCutBest = If_ObjCutBest( pIfObj );
+ if ( pIfMan->pPars->fUserSesLib )
+ {
+ // create the subgraph composed of Abc_Obj_t nodes based on the given cut
+ Abc_Obj_t * pFanins[IF_MAX_FUNC_LUTSIZE];
+ If_CutForEachLeaf( pIfMan, pCutBest, pIfLeaf, i )
+ pFanins[i] = Abc_NodeFromIf_rec(pNtkNew, pIfMan, pIfLeaf, vCover);
+ pNodeNew = Abc_ExactBuildNode( If_CutTruthW(pIfMan, pCutBest), If_CutLeaveNum(pCutBest), If_CutArrTimeProfile(pIfMan, pCutBest), pFanins, pNtkNew );
+ If_ObjSetCopy( pIfObj, pNodeNew );
+ return pNodeNew;
+ }
// create a new node
pNodeNew = Abc_NtkCreateNode( pNtkNew );
- pCutBest = If_ObjCutBest( pIfObj );
-// printf( "%d 0x%02X %d\n", pCutBest->nLeaves, 0xff & *If_CutTruth(pCutBest), pIfMan->pPars->pFuncCost(pCutBest) );
// if ( pIfMan->pPars->pLutLib && pIfMan->pPars->pLutLib->fVarPinDelays )
- if ( !pIfMan->pPars->fDelayOpt && !pIfMan->pPars->fDelayOptLut && !pIfMan->pPars->fDsdBalance && !pIfMan->pPars->fUseTtPerm && !pIfMan->pPars->pLutStruct && !pIfMan->pPars->fUserRecLib && !pIfMan->pPars->nGateSize )
+ if ( !pIfMan->pPars->fDelayOpt && !pIfMan->pPars->fDelayOptLut && !pIfMan->pPars->fDsdBalance && !pIfMan->pPars->fUseTtPerm &&
+ !pIfMan->pPars->pLutStruct && !pIfMan->pPars->fUserRecLib && !pIfMan->pPars->fUserSesLib && !pIfMan->pPars->nGateSize )
If_CutRotatePins( pIfMan, pCutBest );
if ( pIfMan->pPars->fUseCnfs || pIfMan->pPars->fUseMv )
{
diff --git a/src/base/abci/abcMini.c b/src/base/abci/abcMini.c
index bd893b5b..876f4c8c 100644
--- a/src/base/abci/abcMini.c
+++ b/src/base/abci/abcMini.c
@@ -205,7 +205,7 @@ void Abc_NtkMiniAigTest( Abc_Ntk_t * pNtk )
p = Abc_NtkToMiniAig( pNtk );
pNtkNew = Abc_NtkFromMiniAig( p );
Mini_AigStop( p );
- Abc_NtkPrintStats( pNtkNew, 0, 0, 0, 0, 0, 0, 0, 0, 0 );
+ Abc_NtkPrintStats( pNtkNew, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0 );
Abc_NtkDelete( pNtkNew );
// test dumping
diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c
index 40ce38b4..2129782f 100644
--- a/src/base/abci/abcPrint.c
+++ b/src/base/abci/abcPrint.c
@@ -235,7 +235,7 @@ float Abc_NtkGetArea( Abc_Ntk_t * pNtk )
SeeAlso []
***********************************************************************/
-void Abc_NtkPrintStats( Abc_Ntk_t * pNtk, int fFactored, int fSaveBest, int fDumpResult, int fUseLutLib, int fPrintMuxes, int fPower, int fGlitch, int fSkipBuf, int fPrintMem )
+void Abc_NtkPrintStats( Abc_Ntk_t * pNtk, int fFactored, int fSaveBest, int fDumpResult, int fUseLutLib, int fPrintMuxes, int fPower, int fGlitch, int fSkipBuf, int fSkipSmall, int fPrintMem )
{
int nSingles = fSkipBuf ? Abc_NtkGetBufNum(pNtk) : 0;
if ( fPrintMuxes && Abc_NtkIsStrash(pNtk) )
@@ -283,7 +283,7 @@ void Abc_NtkPrintStats( Abc_Ntk_t * pNtk, int fFactored, int fSaveBest, int fDum
if ( Abc_NtkIsNetlist(pNtk) )
{
Abc_Print( 1," net =%5d", Abc_NtkNetNum(pNtk) );
- Abc_Print( 1," nd =%5d", Abc_NtkNodeNum(pNtk) - nSingles );
+ Abc_Print( 1," nd =%5d", fSkipSmall ? Abc_NtkGetLargeNodeNum(pNtk) : Abc_NtkNodeNum(pNtk) - nSingles );
Abc_Print( 1," wbox =%3d", Abc_NtkWhiteboxNum(pNtk) );
Abc_Print( 1," bbox =%3d", Abc_NtkBlackboxNum(pNtk) );
}
@@ -295,7 +295,7 @@ void Abc_NtkPrintStats( Abc_Ntk_t * pNtk, int fFactored, int fSaveBest, int fDum
}
else
{
- Abc_Print( 1," nd =%6d", Abc_NtkNodeNum(pNtk) - nSingles );
+ Abc_Print( 1," nd =%6d", fSkipSmall ? Abc_NtkGetLargeNodeNum(pNtk) : Abc_NtkNodeNum(pNtk) - nSingles );
Abc_Print( 1," edge =%7d", Abc_NtkGetTotalFanins(pNtk) - nSingles );
}
@@ -455,7 +455,7 @@ void Abc_NtkPrintStats( Abc_Ntk_t * pNtk, int fFactored, int fSaveBest, int fDum
fflush( stdout );
if ( pNtk->pExdc )
- Abc_NtkPrintStats( pNtk->pExdc, fFactored, fSaveBest, fDumpResult, fUseLutLib, fPrintMuxes, fPower, fGlitch, fSkipBuf, fPrintMem );
+ Abc_NtkPrintStats( pNtk->pExdc, fFactored, fSaveBest, fDumpResult, fUseLutLib, fPrintMuxes, fPower, fGlitch, fSkipBuf, fSkipSmall, fPrintMem );
}
/**Function*************************************************************
diff --git a/src/base/abci/module.make b/src/base/abci/module.make
index a3c343ee..b97f526f 100644
--- a/src/base/abci/module.make
+++ b/src/base/abci/module.make
@@ -15,7 +15,9 @@ SRC += src/base/abci/abc.c \
src/base/abci/abcDetect.c \
src/base/abci/abcDress.c \
src/base/abci/abcDress2.c \
+ src/base/abci/abcDress3.c \
src/base/abci/abcDsd.c \
+ src/base/abci/abcExact.c \
src/base/abci/abcExtract.c \
src/base/abci/abcFraig.c \
src/base/abci/abcFx.c \
diff --git a/src/base/io/ioReadBench.c b/src/base/io/ioReadBench.c
index 4fb21ad1..4d038200 100644
--- a/src/base/io/ioReadBench.c
+++ b/src/base/io/ioReadBench.c
@@ -94,6 +94,7 @@ Abc_Ntk_t * Io_ReadBenchNetwork( Extra_FileReader_t * p )
// allocate the empty network
pNtk = Abc_NtkStartRead( Extra_FileReaderGetFileName(p) );
+ pNtk->nConstrs = 0;
// go through the lines of the file
vString = Vec_StrAlloc( 100 );
@@ -140,6 +141,7 @@ Abc_Ntk_t * Io_ReadBenchNetwork( Extra_FileReader_t * p )
pTerm = Abc_NtkCreatePo( pNtk );
Abc_ObjAddFanin( pTerm, pNet );
}
+ pNtk->nConstrs++;
}
else
{
diff --git a/src/base/io/ioReadPlaMo.c b/src/base/io/ioReadPlaMo.c
index 1cd453d2..d190d30a 100644
--- a/src/base/io/ioReadPlaMo.c
+++ b/src/base/io/ioReadPlaMo.c
@@ -297,6 +297,32 @@ static inline void Mop_ManRemoveEmpty( Mop_Man_t * p )
/**Function*************************************************************
+ Synopsis [Count how many times each variable appears in the input parts.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Int_t * Mop_ManCollectStats( Mop_Man_t * p )
+{
+ int i, v, iCube, nVars = 32 * p->nWordsIn;
+ Vec_Int_t * vStats = Vec_IntStart( nVars );
+ Vec_IntForEachEntry( p->vCubes, iCube, i )
+ {
+ word * pCube = Mop_ManCubeIn(p, iCube);
+ int nOutLits = Mop_ManCountOnes( Mop_ManCubeOut(p, iCube), p->nWordsOut );
+ for ( v = 0; v < nVars; v++ )
+ if ( Abc_TtGetQua(pCube, v) )
+ Vec_IntAddToEntry( vStats, v, nOutLits );
+ }
+ return vStats;
+}
+
+/**Function*************************************************************
+
Synopsis []
Description []
@@ -306,6 +332,20 @@ static inline void Mop_ManRemoveEmpty( Mop_Man_t * p )
SeeAlso []
***********************************************************************/
+// knowing that cubes are distance-1, find the different input variable
+static inline int Mop_ManFindDiffVar( word * pCube1, word * pCube2, int nWords )
+{
+ int w, i;
+ for ( w = 0; w < nWords; w++ )
+ {
+ word Xor = pCube1[w] ^ pCube2[w];
+ for ( i = 0; i < 32; i++ )
+ if ( (Xor >> (i << 1)) & 0x3 )
+ return w * 32 + i;
+ }
+ assert( 0 );
+ return -1;
+}
// check containment of input parts of two cubes
static inline int Mop_ManCheckDist1( word * pCube1, word * pCube2, int nWords )
{
@@ -439,21 +479,30 @@ Vec_Int_t * Mop_ManFindDist1Pairs( Mop_Man_t * p, Vec_Int_t * vGroup )
return vPairs;
}
// merge distance-1 with identical output part
-int Mop_ManMergeDist1Pairs( Mop_Man_t * p, Vec_Int_t * vGroup, Vec_Int_t * vGroupPrev )
+int Mop_ManMergeDist1Pairs( Mop_Man_t * p, Vec_Int_t * vGroup, Vec_Int_t * vGroupPrev, Vec_Int_t * vStats, int nLimit )
{
Vec_Int_t * vPairs = Mop_ManFindDist1Pairs( p, vGroup );
Vec_Int_t * vPairsNew = Mop_ManCompatiblePairs( vPairs, Vec_IntSize(vGroup) );
- int w, i, c1, c2, nCubes = Vec_IntSize(vGroup) + Vec_IntSize(vGroupPrev);
+ int nCubes = Vec_IntSize(vGroup) + Vec_IntSize(vGroupPrev);
+ int w, i, c1, c2, iCubeNew, iVar;
// move cubes to the previous group
+ word * pCube, * pCube1, * pCube2;
+ Vec_Int_t * vToFree = Vec_IntAlloc( Vec_IntSize(vPairsNew) );
Vec_IntForEachEntryDouble( vPairsNew, c1, c2, i )
{
- int iCubeNew = Vec_IntPop( p->vFree );
+ pCube1 = Mop_ManCubeIn( p, Vec_IntEntry(vGroup, c1) );
+ pCube2 = Mop_ManCubeIn( p, Vec_IntEntry(vGroup, c2) );
+ assert( Mop_ManCheckDist1(pCube1, pCube2, p->nWordsIn) );
- word * pCube = Mop_ManCubeIn( p, iCubeNew );
- word * pCube1 = Mop_ManCubeIn( p, Vec_IntEntry(vGroup, c1) );
- word * pCube2 = Mop_ManCubeIn( p, Vec_IntEntry(vGroup, c2) );
+ // skip those cubes that have frequently appearing variables
+ iVar = Mop_ManFindDiffVar( pCube1, pCube2, p->nWordsIn );
+ if ( Vec_IntEntry( vStats, iVar ) > nLimit )
+ continue;
+ Vec_IntPush( vToFree, c1 );
+ Vec_IntPush( vToFree, c2 );
- assert( Mop_ManCheckDist1(pCube1, pCube2, p->nWordsIn) );
+ iCubeNew = Vec_IntPop( p->vFree );
+ pCube = Mop_ManCubeIn( p, iCubeNew );
for ( w = 0; w < p->nWordsIn; w++ )
pCube[w] = pCube1[w] & pCube2[w];
@@ -467,13 +516,15 @@ int Mop_ManMergeDist1Pairs( Mop_Man_t * p, Vec_Int_t * vGroup, Vec_Int_t * vGrou
Vec_IntPush( vGroupPrev, iCubeNew );
}
- Vec_IntForEachEntry( vPairsNew, c1, i )
+// Vec_IntForEachEntry( vPairsNew, c1, i )
+ Vec_IntForEachEntry( vToFree, c1, i )
{
if ( Vec_IntEntry(vGroup, c1) == -1 )
continue;
Vec_IntPush( p->vFree, Vec_IntEntry(vGroup, c1) );
Vec_IntWriteEntry( vGroup, c1, -1 );
}
+ Vec_IntFree( vToFree );
if ( Vec_IntSize(vPairsNew) > 0 )
Map_ManGroupCompact( vGroup );
Vec_IntFree( vPairs );
@@ -529,7 +580,7 @@ int Mop_ManMergeDist1Pairs2( Mop_Man_t * p, Vec_Int_t * vGroup, Vec_Int_t * vGro
Map_ManGroupCompact( vGroup );
return Count;
}
-int Mop_ManMergeDist1All( Mop_Man_t * p, Vec_Wec_t * vGroups )
+int Mop_ManMergeDist1All( Mop_Man_t * p, Vec_Wec_t * vGroups, Vec_Int_t * vStats, int nLimit )
{
Vec_Int_t * vGroup;
int i, nEqual, nReduce, Count = 0;
@@ -544,7 +595,7 @@ int Mop_ManMergeDist1All( Mop_Man_t * p, Vec_Wec_t * vGroups )
return -1;
}
nEqual = Mop_ManRemoveIdentical( p, vGroup );
- nReduce = Mop_ManMergeDist1Pairs( p, vGroup, Vec_WecEntry(vGroups, i-1) );
+ nReduce = Mop_ManMergeDist1Pairs( p, vGroup, Vec_WecEntry(vGroups, i-1), vStats, nLimit );
//Mop_ManMergeDist1Pairs2( p, vGroup, Vec_WecEntry(vGroups, i-1) );
Count += nEqual + nReduce;
//printf( "Group %3d : Equal =%5d. Reduce =%5d.\n", i, nEqual, nReduce );
@@ -599,16 +650,20 @@ void Mop_ManReduce2( Mop_Man_t * p )
{
abctime clk = Abc_Clock();
int nCubes = Vec_IntSize(p->vCubes);
+ Vec_Int_t * vStats = Mop_ManCollectStats( p );
Vec_Wec_t * vGroups = Mop_ManCreateGroups( p );
+ int nLimit = ABC_INFINITY; // 5 * Vec_IntSum(vStats) / Vec_IntSize(vStats) + 1;
int nOutLits = Mop_ManCountOutputLits( p );
int Count1 = Mop_ManMergeContainAll( p, vGroups );
- int Count2 = Mop_ManMergeDist1All( p, vGroups );
+ int Count2 = Mop_ManMergeDist1All( p, vGroups, vStats, nLimit );
int Count3 = Mop_ManMergeContainAll( p, vGroups );
- int Count4 = Mop_ManMergeDist1All( p, vGroups );
+ int Count4 = Mop_ManMergeDist1All( p, vGroups, vStats, nLimit );
int Count5 = Mop_ManMergeContainAll( p, vGroups );
int Removed = Mop_ManUnCreateGroups( p, vGroups );
int nOutLits2 = Mop_ManCountOutputLits( p );
Vec_WecFree( vGroups );
+//Vec_IntPrint( vStats );
+ Vec_IntFree( vStats );
assert( Removed == Count1 + Count2 + Count3 );
// report
printf( "Cubes: %d -> %d. C = %d. M = %d. C = %d. M = %d. C = %d. Output lits: %d -> %d. ",
diff --git a/src/base/wlc/wlc.h b/src/base/wlc/wlc.h
index 51152fa8..bb5c4bfe 100644
--- a/src/base/wlc/wlc.h
+++ b/src/base/wlc/wlc.h
@@ -259,7 +259,7 @@ extern Vec_Int_t * Wlc_NtkFindUifableMultiplierPairs( Wlc_Ntk_t * p );
extern Wlc_Ntk_t * Wlc_NtkAbstractNodes( Wlc_Ntk_t * pNtk, Vec_Int_t * vNodes );
extern Wlc_Ntk_t * Wlc_NtkUifNodePairs( Wlc_Ntk_t * pNtk, Vec_Int_t * vPairs );
/*=== wlcBlast.c ========================================================*/
-extern Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int fGiaSimple, int fAddOutputs );
+extern Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int iOutput, int nRange, int fGiaSimple, int fAddOutputs, int fBooth );
/*=== wlcCom.c ========================================================*/
extern void Wlc_SetNtk( Abc_Frame_t * pAbc, Wlc_Ntk_t * pNtk );
/*=== wlcNtk.c ========================================================*/
diff --git a/src/base/wlc/wlcBlast.c b/src/base/wlc/wlcBlast.c
index 79ad3659..c86c7cf0 100644
--- a/src/base/wlc/wlcBlast.c
+++ b/src/base/wlc/wlcBlast.c
@@ -143,16 +143,19 @@ void Wlc_BlastShiftRightInt( Gia_Man_t * pNew, int * pNum, int nNum, int * pShif
void Wlc_BlastShiftRight( Gia_Man_t * pNew, int * pNum, int nNum, int * pShift, int nShift, int fSticky, Vec_Int_t * vRes )
{
int nShiftMax = Abc_Base2Log(nNum);
+ int * pShiftNew = ABC_ALLOC( int, nShift );
+ memcpy( pShiftNew, pShift, sizeof(int)*nShift );
if ( nShiftMax < nShift )
{
- int i, iRes = pShift[nShiftMax];
+ int i, iRes = pShiftNew[nShiftMax];
for ( i = nShiftMax + 1; i < nShift; i++ )
- iRes = Gia_ManHashOr( pNew, iRes, pShift[i] );
- pShift[nShiftMax++] = iRes;
+ iRes = Gia_ManHashOr( pNew, iRes, pShiftNew[i] );
+ pShiftNew[nShiftMax++] = iRes;
}
else
nShiftMax = nShift;
- Wlc_BlastShiftRightInt( pNew, pNum, nNum, pShift, nShiftMax, fSticky, vRes );
+ Wlc_BlastShiftRightInt( pNew, pNum, nNum, pShiftNew, nShiftMax, fSticky, vRes );
+ ABC_FREE( pShiftNew );
}
void Wlc_BlastShiftLeftInt( Gia_Man_t * pNew, int * pNum, int nNum, int * pShift, int nShift, int fSticky, Vec_Int_t * vRes )
{
@@ -176,16 +179,19 @@ void Wlc_BlastShiftLeftInt( Gia_Man_t * pNew, int * pNum, int nNum, int * pShift
void Wlc_BlastShiftLeft( Gia_Man_t * pNew, int * pNum, int nNum, int * pShift, int nShift, int fSticky, Vec_Int_t * vRes )
{
int nShiftMax = Abc_Base2Log(nNum);
+ int * pShiftNew = ABC_ALLOC( int, nShift );
+ memcpy( pShiftNew, pShift, sizeof(int)*nShift );
if ( nShiftMax < nShift )
{
- int i, iRes = pShift[nShiftMax];
+ int i, iRes = pShiftNew[nShiftMax];
for ( i = nShiftMax + 1; i < nShift; i++ )
- iRes = Gia_ManHashOr( pNew, iRes, pShift[i] );
- pShift[nShiftMax++] = iRes;
+ iRes = Gia_ManHashOr( pNew, iRes, pShiftNew[i] );
+ pShiftNew[nShiftMax++] = iRes;
}
else
nShiftMax = nShift;
- Wlc_BlastShiftLeftInt( pNew, pNum, nNum, pShift, nShiftMax, fSticky, vRes );
+ Wlc_BlastShiftLeftInt( pNew, pNum, nNum, pShiftNew, nShiftMax, fSticky, vRes );
+ ABC_FREE( pShiftNew );
}
void Wlc_BlastRotateRight( Gia_Man_t * pNew, int * pNum, int nNum, int * pShift, int nShift, Vec_Int_t * vRes )
{
@@ -674,6 +680,7 @@ void Wlc_BlastReduceMatrix( Gia_Man_t * pNew, Vec_Wec_t * vProds, Vec_Wec_t * vL
Vec_IntPush( vProd, 0 );
assert( Vec_IntSize(vProd) == 2 );
}
+// Vec_WecPrint( vProds, 0 );
vLevel = Vec_WecEntry( vLevels, 0 );
Vec_IntClear( vRes );
@@ -684,7 +691,9 @@ void Wlc_BlastReduceMatrix( Gia_Man_t * pNew, Vec_Wec_t * vProds, Vec_Wec_t * vL
Vec_IntPush( vRes, Vec_IntEntry(vProd, 0) );
Vec_IntPush( vLevel, Vec_IntEntry(vProd, 1) );
}
- Wlc_BlastAdder( pNew, Vec_IntArray(vRes), Vec_IntArray(vLevel), nSize );
+ Vec_IntPush( vRes, 0 );
+ Vec_IntPush( vLevel, 0 );
+ Wlc_BlastAdder( pNew, Vec_IntArray(vRes), Vec_IntArray(vLevel), Vec_IntSize(vRes) );
}
void Wlc_BlastMultiplier3( Gia_Man_t * pNew, int * pArgA, int * pArgB, int nArgA, int nArgB, Vec_Int_t * vRes )
{
@@ -728,6 +737,81 @@ void Wlc_BlastSquare( Gia_Man_t * pNew, int * pNum, int nNum, Vec_Int_t * vTmp,
Vec_WecFree( vProds );
Vec_WecFree( vLevels );
}
+void Wlc_BlastBooth( Gia_Man_t * pNew, int * pArgA, int * pArgB, int nArgA, int nArgB, Vec_Int_t * vRes, int fSigned )
+{
+ Vec_Wec_t * vProds = Vec_WecStart( nArgA + nArgB + 3 );
+ Vec_Wec_t * vLevels = Vec_WecStart( nArgA + nArgB + 3 );
+ int FillA = fSigned ? pArgA[nArgA-1] : 0;
+ int FillB = fSigned ? pArgB[nArgB-1] : 0;
+ int i, k, Sign;
+ // create new arguments
+ Vec_Int_t * vArgB = Vec_IntAlloc( nArgB + 3 );
+ Vec_IntPush( vArgB, 0 );
+ for ( i = 0; i < nArgB; i++ )
+ Vec_IntPush( vArgB, pArgB[i] );
+ Vec_IntPush( vArgB, FillB );
+ if ( Vec_IntSize(vArgB) % 2 == 0 )
+ Vec_IntPush( vArgB, FillB );
+ assert( Vec_IntSize(vArgB) % 2 == 1 );
+ // iterate through bit-pairs
+ for ( k = 0; k+2 < Vec_IntSize(vArgB); k+=2 )
+ {
+ int pp = -1;
+ int Q2jM1 = Vec_IntEntry(vArgB, k); // q(2*j-1)
+ int Q2j = Vec_IntEntry(vArgB, k+1); // q(2*j+0)
+ int Q2jP1 = Vec_IntEntry(vArgB, k+2); // q(2*j+1)
+ int Neg = Q2jP1;
+ int One = Gia_ManHashXor( pNew, Q2j, Q2jM1 );
+ int Two = Gia_ManHashMux( pNew, Neg, Gia_ManHashAnd(pNew, Abc_LitNot(Q2j), Abc_LitNot(Q2jM1)), Gia_ManHashAnd(pNew, Q2j, Q2jM1) );
+ for ( i = 0; i <= nArgA; i++ )
+ {
+ int This = i == nArgA ? FillA : pArgA[i];
+ int Prev = i ? pArgA[i-1] : 0;
+ int Part = Gia_ManHashOr( pNew, Gia_ManHashAnd(pNew, One, This), Gia_ManHashAnd(pNew, Two, Prev) );
+
+ pp = Gia_ManHashXor( pNew, Part, Neg );
+
+ if ( pp == 0 )
+ continue;
+ Vec_WecPush( vProds, k+i, pp );
+ Vec_WecPush( vLevels, k+i, 0 );
+ }
+ // perform sign extension
+ Sign = fSigned ? pp : Neg;
+ if ( k == 0 )
+ {
+ Vec_WecPush( vProds, k+i, Sign );
+ Vec_WecPush( vLevels, k+i, 0 );
+
+ Vec_WecPush( vProds, k+i+1, Sign );
+ Vec_WecPush( vLevels, k+i+1, 0 );
+
+ Vec_WecPush( vProds, k+i+2, Abc_LitNot(Sign) );
+ Vec_WecPush( vLevels, k+i+2, 0 );
+ }
+ else
+ {
+ Vec_WecPush( vProds, k+i, Abc_LitNot(Sign) );
+ Vec_WecPush( vLevels, k+i, 0 );
+
+ Vec_WecPush( vProds, k+i+1, 1 );
+ Vec_WecPush( vLevels, k+i+1, 0 );
+ }
+ // add neg to the first column
+ if ( Neg == 0 )
+ continue;
+ Vec_WecPush( vProds, k, Neg );
+ Vec_WecPush( vLevels, k, 0 );
+ }
+ //Vec_WecPrint( vProds, 0 );
+
+ Wlc_BlastReduceMatrix( pNew, vProds, vLevels, vRes );
+
+ Vec_WecFree( vProds );
+ Vec_WecFree( vLevels );
+ Vec_IntFree( vArgB );
+}
+
/**Function*************************************************************
@@ -740,7 +824,7 @@ void Wlc_BlastSquare( Gia_Man_t * pNew, int * pNum, int nNum, Vec_Int_t * vTmp,
SeeAlso []
***********************************************************************/
-Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int fGiaSimple, int fAddOutputs )
+Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int iOutput, int nOutputRange, int fGiaSimple, int fAddOutputs, int fBooth )
{
int fVerbose = 0;
int fUseOldMultiplierBlasting = 0;
@@ -1149,9 +1233,12 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int fGiaSimple,
int * pArg1 = Wlc_VecLoadFanins( vTemp1, pFans1, nRange1, nRangeMax, fSigned );
if ( Wlc_NtkCountConstBits(pArg0, nRangeMax) < Wlc_NtkCountConstBits(pArg1, nRangeMax) )
ABC_SWAP( int *, pArg0, pArg1 );
- Wlc_BlastMultiplier( pNew, pArg0, pArg1, nRangeMax, nRangeMax, vTemp2, vRes, fSigned );
+ if ( fBooth )
+ Wlc_BlastBooth( pNew, pArg0, pArg1, nRange0, nRange1, vRes, fSigned );
+ else
+ Wlc_BlastMultiplier( pNew, pArg0, pArg1, nRangeMax, nRangeMax, vTemp2, vRes, fSigned );
//Wlc_BlastMultiplier3( pNew, pArg0, pArg1, nRange0, nRange1, vRes );
- if ( nRange > nRangeMax + nRangeMax )
+ if ( nRange > Vec_IntSize(vRes) )
Vec_IntFillExtra( vRes, nRange, fSigned ? Vec_IntEntryLast(vRes) : 0 );
else
Vec_IntShrink( vRes, nRange );
@@ -1233,6 +1320,9 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int fGiaSimple,
// create COs
Wlc_NtkForEachCo( p, pObj, i )
{
+ // skip all outputs except the given ones
+ if ( iOutput >= 0 && (i < iOutput || i >= iOutput + nOutputRange) )
+ continue;
// create additional PO literals
if ( vAddOutputs && pObj->fIsFi )
{
diff --git a/src/base/wlc/wlcCom.c b/src/base/wlc/wlcCom.c
index 77bf36ba..2c504127 100644
--- a/src/base/wlc/wlcCom.c
+++ b/src/base/wlc/wlcCom.c
@@ -128,10 +128,10 @@ int Abc_CommandReadWlc( Abc_Frame_t * pAbc, int argc, char ** argv )
switch ( c )
{
case 'o':
- fPrintTree ^= 1;
+ fOldParser ^= 1;
break;
case 'p':
- fOldParser ^= 1;
+ fPrintTree ^= 1;
break;
case 'v':
fVerbose ^= 1;
@@ -338,12 +338,34 @@ int Abc_CommandBlast( Abc_Frame_t * pAbc, int argc, char ** argv )
Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc);
Vec_Int_t * vBoxIds = NULL;
Gia_Man_t * pNew = NULL;
- int c, fGiaSimple = 0, fAddOutputs = 0, fMulti = 0, fVerbose = 0;
+ int c, iOutput = -1, nOutputRange = 2, fGiaSimple = 0, fAddOutputs = 0, fMulti = 0, fBooth = 0, fVerbose = 0;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "comvh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "ORcombvh" ) ) != EOF )
{
switch ( c )
{
+ case 'O':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-O\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ iOutput = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( iOutput < 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;
+ }
+ nOutputRange = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( nOutputRange < 0 )
+ goto usage;
+ break;
case 'c':
fGiaSimple ^= 1;
break;
@@ -353,6 +375,9 @@ int Abc_CommandBlast( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'm':
fMulti ^= 1;
break;
+ case 'b':
+ fBooth ^= 1;
+ break;
case 'v':
fVerbose ^= 1;
break;
@@ -373,8 +398,13 @@ int Abc_CommandBlast( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( vBoxIds == NULL )
Abc_Print( 1, "Warning: There is no multipliers in the design.\n" );
}
+ if ( iOutput >= 0 && iOutput + nOutputRange > Wlc_NtkPoNum(pNtk) )
+ {
+ Abc_Print( 1, "Abc_CommandBlast(): The output range [%d:%d] is incorrect.\n", iOutput, iOutput + nOutputRange - 1 );
+ return 0;
+ }
// transform
- pNew = Wlc_NtkBitBlast( pNtk, vBoxIds, fGiaSimple, fAddOutputs );
+ pNew = Wlc_NtkBitBlast( pNtk, vBoxIds, iOutput, nOutputRange, fGiaSimple, fAddOutputs, fBooth );
Vec_IntFreeP( &vBoxIds );
if ( pNew == NULL )
{
@@ -384,11 +414,14 @@ int Abc_CommandBlast( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_FrameUpdateGia( pAbc, pNew );
return 0;
usage:
- Abc_Print( -2, "usage: %%blast [-comvh]\n" );
+ Abc_Print( -2, "usage: %%blast [-OR num] [-combvh]\n" );
Abc_Print( -2, "\t performs bit-blasting of the word-level design\n" );
+ Abc_Print( -2, "\t-O num : zero-based index of the first word-level PO to bit-blast [default = %d]\n", iOutput );
+ Abc_Print( -2, "\t-R num : the total number of word-level POs to bit-blast [default = %d]\n", nOutputRange );
Abc_Print( -2, "\t-c : toggle using AIG w/o const propagation and strashing [default = %s]\n", fGiaSimple? "yes": "no" );
Abc_Print( -2, "\t-o : toggle using additional POs on the word-level boundaries [default = %s]\n", fAddOutputs? "yes": "no" );
Abc_Print( -2, "\t-m : toggle creating boxes for all multipliers in the design [default = %s]\n", fMulti? "yes": "no" );
+ Abc_Print( -2, "\t-b : toggle generating radix-4 Booth multipliers [default = %s]\n", fBooth? "yes": "no" );
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
diff --git a/src/base/wlc/wlcReadSmt.c b/src/base/wlc/wlcReadSmt.c
index ed6092a5..fcd47274 100644
--- a/src/base/wlc/wlcReadSmt.c
+++ b/src/base/wlc/wlcReadSmt.c
@@ -276,13 +276,9 @@ static inline int Smt_PrsCreateNode( Wlc_Ntk_t * pNtk, int Type, int fSigned, in
assert( fSigned >= 0 );
Wlc_ObjAddFanins( pNtk, Wlc_NtkObj(pNtk, iObj), vFanins );
if ( fSigned )
- {
Wlc_NtkObj(pNtk, iObj)->Signed = fSigned;
-// if ( Vec_IntSize(vFanins) > 0 )
-// Wlc_NtkObj(pNtk, Vec_IntEntry(vFanins, 0))->Signed = fSigned;
-// if ( Vec_IntSize(vFanins) > 1 )
-// Wlc_NtkObj(pNtk, Vec_IntEntry(vFanins, 1))->Signed = fSigned;
- }
+ if ( Type == WLC_OBJ_SHIFT_RA )
+ Wlc_NtkObj(pNtk, iObj)->Signed = 1;
if ( pName == NULL )
{
sprintf( Buffer, "_n%d_", iObj );
@@ -511,6 +507,13 @@ Wlc_Ntk_t * Smt_PrsBuild( Smt_Prs_t * p )
// skip ()
Fan = Vec_IntEntry(vFans, 2);
assert( !Smt_EntryIsName(Fan) );
+ vFans2 = Smt_VecEntryNode(p, vFans, 2);
+ if ( Vec_IntSize(vFans2) > 0 )
+ {
+ printf( "File parsing error: Uninterpreted functions are not supported.\n" );
+ Wlc_NtkFree( pNtk ); pNtk = NULL;
+ goto finish;
+ }
// check type (Bool or BitVec)
Fan = Vec_IntEntry(vFans, 3);
if ( Smt_EntryIsName(Fan) )
@@ -921,6 +924,13 @@ Wlc_Ntk_t * Smt_PrsBuild2( Smt_Prs_t * p )
// skip ()
Fan = Vec_IntEntry(vFans, 2);
assert( !Smt_EntryIsName(Fan) );
+ vFans2 = Smt_VecEntryNode(p, vFans, 2);
+ if ( Vec_IntSize(vFans2) > 0 )
+ {
+ printf( "File parsing error: Uninterpreted functions are not supported.\n" );
+ Wlc_NtkFree( pNtk ); pNtk = NULL;
+ goto finish;
+ }
// check type (Bool or BitVec)
Fan = Vec_IntEntry(vFans, 3);
if ( Smt_EntryIsName(Fan) )
diff --git a/src/base/wlc/wlcReadVer.c b/src/base/wlc/wlcReadVer.c
index 824cf80b..08dc8e98 100644
--- a/src/base/wlc/wlcReadVer.c
+++ b/src/base/wlc/wlcReadVer.c
@@ -1265,10 +1265,10 @@ Wlc_Ntk_t * Wlc_ReadVer( char * pFileName )
// derive topological order
pNtk = Wlc_NtkDupDfs( p->pNtk );
Wlc_NtkTransferNames( pNtk, p->pNtk );
+ pNtk->pSpec = Abc_UtilStrsav( pFileName );
finish:
Wlc_PrsPrintErrorMessage( p );
Wlc_PrsStop( p );
- pNtk->pSpec = Abc_UtilStrsav( pFileName );
return pNtk;
}
@@ -1291,7 +1291,7 @@ void Io_ReadWordTest( char * pFileName )
return;
Wlc_WriteVer( pNtk, "test.v", 0, 0 );
- pNew = Wlc_NtkBitBlast( pNtk, NULL, 0, 0 );
+ pNew = Wlc_NtkBitBlast( pNtk, NULL, -1, 0, 0, 0, 0 );
Gia_AigerWrite( pNew, "test.aig", 0, 0 );
Gia_ManStop( pNew );
diff --git a/src/base/wlc/wlcSim.c b/src/base/wlc/wlcSim.c
index 73d5307f..20ac8c61 100644
--- a/src/base/wlc/wlcSim.c
+++ b/src/base/wlc/wlcSim.c
@@ -129,7 +129,7 @@ Vec_Ptr_t * Wlc_NtkSimulate( Wlc_Ntk_t * p, Vec_Int_t * vNodes, int nWords, int
{
Gia_Obj_t * pObj;
Vec_Ptr_t * vOne, * vRes;
- Gia_Man_t * pGia = Wlc_NtkBitBlast( p, NULL, 0, 0 );
+ Gia_Man_t * pGia = Wlc_NtkBitBlast( p, NULL, -1, 0, 0, 0, 0 );
Wlc_Obj_t * pWlcObj;
int f, i, k, w, nBits, Counter = 0;
// allocate simulation info for one timeframe
generated by cgit v1.2.3 (git 2.25.1) at 2025-08-05 17:09:49 +0000